canonicalBaseRatio_eq_phi_of_uniformClosed_seed
plain-language theorem explainer
Under growth of the base step and seed-size closure on the uniform-closed hierarchy, the canonical base ratio equals the golden ratio φ. Hierarchy and T6 forcing arguments cite this to pin the discrete scale factor without an extra ratio hypothesis. The proof converts seed closure to the golden equation, obtains positivity from growth, and invokes uniqueness of the positive self-similar ratio.
Claim. Let $M$ be a nontrivial multilevel composition (positive level sizes, at least three levels). Suppose the base step grows ($M_0 < M_1$) and the uniform-closed form of $M$ obeys the canonical seed-size law (posting levels $0$ and $1$ has additive size at the forced seed index). Then the canonical base ratio of $M$ equals $\varphi$, the unique positive solution of $r^2 = r + 1$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T6 is the step that forces $\varphi$ as the self-similar fixed point of a discrete ledger hierarchy.
A NontrivialMultilevelComposition is a positive real sequence of level sizes with at least three levels. Canonical growth orientation is the order statement that the first step expands: level $0$ is strictly smaller than level $1$. The canonical seed-size law says that posting the two seed levels closes additively at the already-forced seed index $2$: size at that index equals size$_0$ + size$_1$.
Uniform closure replaces free adjacent ratios by a single base ratio. Seed closure on that uniformized object is equivalent (via an in-module bridge) to the golden constraint on that ratio. Upstream, phi_unique_self_similar records that among positive reals the golden constraint characterizes $\varphi$: if $r>0$ and $r$ is self-similar, then $r=\varphi$.
proof idea
Short tactic proof in four steps. First, apply the equivalence uniformClosed_seed_size_law_iff_golden to the seed hypothesis, obtaining that the canonical base ratio satisfies the golden (self-similarity) equation. Second, growth orientation yields ratio_gt_one_of_canonical_growth, so the base ratio is strictly larger than $1$. Third, linarith downgrades that to positivity. Fourth, feed positivity and the golden equation into PhiForcing.phi_unique_self_similar, which is the standard uniqueness lemma for the positive self-similar ratio.
why it matters
This is a T6 pin inside the complete inevitability chain: once the hierarchy is uniform-closed and seed-closed, and the base step actually grows, the scale factor cannot be any positive self-similar number other than $\varphi$. Downstream it is the field base_ratio_phi_of_growth_seed in canonical_uniform_seed_closure_compatibility, whose doc-comment calls that certificate the Lean replacement for assuming that uniformization still preserves seed posting: the two normal forms commute at the seed-size surface exactly at the golden equation.
In the primer landmarks this is the discrete-ledger half of T6 (φ forced as self-similar fixed point), sitting above T5 J-uniqueness and below the eight-tick and $D=3$ steps. It removes an ad hoc ratio assumption from later hierarchy and constant-derivation arguments that need the base ratio already equal to $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.