experimentalStatus
plain-language theorem explainer
The declaration supplies a four-element list of double-slit falsifiers, each paired with its observed experimental status. A physicist checking the Recognition Science account of interference would cite the list to record that the 8-tick phase model matches all listed outcomes. The definition is a direct enumeration of string pairs with no further reduction or lemma application.
Claim. The experimental status is the list of pairs (``Interference pattern'', ``Observed for all particles''), (``Which-path effect'', ``Confirmed''), (``Quantum eraser'', ``Confirmed''), (``Path-phase relation'', ``Confirmed'').
background
The module QF-012 derives double-slit interference from the 8-tick phase structure of Recognition Science. Two paths accumulate phases from the eight-tick cycle; their difference produces the intensity pattern via the standard cosine term. DoubleSlitFalsifier is the structure that records a potential falsifier together with its status string. Upstream results supply the phase values kπ/4 for k in Fin 8 and the universal forcing self-reference axioms that underwrite the phase coherence.
proof idea
The definition is a direct list literal that enumerates the four verified statuses for the double-slit falsifiers.
why it matters
This definition closes the double-slit module by asserting that every listed prediction of the 8-tick phase model has been confirmed. It therefore supports the module claim that interference arises from phase accumulation over the eight-tick octave (T7). No downstream declarations depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.