seedClosureEquiv_levels_unique
plain-language theorem explainer
Any multilevel hierarchy seed-closure-equivalent to M has exactly the canonical seed-closed level sequence of M. Hierarchy and T5–T6 bridge arguments cite this to pin levels after quotienting by seed closure. The proof is a one-line projection onto the underlying seed-closed-replacement uniqueness lemma.
Claim. Let $M$ and $N$ be nontrivial multilevel compositions (positive real level sequences with at least three levels). If $N$ is seed-closure-equivalent to $M$ (seed-closed replacement of $M$, with levels $0$ and $1$ preserved and the seed post-index equal to the canonical additive closure $M_0+M_1$), then for every index $k$, $N$'s level $k$ equals the $k$-th level of the canonical seed-closed multilevel composition associated to $M$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. At the hierarchy layer, a nontrivial multilevel composition is a positive map $\mathbb{N}\to\mathbb{R}$ with at least three positive levels; uniform adjacent ratios then build the forced scale ladder used toward $\varphi$.
Seed closure is the forcing-relevant quotient at this bridge. The canonical seed-closed multilevel composition of $M$ replaces the seed post-index by the additive closure of the base levels while keeping the rest of the ladder in normal form. Seed-closure equivalence strengthens seed-closed replacement by also fixing levels $0$ and $1$ and identifying the seed level with that additive sum; the module doc calls this the exact quotient used by the universal forcing spine.
Upstream, seed-closed replacements are already unique at the level-sequence layer. The present statement lifts that uniqueness to the full equivalence relation so later certificates can treat any seed-equivalent hierarchy as having the same levels as the canonical closed form of $M$.
proof idea
Term-mode one-liner. Seed-closure equivalence packages a SeedClosedReplacement witness as its replacement field. Apply the upstream theorem that any seed-closed replacement $N$ of $M$ satisfies $N.\mathrm{levels},k = (\mathrm{seedClosedMultilevelComposition},M).\mathrm{levels},k$ for all $k$, feeding that replacement witness. No case split or extra arithmetic is needed here; uniqueness of levels under the weaker replacement relation already implies uniqueness under the stronger equivalence.
why it matters
This pins level sequences after seed-closure quotienting, so the hierarchy ratio $\mathrm{levels},1/\mathrm{levels},0$ that feeds hierarchy_forced is well-defined on the equivalence class. Downstream, canonical_seed_closure_preservation builds the seed-closure preservation certificate (closure equivalence, exact preservation iff, self-equivalence iff) on that normal form.
It is also used by t5_to_t6_bridge_holds, the theorem-backed T5-to-T6 self-similarity bridge: once $J$ is unique (T5), internal hierarchy and realized closed-scale data force $\varphi$ (T6). Without level uniqueness under seed-closure equivalence, the closed-scale normal form would not be canonical across equivalent hierarchies, and the bridge could not treat seed-closed ladders as interchangeable.
In the forcing chain this sits between ledger/recognition structure and the self-similar fixed point $\varphi$, keeping the discrete multilevel data rigid before eight-tick and $D=3$ steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.