seedClosedLevels_eq_original_of_seed_size_law
plain-language theorem explainer
When a multilevel hierarchy already obeys the additive seed-size law at the forced seed-post index, seed closure leaves every level value unchanged. Hierarchy-forcing arguments cite this to treat the seed-closed normal form as the identity on already-compatible data. The proof cases on the seed index: rewrite by the size law there, unfold to identity elsewhere.
Claim. Let $M$ be a nontrivial multilevel composition: a positive real level sequence with at least three positive levels. Write $\ell_*$ for the canonical seed-post index. If $M$ satisfies the seed-size law $M(\ell_*)=M(0)+M(1)$, then for every index $k$ the seed-closed replacement of $M$ has the same level value as $M$ at $k$.
background
The Unified Forcing Chain module aims to force the full T0–T8 stack from the Recognition Composition Law plus normalization and calibration. Inside that chain, multilevel hierarchies package discrete scale data as a positive map $\mathbb{N}\to\mathbb{R}$ with at least three positive levels (nontrivial multilevel composition).
Seed closure is the normal-form step that posts the two seed levels at a forced index (already fixed to $2$ in this development). The remaining compatibility condition is isolated as the canonical seed-size law: the value at that seed-post index equals the sum of levels $0$ and $1$. The structure is kept separate from the posting operation so a later step can derive the law from RCL/posting-potential composition rather than assume it.
This lemma is the one-direction preservation statement: if the original hierarchy already meets that additive law, the seed-closed replacement does not move any level.
proof idea
Fix an arbitrary level index $k$ and case on whether $k$ equals the canonical seed-post index.
At the seed-post index, reduce the closed level to the explicit two-seed posting formula and rewrite by the seed-size-law field of the hypothesis, matching the original level there.
Off that index, unfold the seed-closed multilevel composition and its level map; simplification with the inequality $k\neq\ell_*$ shows the closed level is definitionally the original level.
why it matters
Seed closure is only a harmless normal form on data that already satisfy the additive seed law. That fact is the forward half of the biconditional characterizing exact level-sequence preservation by seed closure, and it underwrites idempotence of the seed-closed normal form at the level surface.
Downstream, the same equality transports structural side conditions through seed closure: zero free-scale (uniform adjacent ratios) and the seed ratio strictly above one both pass from the original hierarchy to its seed-closed replacement once the size law holds. A further composite normal-form lemma uses the same identity after growth and uniform-after-growth closures.
In the forcing narrative this keeps hierarchy bookkeeping honest before $\varphi$-forcing and the eight-tick/D=3 steps: seed posting does not invent new scale data when the additive law is already in force.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.