structure
definition
DecoherenceCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QuantumDecoherenceFromJCost on GitHub at line 44.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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