probability
plain-language theorem explainer
probability defines the Born probability of ledger configuration i inside a normalized quantum state superposition. Audit and complexity modules cite it when bounding coincidence probabilities or resolution times on the phi-ladder. The definition is a one-line wrapper extracting the squared modulus of the selected amplitude.
Claim. Let $n$ be a natural number and let $ψ$ be a quantum state over $n$ ledger configurations with complex amplitudes $ψ_i$. The probability of configuration $i$ is $|ψ_i|^2$.
background
QuantumState is the structure whose fields are a map from Fin n to Ledger configurations, a map from Fin n to complex amplitudes, and the normalization condition that the sum of Complex.normSq over all amplitudes equals 1. The module identifies quantum states with superpositions of ledger entries so that the Born rule can be recovered from J-cost minimization rather than postulated. Upstream QuantumState structures in NoCloning, Unitarity and WavefunctionCollapse supply the same normalized-amplitude pattern in different physical contexts.
proof idea
one-line wrapper that applies Complex.normSq to the amplitude component at index i.
why it matters
The definition supplies the explicit Born rule inside the quantum ledger, which is invoked by printProbability, CoincidenceBound and ResolutionTime. It realizes the module claim that the Born rule emerges from cost minimization and therefore sits between the ledger forcing chain and the later audit of RS constants. No open scaffolding is attached to this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.