pith. machine review for the scientific record. sign in
structure definition def or abbrev high

UniformScaleLadder

show as:
view Lean formalization →

A uniform scale ladder is a sequence of positive real numbers whose adjacent terms differ by a fixed ratio greater than one. Researchers deriving the golden ratio from zero-parameter ledgers cite this structure as the starting object for the no-free-scale argument. The definition is a direct structure whose four fields enforce positivity, the ratio bound, and the uniform multiplicative recurrence.

claimA structure consisting of a function $levels : ℕ → ℝ$, a real number $ratio$, such that $levels(k) > 0$ for every natural number $k$, $ratio > 1$, and $levels(k+1) = ratio · levels(k)$ for every $k$.

background

The module Hierarchy Emergence from Zero-Parameter Scale Closure proves that a zero-parameter comparison ledger with multilevel composition produces a minimal hierarchy and forces φ as the unique admissible scale. The argument proceeds in four steps: multilevel composition induces a scale ladder; absence of free scale parameters forces a uniform ratio; locality forces a finite-order recurrence on level sizes; minimal nondegenerate closure forces the Fibonacci recurrence $L_{k+2} = L_{k+1} + L_k$, hence $σ² = σ + 1$ and $σ = φ$. A scale ladder is the sequence of positive level sizes with uniform scaling ratio extracted from multilevel composition.

proof idea

This is a direct structure definition with no proof body. The fields levels, levels_pos, ratio, ratio_gt_one, and uniform_scaling encode the required positivity, ratio bound, and uniform scaling relation.

why it matters in Recognition Science

UniformScaleLadder is the input type for the parent theorems bridge_T5_T6, minimal_recurrence_forces_golden_equation, hierarchy_emergence_forces_phi, and ledger_forces_phi. These theorems complete the first two steps of the module argument and connect directly to the T5 J-uniqueness and T6 phi-forcing steps of the unified forcing chain. The structure therefore supplies the concrete object on which the zero-parameter ledger forces the golden ratio.

scope and limits

formal statement (Lean)

  36structure UniformScaleLadder where
  37  levels : ℕ → ℝ
  38  levels_pos : ∀ k, 0 < levels k
  39  ratio : ℝ
  40  ratio_gt_one : 1 < ratio
  41  uniform_scaling : ∀ k, levels (k + 1) = ratio * levels k
  42
  43/-- **No-free-scale theorem**: In a zero-parameter ledger, if
  44adjacent level ratios could differ, each independent ratio would
  45constitute a free real parameter.  Therefore all adjacent ratios
  46must be equal, giving a uniform scale ladder. -/

used by (13)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.