theorem
proved
dalembert_cascade
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.StillnessGenerative on GitHub at line 264.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
261
262/-! ## Part VIII: The d'Alembert Cascade -/
263
264theorem dalembert_cascade (a b : ℤ) :
265 Jcost (PhiForcing.φ ^ a * PhiForcing.φ ^ b) +
266 Jcost (PhiForcing.φ ^ a / PhiForcing.φ ^ b) =
267 2 * Jcost (PhiForcing.φ ^ a) + 2 * Jcost (PhiForcing.φ ^ b) +
268 2 * Jcost (PhiForcing.φ ^ a) * Jcost (PhiForcing.φ ^ b) :=
269 dalembert_identity (zpow_pos PhiForcing.phi_pos a) (zpow_pos PhiForcing.phi_pos b)
270
271theorem phi_power_compose (a b : ℤ) :
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