seedUniformGrowthClosed_eq_phiUniform
plain-language theorem explainer
Growth closure, then uniform closure, then seed closure of a nontrivial multilevel hierarchy yields the same level sequence as the direct φ-uniform normal form. Hierarchy and forcing-chain authors cite this when collapsing the three-step closure path onto φ-uniform. The proof rewrites by seed-idempotence after uniform-after-growth, then applies the lemma that uniform-after-growth equals φ-uniform.
Claim. For every nontrivial multilevel composition $M$ (a positive real level sequence with at least three positive entries) and every index $k\in\mathbb{N}$, the $k$-th level after growth closure, then uniform closure, then seed closure of $M$ equals the $k$-th level of the canonical $\varphi$-uniform closed multilevel composition of $M$.
background
The module UnifiedForcingChain proves T0–T8 as forced inevitabilities from the Recognition Composition Law plus normalization and calibration. Multilevel hierarchy data live in NontrivialMultilevelComposition: a map $\mathbb{N}\to\mathbb{R}$ of strictly positive levels with at least three positive entries (levels 0,1,2).
Three canonical closures act on such data. Growth closure produces the growth-closed multilevel composition; uniform closure forces uniform adjacent ratios (no free scale parameters); seed closure is the canonical seed-closed form associated to any positive multilevel composition. Separately, φ-uniform closure builds the direct φ-uniform normal form tied to the self-similar fixed point φ forced at T6.
Upstream, seed closure after uniform-after-growth is already known to leave levels unchanged (idempotence on levels). Uniform closure after growth closure is already identified with the φ-uniform form. This theorem packages those facts into the full three-step path.
proof idea
Term-style tactic proof in two steps. Introduce the level index $k$. Rewrite the left-hand side by the upstream idempotence theorem: seed closure after uniform-after-growth does not change levels, so the triple composition’s levels equal those of uniform-after-growth alone. Discharge the goal by the upstream equality that uniform closure after growth closure equals the φ-uniform closed composition, evaluated at $k$. No new algebra; pure composition of two prior levelwise identities.
why it matters
This is the bridge that says the long closure path (growth → uniform → seed) lands on the same normal form as the direct φ-uniform construction. Downstream it is consumed by the canonical closure-composition certificate, which packages uniform-after-growth equals φ-uniform together with seed-after-uniform-growth idempotence into a single ClosureNormalFormComposition witness.
In the forcing chain this sits under hierarchy normal-form bookkeeping that supports T6 (φ forced as the self-similar fixed point) and the broader claim that discrete ledger self-similarity admits a unique uniform scale. It does not itself force φ or D=3; it certifies that the three named closures commute with the φ-uniform normal form on level sequences, so later certificates need not track intermediate seed/uniform/growth states separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.