The 30 AxReal axioms are satisfiable: a Bishop setoid over the constructed rationals models all 22 laws at zero trusted declarations

Identifier: F:real-axioms-modelled-by-constructed-setoid
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let CReal be the type of regular Cauchy sequences of rationals over the kernel's CONSTRUCTED rationals -- a one-constructor carrier with no quotient -- and let CReal.Equiv be the defined relation x ~ y iff |x_n - y_n| <= 2/(n+1) for every n. Then interpreting the AxReal package's eight carrier/operation symbols at CReal and its equality at CReal.Equiv makes all 22 ordered-commutative-ring laws PROVABLE, each by a theorem whose axiom footprint is empty. Thirteen of the 22 are the AxReal statements verbatim; the other nine mention Eq and are restated over CReal.Equiv, because Eq CReal is not equality of real numbers.

Formal statement

For each law L of the AxReal package, AxReal.CRealModel.L : interpret(type of AxReal.L) := CReal.L, where interpret substitutes the eight CReal symbols for the AxReal ones and rewrites the partial application (Eq AxReal) to CReal.Equiv. The obligation is COMPUTED from the axiom as it stands in the environment, so a changed axiom changes the obligation.

Dependencies

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

3 direct dependencies 4 direct dependents

Evidence

creal-model-add_comm

Kind: kernel-term
Status: checked

Supports: The additive-commutativity law of the AxReal package is modelled by CReal.add_comm, with an empty axiom footprint.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example creal_model_witness 2>/dev/null) && test "$(printf '%s\n' "$out" | grep -Ec '^law[[:space:]]+AxReal[.]add_comm[[:space:]]+CReal[.]add_comm[[:space:]]+\[\][[:space:]]')" -ge 1

Evidence notes

Anchored on the AxReal law name, the CReal witness name AND the empty footprint column, so a rename, a swapped pairing, or a witness that grew a dependency on a trusted declaration all fail. Verified to fail when the subject is mangled.

creal-model-mul_comm

Kind: kernel-term
Status: checked

Supports: A multiplicative law is modelled too -- multiplication is the half that needed a canonical bound derived from regularity.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example creal_model_witness 2>/dev/null) && test "$(printf '%s\n' "$out" | grep -Ec '^law[[:space:]]+AxReal[.]mul_comm[[:space:]]+CReal[.]mul_comm[[:space:]]+\[\][[:space:]]')" -ge 1

Evidence notes

Second law from the other half of the ring structure, so the pair cannot both pass on additive-only work.

creal-model-population

Kind: kernel-term
Status: checked

Supports: All 22 laws are modelled, all footprints empty, and the seven discrimination witnesses hold -- the example exits non-zero otherwise.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example creal_model_witness 2>&1) && test "$(printf '%s\n' "$out" | grep -Ec '22/22 witnesses have an EMPTY axiom footprint')" -ge 1

Evidence notes

Captures BOTH streams: the per-law rows go to stdout and the summary to stderr, so the obvious `2>/dev/null` form silently matches nothing and passes for the wrong reason. Found by running this row before committing it. The population comes from the environment rather than a hand-written table, so dropping a law fails the coverage check instead of shrinking a count.

Provenance

{
  "date": "2026-08-18",
  "established_by": "axeyum-lean-kernel creal + creal_model modules (ADR-0512 phases R2 and R4; agent-creal-*, agent-r4-model lanes)",
  "source": "hand-built from the constructed rationals; Bishop's regular-sequence construction"
}