pathPhase
plain-language theorem explainer
pathPhase computes the phase accumulated along a geometric path of length r at wavelength lambda. Quantum modelers working on double-slit patterns in Recognition Science cite it when converting path differences into phase shifts for interference. The definition is a direct algebraic expression implementing the standard wave relation without lemmas or tactics.
Claim. The phase accumulated along a path of length $r$ with wavelength $lambda$ is given by $phi = 2 pi r / lambda$.
background
The DoubleSlit module derives interference from Recognition Science's 8-tick phase accumulation on two paths. Each path length is converted to a phase that enters the complex amplitude sum, producing the cosine dependence on path difference. The lambda parameter is supplied by RGTransport.lambda, defined as the natural log of the golden ratio phi.
proof idea
The definition is a direct one-line algebraic expression that applies real multiplication and division to 2 * pi * r / lambda. No upstream lemmas are invoked beyond the arithmetic operations on reals.
why it matters
pathPhase is invoked inside amplitude to build the sum of complex exponentials from the two slit paths. It fills the QF-012 target of obtaining the double-slit pattern from the 8-tick phase structure. In the framework it instantiates the T7 eight-tick octave for quantum path phases and supports the downstream intensity and fringe-spacing calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.