DoubleSlitSetup
plain-language theorem explainer
DoubleSlitSetup packages the three positive real parameters needed to specify a double-slit geometry and wavelength. Workers deriving interference from the 8-tick phase accumulation cite it as the common input type for amplitude, intensity, and fringe-spacing calculations. The declaration is a bare structure definition carrying only the positivity side-conditions.
Claim. A double-slit setup is a triple of positive reals $(d,L,λ)$ where $d$ is slit separation, $L$ is screen distance, and $λ$ is wavelength.
background
The module derives double-slit interference from Recognition Science's 8-tick phase structure: two paths accumulate phases whose difference produces the familiar $2+2cos(Δφ)$ intensity. DoubleSlitSetup supplies the geometric inputs that later definitions convert into path lengths and phases. Upstream dependencies include ledger factorization, integration gap $A=1$, and spectral emergence structures that fix the underlying tick counting and $D=3$ geometry.
proof idea
The declaration is a structure definition; no tactics or lemmas are applied.
why it matters
It is the parameter record required by every downstream result in the module (amplitude, intensity, bright_fringes, dark_fringes, fringeSpacing). The module doc positions the construction as the concrete realization of QF-012, interference from 8-tick phase, which sits inside the T7 eight-tick octave of the forcing chain. No open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.