minimalHierarchy_scale_eq_canonical
plain-language theorem explainer
Any minimal discrete hierarchy shares the exact scale sequence of the canonical minimal hierarchy: the k-th rung equals the canonical k-th rung for every k. Hierarchy and φ-forcing arguments cite this uniqueness of the geometric ladder once minimality holds. The proof unfolds the geometric scale map, rewrites the common ratio to φ via the companion ratio lemma, and finishes by reflexivity.
Claim. Let $H$ be a minimal discrete hierarchy (a geometric scale ladder closed under the first non-trivial composition step). Then for every natural number $k$, the $k$-th scale of $H$ equals the $k$-th scale of the canonical minimal hierarchy.
background
The module UnifiedForcingChain assembles the complete inevitability chain from the cost foundation (Recognition Composition Law plus normalization and calibration) through T-1 and T0–T8. In that chain, T6 forces φ as the self-similar fixed point of the discrete ledger.
A GeometricScaleSequence is a geometric ladder with fixed ratio $r>0$, $r\neq 1$. Its $n$-th scale is the obvious power of that ratio. A MinimalHierarchy packages such a sequence together with a closure witness: the ladder is closed under the first non-trivial composition step (the Fibonacci-type relation in the hierarchy-minimality development).
The companion result minimalHierarchy_ratio_eq_phi already pins every minimal hierarchy’s ratio to φ. The present statement lifts that equality from the single ratio parameter to the entire scale sequence, matching the pre-built canonical minimal hierarchy used later in the chain.
proof idea
Introduce the rung index $k$. Unfold the definition of geometric scale (the $k$-th term is a power of the sequence ratio). Rewrite the ratio of $H$ to φ by minimalHierarchy_ratio_eq_phi. Both sides then reduce to the same power of φ, so reflexivity closes the goal. Short tactic proof: unfold, rewrite, rfl.
why it matters
This is the scale half of the canonicality certificate for minimal hierarchies. The parent theorem canonical_minimal_hierarchy_canonicality packages it with the ratio equality into a single MinimalHierarchyCanonicality record (ratio_eq and scale_eq).
In the forcing chain that is the uniqueness of the geometric ladder once minimality and φ-forcing (T6) are in place: every minimal hierarchy is the canonical φ-ladder, not merely ratio-equivalent in the abstract. Downstream structure and cosmology code that indexes rungs by scale k can therefore treat the canonical object as the unique minimal model. It does not itself force D=3 or the eight-tick octave; those sit at T7–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.