A registered result in its source context

FORM.QGEO.01

Original ledger classification: Formal [F] (conditional theorem) + [O] (the seam-deck premise)

Original claim text

LEAN 4 FORMALISATION of the QGEO.SYM.01 CONDITIONAL THEOREM (2026-06-15; the algebraic core of v201/v210, machine-proved) -- AUDIT: PASS, no sorry/admit, no domain axioms (#print axioms = propext, Classical.choice, Quot.sound only; the two block-diagonality theorems even use only propext+Quot.sound). New module TfptCarrier/SeamDeckClosure.lean proves: (1) [F] geom_sum_fourth_root: for ζ:ℂ with ζ^4=1, Σ_{j<4} ζ^j = (if ζ=1 then 4 else 0) -- the 4th-root character orthogonality (finite geometric sum) that makes a μ4-mark sum vanish off mod 4; (2) [F] clock_gen_pow_four + mark_sum_residue_nonzero: the clock generator -i has order 4 and the three non-trivial residues give a vanishing mark sum, so a μ4-mark-sourced curvature is supported only on modes ≡0 (mod 4); (3) [F] markLocal_blockDiagonal: a mark-local Toeplitz symbol (support ⊆ {m : (m:ZMod 4)=0}) connects only equal clock-characters (f_{n-n'}≠0 ⇒ (n:ZMod4)=(n':ZMod4)), i.e. [ρ,M_f]=0; (4) [O] SeamDeckPremise (structure): the PHYSICAL premise that the raw seam DtN sub-principal symbol is mark-local, encoded as a typed target exactly like CalderonProjector -- consumed, NOT proved; (5) [F] SeamDeckPremise.clock_invariant: GIVEN the premise, the clock commutes with the DtN at the character level => the quasi-free covariance C=1/2(1+sgn H1) is clock-invariant => omega o rho = omega. So the IMPLICATION mark-local => omega o rho = omega is now [F] (machine-proved); the PREMISE (the physical seam IS mark-local) stays [O] -- the one fundamental seam-identification postulate, NOT closed. Complements FORM.GLUE.01/FORM.LADDER.01; mirrors v201/v210.

Original classification detail

Formal [F]/[O]: the QGEO.SYM.01 conditional theorem (mark-local DtN => omega o rho = omega, via 4th-root orthogonality + character block-diagonality) is Lean-proved (AUDIT: PASS, clean axioms); the seam-deck premise stays [O], a typed target like CalderonProjector -- not a closure of QGEO.SYM.01

Dependencies as recorded

QGEO.MARKLOCAL.01; QGEO.SUBPRIN.01; QGEO.MARKS.01; FORM.GLUE.01