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

coherenceDecay

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)

  34theorem coherenceDecay (k : ℕ) :
  35    coherenceAtRung (k + 1) / coherenceAtRung k = phi⁻¹ := by

proof body

Term-mode proof.

  36  unfold coherenceAtRung
  37  have hphi_ne := phi_ne_zero
  38  have hpos : 0 < phi ^ (-(k : ℤ)) := zpow_pos phi_pos _
  39  rw [show ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 from by push_cast; ring]
  40  rw [show -((k : ℤ) + 1) = -(k : ℤ) + (-1 : ℤ) from by ring]
  41  rw [zpow_add₀ hphi_ne]
  42  field_simp [hpos.ne']
  43

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.