rcl_seed_potential_surface
plain-language theorem explainer
The Recognition Composition Law in posting-potential form holds for all positive reals: Π(xy)+Π(x/y)=2Π(x)Π(y). Builders of typed seed-posting semantics and the T5–T6 self-similarity bridge cite this as the canonical RCL control surface on the hierarchy. The proof is a one-line term application of the d'Alembert identity for the posting potential.
Claim. For all real $x,y>0$, writing $\Pi$ for the posting potential (the shifted $J$-cost with $J=\Pi-1$), one has $\Pi(xy)+\Pi(x/y)=2\,\Pi(x)\,\Pi(y)$.
background
The Unified Forcing Chain module shows T0–T8 as forced from the cost foundation: Recognition Composition Law (RCL), normalization $F(1)=0$, and calibration $F''(1)=1$. On the $J$-cost the RCL is $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The posting potential $\Pi$ is the shifted control quantity related by $J=\Pi-1$, so the same law becomes the d'Alembert form $\Pi(xy)+\Pi(x/y)=2\Pi(x)\Pi(y)$.
Posting extensivity separates this multiplicative control surface from additive hierarchy observables. Level size is an additive scale/size field; the posting potential is the RCL control field. The tempting identity equating $\Pi$ on a squared seed to a sum of lower seed levels is false; typed seed-posting exists precisely to keep those roles apart. Upstream, the d'Alembert theorem for the posting potential states the identity and records its equivalence to RCL via the shift $J=\Pi-1$.
proof idea
One-line term wrapper. The goal is definitionally identical to the upstream d'Alembert identity for the posting potential (positive $x,y$), so the proof is just that theorem as a term. No unfolding or extra algebra occurs at this site; the algebraic work (unfolding $\Pi$ to $J$-cost and verifying the product identity) lives in the upstream proof.
why it matters
This declaration is the named RCL posting surface used as the control field in typed seed-posting. Downstream, the additive-model, seed-closed, and seed-recognition-work constructors each package a hierarchy's level-size observable together with this surface, so that seed composition obeys d'Alembert/RCL without conflating additive size with multiplicative potential.
It also feeds the T5-to-T6 self-similarity bridge: once T5 has unique $J$ (equivalently unique $\Pi$), the posting surface is the law that closed discrete hierarchies must satisfy, forcing $\varphi$ as the self-similar fixed point (T6 in the forcing chain). Framework landmarks: RCL itself, T5 $J$-uniqueness, and the T6 $\varphi$ step. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.