amplitude
plain-language theorem explainer
The amplitude at screen position y sums the complex phases from the two slit paths in a DoubleSlitSetup. Quantum and cosmology researchers cite it when deriving interference from eight-tick phase accumulation. The definition builds the sum directly via local phase variables computed from path lengths and the wavelength parameter.
Claim. For setup parameters $d>0$, $L>0$, and wavelength $λ>0$, the amplitude at position $y$ is $A(y)=e^{iφ_1}+e^{iφ_2}$, where $φ_1$ and $φ_2$ are the phases accumulated along each path.
background
The module derives double-slit interference from Recognition Science's eight-tick phase structure. Each path accumulates phase via the wavelength, and the difference produces the observed fringes. DoubleSlitSetup supplies the geometric parameters $d$, $L$, and $λ$ together with positivity proofs. Upstream, lambda is defined as $ln(φ)$ in RGTransport, while A denotes the active-edge count per tick in IntegrationGap and related modules.
proof idea
The definition is a direct construction. It binds φ1 to pathPhase applied to pathLength1 and the setup lambda, binds φ2 similarly for the second path, then returns the sum of the two complex exponentials.
why it matters
This definition supplies the amplitude used by amplitude_derivation and fluctuations_from_jcost in Cosmology.PrimordialSpectrum. It realizes the eight-tick phase accumulation (T7) inside the quantum ledger, providing the concrete map from path geometry to the complex sum that later enters power-spectrum calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.