golden_ratio_not_seed_potential_additive
plain-language theorem explainer
Obstruction: the posting potential Π(x)=J(x)+1 does not obey Π(φ²)=Π(φ⁰)+Π(φ¹). Anyone bridging T5 (unique J) to T6 (φ forced) cites this to block a naive additive seed-size law at potential values. The proof substitutes the golden-ratio equation, unfolds Π and J, then obtains a linear-arithmetic contradiction from φ>1.
Claim. Let $\varphi$ be the golden ratio and let $\Pi(x)=J(x)+1=\tfrac12(x+x^{-1})$ be the posting potential built from the recognition cost $J$. Then $\Pi(\varphi^2)\neq\Pi(\varphi^0)+\Pi(\varphi^1)$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T5 pins the unique cost $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger.
The posting potential is the shifted cost $\Pi(x)=J(x)+1=\tfrac12(x+x^{-1})$. It is the surface on which d'Alembert/RCL composition lives. Seed-size semantics of the hierarchy, by contrast, live at the scale/size level, not at raw $\Pi$-values.
Upstream, $\varphi^2=\varphi+1$ is the defining golden-ratio equation (PhiForcing / PhiRing). The present claim is the concrete obstruction that additive closure of $\Pi$ on the first three $\varphi$-powers fails.
proof idea
Proof by contradiction. Assume $\Pi(\varphi^2)=\Pi(\varphi^0)+\Pi(\varphi^1)$. Use $\varphi\neq 0$ (from $\varphi>0$) and the identity $\varphi^2=\varphi+1$. Unfold $\Pi$ and $J$ to explicit rational expressions in $\varphi$, clear denominators with field_simp, then finish by nlinarith against $\varphi>1$ and the golden-ratio equation. Pure algebraic reduction; no external lemmas beyond positivity and $\varphi^2=\varphi+1$.
why it matters
Feeds t5_to_t6_bridge_holds, which packages the T5→T6 self-similarity bridge as theorem-backed. The doc-comment states the methodological point: the seed-size law cannot be derived by asserting additive closure directly at posting-potential values; additivity belongs to hierarchy scale/size semantics, while $\Pi$ supplies the RCL composition surface.
In the forcing chain this sits between T5 (J-uniqueness via d'Alembert + normalization + calibration) and T6 ($\varphi$ forced by self-similarity in the discrete ledger). It keeps the bridge honest: one must not smuggle seed additivity through $\Pi$-arithmetic. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.