UnitarityFalsifier
plain-language theorem explainer
This structure encodes the logical conditions under which the Recognition Science derivation of quantum unitarity from ledger conservation would fail. Physicists testing information preservation in quantum evolution would reference it when assessing experimental constraints. It is introduced as a record type packaging three propositions and an implication that derives a contradiction from non-unitary observation or information loss.
Claim. A falsifier for unitarity consists of propositions $P$ (non-unitary quantum evolution observed), $Q$ (fundamental information loss), $R$ (ledger conservation violated), together with the implication $(P ∨ Q) → ⊥$.
background
The module derives quantum unitarity from ledger conservation, where the ledger acts as a conserved quantity that prevents information creation or destruction and thereby enforces probability conservation. This builds directly on the upstream S-matrix unitarity falsifier, whose doc-comment states: 'S-matrix unitarity would be falsified by: 1. Probability not conserved in scattering 2. Information loss in particle collisions 3. Time-asymmetric scattering amplitudes 4. Violation of optical theorem.' The local theoretical setting is QFT-009, which targets derivation of the evolution operator satisfying $U^†U = UU^† = I$ from ledger principles.
proof idea
This is a structure definition with no proof body. It directly encodes the falsification conditions as named fields in a record type, with the implication field capturing the logical contradiction.
why it matters
The structure feeds the experimentalStatus definition, which populates a list of concrete violation types all marked 'Never observed' or 'Verified to high precision.' It fills the paper proposition on information conservation as the origin of unitarity. Within the Recognition framework it closes the ledger-to-unitarity step, consistent with reversibility from the eight-tick octave and information preservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.