canonical_seed_size_law_of_level_two
plain-language theorem explainer
Packages a raw additive level equation into the canonical seed-size-law certificate for a nontrivial multilevel hierarchy: the size at the forced seed-post index equals the sum of levels 0 and 1. Cited by anyone closing the T5→T6 self-similarity bridge or hierarchy posting. Proof is a one-line structure constructor that installs the given equality as the sole field.
Claim. Let $M$ be a nontrivial multilevel composition (a positive real-valued level map with at least three levels). If the level at the canonical seed-post index equals the sum of the levels at $0$ and $1$, then $M$ satisfies the canonical seed-size law: posting seed levels $0$ and $1$ closes additively at that index.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The T5→T6 step forces $\varphi$ from self-similarity in a discrete ledger hierarchy.
A nontrivial multilevel composition is a map $\mathrm{levels}:\mathbb{N}\to\mathbb{R}$ with every level positive and at least the first three strictly positive. The canonical seed-post index is fixed at $2$: for a local second-order hierarchy the seed levels are $0$ and $1$, and their first local closure lands at the next level.
The structure CanonicalSeedSizeLaw isolates the remaining size equation after that index is forced: posting the two seed levels has additive size, $\mathrm{levels}(2)=\mathrm{levels}(0)+\mathrm{levels}(1)$. It is named separately from the posting operation so a later closure step can derive the law from RCL and posting-potential composition.
proof idea
One-line term-mode constructor. The hypothesis is definitionally the sole field of the seed-size-law structure, so the proof is seed_size_law := hlevel. No lemmas are applied; the declaration is a typed packaging of the raw equality into the named certificate.
why it matters
Sits on the T5→T6 bridge inside the complete inevitability chain. Downstream, t5_to_t6_bridge_holds records that the T5-to-T6 self-similarity bridge is theorem-backed, using hierarchy dynamics that force $\varphi$ from internal hierarchy structure and realized closed scales (primer landmark T6: $\varphi$ as the self-similar fixed point, after T5 J-uniqueness).
The seed-size law is the additive posting identity at the forced index $2$. Separating the certificate from the raw equation lets the next closure step derive additivity from RCL and posting potential rather than assume it. Without this packaging, the hierarchy side of the T5→T6 bridge has no named handle for the size constraint that self-similarity acts on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.