Amplitude
plain-language theorem explainer
Amplitude is the type alias for complex numbers that label ledger branches in the Recognition Science account of quantum states. Workers deriving the Born rule from J-cost minimization in the measurement module would cite this when formalizing superposition weights. The declaration is a one-line abbreviation with no proof obligations or additional axioms.
Claim. An amplitude is a complex number in $ℂ$.
background
The module derives the measurement postulate from ledger commitment: superposition corresponds to uncommitted entries whose branches carry amplitudes, while measurement forces commitment to the minimum-J-cost outcome. Amplitudes therefore serve as the recognition weights whose squared moduli yield probabilities. Upstream, the actualization operator A maps a configuration to its J-minimizing successor, the active-edge count A equals 1 per fundamental tick, and the continuum bridge identifies Laplacian actions on the simplicial ledger with integrated defect terms.
proof idea
Direct abbreviation that identifies Amplitude with the complex numbers ℂ; no lemmas or tactics are applied.
why it matters
The abbreviation supplies the scalar type for all downstream amplitude manipulations, including the equality of path weights to Born probabilities in C2ABridge.weight_equals_born and the non-negativity and bound results in BernsteinInequality. It anchors the ledger-based derivation of the Born rule P ∝ |ψ|² from J-cost, consistent with the Recognition Composition Law and the eight-tick octave that fixes D = 3. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.