looseBVarRange_eq was always a theorem: 28 → 27

[vasnesterov]

Part of #19. Frozen files change — needs your review. Whitelist 28 → 27.

Lean.Expr.looseBVarRange_eq is derivable from Expr.mkData_eq and mkAppData_eq, both already whitelisted. It becomes a @[simp] theorem with the identical statement, so there is no downstream churn.

This is the cheapest of the three reductions. The other two needed a side condition that consumers then had to discharge. This one needs nothing — the condition it requires is the one the axiom already carried. It was always a theorem, sitting in the whitelist unexamined.

#print axioms Lean.Expr.looseBVarRange_eq
→ [propext, Quot.sound, Lean.Expr.mkAppData_eq, Lean.Expr.mkData_eq]

No self-reference. No _native axiom reachable from Axioms.lean.

The side condition is necessary absolutely, not relative to a model

not_looseBVarRange_eq_unconditional (already on master, in Tests/AxiomConsistencyExpr.lean) proves ¬ ∀ e, e.looseBVarRange = e.looseBVarRange' at [propext, Quot.sound] — no axiom at all, since the cached field is 20 bits and the model is unbounded. That is the original False-proof preserved as a live theorem, with a companion lemma recording that its witness fails BVarBounded, so the two results cannot collide. A historical inconsistency that can no longer be silently re-broken.

A structural finding, recorded in the docstring

Only the bvar clause of BVarBounded does any work. The other ten Expr.data clauses pass arguments built from looseBVarRange field reads, which the 20-bit bound covers unconditionally. So its operative content is exactly every bvar index is < 2^20 - 1, and the recursion exists only to reach the leaves. It cannot be weakened at the leaves, and need not be strengthened anywhere else.

Verification — built, not read

• lake build, all default targets, 1291 jobs, exit 0. Zero downstream churn, as the identical-statement claim predicted.
• Count re-derived with guard 1's own instrument (enumerating axiomInfo constants by declaring module, not a grep): 27, with looseBVarRange_eq absent from that list and present as a thmInfo.
• guard 1: … exactly the 27 frozen axioms ✓; guards 2 and 3 unchanged.
• I re-ran the count and the guards independently of the agent that made the edit, and separately confirmed this branch builds without the in-flight Verify/Expr.lean work, so the two landings are not entangled.

Layering

The proof is inline. That inverts nothing — everything it needs is declared above it in the same file. Its private helpers duplicate facts Verify/Expr.lean also proves; that is deliberate, for the same reason the Verify/Level.lean re-proof chose duplication (a shared home would have had to import the frozen file). The docstring says so, so nobody "fixes" it later.

Where this leaves #19

Class (B) — the only class either historical False-proof came from — is now exactly the three container axioms (PersistentArray.WF.toList'_push, PersistentHashMap.WF.toList'_insert, WF.find?_eq). They differ in kind from everything closed so far: their right-hand sides are not bit arithmetic but the correctness of a persistent-array and a HAMT algorithm, so exhibiting a model means proving those algorithms correct. That is the whole remaining consistency risk in the file.

🤖 Generated with Claude Code

[vasnesterov]

I approve, merge