SeedClosedReplacement
plain-language theorem explainer
A seed-closed replacement of a multilevel hierarchy M is any hierarchy N that matches M on every level except the canonical seed post, where N's seed level equals the sum of its level-0 and level-1 values. Self-similarity and hierarchy arguments on the T5–T6 bridge cite this relation as the forcing-relevant quotient. It is a pure Prop structure: two fields, no proof body.
Claim. Let $M$ and $N$ be nontrivial multilevel compositions (positive level sequences $\mathbb{N}\to\mathbb{R}$ with at least three levels). Then $N$ is a seed-closed replacement of $M$ when (i) $N_k=M_k$ for every index $k$ other than the canonical seed-post index, and (ii) the seed-post level of $N$ equals $N_0+N_1$.
background
The module UnifiedForcingChain aims to force the full T0–T8 chain from the Recognition Composition Law plus normalization and calibration. Near the T5→T6 step, discrete hierarchies must be closed under a canonical seed-size law before self-similarity can pin the scale ratio to $\varphi$.
A nontrivial multilevel composition is a positive sequence of real levels with at least three occupied rungs. The seed post is a distinguished index; the seed size law requires that post's level to equal the sum of the two base levels (additive closure of the seed). A seed-closed replacement keeps every non-seed level fixed and enforces that additive law at the seed index.
Upstream, HierarchyForcing supplies the multilevel carrier; the surrounding chain already has unique $J$ (T5) and is preparing the self-similarity fixed-point argument that forces $\varphi$ (T6).
proof idea
Definitional structure, not a proved theorem. The Prop is the conjunction of two fields: universal equality of levels off the canonical seed-post index, and the single additive equation that the seed-post level equals level 0 plus level 1. No tactics or lemmas; downstream theorems inhabit or reason about these fields directly.
why it matters
This is the exact quotient relation used by the universal forcing spine at the hierarchy bridge. It feeds SeedClosureEquiv (replacement plus level-0 preservation), the uniqueness theorem that any seed-closed replacement agrees levelwise with the canonical seed-closed construction, and the self-iff characterizing when a hierarchy is already seed-closed. Those facts sit under T5_To_T6_SelfSimilarity_Bridge: closed observable frameworks with realized hierarchy force the scale ratio $\varphi$. Without a crisp seed-closure predicate, the T6 self-similarity step would smuggle an unstated normalization of the seed rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.