closure_forces_additive

formal source

 113The "additive" nature of scale composition comes from the ledger's
 114posting rule: total recognition work sums, so scales (which measure
 115work at each level) add when events compose. -/
 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
 122  linarith [closure]
 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