destructive_interference
plain-language theorem explainer
Destructive interference holds for two possibility paths when their amplitude is negative at phase differences of odd multiples of pi. Modal geometry researchers in Recognition Science cite it to mark path cancellation in possibility spaces. The definition is a direct encoding that applies the existing interference_amplitude function to the odd-pi condition.
Claim. Two paths $p_1, p_2$ in configuration space exhibit destructive interference when there exists an integer $n$ such that the interference amplitude $I(p_1, p_2, (2n+1)π) < 0$.
background
In ModalGeometry, a Config is a point in recognition state space carrying a positive real value and a time coordinate in ticks, per Possibility.Config. Interference amplitude between paths is defined as the square root of the product of their path weights times the cosine of the supplied phase difference. Upstream, EightTick.phase supplies the discrete 8-tick phases $kπ/4$ for $k=0..7$, while RiemannHypothesis.Wedge.phase supplies the complex exponential form $e^{iw}$. The module develops modal notions of possibility and actualization using these phase and amplitude primitives.
proof idea
This is a direct definition. It invokes interference_amplitude on the two paths at the concrete phase $(2n+1)π$ for integer $n$ and asserts the resulting real value is negative.
why it matters
The definition pairs with the constructive-interference case already present in the same module and supplies the cancellation condition needed for modal path analysis. It draws on the eight-tick phase structure (T7) and the amplitude formula that encodes overlap via path weights. No downstream theorems yet reference it, so its integration into actualization or curvature results remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.