RCLSeedPostingPotentialSemantics
plain-language theorem explainer
Packages concrete potential-level semantics for a seed hierarchy: levels 0,1,2 of a nontrivial multilevel composition equal the posting potential at powers σ⁰,σ¹,σ² of a positive scale, with additive seed closure and an RCL-type surface identity on positive reals. Downstream seed-size and T5→T6 bridge results cite it as the semantic hypothesis. Pure Prop structure; no proof body.
Claim. For a nontrivial multilevel composition $M$ and a real scale $\sigma$, the following hold: $0<\sigma$; the levels of $M$ at indices $0$, $1$, and the canonical seed-post index equal the posting potential at $\sigma^0$, $\sigma^1$, and $\sigma^2$ respectively; the posting potential satisfies $\mathrm{Post}(\sigma^2)=\mathrm{Post}(\sigma^0)+\mathrm{Post}(\sigma^1)$; and for all $x,y>0$, $\mathrm{Post}(xy)+\mathrm{Post}(x/y)=2\,\mathrm{Post}(x)\,\mathrm{Post}(y)$.
background
The module UnifiedForcingChain develops the complete inevitability chain from the cost foundation: absolute floor through T0–T8, driven by the Recognition Composition Law together with normalization and calibration. T5 pins the unique cost $J$, and T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger.
Here a nontrivial multilevel composition $M$ is a hierarchy object with a level sequence. Posting potential is the potential-level image used for seed posting (the multiplicative form of the composition surface, matching the $J+1$ shape of RCL rather than the shifted $J$ form). The seed indices $0,1,2$ are interpreted as $\sigma$ raised to those powers under that potential.
The doc-comment states the intent directly: the level sequence is the posting-potential image of a positive scale at seed indices $0,1,2$, and the remaining closure rule is the semantic statement that the canonical seed composite closes by additive posting.
proof idea
Definitional Prop structure, not a proved theorem. The fields are the semantic hypotheses themselves: positivity of $\sigma$; three level-equalities identifying $M$'s seed levels with posting potentials of $\sigma^0,\sigma^1,\sigma^2$; the additive seed-potential closure identity; and the universal RCL-type posting surface on positive reals. No tactics or upstream lemmas are applied in a body; inhabitants are assembled by supplying proofs of those six fields.
why it matters
This is the semantic interface that lets the forcing chain treat seed hierarchy data at the potential level rather than as bare level labels. The immediate parent is canonical_seed_size_law_of_rcl_potential, whose doc-comment says potential-level seed semantics force the canonical seed-size law: any $M$ and $\sigma$ carrying this structure yield CanonicalSeedSizeLaw M.
It also feeds the T5→T6 self-similarity bridge certificate. That bridge routes closed observable frameworks with realized hierarchy data to the forced scale ratio $\varphi$, and records that bare closed-observable fields alone do not force hierarchy fields such as ratio self-similarity and additive posting. Packaging additive posting and the RCL surface here keeps those hierarchy hypotheses explicit, so nothing is smuggled into T6.
In primer terms this sits on the T5→T6 step: unique $J$ plus self-similar discrete hierarchy forces $\varphi$. The RCL surface field is the potential-level form of the Recognition Composition Law that anchors the whole chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.