seedClosedMultilevelComposition_seed_size_law
plain-language theorem explainer
The seed-closed multilevel composition obeys the seed size law by construction: level size at the canonical seed-post index equals the sum of the two base levels. Hierarchy and φ-forcing arguments cite this to equip the closed replacement with a CanonicalSeedSizeLaw instance. The proof is a one-line simplification that unfolds the seed-closed constructor.
Claim. For any nontrivial multilevel composition $M$ (a positive level-size map $\mathbb{N}\to\mathbb{R}$ with at least three levels), write $M'$ for its seed-closed replacement. Then $M'(\iota_{\mathrm{seed}})=M'(0)+M'(1)$, where $\iota_{\mathrm{seed}}$ is the canonical seed-post index.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Near T6, self-similarity on a discrete ledger forces $\varphi$; multilevel hierarchies supply the scale ladder on which that self-similarity is stated.
A nontrivial multilevel composition is a positive map $\mathrm{levels}:\mathbb{N}\to\mathbb{R}$ with at least three occupied levels. Seed closing rebuilds such a hierarchy so the seed-post slot is filled by the sum of the two base levels, while non-seed levels are preserved. The seed size law is exactly that additive relation at the canonical seed-post index.
Upstream, the nontrivial multilevel structure and related canonical objects (arithmetic, trace, calibration dressings) fix the ambient hierarchy language; this lemma only records what the seed-closed constructor already installs.
proof idea
One-line tactic proof: simp unfolds the definition of the seed-closed multilevel composition. By that constructor, the level sequence is built so the entry at the canonical seed-post index is definitionally the sum of levels $0$ and $1$. No external lemmas are required beyond definitional reduction.
why it matters
This is the definitional witness that seed closing installs the seed size law. Downstream, canonical_seed_size_law_of_seed_closed packages it as a CanonicalSeedSizeLaw instance; seedClosedMultilevelComposition_is_replacement uses the same constructor to show non-seed levels are preserved; typed_seed_posting_of_seed_closed attaches typed seed-posting semantics (level sizes plus J-posting control).
The load-bearing parent is seedClosed_multilevel_forces_phi: once an original hierarchy has zero-free-scale uniformity and a compatible seed-size law, the canonically seed-closed replacement forces $\varphi$ without separately assuming the replacement's uniformity or growth fields. That is the T6 landmark (φ as self-similar fixed point) inside the complete inevitability chain from the cost foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.