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

Jcost_phiLadder_symm

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)

 161theorem Jcost_phiLadder_symm (n : ℤ) :
 162    Jcost (PhiLadder n) = Jcost (PhiLadder (-n)) := by

proof body

Term-mode proof.

 163  simp only [PhiLadder, zpow_neg]
 164  exact Jcost_symm (zpow_pos Constants.phi_pos n)
 165
 166/-- **φⁿ ≥ φ for n ≥ 1**: the ladder climbs above φ for positive rungs. -/

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.