posting_dalembert
plain-language theorem explainer
The d'Alembert identity asserts that the posting potential satisfies Π(xy) + Π(x/y) = 2 Π(x) Π(y) for positive reals x and y. Workers deriving additive scale composition in Recognition Science hierarchies cite it to justify multiplicative structure on geometric sequences without assuming linearity. The proof is a direct algebraic reduction after unfolding PostingPotential as Jcost plus one, clearing denominators via field_simp, and verifying the identity by ring.
Claim. Let $Π(x) = ½(x + x^{-1})$ denote the posting potential. For positive real numbers $x$ and $y$, $Π(xy) + Π(x/y) = 2 Π(x) Π(y)$.
background
The posting potential is defined here as Π(x) := Jcost(x) + 1, where Jcost is the Recognition cost function. This shift converts the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), with J(x) = ½(x + x^{-1}) - 1, into the simpler d'Alembert form. The module derives additive scale composition from the forced RCL, closing Proposition 4.3 of the phi paper without presupposing linearity of the recurrence ℓ_{k+2} = f(ℓ_{k+1}, ℓ_k).
proof idea
The proof is a term-mode reduction. It unfolds PostingPotential and Jcost, introduces the facts that x and y are nonzero from the positivity hypotheses, applies field_simp to clear fractions, and finishes with ring to confirm the algebraic identity.
why it matters
This supplies the core identity used by posting_scales_compose to obtain Π(σ^{j+k}) + Π(σ^{j-k}) = 2 Π(σ^j) Π(σ^k) on geometric sequences. It thereby advances the derivation of additive scale composition from closure, as described in the module documentation for closing Proposition 4.3. In the framework it realizes the extensivity property forced by the RCL at T5 (J-uniqueness) and supports the eight-tick octave at T7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.