module module high

`IndisputableMonolith.QFT.SMatrixUnitarity`

This module encodes the S-matrix as a unitary operator on finite-dimensional Hilbert space within Recognition Science. Researchers deriving scattering amplitudes or probability conservation from the J-cost would cite it. The module consists of interconnected definitions for amplitudes, probabilities, ledgers, and unitarity connections that feed directly into the parent QFT derivations.

claimThe S-matrix $S$ acts as a unitary operator on an $n$-dimensional Hilbert space, so that $S S^{-1} = I$ and the associated amplitude and probability maps satisfy probability conservation via the recognition cost functional.

background

The module imports the RS time quantum from Constants and the J-cost functional from Cost. It defines SMatrix together with amplitude, probability, s_inverse, and ScatteringLedger objects that track cost conservation under scattering. These sit inside the QFT tier of Recognition Science, where the Recognition Composition Law and phi-ladder supply the underlying algebraic structure for unitarity.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the unitarity foundation required by the parent QFT module, which collects Tier 2 derivations of quantum field theory from Recognition Science. It directly enables downstream results such as opticalTheoremFormula and informationPreservation by establishing ledger_cost_conserved and unitarity_means_probability_conserved.

scope and limits

Does not derive the explicit matrix elements of S from the forcing chain T0-T8.
Does not treat infinite-dimensional Hilbert spaces or continuous spectra.
Does not compute numerical cross-sections or phase shifts.
Does not address renormalization or loop corrections.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.QFT module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (17)

structure SMatrix L50
def amplitude L57
def probability L60
theorem s_inverse L70
theorem probability_conserved L86
structure ScatteringEntry L114
structure ScatteringLedger L125
theorem ledger_cost_conserved L135
def ledgerUnitarityConnection L143
theorem unitarity_means_probability_conserved L148
def informationPreservation L154
def opticalTheoremFormula L162
theorem optical_theorem_from_unitarity L168
theorem cpt_s_matrix L179
theorem crossing_symmetry L189
structure UnitarityFalsifier L201
def experimentalStatus L210