posting_scales_compose
plain-language theorem explainer
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.
Claim. Let σ > 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.