phi_power_ratio

formal source

 272    PhiForcing.φ ^ a * PhiForcing.φ ^ b = PhiForcing.φ ^ (a + b) :=
 273  (zpow_add₀ PhiForcing.phi_pos.ne' a b).symm
 274
 275theorem phi_power_ratio (a b : ℤ) :
 276    PhiForcing.φ ^ a / PhiForcing.φ ^ b = PhiForcing.φ ^ (a - b) := by
 277  rw [div_eq_mul_inv, ← zpow_neg, ← zpow_add₀ PhiForcing.phi_pos.ne', sub_eq_add_neg]
 278
 279theorem ladder_cascade_bound (a b : ℤ) :
 280    Jcost (phi_ladder (a + b)) ≤
 281    2 * Jcost (phi_ladder a) + 2 * Jcost (phi_ladder b) +
 282    2 * Jcost (phi_ladder a) * Jcost (phi_ladder b) := by
 283  unfold phi_ladder
 284  rw [← phi_power_compose]
 285  exact Jcost_submult (zpow_pos PhiForcing.phi_pos a) (zpow_pos PhiForcing.phi_pos b)
 286
 287theorem doubling_cascade (n : ℤ) (_hn : n ≠ 0) :
 288    Jcost (phi_ladder (2 * n)) =
 289    2 * (Jcost (phi_ladder n)) ^ 2 + 4 * Jcost (phi_ladder n) := by
 290  unfold phi_ladder
 291  have hphi_pos := PhiForcing.phi_pos
 292  have hd := dalembert_identity (zpow_pos hphi_pos n) (zpow_pos hphi_pos n)
 293  have h_prod : PhiForcing.φ ^ n * PhiForcing.φ ^ n = PhiForcing.φ ^ (2 * n) := by
 294    rw [← zpow_add₀ hphi_pos.ne']; congr 1; ring
 295  have h_div : PhiForcing.φ ^ n / PhiForcing.φ ^ n = 1 :=
 296    div_self (zpow_pos hphi_pos n).ne'
 297  rw [h_prod, h_div, Jcost_unit0] at hd
 298  linarith [sq (Jcost (PhiForcing.φ ^ n))]
 299
 300theorem doubling_cascade_positive (n : ℤ) (hn : n ≠ 0) :
 301    0 < Jcost (phi_ladder (2 * n)) := by
 302  rw [doubling_cascade n hn]
 303  nlinarith [phi_ladder_positive_cost hn, sq_nonneg (Jcost (phi_ladder n))]
 304
 305/-! ## Part IX: Fibonacci Cascade Populates the Full Ladder (Gap C)