theorem proved term proof

`sm_factorization`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 223theorem sm_factorization :
 224    (48 : ℕ) = 6 * 4 * 2 := by norm_num

proof body

Term-mode proof.

 225
 226/-! ## Part 5: Gauge Rank Correspondence -/
 227
 228/-- The **gauge rank** of a layer: the number of independent generators.
 229
 230    For a Lie group of rank r:
 231    - SU(n) has rank n - 1, acts on ℂⁿ (fundamental rep dimension n)
 232    - U(1) has rank 1
 233
 234    The cube layers provide the FUNDAMENTAL REPRESENTATION DIMENSIONS:
 235    - S₃ acts on 3 axes → fundamental rep dimension 3 → SU(3)
 236    - (ℤ/2ℤ)² acts on 2-element subsets → fundamental rep dimension 2 → SU(2)
 237    - ℤ/2ℤ acts on parity → fundamental rep dimension 1 → U(1) -/

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
independent in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
rank in IndisputableMonolith.Foundation.PreTemporalForcingOrder decl_use
independent in IndisputableMonolith.Foundation.RSCoupledAxis decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
parity in IndisputableMonolith.LedgerPostingAdjacency decl_use
U in IndisputableMonolith.Recognition decl_use
rank in IndisputableMonolith.RRF.Theorems.OrderPreservation decl_use