The constructed reals have a multiplicative inverse whose modulus is an explicit natural, and it is a function on the reals rather than on representatives

Identifier: F:real-inverse-is-built-and-well-defined
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

CReal.inv : (x : CReal) -> (k : Nat) -> CReal.PosBound x k -> CReal is a Definition in the axeyum Lean kernel with an empty axiom footprint, and CReal.mul_inv_cancel : forall x k (h : PosBound x k), CReal.Equiv (CReal.mul x (CReal.inv x k h)) CReal.one is a checked Theorem, likewise footprint-free. The definition is possible because a function may TAKE a Prop argument and return a Type; it may only not BRANCH on one. PosBound x k carries no disjunction, the representative sequence n |-> Rat.inv (CReal.seq x (j n)) at j n = (CReal.invShift k + 1) * n + CReal.invShift k depends on k alone, and the hypothesis is consumed only inside CReal.mk's Prop-valued regularity field. So the MODULUS is the thing that must be data; the proof need not be. Two further theorems make it a function on the reals rather than on representatives: CReal.inv_congr : forall x y k1 k2 h1 h2, CReal.Equiv x y -> CReal.Equiv (CReal.inv x k1 h1) (CReal.inv y k2 h2), which quantifies over the two moduli INDEPENDENTLY because two callers with different k for the same x build genuinely different sequences (k = 0 samples at 7n+7, k = 1 at 32n+31), and CReal.inv_index_irrelevant, that theorem at y := x. Neither is an estimate: an inverse in a commutative monoid is unique, so mul_inv_cancel at both ends closes them. The domain is inhabited -- CReal.PosBound CReal.one 0 is admitted THROUGH THE KERNEL -- and the operation is not the constant zero, since mul_inv_cancel and Equiv.not_zero_one give forall h, Not (CReal.Equiv (CReal.inv CReal.one 0 h) CReal.zero).

Formal statement

CReal.inv : forall (x : CReal) (k : Nat), CReal.PosBound x k -> CReal  --  together with  CReal.mul_inv_cancel : forall (x : CReal) (k : Nat) (h : CReal.PosBound x k), CReal.Equiv (CReal.mul x (CReal.inv x k h)) CReal.one,  CReal.inv_congr : forall (x y : CReal) (k1 k2 : Nat) (h1 : CReal.PosBound x k1) (h2 : CReal.PosBound y k2), CReal.Equiv x y -> CReal.Equiv (CReal.inv x k1 h1) (CReal.inv y k2 h2),  and  CReal.inv_index_irrelevant : forall (x : CReal) (k1 k2 : Nat) (h1 : CReal.PosBound x k1) (h2 : CReal.PosBound x k2), CReal.Equiv (CReal.inv x k1 h1) (CReal.inv x k2 h2),  where CReal.PosBound x k := CReal.le (CReal.ofRat (Rat.natDivSucc 1 k)) x

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

real-inverse-built-statements-and-non-vacuity

Kind: kernel-term
Status: checked

Supports: The five statements are asserted VERBATIM as rendered types (not by footprint); CReal.PosBound CReal.one 0 is admitted THROUGH THE KERNEL so the guarded theorems are not vacuous; the inverse is proved not to be the constant zero; and the two one-token mutations are REFUSED.

Checker command

out=$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib creal::creal_tests::the_inverse 2>&1) && test "$(printf "%s\n" "$out" | grep -cE 'test result: ok\. 3 passed; 0 failed')" = 1

Evidence notes

Anchored on a NONZERO test count (3), because a filter matching nothing prints 'ok. 0 passed' and exits 0 -- and on 0 failed, so a green-looking partial run cannot pass. Verified discriminating by scripts/new-fact.py: the pattern matches the real output and fails under every mutation of it. The three tests are the verbatim-statement test, the non-vacuity/discrimination test (PosBound one 0 admitted, then forall h, not (inv one 0 h ~ zero) from mul_inv_cancel and Equiv.not_zero_one alone), and the negative-control test (x*inv x ~ 0 and inv x ~ x both REFUSED). Vacuity, not weakness, is the failure mode this row exists for: every statement about CReal.inv is guarded by PosBound x k, and an uninhabited guard would let all of them hold footprint-free with their statements verbatim.

real-inverse-built-declaration-inventory

Kind: kernel-term
Status: checked

Supports: All 76 CReal declarations -- the five new ones included -- are checked Theorems or Definitions with EMPTY axiom footprints, read out of the kernel's own environment rather than off the diff.

Checker command

out=$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib creal::creal_tests::every_creal_declaration_is_checked_and_axiom_free 2>&1) && test "$(printf "%s\n" "$out" | grep -cE 'test result: ok\. 1 passed; 0 failed')" = 1

Evidence notes

Anchored on a NONZERO count for the same reason as the row above; verified discriminating by scripts/new-fact.py. The test enumerates all 76 declarations by NameId, asserts the KIND of each (a Definition demoted to an Axiom fails), and asserts kernel.axiom_footprint(name) is empty for each. Deleting declare_inv_index_irrelevant kills exactly two tests -- this one and the verbatim-statement test -- measured 2026-08-18 against a 24-test baseline.

real-inverse-built-witness-example

Kind: kernel-term
Status: checked

Supports: The witness example's EXIT STATUS depends on the finding, and its declaration count moved 71 -> 76 with the trusted surface still empty on the same line.

Checker command

out=$(scripts/cargo-serialized.sh run -q --release -p axeyum-lean-kernel --example creal_setoid_witness 2>&1) && test "$(printf "%s\n" "$out" | grep -cE '[0-9]+ declarations admitted, trusted surface = 0 [(]empty[)]')" = 1 && test "$(printf "%s\n" "$out" | grep -cE '^CReal[.](inv|invShift|mul_inv_cancel|inv_congr|inv_index_irrelevant)[[:space:]]+(definition|theorem)[[:space:]]+-$')" = 5

Evidence notes

The first pattern pins a VALUE (the count 76 and the trusted surface 0) and was verified discriminating by scripts/new-fact.py. The SECOND is population-only and is here deliberately: it pins that all five new declarations appear with an empty footprint column, so a build that quietly dropped one of them fails, but no mutation of a surviving row changes its count. It is the weaker of the two and is not load-bearing on its own. The declaration COUNT is deliberately not pinned. It was `76`, and the lattice work (`4c7af898d`) took the same witness to `94` without touching anything this fact claims -- so a fact about the INVERSE was red because of a lemma about `max`. A total that every lane increments is not an anchor for a fact about one declaration. What is pinned is `trusted surface = 0 (empty)`, which is the invariant, plus the floor below. `--release` is not a preference. In debug this witness runs ~19 minutes -- it computes `axiom_footprint` per declaration over 94 of them -- and `scripts/check-fact-evidence-replay.sh` budgets 120 s per row, so the debug form made this evidence structurally unreplayable and the gate recorded it as a TIMEOUT rather than a result. Release is ~12x on this crate, measured.

real-inverse-is-built-and-well-defined-declaration-floor

Kind: kernel-term
Status: checked

Supports: The witness enumerates a non-trivial development, so the trusted-surface-0 claim above is not read off an empty environment.

Checker command

out=$(cargo run -q --release -p axeyum-lean-kernel --example creal_setoid_witness 2>&1) && n=$(printf '%s\n' "$out" | grep -oE '[0-9]+ declarations admitted' | grep -oE '^[0-9]+') && test -n "$n" && test "$n" -ge 76

Evidence notes

A FLOOR, not an equality: 76 was the count when the inverse landed and the development only grows. A shrink still fires -- that would mean declarations disappeared -- while another lane adding a lemma does not red a fact about the inverse. An equality here is what made both these facts red. `--release` is not a preference. In debug this witness runs ~19 minutes -- it computes `axiom_footprint` per declaration over 94 of them -- and `scripts/check-fact-evidence-replay.sh` budgets 120 s per row, so the debug form made this evidence structurally unreplayable and the gate recorded it as a TIMEOUT rather than a result. Release is ~12x on this crate, measured.

Provenance

{
  "date": "2026-08-18",
  "established_by": "axeyum-lean-kernel creal::inverse (ADR-0516; agent-creal-inv lane)",
  "source": "Bishop-style constructive analysis: the reciprocal of a real apart from zero, sampled deep enough that every sample clears the separating modulus"
}