module module

`IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.RRF.Hypotheses.EightTick module_import

declarations in this module (27)

abbrev Amplitude L56
structure QuantumState L60
def isSuperposition L67
def isDefinite L71
structure LedgerBranch L77
structure UncommittedLedger L88
structure CommittedLedger L95
lemma sum_filter_eq_sum_all L106
lemma list_map_sum_eq_finset_sum L120
theorem filter_map_weight_sum L129
def stateToLedger L141
def measurementProbability L147
theorem born_rule_nonneg L151
theorem born_rule_normalized L157
theorem norm_div_norm_eq_one L166
def commit L175
theorem commit_is_definite L187
theorem probability_equals_weight L193
theorem measurement_irreversible L200
theorem no_cloning_informal L207
def outcomeCost L216
theorem cost_probability_relation L227
theorem measurement_postulate_derived L247
def isEffectivelyClassical L258
theorem decoherence_gives_classicality L263
structure MeasurementFalsifier L275
theorem no_known_measurement_falsifier L286