seedClosedMultilevelComposition
plain-language theorem explainer
Any positive multilevel composition has a canonical seed-closed replacement: keep every level fixed except level 2, which is reset to the sum of levels 0 and 1. Hierarchy and normal-form arguments cite this object as the unique local closure that installs the seed-size law by construction. The definition is a structure pack of the seed-closed level map with positivity and the three-level lower bound.
Claim. Given a multilevel composition $M$ with strictly positive levels $M_k>0$ for all $k$ and with $M_0,M_1,M_2>0$, its canonical seed-closed replacement is the multilevel composition whose levels are $M_k$ for $k\neq 2$ and $M_0+M_1$ at the canonical seed-post index $k=2$. The replacement remains strictly positive at every level and still has at least three positive levels.
background
The ambient module is the Unified Forcing Chain: from the Recognition Composition Law plus normalization and calibration, the chain aims to force T-1 through T8 (absolute floor, logic, MP, discreteness, ledger, recognition, unique $J$, $\varphi$, eight-tick, $D=3$).
A nontrivial multilevel composition is a map $\mathrm{levels}:\mathbb{N}\to\mathbb{R}$ that is strictly positive at every index and, in particular, positive on the first three indices. In the local second-order hierarchy picture, indices $0$ and $1$ are the adjacent seed levels; their first local closure is posted at the next index. That posting index is fixed canonically as $2$.
Seed-closed levels are the pointwise rewrite that leaves every level of $M$ alone except at index $2$, where the value is replaced by $M_0+M_1$. The companion positivity lemma records that this rewrite stays strictly positive, using ordinary sum-positivity at the rewritten slot.
proof idea
The definition builds a new nontrivial multilevel composition whose levels field is exactly the seed-closed level sequence of $M$.
Positivity of every level is the already-proved seed-closed positivity lemma. The three-level lower bound is unpacked by cases: levels $0$ and $1$ inherit positivity from $M$; level $2$ is definitionally $M_0+M_1$, and the sum of two positive reals is positive (via the integer/rational addition positivity fact after simplifying the seed-closed and canonical-index definitions).
why it matters
This is the canonical local closure that installs the seed-size law without an extra hypothesis on $M$. Downstream, the seed-closed object is what carries the canonical seed-size law by construction, both in the untyped and typed seed-posting routes. It is the witness used to characterize when seed closure is idempotent on levels: the closed levels agree with the original sequence if and only if $M$ already obeyed the seed-size law.
It also sits inside the hierarchy normal-form pipeline. Closure certificates and the idempotence facts for seed closure after growth and uniform-after-growth closures all route through this replacement, so later $\varphi$-uniform normal forms can assume seed additivity is already enforced. In the forcing-chain narrative this is bookkeeping for discrete multilevel scale structure on the way to self-similarity ($\varphi$) and the octave, not a substitute for T5–T8 themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.