doubling_cascade

formal source

 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)
 306
 307The Fibonacci recurrence φ² = φ + 1 means that adjacent φ-rungs compose
 308into the next rung. This is NOT merely a cost bound — it is a structural
 309identity that forces the ledger to POPULATE successive rungs.
 310
 311Key identity: φ^n + φ^{n+1} = φ^n(1 + φ) = φ^n · φ² = φ^{n+2}
 312
 313Starting from rungs 0 and 1 (which must exist by T4 + T6), the Fibonacci
 314recurrence generates all non-negative rungs. Ledger symmetry J(x) = J(1/x)
 315gives negative rungs. -/
 316
 317/-- **Fibonacci Cascade Identity**: φ^n + φ^{n+1} = φ^{n+2}.