Rational multiplication renormalises

Identifier: F:rat-mul-renormalises
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Rat.mul multiplies two rationals and returns the reduced representative: 2/3 * 3/2 is 1/1, not 6/6. The product of two reduced pairs need not itself be reduced, so multiplication must renormalise or the `reduced` field of the result would be unprovable.

Formal statement

def Rat.mul : ((x0 : Rat) -> ((x1 : Rat) -> Rat))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

1 direct dependencies 2 direct dependents

Evidence

kernel-rat-mul-renormalises

Kind: kernel-term
Status: checked

Supports: 2/3 * 3/2 and 1/1 are the same rational; 1/2 * 1/3 is 1/6; 1/6 and 1/2 are different rationals.

Checker command

test "$(cargo test -p axeyum-lean-kernel --lib rat_mul_renormalises_two_thirds_times_three_halves_to_one 2>&1 | grep -Ec '^test result: ok\. 1 passed')" -ge 1

Evidence notes

Bound to this test by name, and `1 passed` is in the pattern deliberately: a filter matching nothing prints `0 passed` and would otherwise read as success. The test settles the equalities by `Kernel::def_eq` with no lemma -- Nat.gcd, Nat.div and Int.rec all compute -- and includes the inequality `1/6 != 1/2` so that a def_eq comparing everything equal could not make the positive checks vacuous.

footprint-rat-mul-renormalises

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- Rat is built in the integer environment, whose trusted surface is empty

Checker command

cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free integer

Evidence notes

Rat and its operations are admitted into the same environment as the integer development, so an empty trusted surface bounds their footprints. Environment-wide on purpose: a declaration cannot depend on a trusted declaration the environment does not contain.

Provenance

{
  "date": "2026-08-16",
  "established_by": "axeyum-lean-kernel int_prelude::rat (rational-scope lane)",
  "source": "hand-built foundational library"
}