def
definition
phase_45
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gap45.PhysicalMotivation on GitHub at line 132.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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.
136
137 45 = T(9) = T(8+1) = cumulative phase of closed 8-tick cycle. -/
138theorem gap_45_from_phase : phase_45 = 45 := rfl
139
140/-- Alternative: 45 = sum of 1 through 9. -/
141theorem gap_45_as_sum : (List.range 10).sum - 0 = 45 := by native_decide
142
143/-! ## Equivalence with Fibonacci × Closure Derivation -/
144
145/-- T(9) = 9 × 10 / 2 = 45. -/
146theorem triangular_9_via_formula : 9 * 10 / 2 = 45 := rfl
147
148/-- The Fibonacci factor: 5 = Fib(5) = Fib(4) in our indexing. -/
149def fibonacci_factor : ℕ := 5
150
151/-- 9 × 5 = 45. -/
152theorem nine_times_five : closure_number * fibonacci_factor = 45 := rfl
153
154/-- **EQUIVALENCE THEOREM**: The two derivations are algebraically equivalent:
155 T(9) = 45 = (8+1) × 5 = closure × fibonacci.
156
157 But the triangular number interpretation provides physical motivation
158 that the "closure × fibonacci" form lacks. -/
159theorem derivations_equivalent :
160 triangular closure_number = closure_number * fibonacci_factor := by
161 -- T(9) = 45 = 9 × 5
162 rfl