ℚ is a field: Rat.inv is proved to invert, at zero trusted declarations

Identifier: F:rationals-are-a-field-axiom-free
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

The rational prelude's multiplicative inverse Rat.inv has existed since the prelude was written, as a definition with no law about it -- a three-way dispatch on the numerator's sign, with inv 0 = 0 by the usual total convention -- so the development had 22 ordered-RING laws and an operation named inv, and the gap between those two is exactly the gap between a ring and a field. Rat.mul_inv_cancel closes it: for every rational q with 0 < q, Rat.mul q (Rat.inv q) = Rat.one, as a checked kernel Theorem with an empty axiom footprint. The rational prelude's whole trusted surface (Axiom + Opaque + Quotient) remains 0, so ℚ is an ordered field with nothing assumed. Rat.div a b := Rat.mul a (Rat.inv b) is defined through Rat.inv and so had no law behind it either until now.

Formal statement

Rat.mul_inv_cancel : forall (q : Rat), Rat.lt Rat.zero q -> Eq Rat (Rat.mul q (Rat.inv q)) Rat.one

Dependencies

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

0 direct dependencies 1 direct dependents

Evidence

rationals-are-a-field-statement

Kind: kernel-term
Status: checked

Supports: Rat.mul_inv_cancel and Rat.inv_pos are checked Theorems whose RENDERED types are the ones claimed, with empty axiom footprints.

Checker command

out=$(cargo test -q -p axeyum-lean-kernel --lib the_rationals_are_a_field_and_the_inverse_is_positive 2>&1) && test "$(printf '%s\n' "$out" | grep -cE '^test result: ok\. 1 passed; 0 failed')" = 1

Evidence notes

Anchored on a NONZERO test count on the same line as the pass, because a filter that matches nothing prints 'ok. 0 passed' and exits 0 -- this repository's standing inert-gate trap. The test asserts the rendered type verbatim rather than the footprint: an empty footprint on a theorem named mul_inv_cancel that says something weaker would pass a footprint check and fail this one.

rationals-are-a-field-trusted-surface

Kind: kernel-term
Status: checked

Supports: The rational prelude's whole trusted surface is still 0 after the field laws land -- not just the one theorem's footprint.

Checker command

out=$(cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --include-constructed 2>&1) && test "$(printf '%s\n' "$out" | grep -cE '^rat: axiom=0 opaque=0 quotient=0 total_trusted=0$')" = 1

Evidence notes

The --include-constructed flag is REQUIRED and the row is matched whole: axiom=0 alone is not the trusted surface, since Opaque has no proof body and Quotient admits Quot.sound. Confirmed the tool's coverage includes rat by matching the rat row itself rather than by finding no rows.

rationals-are-a-field-computes

Kind: kernel-term
Status: checked

Supports: Rat.inv computes the reciprocal at a point: (2/1)⁻¹ REDUCES to 1/2, so Eq.refl proves it and the kernel checks the reduction.

Checker command

out=$(cargo test -q -p axeyum-lean-kernel --lib the_inverse_computes_the_reciprocal 2>&1) && test "$(printf '%s\n' "$out" | grep -cE '^test result: ok\. 1 passed; 0 failed')" = 1

Evidence notes

mul_inv_cancel's hypothesis is 0 < q, so it says NOTHING about Rat.inv off the positives and a 'reciprocal' agreeing with the real one only there would satisfy it. This row pins the operation by computation instead. Its paired negative control -- the identical Eq.refl script pointed at (2/1)⁻¹ = 2/1 -- is REFUSED by the kernel, in the_inverse_reduction_check_can_fail.

Provenance

{
  "date": "2026-08-18",
  "established_by": "axeyum-lean-kernel rat_prelude::field (ADR-0510; agent-creal-field lane)",
  "source": "the usual construction of ℚ as reduced pairs, with the inverse's three-way sign dispatch discharged by ι-reduction rather than by a lemma"
}