UniformScaleLadder
plain-language theorem explainer
UniformScaleLadder encodes a geometric sequence of positive reals with common ratio σ > 1 obeying the recurrence levels(k+1) = σ · levels(k). Researchers deriving φ from minimal recurrences on zero-parameter ladders cite this structure as the uniform input type. The declaration is a direct structure definition that packages the no-free-scale condition into five explicit fields.
Claim. A uniform scale ladder is a function $levels : ℕ → ℝ$ such that $levels(k) > 0$ for every natural number $k$, together with a real number $σ > 1$ satisfying $levels(k+1) = σ · levels(k)$ for all $k$.
background
The Hierarchy Emergence module proves that a zero-parameter comparison ledger with multilevel composition produces a minimal hierarchy and forces φ as the unique admissible scale. The argument begins by extracting a scale ladder from composition: positive level sizes related by a single ratio. The no-free-scale theorem states that differing adjacent ratios would each introduce an independent free real parameter, so uniformity is required.
proof idea
Structure definition. The five fields are asserted directly: the levels map, its positivity predicate, the ratio value, the strict inequality ratio > 1, and the uniform scaling equation. No lemmas or tactics are invoked.
why it matters
UniformScaleLadder is the common input to bridge_T5_T6, minimal_recurrence_forces_golden_equation, hierarchy_emergence_forces_phi and ledger_forces_phi. It realizes the second step of the module outline: no free scale data forces a uniform ratio. This supplies the uniform ladder required for the T6 landmark in which φ emerges as the self-similar fixed point of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.