codeThreshold_pos

formal source

  30
  31noncomputable def codeThreshold (k : ℕ) : ℝ := (phi ^ k)⁻¹
  32
  33theorem codeThreshold_pos (k : ℕ) : 0 < codeThreshold k :=
  34  inv_pos.mpr (pow_pos phi_pos k)
  35
  36theorem codeThreshold_decay (k : ℕ) :
  37    codeThreshold (k + 1) / codeThreshold k = phi⁻¹ := by
  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
  43structure QECThresholdCert where
  44  five_families : Fintype.card QECCodeFamily = 5
  45  threshold_pos : ∀ k, 0 < codeThreshold k
  46  phi_decay : ∀ k, codeThreshold (k + 1) / codeThreshold k = phi⁻¹
  47
  48noncomputable def qecThresholdCert : QECThresholdCert where
  49  five_families := qecCodeFamilyCount
  50  threshold_pos := codeThreshold_pos
  51  phi_decay := codeThreshold_decay
  52
  53end IndisputableMonolith.Information.QECThresholdFromPhiLadder