seedClosedMultilevelComposition_idempotent_levels
plain-language theorem explainer
The seed-closed normal form of a nontrivial multilevel composition is idempotent on levels: a second seed closure leaves every level value unchanged. Hierarchy and T5–T6 bridge arguments cite this to treat seed closure as a genuine normal form rather than a one-shot rewrite. The proof is a short term application of the seed-size law already satisfied by any seed-closed object.
Claim. Let $M$ be a nontrivial multilevel composition (positive level sequence with at least three levels). For every index $k\in\mathbb{N}$, if $M'$ denotes the canonical seed-closed normal form of $M$, then the seed-closed normal form of $M'$ has the same $k$-th level as $M'$: $(\mathrm{seedClose}(\mathrm{seedClose}(M)))_k = (\mathrm{seedClose}(M))_k$.
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. The T5→T6 step needs self-similarity on a discrete ledger hierarchy; multilevel compositions package that hierarchy as a positive real sequence levels : ℕ → ℝ with at least three occupied rungs (NontrivialMultilevelComposition).
Seed closure is the canonical normal-form operation that enforces the seed-size law on such a hierarchy. The surrounding certificate states that this normal form always exists and is unique up to level equality, preserves the original hierarchy exactly when the seed-size law already holds, and is idempotent. Idempotence at the level-sequence surface is the algebraic content of the present theorem: once closed, further closure is a no-op on levels.
Upstream, the hierarchy structure only demands positivity and three nontrivial levels; the seed-size law and the equality lemma that recovers original levels from that law are what turn closure into a projector.
proof idea
Term-mode one-liner. Instantiate the general fact that seed-closed levels equal the original levels whenever the seed-size law holds, applied not to $M$ but to the already seed-closed object seedClosedMultilevelComposition M. The second hypothesis is the lemma that every seed-closed multilevel composition satisfies the canonical seed-size law. Chaining those two facts yields levelwise equality of double closure with single closure.
why it matters
Idempotence is one of the three legs of the canonical seed-closure preservation certificate (canonical_seed_closure_preservation): equivalence of the closed form, exact preservation iff the seed-size law, and self-equivalence/idempotence. That certificate is quoted by the T5-to-T6 self-similarity bridge (t5_to_t6_bridge_holds), which packages uniqueness of $J$, internal hierarchy forcing of $\varphi$, and realized closed-scale normal-form equivalence.
In the forcing chain this sits between T5 (unique $J(x)=\cosh(\log x)-1$) and T6 ($\varphi$ as the self-similar fixed point). Without levelwise idempotence, seed closure would not be a normal form and the closed-scale route to $\varphi$ would not be stable under re-application. No open scaffold remains here: the claim is fully proved and only feeds higher bridge assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.