`cube_face_equicardinal`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.CubeFaceUniversality
domain: CrossDomain
line: 69 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.CubeFaceUniversality on GitHub at line 69.

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

  66theorem q3_euler : (8 : ℤ) - 12 + 6 = 2 := by decide
  67
  68/-- Any two cube-face domains are equicardinal. -/
  69theorem cube_face_equicardinal
  70    {A B : Type} [Fintype A] [Fintype B]
  71    (hA : HasCubeFaceCount A) (hB : HasCubeFaceCount B) :
  72    Fintype.card A = Fintype.card B := by
  73  rw [hA, hB]
  74
  75/-- Standard Model total fermion count: 6 quarks + 6 leptons = 12. -/
  76theorem quark_lepton_sum :
  77    Fintype.card Quark + Fintype.card Lepton = 12 := by
  78  rw [quark_has_6, lepton_has_6]
  79
  80/-- Total with antiparticles: 2 · 12 = 24. -/
  81theorem fermion_antifermion_total :
  82    2 * (Fintype.card Quark + Fintype.card Lepton) = 24 := by
  83  rw [quark_has_6, lepton_has_6]
  84
  85/-- Three cube-face structures combine: 6³ = 216. -/
  86theorem cube_face_cubed
  87    {A B C : Type} [Fintype A] [Fintype B] [Fintype C]
  88    (hA : HasCubeFaceCount A) (hB : HasCubeFaceCount B) (hC : HasCubeFaceCount C) :
  89    Fintype.card (A × B × C) = 216 := by
  90  unfold HasCubeFaceCount at hA hB hC
  91  simp [Fintype.card_prod, hA, hB, hC]
  92
  93/-- 216 = 6³. -/
  94theorem six_cubed : (6 : ℕ)^3 = 216 := by decide
  95
  96structure CubeFaceUniversalityCert where
  97  quark_6 : HasCubeFaceCount Quark
  98  lepton_6 : HasCubeFaceCount Lepton
  99  cortical_6 : HasCubeFaceCount CorticalLayer

papers checked against this theorem

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