electronSetup
ElectronSetup supplies concrete numerical values for a double-slit experiment using electrons, with slit separation 1 micrometer, screen distance 1 meter, and wavelength 1 nanometer. Researchers deriving quantum interference patterns from Recognition Science's eight-tick phase structure would reference this instance when instantiating the general parameter record. The definition is a direct record construction that discharges the three positivity conditions via norm_num.
claimThe electron setup is the record with slit separation $d = 10^{-6}$ m, screen distance $L = 1$ m, wavelength $lambda = 10^{-9}$ m, together with proofs that each parameter is positive.
background
DoubleSlitSetup is the structure holding three real parameters for a double-slit experiment: slit separation d, distance to screen L, and particle wavelength lambda, each required to be positive. The module derives the interference pattern from Recognition Science's eight-tick phase accumulation, where each path accumulates phases of the form k pi / 4 for k in 0 to 7. Upstream results include the phase definition from EightTick, the J-cost structure from PhiForcingDerived, and the ledger factorization from DAlembert.
proof idea
The definition constructs the DoubleSlitSetup record by supplying the three numerical values and discharging the positivity hypotheses d_pos, L_pos, and lambda_pos via the norm_num tactic.
why it matters in Recognition Science
This definition supplies a concrete electron instance inside the double-slit module whose goal is to obtain interference from the eight-tick phase (T7 of the forcing chain). It supports subsequent sibling definitions that compute path phases, phase differences, and intensity oscillations. The module itself targets the paper proposition on interference from RS phase structure.
scope and limits
- Does not derive the numerical values from Recognition Science axioms.
- Does not compute the resulting interference pattern or fringe spacing.
- Does not generalize the setup to other particles or wavelengths.
- Does not incorporate relativistic or quantum-field corrections.
formal statement (Lean)
59noncomputable def electronSetup : DoubleSlitSetup := {
proof body
Definition body.
60 d := 1e-6, -- 1 μm slit separation
61 L := 1, -- 1 m to screen
62 lambda := 1e-9, -- ~1 nm wavelength (for keV electrons)
63 d_pos := by norm_num,
64 L_pos := by norm_num,
65 lambda_pos := by norm_num
66}
67
68/-! ## Path Phases -/
69
70/-- The phase accumulated along a path of length r.
71 φ = 2π × r / λ = k × r (where k = 2π/λ) -/