posting_pos
plain-language theorem explainer
The posting potential Π(x) is strictly positive for every positive real x. Researchers deriving additive scale composition from the Recognition Composition Law cite this to guarantee well-defined costs in hierarchy levels. The term proof unfolds the definition to Jcost(x) + 1, records the non-negative square of (x - x^{-1}), the positivity of the reciprocal, and closes via nlinarith on the product of positives.
Claim. For every real number $x > 0$, the posting potential satisfies $Π(x) > 0$, where $Π(x) := J(x) + 1 = ½(x + x^{-1})$ and $J$ is the J-cost function.
background
The module derives additive scale composition from the forced Recognition Composition Law without assuming linearity, closing Proposition 4.3 of the phi paper. The posting potential is defined as the shifted J-cost: $Π(x) := Jcost(x) + 1 = ½(x + x^{-1})$, which satisfies the d'Alembert identity $Π(xy) + Π(x/y) = 2Π(x)Π(y)$. Jcost itself is the unique function satisfying the RCL $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ with $J(x) = ½(x + x^{-1}) - 1$. Upstream results supply the canonical identity event at the J-cost minimum and the structure of recognition-weighted derivations that rely on positive potentials.
proof idea
The proof is a term-mode reduction. It unfolds PostingPotential and Jcost, obtains $x ≠ 0$ from the hypothesis, records the non-negative square of $(x - x^{-1})$, establishes positivity of the reciprocal, and applies nlinarith to the product of the two positive factors.
why it matters
This positivity lemma underpins the d'Alembert identity for posting potentials, which the module uses to force additive scale composition from the RCL. It directly supports the self-similar fixed point phi and the eight-tick octave in the unified forcing chain (T5-T7). The result ensures potentials remain positive on the phi-ladder, consistent with D = 3 and the alpha band, without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.