No function on all of the constructed reals is a multiplicative inverse, and the modulus that would make one possible cannot be extracted from positivity

Identifier: F:real-inverse-is-partial-and-its-modulus-is-data
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Two statements about the constructed reals CReal, both proved with empty axiom footprints. (1) CReal.no_total_inverse: for every f : CReal -> CReal it is false that CReal.Equiv (CReal.mul x (f x)) CReal.one for all x -- evaluate at zero, where mul_comm and mul_zero make the product Equiv-equal to zero, and Equiv.not_zero_one refutes zero ≈ one by computation at index 3. So the multiplicative inverse is PARTIAL as a matter of proof, not of scope. (2) CReal.pos_of_pos_bound and CReal.pos_bound_of_lt: CReal.lt CReal.zero x and Exists (k : Nat), CReal.le (CReal.ofRat (Rat.natDivSucc 1 k)) x are the same proposition, so the separating modulus a constructive inverse needs always exists -- and it exists inside an Exists, which is a Prop, so Exists.rec eliminates only into Prop and that k can never be extracted into a CReal. Together they say the inverse must take its modulus as an explicit Nat argument. The proof, by contrast, need not be data: a function may TAKE a Prop argument and return a Type, so inv : (x : CReal) -> (k : Nat) -> PosBound x k -> CReal is definable while inv : (x : CReal) -> Apart x zero -> CReal is not, Apart being an Or that would have to be branched on.

Formal statement

CReal.no_total_inverse : forall (f : CReal -> CReal), Not (forall (x : CReal), CReal.Equiv (CReal.mul x (f x)) CReal.one)  --  together with  CReal.pos_of_pos_bound : forall (x : CReal) (k : Nat), CReal.PosBound x k -> CReal.lt CReal.zero x  and  CReal.pos_bound_of_lt : forall (x : CReal), CReal.lt CReal.zero x -> Exists Nat (fun (k : Nat) => CReal.PosBound x k),  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 1 direct dependents

Evidence

real-inverse-no-total-inverse

Kind: kernel-term
Status: checked

Supports: CReal.no_total_inverse is a checked Theorem -- not an axiom, not an opaque -- with an empty footprint, and the witness example's EXIT STATUS depends on its presence.

Checker command

out=$(cargo run -q --release -p axeyum-lean-kernel --example creal_setoid_witness 2>&1) && test "$(printf '%s\n' "$out" | grep -cE 'no total inverse exists = true')" = 1 && test "$(printf '%s\n' "$out" | grep -cE '[0-9]+ declarations admitted, trusted surface = 0 \(empty\)')" = 1

Evidence notes

Two anchors on one run: the guard flag, and the declaration count (76 at the time of writing; a slice that adds declarations bumps it deliberately) with the trusted surface on the same line. Deleting declare_no_total_inverse flips the example to exit 1 with a matching FAIL line and kills exactly two tests (measured); the count anchor stops the row surviving a build that quietly dropped declarations. 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-modulus-cannot-be-extracted

Kind: kernel-term
Status: checked

Supports: The two directions between positivity and a witnessed modulus are checked Theorems whose RENDERED types are the ones claimed, including the Exists that cannot be eliminated into Type.

Checker command

out=$(cargo test -q -p axeyum-lean-kernel --lib creal::creal_tests::positivity_and_a_witnessed_modulus_are_the_same_proposition 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 pass line, because a filter matching nothing prints 'ok. 0 passed' and exits 0. The test renders the types verbatim: an Exists in the CONCLUSION is what makes the modulus inextractable, and a version stating PosBound for a fixed k would pass a footprint check and fail this one.

real-inverse-negative-control

Kind: kernel-term
Status: checked

Supports: The negative control: the no_total_inverse script pointed at a FALSE statement is REFUSED by the kernel, so the theorem closes on the content of Equiv.not_zero_one and not on a shape that would go through for any right-hand side.

Checker command

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

Evidence notes

The mutated statement is 'no f makes x * f x ≈ 0 for every x', which is FALSE -- f := fun _ => zero satisfies it by mul_zero -- so a script proving it would prove anything. Without this row the other two would pass just as happily against a refutation that never used its hypothesis.

real-inverse-is-partial-and-its-modulus-is-data-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::field (ADR-0510; agent-creal-field lane)",
  "source": "Bishop-style constructive analysis: the inverse is defined on the reals APART from zero, and the apartness must carry the separating modulus"
}