SMatrix
plain-language theorem explainer
The SMatrix structure packages an n by n complex matrix with the built-in condition that its conjugate transpose times itself equals the identity matrix. Researchers deriving scattering amplitudes and probability conservation from Recognition Science ledger balance would cite this as the carrier for finite-dimensional transition operators. The definition imposes unitarity directly as a structural field, supplying the axiom for all module theorems on conserved probabilities.
Claim. A structure consisting of an $n$ by $n$ complex matrix $S$ together with the axiom $S^dagger S = I_n$, where the entries of $S$ give transition amplitudes between states in an $n$-dimensional Hilbert space.
background
The module QFT.SMatrixUnitarity targets derivation of S-matrix unitarity from Recognition Science ledger conservation, in which every recognition event preserves total J-cost through balanced double-entry accounting. The S-matrix encodes the map from initial states at $t to -infty$ to final states at $t to +infty$, with unitarity enforcing that no probability is lost. Upstream results supply the relativistic action $S[g, psi; C_lag, alpha] := S_EH[g] + S_psi[g,psi]$ (ILG.Action.S) and the foundational reductions from seven axioms to four structural conditions (PrimitiveDistinction.from) plus meta-realization certificates (UniversalForcingSelfReference.for).
proof idea
This is a structure definition that directly bundles the matrix field with the unitary field enforcing matrix.conjTranspose * matrix = 1. No lemmas or tactics are invoked; the unitarity condition is taken as the defining property.
why it matters
SMatrix is the root declaration feeding amplitude, probability, s_inverse, probability_conserved, optical_theorem_from_unitarity, and unitarity_means_probability_conserved. It supplies the formal object for the QFT-012 paper proposition that ledger conservation forces S dagger S = I, thereby linking Recognition Science conservation laws to standard QFT probability preservation. The structure leaves open the extension to infinite-dimensional Hilbert spaces required for full continuum QFT.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.