TFPT scientific source excerpt
Original repository path: experiments/lean4-carrier-rigidity/TfptCarrier/GlueUniqueness.lean
Original file SHA-256: 51e98673e96f4344fec729c2874a947dcc1f31f5787983af3267e113fd329df2
Inclusive original lines: 34-132
Line numbers below refer to the original source.
This bounded excerpt is source evidence; it is not a new proof/checker run.
Conversation metadata and personal execution details are omitted where indicated.

000034 | import Mathlib.Tactic
000035 | 
000036 | namespace TFPT.Carrier.GlueUniqueness
000037 | 
000038 | /-- Group element of the discriminant group `A = ℤ₄ × ℤ₄`, as `Fin 4 × Fin 4`
000039 | with componentwise addition mod 4 (we keep it concrete for kernel `decide`). -/
000040 | abbrev El := Fin 4 × Fin 4
000041 | 
000042 | /-- Addition mod 4 on the discriminant group. -/
000043 | def add (a b : El) : El := (a.1 + b.1, a.2 + b.2)
000044 | 
000045 | /-- The integer-valued quadratic-form representative: `q(x,y) = (5x²+3y²)/8
000046 | mod 1` vanishes iff `(5x² + 3y²) mod 8 = 0`. -/
000047 | def qZ (a : El) : ℕ := (5 * a.1.val ^ 2 + 3 * a.2.val ^ 2) % 8
000048 | 
000049 | /-- Isotropy: the quadratic form vanishes (mod 1). -/
000050 | def isotropic (a : El) : Prop := qZ a = 0
000051 | 
000052 | instance (a : El) : Decidable (isotropic a) := by unfold isotropic; infer_instance
000053 | 
000054 | /-- The cyclic subgroup generated by `g` (as the explicit four-element orbit;
000055 | for order-4 elements of `ℤ₄ × ℤ₄` this is the full subgroup). -/
000056 | def orbit (g : El) : List El := [(0, 0), g, add g g, add (add g g) g]
000057 | 
000058 | /-- **(1) Isotropic elements, classified.**  Exactly six of the sixteen
000059 | elements are isotropic: `(0,0), (1,1), (1,3), (2,2), (3,1), (3,3)`. -/
000060 | theorem isotropic_elements_classified :
000061 |     ∀ a : El, isotropic a ↔
000062 |       a ∈ ([((0:Fin 4),(0:Fin 4)), (1,1), (1,3), (2,2), (3,1), (3,3)] : List El) := by
000063 |   decide
000064 | 
000065 | /-- **(2) Order-4 isotropic generators.**  The isotropic elements of order 4
000066 | (i.e. with an odd coordinate) are exactly `(1,1), (1,3), (3,1), (3,3)`. -/
000067 | theorem isotropic_order4_classified :
000068 |     ∀ a : El, (isotropic a ∧ (a.1.val % 2 = 1 ∨ a.2.val % 2 = 1)) ↔
000069 |       a ∈ ([((1:Fin 4),(1:Fin 4)), (1,3), (3,1), (3,3)] : List El) := by
000070 |   decide
000071 | 
000072 | /-- The first Lagrangian glue `H₁ = ⟨(1,1)⟩`. -/
000073 | def H1 : List El := orbit (1, 1)
000074 | 
000075 | /-- The second Lagrangian glue `H₂ = ⟨(1,3)⟩`. -/
000076 | def H2 : List El := orbit (1, 3)
000077 | 
000078 | /-- **(2'a) `⟨(3,3)⟩ = H₁` as element sets** (the four generators give only
000079 | two subgroups, first pair). -/
000080 | theorem orbit33_eq_H1 : ∀ a : El, a ∈ orbit (3, 3) ↔ a ∈ H1 := by
000081 |   decide
000082 | 
000083 | /-- **(2'b) `⟨(3,1)⟩ = H₂` as element sets** (second pair). -/
000084 | theorem orbit31_eq_H2 : ∀ a : El, a ∈ orbit (3, 1) ↔ a ∈ H2 := by
000085 |   decide
000086 | 
000087 | /-- **(2'c) Both glues are fully isotropic** (explicit element check:
000088 | `H₁ = {0,(1,1),(2,2),(3,3)}`, `H₂ = {0,(1,3),(2,2),(3,1)}`). -/
000089 | theorem glues_isotropic :
000090 |     qZ (0, 0) = 0 ∧ qZ (1, 1) = 0 ∧ qZ (2, 2) = 0 ∧ qZ (3, 3) = 0 ∧
000091 |     qZ (1, 3) = 0 ∧ qZ (3, 1) = 0 := by
000092 |   decide
000093 | 
000094 | /-- **(3) Klein exclusion.**  The unique Klein four-subgroup
000095 | `{0,(2,0),(0,2),(2,2)}` of `ℤ₄ × ℤ₄` is not isotropic: `qZ (2,0) = 4 ≠ 0`.
000096 | Hence every order-4 isotropic subgroup contains an order-4 element, is
000097 | cyclic, and by (2)/(2') equals `H₁` or `H₂`: the Lagrangian glue is unique
000098 | up to the spinor swap. -/
000099 | theorem klein_not_isotropic : ¬ isotropic ((2 : Fin 4), (0 : Fin 4)) := by
000100 |   decide
000101 | 
000102 | /-- **(3') The spinor swap `(x,y) ↦ (x,-y)` exchanges the two glues**
000103 | (stated as the explicit image lists: `swap(H₁) = ⟨(1,3)⟩`-orbit and
000104 | `swap(H₂) = ⟨(1,1)⟩`-orbit). -/
000105 | theorem spinor_swap_exchanges :
000106 |     H1.map (fun a => ((a.1, -a.2) : El)) = [(0, 0), (1, 3), (2, 2), (3, 1)] ∧
000107 |     H2.map (fun a => ((a.1, -a.2) : El)) = [(0, 0), (1, 1), (2, 2), (3, 3)] := by
000108 |   decide
000109 | 
000110 | /-- **(4) The unique halfway stage.**  The only isotropic element of exact
000111 | order 2 is `(2,2)`; the unique isotropic order-2 subgroup is `{0,(2,2)}`
000112 | (the `SO(16)₁` intermediate of the extension tower). -/
000113 | theorem unique_halfway_stage :
000114 |     ∀ a : El, (isotropic a ∧ a ≠ (0, 0) ∧ add a a = (0, 0)) ↔
000115 |       a = ((2 : Fin 4), (2 : Fin 4)) := by
000116 |   decide
000117 | 
000118 | /-- **Carrier Index Lemma (v89, arithmetic core).**
000119 | `μ(carrier) = μ(D₅)·μ(A₃) = 16`, `μ(E₈) = 1`; the KLM relation
000120 | `μ_A = [B:A]² μ_B` forces the Jones index `[B:A] = 4 = |μ₄| = |ℤ₂|²`,
000121 | and μ-additivity `16 / 4² = 1` recovers holomorphy from the index. -/
000122 | theorem carrier_index_lemma :
000123 |     4 * 4 = 16 ∧ (4 : ℕ) ^ 2 * 1 = 16 ∧ 16 / 4 ^ 2 = 1 ∧ 4 = 2 ^ 2 := by
000124 |   decide
000125 | 
000126 | /-- **Level-1 current check (v89).**  The three non-vacuum glue sectors are
000127 | currents: with weights in eighths, `h(v)+h(6) = 4/8+4/8 = 1`,
000128 | `h(s)+h(4̄) = 5/8+3/8 = 1`, `h(c)+h(4) = 5/8+3/8 = 1`; and the adjoint
000129 | branching `248 = 45 + 15 + 64 + 64 + 60` closes. -/
000130 | theorem glue_sectors_are_currents :
000131 |     4 + 4 = 8 ∧ 5 + 3 = 8 ∧ 45 + 15 + 16 * 4 + 16 * 4 + 10 * 6 = 248 := by
000132 |   decide