measurementBasisCount

formal source

  26  | position | momentum | spin | energy | angularMomentum
  27  deriving DecidableEq, Repr, BEq, Fintype
  28
  29theorem measurementBasisCount : Fintype.card MeasurementBasis = 5 := by decide
  30
  31/-- Before measurement: superposition has positive recognition cost. -/
  32theorem superposition_has_cost {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  33    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  34
  35/-- After measurement: definite outcome = J = 0. -/
  36theorem measurement_outcome_equilibrium : Jcost 1 = 0 := Jcost_unit0
  37
  38structure WaveFunctionCollapseCert where
  39  five_bases : Fintype.card MeasurementBasis = 5
  40  superposition_cost : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  41  measurement_equilibrium : Jcost 1 = 0
  42
  43def waveFunctionCollapseCert : WaveFunctionCollapseCert where
  44  five_bases := measurementBasisCount
  45  superposition_cost := superposition_has_cost
  46  measurement_equilibrium := measurement_outcome_equilibrium
  47
  48end IndisputableMonolith.Physics.WaveFunctionCollapseFromJCost