seedClosedMultilevelComposition_equiv
plain-language theorem explainer
The canonical seed-closed replacement of any nontrivial multilevel hierarchy is forcing-equivalent to the original: levels 0 and 1 stay fixed, and the seed-post level is the additive closure of that pair. Cited by the T5–T6 self-similarity bridge and by seed-closure preservation certificates. Proof fills the equivalence structure from the replacement lemma plus direct simplification of the closed level sequence.
Claim. For every nontrivial multilevel composition $M$ (a strictly positive level sequence with at least three levels), let $N$ be its canonical seed-closed replacement. Then $N$ is forcing-equivalent to $M$: $N$ is a seed-closed replacement of $M$, $N$'s levels $0$ and $1$ equal those of $M$, and $N$ at the canonical seed-post index equals $M$'s level $0$ plus level $1$.
background
The Unified Forcing Chain module shows T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Multilevel compositions are positive real level sequences with at least three levels; they encode the discrete hierarchy that later forces self-similarity and $\varphi$.
Seed-closure rewrites only the canonical seed-post index (level $2$): replace it by level $0$ plus level $1$, leave every other level unchanged. The resulting object is again a nontrivial multilevel composition. Forcing-relevant equivalence between a hierarchy and a candidate replacement requires four facts: the replacement is seed-closed over the original, levels $0$ and $1$ agree, and the seed-post level is exactly that additive closure.
Upstream, the replacement property of the canonical construction is already proved; the level-sequence rewrite is definitional. This theorem packages those facts into the exact quotient relation the universal forcing spine uses at the seed-closure bridge.
proof idea
Construct the equivalence structure fieldwise. The replacement field is the prior theorem that the canonical seed-closed composition is a seed-closed replacement. Levels $0$ and $1$ are immediate by unfolding the seed-closed level map (the rewrite fires only at the seed-post index). For the seed-post field, rewrite the goal as equality of the closed level at the canonical index with the sum of the original seed levels, then simplify the closed-level definition and the index constant $2$.
why it matters
This is the forcing-equivalence certificate that the canonical seed-closed replacement is the right quotient of the original hierarchy. Downstream it is the closure_equiv field of the canonical seed-closure preservation certificate, and it feeds the lemma that seed-closure preserves the base ratio of levels $1/0$.
That ratio preservation and the closed-scale normal form sit on the T5-to-T6 self-similarity bridge: unique $J$ (T5) plus a realized closed hierarchical scale force $\varphi$ as the self-similar fixed point (T6). Without a proved equivalence between a hierarchy and its seed-closed form, the bridge would only have a construction, not a forcing identification. In the primer chain this is infrastructure for T6, not a new physical constant, but it is the precise relation the spine quotes when it says seed-closure does not change the forcing content of the hierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.