`cube_uniqueness`

proved

show as: view math explainer →

module: IndisputableMonolith.Meta.LedgerUniqueness
domain: Meta
line: 136 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Meta.LedgerUniqueness on GitHub at line 136.

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

 133
 134/-- The cube Q₃ is the unique linking-compatible polytope.
 135    (Reformulated: Linking structure implies D=3) -/
 136theorem cube_uniqueness :
 137    ∀ D : ℕ, (linkingNumber D ≠ 0) ↔ D = 3 := by
 138  intro D
 139  constructor
 140  · intro h
 141    unfold linkingNumber at h
 142    split_ifs at h with hD
 143    · exact hD
 144    · contradiction
 145  · intro h
 146    rw [h]
 147    unfold linkingNumber
 148    simp
 149
 150/-! ## 8-Tick Uniqueness -/
 151
 152/-- A Gray code cycle of length T on D dimensions. -/
 153def grayCodeCycleLength (D : ℕ) : ℕ := 2^D
 154
 155/-- For D=3, the minimal complete cycle is 8 = 2³. -/
 156theorem eight_tick_minimal :
 157    grayCodeCycleLength 3 = 8 := by
 158  unfold grayCodeCycleLength
 159  norm_num
 160
 161/-- No shorter cycle covers the cube. -/
 162theorem no_shorter_cycle :
 163    ∀ T : ℕ, T < 8 → ¬∃ (cycle : Fin T → Fin 8), Function.Bijective cycle := by
 164  intro T hT
 165  intro ⟨cycle, hBij⟩
 166  -- Bijection requires |domain| = |codomain|

papers checked against this theorem

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