seedClosedMultilevelComposition_is_replacement
plain-language theorem explainer
The canonically seed-closed multilevel composition is a seed-closed replacement of any nontrivial hierarchy: non-seed levels are copied unchanged, and the seed post obeys the size law (level 2 equals level 0 plus level 1). Cited by the seed-closure equivalence and the T5-to-T6 self-similarity bridge. Proof is a two-field structure inhabitant: unfold-and-simp for preservation, plus the dedicated seed-size law.
Claim. For any nontrivial multilevel composition $M$ (positive real levels with at least three occupied rungs), the canonically seed-closed composition built from $M$ is a seed-closed replacement of $M$: every level other than the canonical seed post agrees with $M$, and the seed-post level equals the sum of levels $0$ and $1$.
background
The Unified Forcing Chain module shows T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The T5→T6 step needs self-similarity on a discrete multilevel hierarchy of positive real scales.
A nontrivial multilevel composition is a map $\mathbb{N}\to\mathbb{R}$ with strictly positive values and at least three occupied levels. Seed-closing replaces the canonical seed post (index 2) by the sum of levels 0 and 1, leaving every other level fixed; that construction is seedClosedLevels, packaged as a multilevel composition by seedClosedMultilevelComposition.
A seed-closed replacement of $M$ by $N$ is the Prop that $N$ preserves all non-seed levels of $M$ and satisfies the seed size law $N_2 = N_0 + N_1$. This theorem asserts that the canonical seed-closed object meets exactly those two obligations relative to the input hierarchy.
proof idea
Inhabit the two-field structure SeedClosedReplacement M (seedClosedMultilevelComposition M).
For preserves_nonseed: fix $k$ with $k\neq$ canonical seed-post index; unfold the seed-closed composition and the underlying level map seedClosedLevels; the defining if then reduces by simp with the inequality hypothesis to equality of levels.
For seed_size: apply the already-proved law seedClosedMultilevelComposition_seed_size_law M, which states that the seed-post level of the closed composition equals the sum of its levels 0 and 1.
why it matters
Seed closure is the normal-form step that lets hierarchy dynamics force $\varphi$ as the unique self-similar ratio (T6 in the forcing chain, after T5 J-uniqueness). Without a proved replacement witness, later equivalence and bridge theorems cannot treat the closed hierarchy as interchangeable with the original for forcing purposes.
Immediate parent: seedClosedMultilevelComposition_equiv, which packages this replacement with level-0/1 agreements into SeedClosureEquiv. That equivalence is consumed by t5_to_t6_bridge_holds, the theorem-backed T5-to-T6 self-similarity bridge (internal hierarchy forces $\varphi$; realized closed scale forces $\varphi$).
In framework terms this is plumbing on the T5→T6 link of the complete inevitability chain, not a new physical constant, but it discharges the seed-size obligation that self-similarity arguments assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.