phi_ladder_ne_one

formal source

  54    zpow_right_strictMono₀ hφ_gt
  55  exact hn (hmono.injective (heq.trans h0.symm))
  56
  57theorem phi_ladder_ne_one {n : ℤ} (hn : n ≠ 0) : phi_ladder n ≠ 1 :=
  58  phi_zpow_ne_one hn
  59
  60/-! ## Part II: Positive Cost on the φ-Ladder -/
  61
  62theorem phi_ladder_positive_cost {n : ℤ} (hn : n ≠ 0) :
  63    0 < Jcost (phi_ladder n) :=
  64  Jcost_pos_of_ne_one (phi_ladder n) (phi_ladder_pos n) (phi_ladder_ne_one hn)
  65
  66theorem phi_cost_eq : LawOfExistence.J PhiForcing.φ = PhiForcing.φ - 3 / 2 :=
  67  PhiForcing.J_phi
  68
  69theorem phi_cost_pos : 0 < LawOfExistence.J PhiForcing.φ := by
  70  rw [phi_cost_eq]; linarith [PhiForcing.phi_gt_onePointSix]
  71
  72theorem phi_perturbation_bounded : LawOfExistence.J PhiForcing.φ < 1 := by
  73  rw [phi_cost_eq]; linarith [PhiForcing.phi_lt_two]
  74
  75/-! ## Part III: φ-Structure in Configurations -/
  76
  77def has_phi_structure {N : ℕ} (c : InitialCondition.Configuration N) : Prop :=
  78  ∃ i j : Fin N, ∃ n : ℤ, n ≠ 0 ∧ c.entries i / c.entries j = PhiForcing.φ ^ n
  79
  80theorem unity_has_no_phi_structure {N : ℕ} (hN : 0 < N) :
  81    ¬ has_phi_structure (InitialCondition.unity_config N hN) := by
  82  intro ⟨i, j, n, hn, hratio⟩
  83  simp only [InitialCondition.unity_config] at hratio
  84  have h_div : (1 : ℝ) / 1 = PhiForcing.φ ^ n := hratio
  85  simp at h_div
  86  exact phi_zpow_ne_one hn h_div.symm
  87