`gauge_sector_dim`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.SpectralEmergence
domain: Foundation
line: 174 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.SpectralEmergence on GitHub at line 174.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 171
 172/-- **THEOREM**: The gauge sector dimensions (excluding conjugate) sum to 6.
 173    This is the dimension of the "physical" representation. -/
 174theorem gauge_sector_dim :
 175    SpectralSector.dim .color +
 176    SpectralSector.dim .weak +
 177    SpectralSector.dim .hypercharge = 6 := by
 178  norm_num [SpectralSector.dim]
 179
 180/-- **THEOREM**: The residual dimension (conjugate sector) is forced:
 181    8 - 6 = 2 = dim(conjugate). -/
 182theorem conjugate_dim_forced :
 183    V 3 - (SpectralSector.dim .color +
 184            SpectralSector.dim .weak +
 185            SpectralSector.dim .hypercharge) =
 186    SpectralSector.dim .conjugate := by
 187  norm_num [V, SpectralSector.dim]
 188
 189/-- **THEOREM**: Total gauge generators: 8 + 3 + 1 = 12 = |E(Q₃)|.
 190    The gauge degrees of freedom equal the edge count of Q₃. -/
 191theorem gauge_generators_eq_edges :
 192    SpectralSector.gauge_rank .color +
 193    SpectralSector.gauge_rank .weak +
 194    SpectralSector.gauge_rank .hypercharge = E 3 := by
 195  norm_num [SpectralSector.gauge_rank, E]
 196
 197/-! ## Part 3: Generation Structure — Three Families from Face Pairs
 198
 199The Q₃ cube has 6 faces organized into 3 opposite pairs. Each face pair
 200corresponds to a normal axis. The 3 face pairs force exactly 3 generations
 201of fermions. -/
 202
 203/-- **THEOREM**: D = 3 forces exactly 3 generations. -/
 204theorem three_generations : face_pairs 3 = 3 := by native_decide

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.