posting_scales_compose

formal source

  95
  96This is the RS-native form of "scale composition is governed by
  97the posting potential's multiplicative structure." -/
  98theorem posting_scales_compose (σ : ℝ) (hσ : 0 < σ) (j k : ℕ) :
  99    PostingPotential (σ ^ j * σ ^ k) + PostingPotential (σ ^ j / σ ^ k) =
 100      2 * PostingPotential (σ ^ j) * PostingPotential (σ ^ k) :=
 101  posting_dalembert (σ ^ j) (σ ^ k) (pow_pos hσ j) (pow_pos hσ k)
 102
 103/-! ## Additive Scale Composition from Closure -/
 104
 105/-- **Theorem**: Closure of a geometric scale sequence under additive
 106composition forces `scale 0 + scale 1 = scale 2`.
 107
 108This is the RS-internal replacement for the `HasAdditiveComposition`
 109axiom.  The additive structure is not assumed; it follows from the
 110physical requirement that composing level-0 and level-1 events must
 111produce a level-2 event.
 112
 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 < σ)