triangular_8

formal source

 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
 130
 131/-- The cumulative phase over a closed 8-tick cycle. -/
 132def phase_45 : ℕ := cumulative_phase closure_number
 133
 134/-- **MAIN THEOREM**: The 45-tick period emerges from cumulative phase
 135    accumulation over a closed 8-tick cycle.