CanonicalSeedSizeLaw
plain-language theorem explainer
A Prop certificate that a nontrivial multilevel hierarchy obeys additive seed size: the level at the canonical seed-post index equals the sum of levels 0 and 1. Hierarchy and φ-forcing arguments cite it when closing seed posting before extracting the base ratio. It is a bare structure field, not a proved equation; uniqueness is propositional (Subsingleton).
Claim. For a nontrivial multilevel composition $M$, the canonical seed-size law holds when the size of the level at the canonical seed-post index equals the sum of the sizes of levels $0$ and $1$: $\mathrm{levels}_M(i_{\mathrm{seed}})=\mathrm{levels}_M(0)+\mathrm{levels}_M(1)$. (The seed index itself is already fixed at $2$.)
background
In the Unified Forcing Chain, T0–T8 are derived from the Recognition Composition Law plus normalization and calibration. After discreteness and ledger structure, hierarchies of levels appear; self-similarity on those levels is what forces $\varphi$ (T6).
A NontrivialMultilevelComposition packages a discrete hierarchy with level sizes. The canonical seed-post index is already forced to be $2$ (two seed levels). What remains is a pure size identity: posting levels $0$ and $1$ has additive size at that index.
The certificate is named separately from the posting operation so later steps can derive the size law from RCL or posting-potential composition, rather than baking additivity into the operation definition.
proof idea
Definitional structure, not a derived theorem. The body is a single Prop field equating M.levels at the canonical seed-post index with the sum of levels $0$ and $1$. A companion Subsingleton instance shows any two such certificates are definitionally equal (rfl). Constructors elsewhere (additive posting models, RCL posting, level-two data, admissible orbits) inhabit the field by proving that equation.
why it matters
Isolates the additive seed-size step that sits between hierarchy setup and $\varphi$-forcing. Downstream, canonical_seed_posting_of_size_law rebuilds the seed posting operation from this certificate; canonicalBaseRatio_eq_phi_of_uniform_seed and the uniform-closed variant use seed closure plus growth (and uniform scale) to conclude the canonical base ratio equals $\varphi$ (T6 landmark). Admissible-orbit reflection supplies the law automatically and folds it into normal-form certificates. Keeping size separate from posting lets RCL-based composition discharge the law rather than assume it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.