probability
plain-language theorem explainer
The declaration defines the transition probability between states i and j for an S-matrix as the squared modulus of the corresponding amplitude entry. Scattering theorists working in Recognition Science QFT cite it when connecting ledger conservation to Born-rule outcomes in scattering. It is a direct one-line extraction of the modulus squared.
Claim. For an S-matrix $S$ on an $n$-dimensional space, the transition probability from state $i$ to state $j$ is the square of the modulus of the amplitude entry connecting those states.
background
The module derives S-matrix unitarity from Recognition Science ledger conservation, where the S-matrix relates initial and final states via $|final⟩ = S|initial⟩$ and unitarity encodes probability conservation. The referenced SMatrix structure consists of an $n$ by $n$ complex matrix together with the condition that its conjugate transpose times itself equals the identity. This probability definition parallels the Born-rule extraction in QuantumLedger.probability, which computes the squared norm of amplitudes for a quantum state configuration.
proof idea
One-line definition that applies the squared modulus operator to the amplitude entry of the S-matrix.
why it matters
This definition supplies the probability interpretation required for the unitarity theorems and conservation statements in the module. It realizes the core mechanism that ledger balance preservation forces probability conservation, as stated in the module's target of deriving unitarity from ledger structure. It supports downstream audit structures that verify consistency of constants and coincidence bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.