Delete the false axiom liftLooseBVars_eq: 29 → 28

[vasnesterov]

Part of #19. Frozen files change — needs your review.

Lean.Expr.liftLooseBVars_eq is false, and it has zero dependents, so this deletes it rather than weakening it. Whitelist 29 → 28.

The defect

The C wrapper starts with a bignum guard, before the algorithm:

if (!lean_is_scalar(s) || !lean_is_scalar(d)) { lean_inc(e); return e; }

Witness e := .bvar 0, s := 0, d := 2^63. Checked by two different instruments, because the two sides cannot be evaluated in one expression — #eval of the model's answer trips lean_expr_mk_data's own panic:

side	instrument	result
C	differential test on compiled code	#eval idx ((Expr.bvar 0).liftLooseBVars 0 (2^63)) → "bvar 0"
model	kernel reduction	liftLooseBVars' (.bvar 0) 0 (2^63) = .bvar (2^63)

So the axiom asserts .bvar 0 = .bvar (2^63).

Unlike the panic cases fixed earlier, the call completes — no panic, both arguments ordinary. Only the model's output is not runtime-constructible.

Why delete rather than bound

An axiom-cone scan (Lean.collectAxioms) over every non-internal Lean4Lean.* declaration:

axiom	dependents
liftLooseBVars_eq	0
the other 13 in scope	35 – 162 each

Zero for a structural reason: the checker never calls Expr.liftLooseBVars. A grep could not have established this — the axiom is @[simp] and has no explicit call sites either way, while a @[simp] lemma that fires does appear in the proof term. So deletion cannot break a proof.

The model liftLooseBVars' stays, decided by the same instrument rather than by eye: a constant-dependency scan gives it 29 direct users including instantiate1'. It is the axiom that was false, not the model. A tombstone in Axioms.lean records all of this in place.

If you would rather keep a bounded statement than delete: the guard needs both arguments, s < 2^63 ∧ d < 2^63, not d alone — and a USize restatement does not fit without changing the signature.

Verification

• Count re-derived independently using guard 1's own method (enumerating axiomInfo constants whose defining module is Lean4Lean.Verify.Axioms): 28, list matching the whitelist name-for-name.
• All 8 count sites in Guard.lean updated. The two historical re-pin sentences left as history; a new paragraph records this one.
• lake build exit 0; Lean4Lean.Tests exit 0.
• guard 1: … exactly the 28 frozen axioms ✓; guards 2 and 3 unchanged.
• The Level section is untouched — another stream is working there and may also re-pin; whoever lands second re-pins again.

Method correction, in §2 where the next audit starts

Check 1 read the C workers faithfully and skipped the extern "C" wrapper, which is where argument validation lives.

For any @[extern] axiom, read the wrapper first and enumerate every early return before reading the algorithm.

A Nat crossing into C arrives boxed and is always lean_is_scalar-guarded at 2^63; the guard either panics or silently substitutes a fallback — and the fallback is what the axiom must match. Seven of fourteen axioms in scope sit on one, resolving four different ways: one false (this one), two surviving with machine-checked agreement lemmas, one surviving for a reason the audit had not stated, and two whose side condition turns out necessary but not sufficient.

Companion rule also recorded: an identity holding only through an @[extern]/@[export] linker pairing is weaker than a definitional one and can never be discharged by rfl — so record which kind you have. One axiom's stated justification was wrong in exactly that way, while its verdict was right.

🤖 Generated with Claude Code

[vasnesterov]

I approve, merge