lemma proved term proof

`phi_pow_strictMono`

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

formal statement (Lean)

  65lemma phi_pow_strictMono {m n : ℕ} (hmn : m < n) : phi ^ m < phi ^ n := by

Term-mode proof.

  66  have hphi_pos : 0 < phi := phi_pos
  67  exact pow_lt_pow_right₀ one_lt_phi hmn
  68
  69/-- **J(φ^m) < J(φ^n) FOR m < n**. -/

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

Jcost_phi_pow_strictMono in IndisputableMonolith.Papers.GCIC.LocalCacheForcing decl_use

Lean names referenced from this declaration's body.