A Lean query module over the constructed reals shrinks 257x when the shared development is imported rather than inlined

Identifier: F:lean-query-module-shrinks-by-a-shared-import
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

Rendering a refutation over the constructed reals as a query module that imports a separately-compiled shared development, instead of a single self-contained file, takes the per-query artefact from 1,304,276 bytes to 5,056 bytes (257x); the shared module is byte-identical across the three front-door fixtures; the two halves together cover the kernel's axiom footprint exactly; and every refutation still rests on zero carrier axioms. The split is a strictly weaker artefact: it needs the shared module compiled to an .olean and found on LEAN_PATH (ADR-0511).

Formal statement

Let K be the kernel state of `LraReconstructCtx::try_new_over_constructed_reals()` extended with a refutation `p : False` for the query `x < 0 and 0 <= x`, C the set of declaration names present before the query symbols were admitted, and R = C intersect `declarations_reached([False, p])`. Then |render_lean_module_compact_importing(K, p, render_lean_prelude_module(K, R))| = 5056 and |render_lean_module_compact(K, p)| = 1304276; the prelude module is a function of R alone, so it is byte-identical for every query with the same R; and every name in `axiom_footprint(p)` is declared by an `axiom` line in exactly one of the two modules, with the query module declaring no `axiom` outside that footprint.

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

F:lean-query-module-shrinks-by-a-shared-import-1

Kind: instance-pin
Status: checked

Supports: The shared half is a function of the ROOT SET and nothing else, so one compiled `.olean` serves the whole query family. Without this the split is a relabelling: each query would need its own prelude and the per-query total would be unchanged.

Checker command

out=$(cargo run -q -p axeyum-solver --features full --example shared_prelude_module -- --require-split 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'the shared module is byte-identical across fixtures: true')" -ge 1

Evidence notes

Verified discriminating by scripts/new-fact.py: the pattern matches the real output and fails on mutated output. Anchored on the byte-identity verdict rather than on the shared module's size: a size match is consistent with two different modules of equal length, and identity is the property the claim needs.

F:lean-query-module-shrinks-by-a-shared-import-2

Kind: instance-pin
Status: checked

Supports: Nothing the kernel's `axiom_footprint` counts went missing when the module was split, and the query half introduced no assumption the kernel did not count. This is the split's form of the invariant `front_door_carrier --require-axiom-free` enforces on the single file; a smaller artefact that dropped a footprint entry would be a regression however good the byte count looked. It is coverage and NOT a summed line count, because the shared half legitimately carries axioms a given refutation never reaches.

Checker command

out=$(cargo run -q -p axeyum-solver --features full --example shared_prelude_module -- --require-split 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'the two halves cover the kernel footprint exactly: true')" -ge 1

Evidence notes

Verified discriminating by scripts/new-fact.py: the pattern matches the real output and fails on mutated output. Anchored on the two-directional coverage verdict, not on an axiom-line count. A count is what the single-file invariant uses and it is WRONG here — the shared half is rooted at a union over the query family, so it carries axioms this refutation never reaches and a sum would exceed the footprint for a module set that is entirely correct.

F:lean-query-module-shrinks-by-a-shared-import-3

Kind: instance-pin
Status: checked

Supports: The headline result is unmoved by the layout change: the refutation still rests on zero CARRIER axioms, only on the query's own variable and hypotheses. This is what stops the byte saving from being bought by re-admitting an assumption.

Checker command

out=$(cargo run -q -p axeyum-solver --features full --example shared_prelude_module -- --require-split 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'refutations still rest on zero carrier axioms: true')" -ge 1

Evidence notes

Verified discriminating by scripts/new-fact.py: the pattern matches the real output and fails on mutated output. Anchored on the carrier-axiom verdict, which is computed from `Kernel::axiom_footprint` (this kernel's `#print axioms`) and not from module text.

F:lean-query-module-shrinks-by-a-shared-import-4

Kind: instance-pin
Status: checked

Supports: The saving is real on every fixture, not only the one the byte figures quote — the weakest of the three is 91x.

Checker command

out=$(cargo run -q -p axeyum-solver --features full --example shared_prelude_module -- --require-split 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'every query module is at least 50x smaller: true')" -ge 1

Evidence notes

Verified discriminating by scripts/new-fact.py: the pattern matches the real output and fails on mutated output. Anchored on the floor verdict, which is over the MINIMUM factor across the three fixtures, so a regression on any one of them fails it.

F:lean-query-module-shrinks-by-a-shared-import-5

Kind: instance-pin
Status: checked

Supports: The exact bytes, on the fixture the title quotes. The other four rows are verdicts a rewrite could keep true while the numbers moved; this one pins them.

Checker command

out=$(cargo run -q -p axeyum-solver --features full --example shared_prelude_module -- --require-split 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec '5056 B query \+ 1715764 B shared')" -ge 1

Evidence notes

Verified discriminating by scripts/new-fact.py: the pattern matches the real output and fails on mutated output. Anchored on the two byte counts printed together on one line, so neither can drift without the other being noticed. It is the row that fails first if the carrier grows or the writer regresses.

Provenance

{
  "date": "2026-08-18",
  "established_by": "agent-lean-prelude-module",
  "source": "ADR-0511; crates/axeyum-solver/examples/shared_prelude_module.rs; crates/axeyum-lean-kernel/tests/real_lean_shared_prelude_crosscheck.rs"
}