seedClosedLevels_eq_original_iff_seed_size_law
plain-language theorem explainer
For any nontrivial multilevel hierarchy, the canonical seed-closed normal form leaves every level unchanged if and only if the hierarchy already obeys the seed-size law (level 2 equals level 0 plus level 1). Hierarchy and T5–T6 bridge arguments cite this as the exact-preservation criterion. The proof is a short iff: one arm specializes equality at the canonical seed index 2; the other reuses the existing one-direction lemma.
Claim. Let $M$ be a nontrivial multilevel composition (positive level sequence with at least three levels). Write $M^{\mathrm{sc}}$ for its canonical seed-closed replacement. Then $(\forall k,\, M^{\mathrm{sc}}.\mathrm{levels}(k)=M.\mathrm{levels}(k))$ if and only if $M$ satisfies the canonical seed-size law $M.\mathrm{levels}(2)=M.\mathrm{levels}(0)+M.\mathrm{levels}(1)$.
background
This sits in the Unified Forcing Chain module, which derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The local objects are multilevel hierarchies: a NontrivialMultilevelComposition is a positive real level sequence with at least three levels, the raw data for discrete self-similar scale structure that later forces $\varphi$ (T6).
Seed closure is the canonical normal form that posts the adjacent seed levels 0 and 1. The posting index is forced to be canonical_seed_post_index $=2$ ("their first local closure lands at the next level"). The remaining size constraint is isolated as CanonicalSeedSizeLaw: posting those two seeds has additive size, $M.levels(2)=M.levels(0)+M.levels(1)$. The structure is named separately so a later step can derive the law from RCL/posting-potential composition rather than assume it.
The theorem equates two surface statements: full level-sequence equality after seed closure, versus possession of that size certificate.
proof idea
Term-mode constructor on the biconditional.
Forward: assume every level of the seed-closed hierarchy equals the original. Specialize at canonical_seed_post_index ($=2$). After unfolding, rewrite with seedClosedLevels_two (the seed-closed level at 2 is the sum of levels 0 and 1) and symmetrize to obtain the single field of CanonicalSeedSizeLaw.
Reverse: one-line application of the existing lemma seedClosedLevels_eq_original_of_seed_size_law, which already proves that the size law implies full level-sequence preservation under seed closure.
why it matters
Exact preservation under seed closure is the hinge between "already self-similar at the seed" and "seed closure is a no-op on levels." Downstream, canonical_seed_closure_preservation packages this iff as its exact_preservation_iff field, together with equivalence and self-equivalence certificates. That preservation bundle feeds the T5-to-T6 bridge (t5_to_t6_bridge_holds), whose doc states the bridge is theorem-backed: unique $J$ (T5) plus internal hierarchy self-similarity force $\varphi$ as the discrete fixed point (T6 in the forcing chain).
In framework terms this is bookkeeping on the path from T5 (J-uniqueness via d'Alembert, normalization, calibration) into T6 ($\varphi$ forced by self-similarity in the discrete ledger). Without a clean criterion for when seed closure preserves levels, the realized-closed-scale normal-form equivalence used in the bridge would not be pin-downable. The declaration itself is fully proved; it does not close the RCL-derivation of the size law, only isolates when preservation holds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.