canonical_seed_size_law_of_additive_posting_model
plain-language theorem explainer
Any multilevel hierarchy equipped with an additive seed-posting model automatically satisfies the canonical seed-size law: the size at the forced seed index equals the sum of the sizes of levels 0 and 1. Hierarchy and T5–T6 bridge arguments cite this to discharge the remaining size identity once posting is additive. The proof is a five-step rewrite chain through the model axioms.
Claim. Let $M$ be a nontrivial multilevel composition (positive level sizes with at least three levels). Suppose there is an event type with a level-representing map, an additive size observable, and a posting composition such that (i) each level size equals the size of its representing event, (ii) posting the level-$0$ and level-$1$ events yields the canonical seed event, and (iii) size is additive under posting. Then $M$ obeys the canonical seed-size law: the level size at the canonical seed index equals the sum of the level sizes at $0$ and $1$.
background
The Unified Forcing Chain module aims to force the full T0–T8 ladder from the Recognition Composition Law plus normalization and calibration. In the hierarchy layer, a nontrivial multilevel composition is a positive real sequence of level sizes with at least three levels. The seed index is already fixed at $2$ (canonical seed post index); what remains is a size identity for that seed.
An additive seed-posting model packages lower-level ledger semantics: hierarchy levels are read as sizes of representing events; posting the two seed-level events produces the canonical seed event; and the size observable is additive under that posting. The canonical seed-size law is the isolated certificate that posting levels $0$ and $1$ closes at the seed index with additive size, deliberately separated from the posting operation so later steps can derive it from RCL or posting-potential control.
This theorem is the forcing direction: any such additive model yields the size law, so the bridge need not assume the law as an independent axiom once additive posting is in place.
proof idea
Pure rewrite proof on the single field seed_size_law. Start from the left-hand side $M.\mathrm{levels}$ at the canonical seed index. Replace it by the size of the representing seed event via level_size_eq. Unfold that event as the compose of the level-$0$ and level-$1$ events via seed_event_composes. Apply size_additive to split into a sum of sizes. Rewrite each summand back to $M.\mathrm{levels},0$ and $M.\mathrm{levels},1$ by the converse of level_size_eq. No external lemmas beyond the model fields.
why it matters
This closes the size half of the seed-posting bridge inside the forcing chain. Downstream it feeds t5_to_t6_bridge_holds, whose doc-comment states that the T5-to-T6 self-similarity bridge is theorem-backed; that bridge packages uniqueness of $J$ (T5) into the internal-hierarchy and realized-closed-scale routes that force $\varphi$ (T6).
In the primer landmarks, T5 is $J$-uniqueness ($J(x)=\cosh(\log x)-1$) and T6 is $\varphi$ as the self-similar fixed point of the discrete ledger. The seed-size law is the concrete additive identity that lets hierarchy composition talk about posting two unit seeds without free scale parameters. Combined with the companion uniqueness instance for additive models, it keeps the typed bridge thin: additivity of level size comes from the event-size observable, while posting potential separately supplies the RCL/d'Alembert control surface.
No scaffolding remains on this arrow; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.