experimentalStatus
plain-language theorem explainer
The definition experimentalStatus assembles a list of three candidate S-matrix unitarity violations, each pairing a violation type with its observable signature and current experimental status. A physicist deriving unitarity from ledger conservation would cite the list to document that no violations appear in data. The construction is a direct record list with no lemmas or reductions.
Claim. The experimental status of S-matrix unitarity is the list of falsifiers consisting of (violation type ``Probability non-conservation'', signature ``Missing energy/momentum'', status ``Never observed''), (violation type ``Information loss'', signature ``Non-unitary evolution'', status ``Never observed''), and (violation type ``Optical theorem violation'', signature ``Cross-section mismatch'', status ``Verified to high precision'').
background
The QFT module derives S-matrix unitarity from Recognition Science ledger conservation, where balanced double-entry J-cost entries force probability conservation and thus S†S = 1. The sibling structure UnitarityFalsifier records a violation type, its manifestation signature, and observational status; the module doc states that no unitarity violation has ever been observed. Upstream results supply the identical structure definition from the same module and a related falsifier structure from the Unitarity module whose fields encode non-unitary evolution or information loss as conditions that would falsify the derivation.
proof idea
The definition constructs the list of three UnitarityFalsifier records by supplying their three fields inline for each entry. No lemmas are invoked and no tactics are used; it is a pure data definition.
why it matters
This definition supports the module target of deriving S-matrix unitarity from ledger conservation by cataloging the empirical absence of violations. It aligns with Recognition Science landmarks that probability conservation follows from J-cost balance on the phi-ladder. No parent theorems appear in the used-by graph, and the entry touches the empirical closure of the unitarity argument without addressing open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.