PostingPotential
plain-language theorem explainer
PostingPotential defines the shifted J-cost Π(x) := J(x) + 1, which equals ½(x + x⁻¹) and normalizes to 1 at x = 1. Workers on scale composition in the Recognition framework cite it to obtain the d'Alembert identity directly from the RCL without extra assumptions. The definition is a one-line algebraic shift that supplies the normalized potential used by the four downstream posting lemmas.
Claim. Define the posting potential by Π(x) := J(x) + 1, where J(x) = ½(x + x⁻¹) − 1. Equivalently, Π(x) = ½(x + x⁻¹) for x > 0.
background
The module derives additive scale composition from the Recognition Composition Law (RCL) without assuming linearity, closing Proposition 4.3 of the phi paper. The RCL states J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y) with J(x) = ½(x + x⁻¹) − 1. Posting potential is the shifted cost that satisfies the d'Alembert equation Π(xy) + Π(x/y) = 2 Π(x) Π(y).
proof idea
One-line definition that adds the constant 1 to Jcost x. The normalization Π(1) = 1 follows immediately by substitution and the fact that J(1) = 0.
why it matters
Supplies the normalized potential required by posting_dalembert, posting_one, posting_pos and posting_scales_compose. These lemmas convert the RCL into multiplicative composition of potentials and then into additive scale recurrence, directly addressing the objection to Proposition 4.3. The construction sits between T5 (J-uniqueness) and the eight-tick octave, providing the bridge from cost to geometric scale sequences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.