growthClosedMultilevelComposition_base_ratio
plain-language theorem explainer
Any nontrivial multilevel composition, after growth closure, has canonical base ratio exactly φ. Hierarchy and forcing-chain arguments cite this when normalizing discrete level stacks toward the self-similar φ ladder. The proof is a short term reduction: unfold the base-ratio definition to the closed level-1/level-0 quotient and simplify.
Claim. Let $M$ be a nontrivial multilevel composition (a positive real sequence of levels with at least three positive entries). Write $M^{\mathrm{gc}}$ for its growth-closed form. Then the canonical base ratio of $M^{\mathrm{gc}}$ equals $\varphi$, i.e. $\mathrm{levels}^{\mathrm{gc}}(1)/\mathrm{levels}^{\mathrm{gc}}(0)=\varphi$.
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 step is the discrete hierarchy side of T6: φ is forced as the self-similar fixed point of a discrete ledger of scales.
A nontrivial multilevel composition is a positive map $\mathbb{N}\to\mathbb{R}$ with at least three positive levels. Growth closure rebuilds that stack into a normal form whose successive scales obey a fixed growth law; the canonical base ratio is the first adjacent ratio (level 1 over level 0) of that closed stack. Upstream, φ is the unique positive self-similar scale from PhiForcing; the closed levels are the concrete sequence growthClosedLevels attached to the closed composition.
The claim is independent of the seed ratios of $M$: once growth is closed, the base step is forced to φ.
proof idea
Term-mode, three steps. First change rewrites the goal as the explicit quotient growthClosedLevels M 1 / growthClosedLevels M 0 = φ, which is the definition of canonicalBaseRatio on the growth-closed object. Then simp [growthClosedLevels] unfolds the closed-level formula so the quotient becomes an algebraic expression already known to equal φ. Finally field_simp clears the denominator, using positivity of level 0 from M.levels_pos. No external lemmas beyond the definitions and that positivity fact.
why it matters
This is the base-ratio half of the growth-closure normal form used throughout the hierarchy forcing path to T6 (φ forced). Downstream, canonical_growth_closure_preservation packages it with growth normal form and the exact-preservation criterion: growth closure preserves the original hierarchy exactly when the original first step is already the canonical φ-step. It is also consumed by uniformClosed_after_growthClosed_eq_phiUniform and uniformAfterGrowth_seed_size_law, which show that uniform closure after growth lands on the φ-uniform stack and satisfies the canonical seed-size law.
In the forcing chain this pins the first rung of the discrete scale ladder to φ, so later eight-tick (T7) and D=3 (T8) arguments inherit a φ-normalized hierarchy rather than a free base ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.