`unique_321_partition_example`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.GaugeGroupCube
domain: Foundation
line: 40 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.GaugeGroupCube on GitHub at line 40.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  37
  38/-- The (3,2,1) partition is the unique decreasing partition of 6 into 3 parts
  39    where first part = D = 3. -/
  40theorem unique_321_partition_example :
  41    gaugeRankSU3 = 3 ∧ gaugeRankSU2 = 2 ∧ gaugeRankU1 = 1 ∧
  42    gaugeRankSU3 ≥ gaugeRankSU2 ∧ gaugeRankSU2 ≥ gaugeRankU1 := by
  43  decide
  44
  45/-- Cube face-pair count = 3 (D=3 spatial dimension). -/
  46def cubeFacePairs : ℕ := 3
  47
  48theorem cubeFacePairs_eq_3 : cubeFacePairs = 3 := rfl
  49
  50/-- SU(3) rank matches cube face-pair count. -/
  51theorem su3_rank_eq_face_pairs : gaugeRankSU3 = cubeFacePairs := rfl
  52
  53structure GaugeCubeCert where
  54  total_rank : gaugeRankSU3 + gaugeRankSU2 + gaugeRankU1 = 6
  55  decomp : gaugeRankSU3 = 3 ∧ gaugeRankSU2 = 2 ∧ gaugeRankU1 = 1
  56  su3_from_cube : gaugeRankSU3 = cubeFacePairs
  57  decreasing_partition : gaugeRankSU3 ≥ gaugeRankSU2 ∧ gaugeRankSU2 ≥ gaugeRankU1
  58
  59def gaugeCubeCert : GaugeCubeCert where
  60  total_rank := totalGaugeRank
  61  decomp := rankDecomposition
  62  su3_from_cube := su3_rank_eq_face_pairs
  63  decreasing_partition := ⟨by decide, by decide⟩
  64
  65end IndisputableMonolith.Foundation.GaugeGroupCube

papers checked against this theorem

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