A five-constraint critical chain against a delivery deadline, refuted in the Lean kernel

Ran 2026-08-14. `lra_farkas_certificate` on the five core rows returns five atoms with multipliers ALL EQUAL TO 1 -- the textbook negative-cycle refutation, 6+5+6+3 = 20 against a ceiling of 16, excess 4 -- and `FarkasCertificate::verify()` re-derives it from scratch in exact rationals (nonnegative multipliers, at least one positive, every variable cancels, surviving constant relation unsatisfiable), sharing no code with the Fourier-Motzkin elimination that found it. `reconstruct_lra_proof` then builds a Lean kernel term whose `infer` succeeds and whose inferred type is `def_eq` to `False`. The example ASSERTS that the term rests on exactly 5 hypothesis axioms, one per core row, and exits 1 otherwise. `--require-kernel` makes the whole route a ratchet: if the reconstruction ever declines this query, the command fails rather than reporting a stop.

The rendered module declares 26 axioms: 17 ordered-field prelude (the `AxReal` carrier, its operations, and the order/additive laws), 4 variable axioms (one abstract `AxReal` per start time), and 5 hypothesis axioms (one per core row, in the canonical `le L zero` form). This route IS NOT AXIOM-FREE and cannot presently be: `crates/axeyum-lean-kernel/src/arith_prelude.rs` declares `AxReal` and every field law through `declare_axiom`, with no theorems and no inductives, so `[]` here would be a lie the validator would have accepted (it only rejects `[]` off the kernel-lean route). WHAT THE FACADE DOES -- this paragraph is REPLACED, not renumbered. It used to read: `prove_unsat_to_lean_module` on the SAME five rows routes to `ProofFragment::LraDpll` and emits a 21-line STRUCTURAL SHIM (`axiom prop : P`, `axiom hyp : Not P`, `theorem _ : False := hyp prop`) with no arithmetic in it, so calling that 'the Farkas proof reached the kernel' would be false. That stopped being true when the facade dispatch was fixed on 2026-08-15. Measured 2026-08-18 on this same instance: the facade routes to `ProofFragment::Lra`, emits a 62-line module that CARRIES ordered-field content (it declares an `axeyum.reconstruct.lra.hyp._N : AxReal.le ...` hypothesis axiom), self-labels `theory-reconstruction`, and the strict front door `prove_unsat_to_lean_theory_module` ACCEPTS it as `Lra` instead of declining -- so `--require-kernel` is a live ratchet on the facade route too, not only on the direct one. The example still prints and labels both routes, and still cross-checks its structural scan against the module's self-label, because the scan was silently broken for as long as the facade emitted a shim. SIZE: the kernel proof term is 5,101,317 bytes and the rendered module 5,105,945 (measured 2026-08-18). This number DRIFTS with the prelude and nothing gates it -- the 5,099,060 recorded on 2026-08-14 was 2,257 bytes smaller -- so read it as ~5.1 MB with a date, not as a pin. The prelude has no numerals, so the constant 20 reconstructs as a 20-fold `AxReal.add AxReal.one` chain and every cancellation is an explicit Eq-rewrite; a 5-row explanation becomes a 5 MB proof term. RE-RUN 2026-08-19 after ADR-0522 renamed the axiomatized package `Real` -> `AxReal`: the same checker_command exits 0 with `kernel axioms 26 = 17 prelude + 4 variable + 5 hypothesis`, so the 17 prelude rows above are the same 17 declarations under their new spelling and no row was transcribed from the old run. The module grew to 6,010,498 bytes and the proof term to 6,004,703 -- the rename is +2 bytes per occurrence and the term is mostly occurrences; the size still DRIFTS and is still not pinned. That re-run also REPAIRED this evidence: the example's `carries ordered-field content` scan matched `ty.contains("Real.le")`, which `CReal.le` satisfies, so it had been reporting the right verdict for the wrong carrier ever since the facade route moved to the constructed reals. It now names both carriers in full.