module module

`IndisputableMonolith.QFT.SMatrixUnitarity`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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