seedClosedLevels
plain-language theorem explainer
Given a multilevel composition with positive level sizes, the seed-closed level map replaces the size at the canonical post index (level 2) by the sum of the two seed levels and leaves every other index unchanged. Hierarchy and forcing arguments cite it when enforcing local seed-size closure before ratio comparisons. The body is a one-line piecewise assignment on the naturals.
Claim. For a nontrivial multilevel composition $M$ with positive level sizes $\ell:\mathbb{N}\to\mathbb{R}$ (at least three levels), the seed-closed sequence is $\ell^{\mathrm{sc}}(k)=\ell(0)+\ell(1)$ when $k=2$ (the canonical seed-post index), and $\ell^{\mathrm{sc}}(k)=\ell(k)$ otherwise.
background
The Unified Forcing Chain module aims to derive the full T-1 through T8 stack as inevitabilities from the Recognition Composition Law plus normalization and calibration. Multilevel composition is the discrete hierarchy language used when forcing self-similarity and scale ratios along that chain.
A nontrivial multilevel composition supplies a level-size map $\ell:\mathbb{N}\to\mathbb{R}$ that is strictly positive at every index and, in particular, positive on levels $0,1,2$. The canonical seed-post index is fixed at $2$: seed levels $0$ and $1$ close locally by posting their sum at the next rung.
Seed-closure is the bookkeeping step that installs that local sum law into an arbitrary hierarchy before one asks whether the original sequence already obeyed it, or builds a closed multilevel object for ratio and self-similarity arguments.
proof idea
Pure definition, not a proved theorem. On input hierarchy $M$, return the function that at index $k$ branches on equality with the canonical seed-post index $2$: if equal, emit $\ell(0)+\ell(1)$; otherwise emit $\ell(k)$. No lemmas are applied; downstream simp lemmas unfold this case split at $0$, $1$, and $2$.
why it matters
This map is the level-sequence core of seed-closed multilevel composition and the comparison theorems that relate closure to the canonical seed-size law. Downstream results include positivity of the closed sequence, the simp evaluations at $0,1,2$, the implication that seed-size law yields an unchanged sequence, and the iff characterizing when closure is the identity on levels.
In the forcing chain this is local hierarchy hygiene before self-similarity and discrete scale forcing (the T6 $\varphi$ step and the broader complete-inevitability narrative). It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only standardizes how adjacent seed levels post to level $2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.