module module high

`IndisputableMonolith.Quantum.DoubleSlit`

The DoubleSlit module supplies type definitions and functions that parameterize a double-slit experiment inside Recognition Science. It encodes geometry, path lengths, phases, amplitudes, and intensities using the RS time quantum. The module serves as a building block for quantum-domain calculations and contains only definitions.

claimDoubleSlitSetup with slit separation and wavelength in RS units; pathPhase, pathDifference, phaseDifference, amplitude, intensity as functions of geometry; intensity_oscillates, max_intensity, fringeSpacing derived from those quantities.

background

Recognition Science starts from the forcing chain (T0-T8) and the Recognition Composition Law, with the fundamental time quantum τ₀ = 1 tick supplied by the imported Constants module. The present module operates in the quantum domain and introduces concrete parameter objects for interference. Sibling declarations define DoubleSlitSetup, electronSetup, pathPhase, pathLength1, pathLength2, pathDifference, phaseDifference, amplitude, intensity, intensity_oscillates, max_intensity, and fringeSpacing.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the parameter set required for any downstream treatment of double-slit interference inside the quantum section of Recognition Science. It directly supports calculations that must remain consistent with RS-native units and the eight-tick octave.

scope and limits

Does not prove any interference formula from the Recognition Composition Law.
Does not link slit parameters to the phi-ladder or mass formula.
Does not contain numerical evaluation or comparison with measured fringe data.
Does not import or reference the J-function or defectDist.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (25)

structure DoubleSlitSetup L46
def electronSetup L59
def pathPhase L72
def pathLength1 L76
def pathLength2 L80
def pathDifference L84
def phaseDifference L89
def amplitude L96
def intensity L103
theorem intensity_oscillates L108
theorem max_intensity L112
def fringeSpacing L121
lemma neg_one_zpow_sq L127
lemma cos_int_mul_pi_sq L135
lemma cos_half_odd_mul_pi L140
theorem bright_fringes L147
theorem dark_fringes L159
theorem interference_from_8tick L179
theorem single_particle_interference L187
theorem which_path_destroys_interference L197
theorem quantum_eraser L208
def predictions L220
def experiments L232
structure DoubleSlitFalsifier L246
def experimentalStatus L253