canonical_seed_size_law_of_rcl_potential
plain-language theorem explainer
Potential-level seed posting semantics force the canonical seed-size law on a nontrivial multilevel hierarchy: the level at the canonical seed index equals the sum of levels 0 and 1. Anyone bridging T5 (unique J-cost) to T6 (φ forced by self-similarity) cites this certificate. The proof is a short rewrite that unpacks the three posting-potential level equalities and applies the additive closure already stored in the semantics.
Claim. Let $M$ be a nontrivial multilevel composition with positive level sequence $\ell:\mathbb{N}\to\mathbb{R}$, and let $\sigma>0$ be a scale such that $\ell(0)$, $\ell(1)$, and $\ell(2)$ equal the posting potentials of $\sigma^0$, $\sigma^1$, and $\sigma^2$ respectively, with additive potential-level seed closure. Then the canonical seed-size law holds: $\ell(2)=\ell(0)+\ell(1)$.
background
The Unified Forcing Chain module derives T0–T8 as forced inevitabilities from the Recognition Composition Law together with normalization and calibration. Between unique $J$ (T5) and forced $\varphi$ (T6) sits a self-similarity bridge that needs a discrete hierarchy with a closed seed scale.
A nontrivial multilevel composition is a positive real-valued level map with at least three positive levels. The canonical seed-size law isolates the remaining size identity once the seed post index is already forced to $2$: posting levels $0$ and $1$ closes additively at that index. It is kept separate from the posting operation so the next closure step can derive it from RCL/posting-potential composition.
Potential-level seed posting semantics interpret those three seed levels as the posting-potential image of a positive scale $\sigma$ at powers $0$, $1$, and $2$, and package the additive closure rule at the potential level ("the canonical seed composite closes by additive posting").
proof idea
Single-field tactic proof of the seed-size identity. Rewrite the three level equalities from the semantics (levels $2$, $0$, and $1$ as posting potentials of $\sigma^2$, $\sigma^0$, and $\sigma^1$). After those rewrites the goal is exactly the seed-potential-closure field of the semantics, which is applied directly. No external lemmas beyond the structure fields; pure unpacking of the hypothesis.
why it matters
Feeds t5_to_t6_bridge_holds, whose doc states that "the T5-to-T6 self-similarity bridge is theorem-backed." That bridge is the step from unique $J$-cost (T5) to $\varphi$ as the self-similar fixed point (T6) in the forcing chain. By obtaining the seed-size law from RCL posting-potential semantics rather than assuming it, the chain keeps the complete-inevitability claim: hierarchy self-similarity is forced by cost composition, not postulated. Framework landmarks: T5 $J$-uniqueness ($J(x)=(x+x^{-1})/2-1$), T6 $\varphi$ forced, and the RCL itself as the single axiom bundle driving the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.