module module moderate

`IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse`

This module introduces definitions for quantum amplitudes, states, and measurement structures in the Recognition Science framework. It equips the quantum domain with ledger-based representations of superposition and collapse using the imported 8-tick discretization. Researchers modeling quantum processes within RS would cite it for the basic interface to amplitudes and committed ledgers. The module is purely definitional with no theorems or proofs.

claimAmplitude is a complex number $z \in \mathbb{C}$. QuantumState, isSuperposition, isDefinite, LedgerBranch, UncommittedLedger, and CommittedLedger organize superpositions and measurement outcomes. measurementProbability computes outcome weights from ledger branches.

background

The module sits in the quantum domain and imports the RS time quantum $ au_0 = 1$ tick together with the explicit 8-tick discretization hypothesis. The latter states that time and process are discretized into 8-beat cycles and supplies a testing interface rather than an axiom.

Core objects are introduced via sibling declarations: Amplitude as a complex number, QuantumState as a ledger representation, predicates isSuperposition and isDefinite, and the three ledger types (LedgerBranch, UncommittedLedger, CommittedLedger) that track uncommitted versus committed measurement branches. Helper lemmas such as sum_filter_eq_sum_all and filter_map_weight_sum support summation over filtered states.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the base objects required for any later treatment of wavefunction collapse and measurement probabilities inside Recognition Science. It directly incorporates the eight-tick octave (T7) via the EightTick import and the fundamental time quantum from Constants. No downstream theorems are recorded yet, indicating the module is an early scaffolding layer for the quantum measurement development.

scope and limits

Does not contain dynamical equations for collapse.
Does not derive the Born rule or measurement probabilities from RCL.
Does not connect amplitudes to the phi-ladder or mass formulas.
Does not prove uniqueness or invariance properties of states.

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