s_inverse
plain-language theorem explainer
The theorem shows that an S-matrix obeying S dagger S equals the identity also satisfies S S dagger equals the identity. Researchers deriving probability conservation from ledger balance in Recognition Science QFT models cite this to close the unitarity loop. The proof is a one-line wrapper that invokes the SMatrix unitary hypothesis and rewrites via the matrix commutativity lemma for square matrices.
Claim. Let $S$ be an $n$ by $n$ complex matrix satisfying $S^dagger S = I_n$. Then $S S^dagger = I_n$.
background
In the QFT-012 development the S-matrix maps initial ledger states at negative infinity to final states at positive infinity while preserving total J-cost. The SMatrix n structure packages an n by n complex matrix together with the hypothesis that its conjugate transpose times itself equals the identity; this hypothesis is the Recognition Science encoding of ledger conservation. Upstream results from QuantumLedger.probability supply the Born-rule interpretation of matrix elements as probabilities, while PhiForcingDerived.of and DAlembert.LedgerFactorization.of calibrate the underlying J-cost functional that forces the conservation law.
proof idea
The proof extracts the unitary hypothesis S.matrix.conjTranspose * S.matrix = 1 from the SMatrix structure, then applies the Mathlib lemma Matrix.mul_eq_one_comm to commute the factors and obtain the reverse product equal to the identity.
why it matters
This declaration supplies the missing direction required by the downstream probability_conserved theorem, which states that the sum of squared amplitudes over final states equals one for any initial state. It thereby completes the derivation of S-matrix unitarity from ledger conservation in the module, directly supporting the optical theorem and information-preservation claims. Within the Recognition framework the result reinforces the link between T5 J-uniqueness, the eight-tick octave, and D=3 spatial emergence by guaranteeing no information loss under scattering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.