coherenceDecay

formal source

  31
  32noncomputable def coherenceAtRung (k : ℕ) : ℝ := phi ^ (-(k : ℤ))
  33
  34theorem coherenceDecay (k : ℕ) :
  35    coherenceAtRung (k + 1) / coherenceAtRung k = phi⁻¹ := by
  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
  44structure DecoherenceCert where
  45  five_mechanisms : Fintype.card DecoherenceMechanism = 5
  46  phi_decay : ∀ k, coherenceAtRung (k + 1) / coherenceAtRung k = phi⁻¹
  47
  48noncomputable def decoherenceCert : DecoherenceCert where
  49  five_mechanisms := decoherenceMechanismCount
  50  phi_decay := coherenceDecay
  51
  52end IndisputableMonolith.Physics.QuantumDecoherenceFromJCost