theorem
proved
tactic proof
additive_closure_golden
show as:
view Lean formalization →
formal statement (Lean)
126theorem additive_closure_golden (levels : ℕ → ℝ)
127 (levels_pos : ∀ k, 0 < levels k)
128 (σ : ℝ) (_hσ : 1 < σ)
129 (uniform : ∀ k, levels (k + 1) = σ * levels k)
130 (closure : levels 2 = levels 1 + levels 0) :
131 σ ^ 2 = σ + 1 := by
proof body
Tactic-mode proof.
132 have h0 : levels 0 ≠ 0 := ne_of_gt (levels_pos 0)
133 have h1 := uniform 0
134 have h2 := uniform 1
135 have h_sq : levels 2 = σ ^ 2 * levels 0 := by
136 rw [h2, h1]; ring
137 have h_rhs : levels 2 = (σ + 1) * levels 0 := by
138 rw [closure, h1]; ring
139 have : (σ ^ 2 - (σ + 1)) * levels 0 = 0 := by
140 calc (σ ^ 2 - (σ + 1)) * levels 0
141 = σ ^ 2 * levels 0 - (σ + 1) * levels 0 := by ring
142 _ = levels 2 - levels 2 := by rw [← h_sq, h_rhs]
143 _ = 0 := by ring
144 rcases mul_eq_zero.mp this with hzero | hsize
145 · linarith
146 · exact (h0 hsize).elim
147
148/-! ## Discrete Coefficients -/
149
150/-- In the general additive recurrence `ℓ₂ = α ℓ₁ + β ℓ₀`,
151the coefficients α, β count sub-events. In a countable carrier,
152these counts are non-negative integers.
153
154The zero-parameter condition further forces `(α, β) = (1, 1)`:
155any other pair has `max(α, β) ≥ 2`, introducing descriptional
156complexity that the zero-parameter posture forbids.
157
158This theorem proves that natural-number coefficients with
159`max(a, b) = 1` forces the Fibonacci recurrence. -/