Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `Normal form for distance logic`

groundedproofs/Lax3Proofs/Assembly.lean · lax-3

What this proof establishes

thm✓Lax3.NormalForm

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

The normal form for distance logic (Corollary 7 of arXiv:2606.23180): for q≥1q ≥ 1, every formula of distance rank (k,q)(k, q) is equivalent to a boolean combination of local formulas of distance rank (k,q)(k, q) and the written-out sentences "there are tt vertices, pairwise at distance larger than rr, all satisfying ββ".

Proof strategy

The claim Lax3.Locality.localityLax3.Locality.locality at the maximum-size scatter choice, with the same boolean combination. Its discharge is localitylocality above. With that choice a scatter sentence is definable in the logic — Lax3Proofs.ScatterFml.satscatterFmlLax3Proofs.ScatterFml.sat_scatterFml — so replacing each scatter atom's evaluation by satisfaction of scatterFmlscatterFml changes no truth value, and Lax3Proofs.BCAlgebra.evalcongrLax3Proofs.BCAlgebra.eval_congr carries the replacement through the combination. The five conditions the corollary states about a scatter atom are the five bridges of Lax3Proofs.ScatterFmlLax3Proofs.ScatterFml applied to the distance rank the locality theorem already provides; q≥1q ≥ 1 is used by exactly one of them, the one that climbs the rank witness back to (k+1,q−1)(k + 1, q − 1).