`ScatteringEntry`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.SMatrixUnitarity
domain: QFT
line: 114 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.QFT.SMatrixUnitarity on GitHub at line 114.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 111/-! ## Ledger Model of Scattering -/
 112
 113/-- A ledger entry representing a particle state. -/
 114structure ScatteringEntry where
 115  /-- Particle type (index). -/
 116  particleType : ℕ
 117  /-- Momentum. -/
 118  momentum : ℝ
 119  /-- The J-cost of this entry. -/
 120  cost : ℝ
 121  /-- Cost is non-negative. -/
 122  cost_nonneg : cost ≥ 0
 123
 124/-- A scattering ledger with initial and final states. -/
 125structure ScatteringLedger where
 126  /-- Initial state entries. -/
 127  initial : List ScatteringEntry
 128  /-- Final state entries. -/
 129  final : List ScatteringEntry
 130  /-- Total cost is conserved. -/
 131  cost_conserved : (initial.map ScatteringEntry.cost).sum =
 132                   (final.map ScatteringEntry.cost).sum
 133
 134/-- **THEOREM (Ledger Conservation)**: The total J-cost is preserved in scattering. -/
 135theorem ledger_cost_conserved (L : ScatteringLedger) :
 136    (L.initial.map ScatteringEntry.cost).sum = (L.final.map ScatteringEntry.cost).sum :=
 137  L.cost_conserved
 138
 139/-! ## Connecting Ledger to Unitarity -/
 140
 141/-- The key insight: ledger conservation IS unitarity.
 142    The ledger's double-entry structure forces probability conservation. -/
 143def ledgerUnitarityConnection : String :=
 144  "Ledger cost balance ⟺ Probability normalization ⟺ S†S = I"

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.