seedClosureEquiv_refl_of_seed_size_law
plain-language theorem explainer
A multilevel hierarchy that already obeys the canonical seed-size law is seed-closure-equivalent to itself. Anyone working the T5→T6 self-similarity bridge cites this reflexivity direction. The proof is a direct structure construction: identity on non-seed levels plus the given additive seed law.
Claim. Let $M$ be a nontrivial multilevel composition (positive level sizes, at least three levels). If $M$ satisfies the canonical seed-size law $M(\ell_*)=M(0)+M(1)$ at the forced seed index $\ell_*$, then $M$ is seed-closure-equivalent to itself: the seed-closed replacement of $M$ may be taken to be $M$, levels $0$ and $1$ are preserved, and the seed level equals the additive closure of the two seed levels.
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 one needs a discrete multilevel hierarchy whose seed posting is already closed under the canonical size rule, so that self-similarity can pin $\varphi$.
A nontrivial multilevel composition is a positive real-valued level function with at least three levels. The canonical seed-size law isolates the remaining size constraint after the seed index is forced to $2$: posting levels $0$ and $1$ must close additively at that index, $M(\ell_*)=M(0)+M(1)$. Seed-closure equivalence is the forcing-relevant quotient relation: a replacement $N$ of $M$ agrees on all non-seed levels, preserves levels $0$ and $1$, and realizes the seed level as that additive closure. The doc-comment states the claim directly: a hierarchy already satisfying the seed-size law is preserved by seed closure as an equivalence to itself.
proof idea
Term-mode structure construction, not a multi-step tactic script. The SeedClosureEquiv M M record is filled fieldwise: the seed-closed replacement of $M$ by itself is witnessed by reflexivity on every non-seed level together with hsize.seed_size_law at the seed index; level0 and level1 are rfl; level2 is again hsize.seed_size_law. No external lemmas beyond the structure fields of CanonicalSeedSizeLaw and SeedClosureEquiv are required.
why it matters
This is the reflexivity half of the seed-closure fixed-point characterization used on the T5→T6 bridge. Downstream, seedClosureEquiv_self_iff_seed_size_law packages the biconditional (self-equivalence iff the seed-size law), and seedClosedReplacement_self_iff_seed_size_law does the same for the underlying replacement relation. Those characterizations feed t5_to_t6_bridge_holds, which records that the T5-to-T6 self-similarity bridge is theorem-backed once J-uniqueness is in hand.
In the forcing chain primer this sits between T5 (unique $J(x)=(x+x^{-1})/2-1$) and T6 ($\varphi$ forced as the self-similar fixed point). Without a clean reflexivity certificate, the hierarchy cannot be treated as already closed under seed posting, and the discrete self-similarity argument that pins $\varphi$ does not start. The declaration closes no open scaffold; it is a proved building block for that bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.