DoubleSlitSetup
The structure packages geometric and wavelength parameters for modeling double-slit interference via eight-tick phase accumulation in Recognition Science. Researchers deriving fringe patterns from path-length differences would cite it as the common input type. As a pure structure definition it carries no proof body and directly supplies the fields required by the amplitude and intensity calculations that follow.
claimA structure consisting of positive real numbers $d$, $L$, and $λ$ (slit separation, screen distance, and wavelength) together with the three positivity assertions $d>0$, $L>0$, $λ>0$.
background
The module develops double-slit interference from Recognition Science's eight-tick phase structure. Two paths accumulate phases whose difference yields the intensity $I(y) = 4cos²(Δφ/2)$, recovering the standard bright and dark fringes with spacing $Δy = λL/d$ (T7 eight-tick octave). The structure supplies the three positive real inputs needed to define path lengths and phase differences in that derivation.
proof idea
This is a structure definition with no proof body; it simply declares the three fields and their positivity constraints.
why it matters in Recognition Science
It is the common parameter type for the amplitude definition, intensity function, fringe-spacing definition, and the bright-fringes and dark-fringes theorems in the same module. The module documentation states the target as deriving interference from eight-tick phase accumulation (QF-012), thereby linking the eight-tick octave (T7) to an observable quantum pattern inside the Recognition Science framework.
scope and limits
- Does not derive phase values or intensity formulas.
- Does not assign numerical values to the parameters.
- Does not incorporate J-cost, defect distance, or phi-ladder rungs.
- Does not address particle statistics or relativistic corrections.
formal statement (Lean)
46structure DoubleSlitSetup where
47 /-- Slit separation (meters). -/
48 d : ℝ
49 /-- Distance to screen (meters). -/
50 L : ℝ
51 /-- Wavelength of particle (meters). -/
52 lambda : ℝ
53 /-- All positive. -/
54 d_pos : d > 0
55 L_pos : L > 0
56 lambda_pos : lambda > 0
57
58/-- A standard setup for electrons. -/