DoubleSlitFalsifier
plain-language theorem explainer
DoubleSlitFalsifier defines a record pairing a descriptive string for a potential falsifier with its status string, cataloging checks for the double-slit interference derivation in Recognition Science. Physicists testing the 8-tick phase model cite it to enumerate concrete experimental tests such as presence of interference patterns for particles. The definition is a direct structure declaration introducing two string fields with no proof obligations or computational content.
Claim. A double-slit falsifier is a pair $(f, s)$ where $f$ is a string naming a potential falsification (such as absence of interference) and $s$ is a string reporting its experimental status.
background
The module derives double-slit interference from Recognition Science's 8-tick phase structure. Two paths (left and right slits) each accumulate 8-tick phases; the phase difference depends on path length and produces intensity proportional to $2 + 2 cos(Δφ)$. Upstream structures supply supporting pieces: J-cost minimization is strictly convex with unique minimum at argument 1, spectral emergence forces SU(3)×SU(2)×U(1) gauge content together with three generations, and RS-native units fix ħ = φ^{-5}.
proof idea
The declaration is a structure definition that introduces exactly two fields, falsifier and status. No lemmas are applied and no tactics are used; it functions as a plain data type for downstream lists.
why it matters
The structure supplies the type for experimentalStatus, which records that all four listed predictions (interference pattern, which-path effect, quantum eraser, path-phase relation) are confirmed. It completes the falsification criteria for the QF-012 derivation of interference from the eight-tick octave (T7) and thereby anchors the double-slit case inside the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.