phiUniformClosedLevels_eq_original_iff_uniform_growth_seed
plain-language theorem explainer
The φ-uniform normal form of a multilevel hierarchy agrees levelwise with the original hierarchy if and only if that hierarchy already obeys the three canonical laws: uniform adjacent scaling by its own base ratio, growth at the first step, and additive seed closure at index 2. Hierarchy and φ-forcing arguments cite this as the exact fixed-point criterion for the normal form. One direction transports the closed form's built-in laws across level equality; the other is a one-line appeal to the constructive sufficiency lemma.
Claim. Let $M$ be a nontrivial multilevel composition (positive real levels with at least three levels). Write $M^\varphi$ for its $\varphi$-uniform closed normal form. Then $M^\varphi_k = M_k$ for every level index $k$ if and only if: (i) $M_{k+1} = (M_1/M_0)\, M_k$ for all $k$ (uniform scale by the base ratio), (ii) $M_0 < M_1$ (growth orientation), and (iii) $M_2 = M_0 + M_1$ (canonical seed-size law at the forced seed-post index $2$).
background
This sits in the Unified Forcing Chain module, which derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The local objects are multilevel hierarchies: maps $\mathbb{N}\to\mathbb{R}$ with strictly positive levels and at least three levels occupied.
The canonical base ratio of such an $M$ is $M_1/M_0$. Three theorem-shaped certificates replace raw free hypotheses: the uniform-scale law (every adjacent step multiplies by that base ratio), growth orientation ($M_0 < M_1$), and the seed-size law ($M_2 = M_0 + M_1$, with seed-post index forced to $2$). The $\varphi$-uniform closed multilevel composition is the normal form that rebuilds levels so these three laws hold with base ratio pinned to $\varphi$ (the T6 self-similar fixed point).
Upstream, the closed form already carries certificates phiUniformClosed_uniform_scale, phiUniformClosed_growth, and phiUniformClosed_seed_size_law, and its base ratio equals $\varphi$. The present statement is the fixed-point characterization: the normal form is the identity on levels exactly when $M$ already satisfied the three laws.
proof idea
Biconditional by constructor.
Forward: assume levelwise equality $M^\varphi_k = M_k$. First recover that the canonical base ratio of $M$ equals $\varphi$, by rewriting the closed-form identity phiUniformClosed_base_ratio at indices $0$ and $1$ via the equality. Then package the three certificates: transport phiUniformClosed_uniform_scale's adjacent-step identity across equality (after rewriting its base ratio to $\varphi$ and then to $M$'s base ratio); transport phiUniformClosed_growth.base_step_grows at levels $0,1$; transport phiUniformClosed_seed_size_law at the seed-post index $2$ and at $0,1$.
Reverse: one-line application of the already-proved sufficiency lemma phiUniformClosedLevels_eq_original_of_uniform_growth_seed, feeding the three conjuncts of the hypothesis.
why it matters
This is the exact fixed-point criterion for the $\varphi$-uniform normal form on multilevel hierarchies. It feeds directly into canonical_phi_uniform_closure, which packages the closed form's uniform, growth, and seed certificates into a single PhiUniformClosure witness for any nontrivial multilevel composition.
In the forcing chain this sits at the T6 layer: $\varphi$ is forced as the self-similar fixed point of discrete ledger scaling. The three laws are the theorem-shaped replacements for the older free hypotheses (no free scale, ratio greater than one, seed posting size). Establishing when the normal form is already the original hierarchy closes the loop between "impose $\varphi$-uniform structure" and "the hierarchy was already $\varphi$-ready," which the complete inevitability chain needs before eight-tick (T7) and $D=3$ (T8) arguments can treat the ladder as canonically scaled.
No scaffolding remains here: the claim is fully proved and only packages existing closed-form certificates plus the constructive converse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.