electronSetup
plain-language theorem explainer
electronSetup supplies a concrete DoubleSlitSetup record with slit separation 1 μm, screen distance 1 m and wavelength 1 nm for keV electrons. Workers deriving the double-slit pattern from 8-tick phase accumulation would cite this as the reference electron instance. The definition is a direct record literal whose three positivity fields are discharged by norm_num.
Claim. The electron double-slit setup consists of slit separation $d=10^{-6}$, screen distance $L=1$ and wavelength $λ=10^{-9}$ (in meters), each satisfying the positivity condition $>0$.
background
DoubleSlitSetup is the structure whose fields are slit separation $d$, screen distance $L$ and wavelength $λ$, together with the three positivity hypotheses $d>0$, $L>0$, $λ>0$. The module QF-012 aims to obtain the interference pattern from Recognition Science's eight-tick phase structure, where each path accumulates phases of the form $kπ/4$ for $k=0..7$ and the intensity follows from $|e^{iφ_L}+e^{iφ_R}|^2$. Upstream structures such as EightTick.phase supply the periodic phase values used in later sibling definitions.
proof idea
The definition is a one-line record construction that assigns the three numerical values and discharges the positivity hypotheses by norm_num.
why it matters
This definition supplies the concrete parameters required by the QF-012 derivation of double-slit interference from the eight-tick octave. It precedes the sibling definitions of pathPhase, phaseDifference and intensity that implement the pattern. The module targets a Foundations of Physics paper proposition on interference emerging from RS phase accumulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.