seedClosedReplacement_self_iff_seed_size_law
plain-language theorem explainer
A multilevel hierarchy is seed-closed as a replacement of itself exactly when it already obeys the canonical seed-size law (seed post equals sum of levels 0 and 1). Hierarchy-forcing and seed-closure arguments cite this to collapse self-replacement to a pure size certificate. The proof is a short bidirectional constructor: one side projects the seed-size field; the other reuses the reflexive seed-closure equivalence built from that law.
Claim. For any nontrivial multilevel composition $M$ (positive real level sizes, at least three levels), $M$ is a seed-closed replacement of itself if and only if $M$ satisfies the canonical seed-size law $M_{\mathrm{seed}} = M_0 + M_1$ at the forced seed-post index.
background
The Unified Forcing Chain module derives T-1 through T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Hierarchy forcing sits in the discrete ledger / self-similarity segment that feeds φ and the octave structure.
A nontrivial multilevel composition is a map from level indices to positive reals with at least three positive levels. The canonical seed-size law isolates one remaining arithmetic constraint once the seed post index is already forced to 2: posting seed levels 0 and 1 closes with additive size, $M_{\mathrm{seed}} = M_0 + M_1$.
A seed-closed replacement of $M$ by $N$ preserves every non-seed level and requires $N$ itself to obey that additive seed-size law. Self-replacement ($N = M$) therefore asks when $M$ already meets the seed constraint while trivially preserving its own non-seed levels.
proof idea
Bidirectional constructor on the ↔.
Forward: from a self seed-closed replacement, project the seed_size field and pack it as the sole field of the canonical seed-size law certificate.
Reverse: given the seed-size law on $M$, apply seedClosureEquiv_refl_of_seed_size_law to obtain the reflexive seed-closure equivalence of $M$ with itself, then take its replacement projection. Non-seed preservation is automatic for $N = M$; the size law is exactly the hypothesis.
why it matters
In the forcing chain, seed posting is the discrete arithmetic step that must close before higher hierarchy ratios and self-similarity (toward T6 φ and the eight-tick octave) can be treated as forced rather than optional. Separating the size law from the replacement structure lets later RCL/posting-potential arguments discharge only the additive identity, then recover full seed-closure for free on the diagonal.
The doc-comment states the content directly: self seed-closed replacement holds exactly when the canonical seed-size law already holds. No downstream consumers are wired yet (used_by empty), so this is presently a local bridge lemma inside UnifiedForcingChain, ready for seed-closure and hierarchy-forcing parents once those cite the iff.
It does not itself force φ, D = 3, or the alpha band; it only equates two certificates used in that scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.