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

ladder_cascade_bound

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)

 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

proof body

Term-mode proof.

 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

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.