phi_ladder

formal source

  41
  42/-! ## Part I: The φ-Ladder -/
  43
  44noncomputable def phi_ladder (n : ℤ) : ℝ := PhiForcing.φ ^ n
  45
  46theorem phi_ladder_pos (n : ℤ) : 0 < phi_ladder n :=
  47  zpow_pos PhiForcing.phi_pos n
  48
  49theorem phi_zpow_ne_one {n : ℤ} (hn : n ≠ 0) : PhiForcing.φ ^ n ≠ 1 := by
  50  have hφ_gt := PhiForcing.phi_gt_one
  51  intro heq
  52  have h0 : PhiForcing.φ ^ (0 : ℤ) = 1 := zpow_zero _
  53  have hmono : StrictMono fun m : ℤ => PhiForcing.φ ^ m :=
  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