canonical_seed_posting_of_size_law
plain-language theorem explainer
From a nontrivial multilevel composition equipped with the canonical seed-size law, assemble the seed posting operation used by the hierarchy bridge. Anyone citing the T5→T6 self-similarity step needs this local closure. The proof is a three-field structure assembly: forced seed index, definitional equality to level 2, and the additive size hypothesis copied through.
Claim. Let $M$ be a nontrivial multilevel composition. Suppose the canonical seed-size law holds: the level at the canonical seed-post index equals the sum of levels $0$ and $1$. Then $M$ carries a canonical seed posting operation at that index: the post index is $2$, and the posted level has additive size $M.\\mathrm{levels}(2)=M.\\mathrm{levels}(0)+M.\\mathrm{levels}(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 hierarchy.
A NontrivialMultilevelComposition supplies only a positive level sequence. It does not by itself include a posting/composition operation, so the additive relation used by the hierarchy bridge cannot be read off bare structure. The seed-size law isolates exactly that missing datum: posting levels $0$ and $1$ closes at the canonical seed index (already forced to be $2$) with additive size.
The seed posting operation is the theorem-facing closure object for that local pair. Full all-pairs posting is stronger than the bridge needs; only the primitive closure $0$ posted with $1$ lands at $2$ with additive size is required for the T5→T6 recurrence.
proof idea
Term-mode structure construction, not a tactic walk. The goal is a CanonicalSeedPostingOperation at the canonical seed-post index. Fill three fields: (1) seed_index by the already-proved certificate that the canonical index is a valid seed-post index; (2) post01_eq_two by rfl (the index is definitionally $2$); (3) seed_level_posting by projecting the additive equality out of the input size-law hypothesis. No further lemmas are invoked.
why it matters
This is the first named closure that turns a raw equality into a canonical posting construction for the hierarchy bridge. Downstream it feeds t5_to_t6_bridge_holds, which packages the T5→T6 self-similarity bridge as theorem-backed once J-uniqueness is available.
In the forcing chain, T6 ($\varphi$ forced by self-similarity in the discrete ledger) sits immediately after T5 (unique $J$). The bridge needs a local additive posting law on seed levels; without this certificate the recurrence would rest on an anonymous equality. The module doc frames the stronger claim: every step T−1 through T8 is forced, not merely compatible. This lemma closes the seed-posting gap inside that T5→T6 link.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.