SeedClosurePreservation
plain-language theorem explainer
For a nontrivial multilevel composition hierarchy, the seed-closure certificate packages six reflection properties: the canonical seed-closed normal form is equivalent to the original; exact level preservation and self-equivalence each hold iff the seed-size law holds; closure is idempotent on levels; the normal form is unique among equivalents; and the base ratio of levels is preserved. Anyone working the T5-to-T6 self-similarity bridge cites this bundle. It is a pure Prop structure (definitional certificate), not a proved theorem.
Claim. For a nontrivial multilevel composition $M$, a seed-closure preservation certificate asserts: (i) $M$ is seed-closure equivalent to its canonical seed-closed normal form $M^\ast$; (ii) $M^\ast$ has exactly the same levels as $M$ if and only if $M$ obeys the canonical seed-size law (seed level equals the sum of levels $0$ and $1$); (iii) $M$ is seed-closure equivalent to itself iff that same law holds; (iv) applying seed closure twice leaves levels unchanged; (v) every hierarchy seed-closure equivalent to $M$ has the levels of $M^\ast$; (vi) the base ratio $\mathrm{levels}(1)/\mathrm{levels}(0)$ is unchanged by seed closure.
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law with normalization and calibration. The T5→T6 step needs a discrete multilevel hierarchy whose scale ratio becomes $\varphi$ under self-similarity. Hierarchies here are nontrivial multilevel compositions: sequences of positive level sizes with composition structure.
Seed closure replaces a hierarchy by a normal form in which the seed level (canonical index 2) is the additive closure of levels 0 and 1. Seed-closure equivalence requires a seed-closed replacement that preserves levels 0 and 1 and sets the seed level to that sum. The canonical seed-size law is exactly the statement that the original hierarchy already has additive seed size at that index.
This structure packages the reflection properties of that normal-form operation so the bridge can quote a single certificate rather than six separate lemmas.
proof idea
This declaration is a Prop-valued structure, not a theorem. It bundles six named fields that a later constructor must inhabit. The companion Subsingleton instance is proved by rfl: any two certificates for fixed $M$ are definitionally equal as pure propositions. The actual content is discharged by the canonical constructor theorem, which fills the fields from lemmas establishing seed-closed equivalence of the normal form, the iff between exact level preservation and the seed-size law, the iff between self-equivalence and that law, idempotence of double closure on levels, uniqueness of normal-form levels among equivalents, and preservation of the base ratio.
why it matters
The certificate is the exact reflection theorem for the seed-closure bridge on the path from T5 (unique $J$-cost) to T6 ($\varphi$ forced as the self-similar fixed point). Downstream, the canonical constructor inhabits the certificate for every nontrivial multilevel composition, and the T5→T6 self-similarity bridge routes through hierarchy dynamics that need the base ratio preserved and the normal form unique. Without base-ratio preservation, the scale ratio fed to self-similarity could drift under normalization; without the seed-size law equivalences, exact preservation would be an extra assumption rather than a forced dichotomy. This sits inside the Complete Inevitability Chain of the module: every step forced from RCL, not merely compatible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.