structure
definition
WaveFunctionCollapseCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.WaveFunctionCollapseFromJCost on GitHub at line 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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