A Farkas refutation closes over the constructed reals resting on zero carrier axioms, where the same refutation over the axiomatized AxReal package rests on 30

Identifier: F:farkas-refutation-over-constructed-reals
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let the ordered-ring reconstruction be given a ring signature whose carrier is CReal -- the Bishop setoid of regular rational sequences -- and whose equality is the DEFINED relation CReal.Equiv rather than the kernel's Eq. Then for each of five infeasible linear/SOS systems the reconstruction closes a kernel-checked False whose axiom footprint contains NO carrier axiom: the residue is exactly the query's own variable and hypothesis axioms. Over the axiomatized AxReal package the identical refutations carry 30 carrier axioms, which is the whole of this repository's remaining trusted surface. Separately, the equality slot the reconstruction needs costs 18 DECLARED AXIOMS over AxReal and 0 declarations over CReal, because the nine slot members are CReal's own theorems and are adopted rather than assumed.

Formal statement

For each fixture F, reconstruct(F, RingSignature { r := CReal, equality := Defined CReal.Equiv, .. }) yields a term of type False whose Kernel::axiom_footprint, intersected with the abstracted ordered-ring telescope, is empty. Carrier axioms are MEASURED as footprint intersect telescope, not selected by name prefix. The generalized (carrier-free) form has 39 ring binders, an empty footprint, and zero kernel-Eq constants in the proof term.

Dependencies

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

2 direct dependencies 1 direct dependents

Evidence

creal-equality-slot-costs-nothing

Kind: kernel-term
Status: checked

Supports: The equality slot is ADOPTED from CRealPrelude at 0 declarations added, against 18 axioms declared for the same slot over AxReal.

Checker command

out=$(cargo run -q -p axeyum-solver --features full --example ordered_ring_refutation -- --constructed-reals 2>&1) && test "$(printf '%s\n' "$out" | grep -Ec '^[[:space:]]+equality slot: .CReal[.]Equiv. adopted from CRealPrelude -- 0 declarations added [(]the .AxReal. route declares 18 AXIOMS')" -ge 1

Evidence notes

Anchored on BOTH numbers in one line, so the row fails if adoption starts declaring anything and equally if the AxReal comparison it is measured against stops being 18. Both are read from Environment::len before and after, not from a constant. Verified to fail when the line is mutated to '18 declarations added'.

no-carrier-axiom-in-any-fixture

Kind: kernel-term
Status: checked

Supports: All five fixtures close a False over CReal with zero carrier axioms in the footprint.

Checker command

out=$(cargo run -q -p axeyum-solver --features full --example ordered_ring_refutation -- --constructed-reals 2>&1) && test "$(printf '%s\n' "$out" | grep -cE '^[[:space:]]+over CReal : closed False -- footprint [0-9]+ of which 0 are CARRIER axioms')" = 5

Evidence notes

Counts rather than greps: `grep -q` would pass on ONE surviving fixture if the other four regressed or were dropped. The footprint size is left free because it is the query's own variables and hypotheses and legitimately differs per fixture (2 to 7); what is pinned is that none of it is carrier. Verified to fail when a single row is mutated to '1 are CARRIER axioms'.

the-real-comparison-is-not-vacuous

Kind: kernel-term
Status: checked

Supports: The same five fixtures over the axiomatized AxReal package carry 30 carrier axioms each, so the CReal result is a reduction rather than a measurement of nothing.

Checker command

out=$(cargo run -q -p axeyum-solver --features full --example ordered_ring_refutation -- --constructed-reals 2>&1) && test "$(printf '%s\n' "$out" | grep -cE '^[[:space:]]+over AxReal: closed False -- footprint [0-9]+ of which 30 are CARRIER axioms')" = 5

Evidence notes

Without this row the fact would still pass if the AxReal route quietly stopped depending on its own axioms, which would mean the comparison had become trivial rather than that CReal had achieved anything. 30 is the ledger's whole `real` trusted surface, so this row also fails if that number moves for any reason.

population-verdict

Kind: kernel-term
Status: checked

Supports: The example's own aggregate verdict, which it computes from the per-fixture measurements rather than printing unconditionally.

Checker command

out=$(cargo run -q -p axeyum-solver --features full --example ordered_ring_refutation -- --constructed-reals 2>&1) && test "$(printf '%s\n' "$out" | grep -xEc 'closed refutations over the CONSTRUCTED reals rest on zero carrier axioms: true')" -ge 1

Evidence notes

`grep -x` on the whole line including the trailing `true`: an unanchored match would also accept the `false` rendering of the same sentence. The example's exit status is 0 either way, so a row checking only the command's exit code would pass on a negative result -- the failure mode this ledger keeps finding. Both streams are captured (`2>&1`) because a summary on stderr with `2>/dev/null` matches nothing and passes for the wrong reason.

Provenance

{
  "date": "2026-08-18",
  "established_by": "adopt_setoid_equality + RingSignature seam (agent-real-migration, agent-creal-reconstruct lanes); ADR-0512 phase R4",
  "source": "hand-built; Farkas' lemma over an ordered commutative ring, instantiated at a constructed carrier"
}