canonical_seed_closure_preservation
plain-language theorem explainer
For any nontrivial multilevel composition, the canonical seed-closed replacement is a unique normal form that is seed-closure equivalent to the original, preserves the base ratio, is idempotent, and matches the original levels exactly iff the seed-size law already holds. The T5-to-T6 self-similarity bridge cites this certificate. The proof is a structure assembly: each field is discharged by a named prior lemma.
Claim. Let $M$ be a nontrivial multilevel composition (positive level sequence with at least three levels). Then the canonical seed-closed replacement of $M$ satisfies the full seed-closure preservation package: it is seed-closure equivalent to $M$; its levels equal those of $M$ for every index if and only if $M$ obeys the canonical seed-size law; self-equivalence under seed closure is likewise equivalent to that law; applying seed closure twice leaves levels unchanged; any hierarchy seed-equivalent to $M$ has exactly those closed levels; and the base ratio $\mathrm{levels}(1)/\mathrm{levels}(0)$ is preserved.
background
The Unified Forcing Chain module shows T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. The T5→T6 step needs self-similarity on a discrete multilevel hierarchy: after unique $J$ is forced, $\varphi$ must arise as the fixed scale of a closed level ladder.
A nontrivial multilevel composition is a positive real sequence of levels with at least three occupied rungs. Seed closure replaces an arbitrary such hierarchy by a canonical seed-closed form. Seed-closure equivalence identifies hierarchies that agree after that replacement. The seed-size law is the exact condition under which closure does not move any level.
SeedClosurePreservation packages the reflection facts: existence of a unique normal form, the iff with the seed-size law, idempotence, and base-ratio invariance. Upstream lemmas already prove each clause separately for the canonical replacement.
proof idea
Tactic-mode structure construction for SeedClosurePreservation M. Each field is a one-line appeal to a prior theorem on the same $M$:
closure_equiv←seedClosedMultilevelComposition_equivexact_preservation_iff←seedClosedLevels_eq_original_iff_seed_size_lawself_equiv_iff←seedClosureEquiv_self_iff_seed_size_lawidempotent←seedClosedMultilevelComposition_idempotent_levelsunique_normal_form← intro on $N$ andseedClosureEquiv_levels_uniquebase_ratio_preserved←seedClosedMultilevelComposition_preserves_base_ratio
No new algebra; the certificate is the bundled interface those lemmas already justify.
why it matters
This is the exact reflection theorem for the seed-closure bridge inside the forcing chain. Downstream, t5_to_t6_bridge_holds consumes it when assembling the T5-to-T6 self-similarity bridge (unique $J$ forces $\varphi$ as the closed-scale fixed point). That bridge is the formal link from T5 (J-uniqueness via d'Alembert plus normalization) to T6 ($\varphi$ forced by self-similarity on the discrete ledger).
Without a single Prop that records equivalence, exact-preservation iff, uniqueness, idempotence, and base-ratio preservation together, the T5→T6 argument would re-open those obligations at each use site. The certificate keeps the hierarchy normal-form story local and reusable. Framework landmark: T6 in the T0–T8 chain, after RCL-forced unique $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.