seedClosedReplacement_levels_unique
plain-language theorem explainer
Any multilevel hierarchy that is a seed-closed replacement of M must match the canonical seed-closed level sequence of M at every index. Hierarchy and T5–T6 bridge arguments cite this to pin the discrete scale ladder once the seed post is closed. The proof is a short case split on the canonical seed index, using preservation off-seed and the seed-size law on-seed.
Claim. Let $M$ and $N$ be nontrivial multilevel compositions (positive level maps $\mathbb{N}\to\mathbb{R}$ with at least three positive levels). If $N$ is a seed-closed replacement of $M$—it agrees with $M$ at every level except the canonical seed post, and at that post it obeys the seed size law $\mathrm{levels}(k_*)=\mathrm{levels}(0)+\mathrm{levels}(1)$—then for every $k$, the levels of $N$ equal those of the canonical seed-closed multilevel composition built from $M$.
background
The module UnifiedForcingChain aims to force the full T0–T8 chain from the Recognition Composition Law plus normalization and calibration. In that setting, hierarchies are modeled by NontrivialMultilevelComposition: a positive real level sequence with at least three positive rungs, the discrete scale data that later forces self-similarity and $\varphi$.
A seed-closed replacement of $M$ is any composition $N$ that keeps every non-seed level of $M$ fixed and replaces the canonical seed post by the additive seed-size law (level at the seed index equals level 0 plus level 1). The canonical object seedClosedMultilevelComposition M is the standard such closure of $M$ (via seedClosedLevels).
This uniqueness statement is the level-sequence half of seed closure: once you know $N$ is some seed-closed replacement, its entire level map is forced to equal the canonical closed one. That is the algebraic input later packaged as seed-closure equivalence and fed into the T5-to-T6 self-similarity bridge.
proof idea
Term-mode proof by intro k and a by_cases on whether $k$ equals the canonical seed post index.
On the seed index: substitute, rewrite by the seed-size field of the replacement hypothesis, then rewrite levels 0 and 1 via preserves_nonseed (both are non-seed), and simplify against the definition of the canonical seed-closed composition.
Off the seed index: rewrite by preserves_nonseed, unfold the canonical seed-closed composition and its level map, and simplify with the inequality hypothesis. No external lemmas beyond the structure fields and the local canonical definitions.
why it matters
In the forcing chain, T5 pins the unique cost $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger. Between them sits hierarchy dynamics: multilevel compositions and their closed scale normal forms.
This theorem supplies uniqueness of level sequences for seed-closed replacements. Downstream, seedClosureEquiv_levels_unique is the one-line lift to seed-closure equivalence ("any hierarchy seed-equivalent to $M$ has the canonical seed-closed level sequence"), and t5_to_t6_bridge_holds records that the T5-to-T6 self-similarity bridge is theorem-backed, including realized closed-scale normal-form equivalence. Without level uniqueness, the closed-scale normal form would not be canonical, and the internal hierarchy route to $\varphi$ would not be forced.
It is a small but load-bearing uniqueness step inside the Complete Inevitability Chain, not a physics endpoint by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.