pith. machine review for the scientific record. sign in
theorem proved term proof high

phi_ladder_growth

show as:
view Lean formalization →

Consecutive rungs on the φ-ladder satisfy the exact scaling ratio φ. Researchers deriving the thermal eigenvalue in the recognition lattice RG flow would cite this result. The proof reduces the ratio algebraically after confirming φ is nonzero via a direct invocation of phi_ne_zero followed by field simplification and ring normalization.

claim$φ^{n+1} / φ^n = φ$ for every natural number $n$.

background

The module establishes the thermal fixed-point operator on the recognition lattice (ℤ³ with unit cell Q₃). The φ-ladder is the unique geometric scaling sequence forced by T6 self-similarity, satisfying φ² = φ + 1. Consecutive rungs obey the Fibonacci recurrence whose characteristic polynomial λ² − λ − 1 has φ as its unique positive root, so the thermal growth rate per ladder step equals φ and the leading correlation-length exponent is ν₀ = 1/φ.

proof idea

One-line wrapper that first obtains phi^n ≠ 0 from phi_ne_zero, then applies field_simp to clear the division and ring to normalize the powers.

why it matters in Recognition Science

This supplies the direct scaling identity needed to reach the forced thermal eigenvalue y_t = φ in the derivation chain from PhiForcing (T6) through the Fibonacci cascade to ν₀ = 1/φ. It anchors the renormalization-group fixed point in the recognition lattice and feeds the thermal_eigenvalue family of results.

scope and limits

formal statement (Lean)

  71theorem phi_ladder_growth (n : ℕ) :
  72    phi ^ (n + 1) / phi ^ n = phi := by

proof body

Term-mode proof.

  73  have h : phi ^ n ≠ 0 := pow_ne_zero _ phi_ne_zero
  74  field_simp
  75  ring
  76
  77/-! ## 3. The Forced Thermal Eigenvalue -/
  78
  79/-- The thermal eigenvalue of the recognition-lattice RG fixed point.
  80
  81    **Why this value is forced:**
  82    1. The φ-ladder is the unique geometric scaling sequence in the
  83       recognition lattice (PhiForcing: r² = r + 1 ↔ r = φ).
  84    2. Consecutive rungs satisfy the Fibonacci recurrence
  85       (`fibonacci_recurrence`), whose characteristic polynomial
  86       is λ² − λ − 1.
  87    3. φ is the unique positive root of this polynomial
  88       (`fibonacci_char_poly_unique_pos_root`).
  89    4. The thermal growth rate per ladder step is therefore φ and
  90       nothing else. -/

depends on (20)

Lean names referenced from this declaration's body.