theorem proved term proof

`codeThreshold_decay`

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

formal statement (Lean)

  36theorem codeThreshold_decay (k : ℕ) :
  37    codeThreshold (k + 1) / codeThreshold k = phi⁻¹ := by

Term-mode proof.

  38  unfold codeThreshold
  39  have hk := (pow_pos phi_pos k).ne'
  40  rw [pow_succ, mul_inv]
  41  field_simp [hk, phi_ne_zero]
  42

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

qecThresholdCert in IndisputableMonolith.Information.QECThresholdFromPhiLadder decl_use

Lean names referenced from this declaration's body.

phi_ne_zero in IndisputableMonolith.Constants decl_use
codeThreshold in IndisputableMonolith.Information.QECThresholdFromPhiLadder decl_use
phi_ne_zero in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
phi_ne_zero in IndisputableMonolith.PhiSupport.Lemmas decl_use