`PhiLadder`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.PhiEmergence
domain: Foundation
line: 83 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.PhiEmergence on GitHub at line 83.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  80/-! ## The φ-Ladder -/
  81
  82/-- The φ-ladder: all stable positions are φ^n for integer n. -/
  83def PhiLadder : Set ℝ := { x | ∃ n : ℤ, x = φ^n }
  84
  85/-- φ^n is always positive for any integer n -/
  86theorem phi_pow_pos (n : ℤ) : φ^n > 0 := by
  87  exact zpow_pos phi_pos n
  88
  89/-- Adjacent rungs of the ladder have ratio φ -/
  90theorem phi_ladder_ratio (n : ℤ) : φ^(n+1) / φ^n = φ := by
  91  have h : φ ≠ 0 := ne_of_gt phi_pos
  92  have hn : φ^n ≠ 0 := zpow_ne_zero n h
  93  rw [zpow_add_one₀ h]
  94  field_simp [hn]
  95
  96/-- The ladder is closed under multiplication by φ -/
  97theorem phi_ladder_mul_closed (x : ℝ) (hx : x ∈ PhiLadder) :
  98    x * φ ∈ PhiLadder := by
  99  obtain ⟨n, rfl⟩ := hx
 100  use n + 1
 101  rw [zpow_add_one₀ (ne_of_gt phi_pos)]
 102
 103/-- The ladder is closed under division by φ -/
 104theorem phi_ladder_div_closed (x : ℝ) (hx : x ∈ PhiLadder) :
 105    x / φ ∈ PhiLadder := by
 106  obtain ⟨n, rfl⟩ := hx
 107  use n - 1
 108  rw [zpow_sub_one₀ (ne_of_gt phi_pos)]
 109  rw [div_eq_mul_inv]
 110
 111/-! ## J-cost at φ-Ladder Positions -/
 112
 113/-- J-cost formula applied to φ -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.