module module moderate

`IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse`

The module defines quantum amplitudes as complex numbers along with states, superposition checks, and measurement probabilities for wavefunction collapse modeling in Recognition Science. Researchers working on quantum measurement within the RS framework would cite it. The module structures these definitions around the imported 8-tick discretization hypothesis and RS time quantum without proofs.

claimAn amplitude is a complex number $A$. The module introduces quantum states, predicates for superposition and definiteness, ledger branches for committed and uncommitted states, and a measurement probability function built on the 8-tick cycle.

background

The module operates in the quantum domain of Recognition Science, which derives all physics from a single functional equation and the T0-T8 forcing chain. It imports the fundamental RS time quantum τ₀ = 1 tick from Constants and the explicit 8-tick hypothesis from EightTick, which states that time and process are discretized into 8-beat cycles as a testable hypothesis about observed traces rather than a definitional axiom.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the quantum measurement interface that connects the 8-tick hypothesis to wavefunction concepts, providing definitions that would feed higher-level results on collapse and measurement in the Recognition Science framework. It supports the quantum domain by organizing amplitudes, states, and probabilities around the imported constants and discretization.

scope and limits

Does not derive the 8-tick hypothesis from the forcing chain.
Does not simulate or predict specific collapse dynamics.
Does not link amplitudes to mass formulas or the phi-ladder.
Does not prove any theorem on measurement outcomes.

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