posting_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove the d'Alembert identity itself.
- Does not address arguments outside the positive reals.
- Does not connect directly to mass formulas or the phi-ladder.
- Does not assume or derive any specific numerical value for phi.
formal statement (Lean)
68theorem posting_pos (x : ℝ) (hx : 0 < x) : 0 < PostingPotential x := by
proof body
Term-mode proof.
69 unfold PostingPotential Jcost
70 have hx_ne : x ≠ 0 := ne_of_gt hx
71 have h := sq_nonneg (x - x⁻¹)
72 have hx_inv_pos : 0 < x⁻¹ := inv_pos.mpr hx
73 nlinarith [mul_pos hx hx_inv_pos]
74
75/-- The d'Alembert identity for the posting potential:
76Π(xy) + Π(x/y) = 2 Π(x) Π(y).
77
78This is the fundamental identity governing how posting potentials
79compose. It is equivalent to the RCL via the shift J = Π − 1. -/