additive_closure_golden

formal source

 123
 124/-- The additive closure relation on a uniform scale ladder yields
 125the golden equation σ² = σ + 1. -/
 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
 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.