lemma
proved
triangular_4
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gap45.PhysicalMotivation on GitHub at line 99.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
96@[simp] lemma triangular_3 : triangular 3 = 6 := rfl
97
98/-- T(4) = 10. -/
99@[simp] lemma triangular_4 : triangular 4 = 10 := rfl
100
101/-- T(5) = 15. -/
102@[simp] lemma triangular_5 : triangular 5 = 15 := rfl
103
104/-- T(8) = 36. -/
105@[simp] lemma triangular_8 : triangular 8 = 36 := rfl
106
107/-- **KEY RESULT**: T(9) = 45. -/
108@[simp] theorem triangular_9_is_45 : triangular 9 = 45 := rfl
109
110/-! ## The Closure Principle -/
111
112/-- The 8-tick period (from ledger coverage of 2^D with D=3). -/
113def eight_tick : ℕ := 8
114
115/-- The closure number: to close an 8-tick cycle, you need 8+1 = 9 steps.
116 This is the "fence-post" principle: 8 sections need 9 posts. -/
117def closure_number : ℕ := eight_tick + 1
118
119/-- Closure number = 9. -/
120@[simp] theorem closure_number_eq_9 : closure_number = 9 := rfl
121
122/-! ## Cumulative Phase as Triangular Number -/
123
124/-- **PHYSICAL PRINCIPLE**: The cumulative phase over a closed cycle is the
125 triangular number of the closure count.
126
127 Each tick k contributes a phase proportional to k (linear cost accumulation).
128 Over a closed cycle of n steps, total cumulative phase = T(n). -/
129def cumulative_phase (n : ℕ) : ℕ := triangular n