module module high

`IndisputableMonolith.Quantum.DoubleSlit`

This module supplies the parameter definitions for modeling a double-slit interference experiment inside the Recognition Science framework. It introduces setup objects, path phases, amplitude, and intensity expressions that produce the expected oscillatory fringes. Quantum physicists exploring RS-native derivations of interference would cite these definitions. The module consists entirely of definitions with no theorems or proofs.

claimParameters for the double-slit experiment: setup configuration, path lengths $L_1$ and $L_2$, phase difference along each path, amplitude $A$, and intensity $I$ that oscillates with fringe spacing determined by wavelength in RS units.

background

The module resides in the Quantum domain and imports only the Constants module, whose sole documented content is the fundamental RS time quantum defined by τ₀ = 1 tick. It introduces a collection of sibling definitions (DoubleSlitSetup, electronSetup, pathPhase, pathLength1, pathLength2, pathDifference, phaseDifference, amplitude, intensity, intensity_oscillates, max_intensity, fringeSpacing) that together encode the geometry and wave-like quantities needed for interference calculations. The local theoretical setting is the standard double-slit configuration expressed in RS-native units, where phase accumulation follows from the J-cost or phi-ladder structure already present in the imported constants.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete parameter layer required to embed the double-slit experiment inside the Recognition Science forcing chain (T0–T8) and Recognition Composition Law. It prepares the ground for later derivations of intensity patterns and fringe spacing that would follow from the eight-tick octave and D = 3 spatial dimensions. No downstream theorems are recorded yet, but the definitions directly support the framework’s program of recovering quantum interference from the single functional equation.

scope and limits

Does not derive the intensity formula from the J-cost functional equation.
Does not include numerical evaluation for specific slit separations or screen distances.
Does not address which-path information or decoherence mechanisms.
Does not generalize to multi-slit or multi-particle interference.

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