The rational smart constructor normalises

Identifier: F:rat-normalize-reduces
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Rat.normalize sends 2/4 and 1/2 to the same rational, and distinguishes 1/2 from 1/3. The rationals are built as a normalised structure over the proved integers, with both proof fields discharged by the constructor.

Formal statement

def Rat.normalize : ((x0 : Int) -> ((x1 : AxNat) -> ((x2 : AxNat.le (AxNat.succ AxNat.zero) x1) -> 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.normalize

Kind: kernel-term
Status: checked

Supports: normalize 2 4 and normalize 1 2 are definitionally the same Rat; normalize 1 2 and normalize 1 3 are not.

Checker command

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

Evidence notes

Bound to this single test by name, and the `1 passed` in the pattern is deliberate: a filter that matches nothing prints `0 passed` and would otherwise read as success -- the inert-gate trap this repository has been bitten by. The test decides equality by `Kernel::def_eq` with no lemma, which works only because Nat.gcd, Nat.div and Int.rec all compute, and it requires 1/2 and 1/3 to be DISTINGUISHABLE so the equality check is not vacuous.

footprint-rat

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, Rat.mk and Rat.normalize are admitted into the same environment as the integer development, so the empty trusted surface bounds their footprints too. Not a quotient: this kernel's quotient package has no Quot.sound (ADR-0456), so a setoid construction is inexpressible here -- and Lean core's own Rat is likewise a normalised structure, not a quotient.

Provenance

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