UnitarityFalsifier
plain-language theorem explainer
The UnitarityFalsifier structure catalogs hypothetical violations of S-matrix unitarity that would arise if ledger conservation failed in Recognition Science. QFT phenomenologists testing probability conservation or information preservation in scattering would cite it when discussing experimental bounds. It is introduced as a plain record type with three string fields for violation category, observable signature, and empirical status.
Claim. A record type with three fields: violation type (a string naming the potential breach), manifestation signature (a string describing its observable form), and status (a string reporting current empirical standing), representing falsifiers such as non-conserved probability in scattering or information loss in collisions.
background
The QFT-012 module derives S-matrix unitarity from ledger conservation, where the ledger functions as a balanced double-entry system that preserves total J-cost across scattering events. Upstream results include RSNativeUnits.status, which fixes native units with c = 1, ħ = φ^{-5}, and the φ-ladder, and LedgerFactorization.of, which structures the positive reals under multiplication together with J calibration. PhiForcingDerived.of supplies the underlying J-cost definition used in the conservation argument.
proof idea
This is a structure definition that directly introduces the three-field record type. No lemmas are applied and no tactics are used; the declaration simply records the documented fields for violation, signature, and status.
why it matters
The definition feeds experimentalStatus in the same module, which instantiates concrete cases such as probability non-conservation and optical-theorem mismatch, all marked never observed. It supports the module target of deriving unitarity from ledger conservation (PRD paper proposition) and connects to the downstream UnitarityFalsifier in QFT.Unitarity that encodes the logical negation of non-unitary evolution or ledger violation. It touches the open question of whether ledger balance holds exactly for all high-energy scattering processes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.