No shipped reconstruction route BUILDS the AxReal axiom package: the trusted surface is declared but never reached

Identifier: F:shipped-front-door-reaches-no-real-axiom
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

The 30 declarations of the axiomatized AxReal package are this repository's entire remaining trusted surface (real: axiom=30, and 30 of 30 rows of the Lean axiom ledger). No route reachable from prove_unsat_to_lean_module -- the public entry point that turns an unsatisfiable query into a self-contained Lean module -- constructs them. Measured by a process-global counter on build_arith_prelude itself, driven through the front door on one fixture per arithmetic arm (Lra, Sos, DisjunctiveLra, IntFarkas): the count is zero after all four, and one after the same process builds the package on purpose. This is strictly stronger than the emitted proof term having an empty AxReal footprint, and the two answers were different until 2026-08-18: the IntFarkas arm refuted over AxReal, abstracted all 30 constants back out and instantiated at the integers, so it built the whole trusted surface to produce a module that named none of it.

Formal statement

Let B(t) be the value of axeyum_lean_kernel::arith_prelude_builds() -- a process-global counter incremented by build_arith_prelude, the only public entry point that declares the 30 AxReal axioms into a kernel. In a process that has built nothing, B = 0; after prove_unsat_to_lean_module(F) returns for each of four fixtures F, one per arithmetic fragment (Lra, Sos, DisjunctiveLra, IntFarkas), B = 0 still; after LraReconstructCtx::try_new() is then called in the same process, B = 1.

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

shipped-front-door-reaches-no-real-axiom-1

Kind: kernel-term
Status: checked

Supports: The negative control: the counter DOES move. After the four measurements the same process builds the AxReal package on purpose and the counter reads 1.

Checker command

out=$(cargo test -q -p axeyum-solver --features full --test front_door_reaches_no_real_axiom -- --nocapture 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'FRONT_DOOR_REACH control \| arith_prelude_builds=1$')" -ge 1

Evidence notes

Without this row every other row here would pass just as happily against an arith_prelude_builds() wired to return 0. This is the row that makes the four zeros a finding rather than a broken instrument, and it is anchored on the value 1 -- not on `nonzero` -- because the control builds the package exactly once.

shipped-front-door-reaches-no-real-axiom-2

Kind: kernel-term
Status: checked

Supports: The purely conjunctive real Farkas arm reaches no AxReal axiom.

Checker command

out=$(cargo test -q -p axeyum-solver --features full --test front_door_reaches_no_real_axiom -- --nocapture 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'fragment=Lra module=[0-9]+ arith_prelude_builds=0$')" -ge 1

Evidence notes

Anchored on the fragment AND the counter value on the same line, so a fixture that silently stopped routing to Lra cannot satisfy it. `module=[0-9]+` is left free because the module size is not the claim.

shipped-front-door-reaches-no-real-axiom-3

Kind: kernel-term
Status: checked

Supports: The sum-of-squares arm -- the only one that touches the multiplicative laws and sq_nonneg -- reaches no AxReal axiom.

Checker command

out=$(cargo test -q -p axeyum-solver --features full --test front_door_reaches_no_real_axiom -- --nocapture 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'fragment=Sos module=[0-9]+ arith_prelude_builds=0$')" -ge 1

Evidence notes

Same anchoring. Sos is listed separately from Lra because it is a different reconstructor (reconstruct_sos_to_lean_module), not a different fixture through the same one.

shipped-front-door-reaches-no-real-axiom-4

Kind: kernel-term
Status: checked

Supports: The Or.rec case-split arm reaches no AxReal axiom.

Checker command

out=$(cargo test -q -p axeyum-solver --features full --test front_door_reaches_no_real_axiom -- --nocapture 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'fragment=DisjunctiveLra module=[0-9]+ arith_prelude_builds=0$')" -ge 1

Evidence notes

Same anchoring. `fragment=DisjunctiveLra` cannot be matched by the Lra pattern only because that pattern requires the space after `Lra`; both are pinned separately so a collapse of one arm into the other is visible.

shipped-front-door-reaches-no-real-axiom-5

Kind: kernel-term
Status: checked

Supports: The integer Farkas arm -- the one that DID build all 30 until 2026-08-18 -- reaches no AxReal axiom.

Checker command

out=$(cargo test -q -p axeyum-solver --features full --test front_door_reaches_no_real_axiom -- --nocapture 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'fragment=IntFarkas module=[0-9]+ arith_prelude_builds=0$')" -ge 1

Evidence notes

The row this fact exists for. Restore the pre-2026-08-18 body of reconstruct_int_farkas_to_lean_module and this row is the one that fails -- mutation-checked, and all nine tests of tests/farkas_over_the_integers.rs, the suite named for this route, pass under that mutation because they assert on the module and the footprint, both of which were already clean.

shipped-front-door-reaches-no-real-axiom-6

Kind: kernel-term
Status: checked

Supports: The measurement ran to completion: the single test in this binary passed, so no fixture was skipped and no assertion was left unevaluated.

Checker command

out=$(cargo test -q -p axeyum-solver --features full --test front_door_reaches_no_real_axiom -- --nocapture 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'test result: ok\. 1 passed')" -ge 1

Evidence notes

Completion alone is not a finding, which is why this row is not the only one. It is here because the counter rows are printed BEFORE they are asserted: an output carrying four `arith_prelude_builds=0` lines and a failed assertion afterwards would satisfy the pattern rows on its own.

shipped-front-door-reaches-no-real-axiom-7

Kind: kernel-term
Status: checked

Supports: The POPULATION: exactly four fixtures reported zero. A row that stopped being measured -- deleted, renamed, or routed to a different fragment -- fails this count instead of shrinking the evidence silently.

Checker command

out=$(cargo test -q -p axeyum-solver --features full --test front_door_reaches_no_real_axiom -- --nocapture 2>&1) && test "$(printf "%s\n" "$out" | grep -cE 'FRONT_DOOR_REACH .*arith_prelude_builds=0$')" = 4

Evidence notes

The count is 4 and not `at least one`. `grep -q` over the same pattern would pass on a single surviving fixture, which is exactly how the previous gate for this claim (examples/front_door_carrier.rs, three real-typed fixtures) reported an axiom-free front door while the integer arm built all 30: it was never pointed at that arm.

Provenance

{
  "date": "2026-08-18",
  "established_by": "axeyum-lean-kernel arith_prelude::arith_prelude_builds + axeyum-solver tests/front_door_reaches_no_real_axiom.rs (agent-retire-real lane, commit b20720e9f)",
  "source": "measured in this repository; no external source"
}