pith. machine review for the scientific record. sign in
theorem proved tactic proof

doubling_cascade

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Tactic-mode proof.

 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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.