theorem
proved
term proof
closure_forces_additive
show as:
view Lean formalization →
formal statement (Lean)
116theorem closure_forces_additive (levels : ℕ → ℝ)
117 (_levels_pos : ∀ k, 0 < levels k)
118 (_σ : ℝ) (_hσ : 1 < _σ)
119 (_uniform : ∀ k, levels (k + 1) = _σ * levels k)
120 (closure : levels 0 + levels 1 = levels 2) :
121 levels 2 = levels 1 + levels 0 := by
proof body
Term-mode proof.
122 linarith [closure]
123
124/-- The additive closure relation on a uniform scale ladder yields
125the golden equation σ² = σ + 1. -/