PostingPotential
The declaration defines the posting potential as the J-cost shifted by one unit, yielding Π(x) = ½(x + x^{-1}). Researchers deriving additive scale composition from the Recognition Composition Law cite this normalization to close Proposition 4.3 without presupposing linearity. The definition is a direct algebraic shift that immediately enables the d'Alembert identity for compound scales.
claimDefine the posting potential by $Π(x) := J(x) + 1$, where $J(x) = ½(x + x^{-1}) - 1$ denotes the J-cost. Equivalently, $Π(x) = ½(x + x^{-1})$ for $x > 0$.
background
The Posting Extensivity module starts from the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and introduces the shifted posting potential to obtain a multiplicative composition rule. J-cost itself is the function J(x) = ½(x + x^{-1}) - 1 that quantifies the recognition cost of comparing scale x against its reciprocal. The shift Π(x) = J(x) + 1 normalizes the potential so that Π(1) = 1 and converts the RCL into the d'Alembert form Π(xy) + Π(x/y) = 2Π(x)Π(y).
proof idea
The definition is a direct one-line wrapper that applies the constant shift +1 to the J-cost function. No lemmas or tactics are invoked; the body simply re-expresses Jcost x in the normalized form required downstream.
why it matters in Recognition Science
PostingPotential supplies the normalized object that feeds posting_dalembert, posting_scales_compose, and the closure arguments that force additive level sizes ℓ_{k+2} = ℓ_{k+1} + ℓ_k. It thereby closes the linearity gap in Proposition 4.3 of the phi paper by converting the RCL into an extensive posting structure. In the broader framework this step links the Recognition Composition Law to the eight-tick octave and the emergence of D = 3 without external linearity assumptions.
scope and limits
- Does not derive the Recognition Composition Law.
- Does not fix the numerical value of the self-similar ratio σ.
- Does not embed the scales into a specific spatial lattice.
- Does not compute explicit mass or coupling values on the phi-ladder.
formal statement (Lean)
60noncomputable def PostingPotential (x : ℝ) : ℝ := Jcost x + 1
proof body
Definition body.
61
62/-- Π(1) = 1: the posting potential is normalized. -/