posting_scales_compose
Researchers deriving additive scale composition in Recognition Science cite this result to obtain the d'Alembert identity on geometric sequences without presupposing linearity. For positive real σ and natural numbers j, k the posting potential satisfies Π(σ^{j+k}) + Π(σ^{j-k}) = 2 Π(σ^j) Π(σ^k) where Π(x) = ½(x + x^{-1}). The proof is a direct one-line instantiation of the general d'Alembert lemma on the powered arguments after checking positivity.
claimLet σ > 0 be real and let j, k be natural numbers. Let Π(x) := ½(x + x^{-1}). Then Π(σ^{j+k}) + Π(σ^{j-k}) = 2 Π(σ^j) Π(σ^k).
background
The module derives additive scale composition from the Recognition Composition Law without assuming linearity of the recurrence. PostingPotential is defined as Π(x) := Jcost(x) + 1 = ½(x + x^{-1}), the shifted cost that satisfies the d'Alembert equation. The local setting is the RS-internal route to Proposition 4.3: the RCL J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y) forces multiplicative structure on posting potentials for geometric scales σ^k. Upstream, the Composition class from CostAxioms supplies the axiom that for all positive x, y the functional equation F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y) holds.
proof idea
The proof is the term posting_dalembert (σ ^ j) (σ ^ k) (pow_pos hσ j) (pow_pos hσ k). It is a one-line wrapper that applies the general d'Alembert identity for PostingPotential to the positive arguments σ^j and σ^k.
why it matters in Recognition Science
This theorem supplies the multiplicative form of scale composition required by the Recognition Composition Law, enabling derivation of additive level composition in the phi-ladder without external linearity assumptions. It supports the closure arguments that replace the HasAdditiveComposition axiom and contributes to closing Proposition 4.3 of the phi paper. In the framework it instantiates the RCL at geometric scales, consistent with T5 J-uniqueness and the forced self-similar fixed point.
scope and limits
- Does not establish the full additive recurrence for arbitrary non-geometric scales.
- Does not derive the numerical value of the scale ratio σ or the phi fixed point.
- Does not address continuous or non-discrete hierarchy levels.
formal statement (Lean)
98theorem posting_scales_compose (σ : ℝ) (hσ : 0 < σ) (j k : ℕ) :
99 PostingPotential (σ ^ j * σ ^ k) + PostingPotential (σ ^ j / σ ^ k) =
100 2 * PostingPotential (σ ^ j) * PostingPotential (σ ^ k) :=
proof body
Term-mode proof.
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. -/