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

phi_cost_fixed_point

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  69theorem phi_cost_fixed_point : phi = 1 + 1 / phi := by

proof body

Term-mode proof.

  70  have hsq := phi_sq_eq
  71  have hne := phi_ne_zero
  72  field_simp at hsq ⊢; linarith
  73
  74/-! ## The φ-Harmonic Theorem -/
  75
  76/-- For any positive frequency f, the first φ-harmonic is f × φ.
  77    This is the minimal-cost non-trivial resonance above f.
  78
  79    The forcing chain:
  80    1. J(r) is the cost of ratio r (from T5)
  81    2. Self-similar ratios (r² = r + 1) are the scale-invariant resonances
  82    3. φ is the unique positive self-similar ratio (from T6)
  83    4. Therefore f × φ is the unique first φ-harmonic of f -/

depends on (19)

Lean names referenced from this declaration's body.