interference_amplitude
plain-language theorem explainer
Modal geometry defines the interference amplitude between two possibility paths as the square root of the product of their weights multiplied by the cosine of the phase difference. Developers of modal interference conditions cite this when characterizing path reinforcement or cancellation in recognition spaces. The definition is a direct algebraic expression that substitutes the PathWeight function and applies the real cosine.
Claim. $I(γ_1, γ_2, Δφ) := √(W[γ_1] ⋅ W[γ_2]) ⋅ cos(Δφ)$, where each γ is a list of configurations (positive real value with time coordinate) and W[γ] = exp(−C[γ]) is the path weight.
background
The ModalGeometry module develops geometric structure for modal logic on top of Possibility and Actualization. Configurations are simplified points in recognition state space, each carrying a positive real value and a time coordinate in ticks. PathWeight is the exponential of the negative path action and is the quantity that gives rise to the Born rule.
proof idea
This is a direct definition that applies PathWeight to each list, takes the real square root of their product, and multiplies by the cosine of the supplied phase difference. It draws the phase concept from the 8-tick phase definition and the unimodular phase construction in the RiemannHypothesis wedge.
why it matters
The definition supplies the common expression used by constructive_interference and destructive_interference, which in turn support the lemma constructive_at_zero. It fills the modal-geometry slot in the Recognition framework, connecting possibility-path overlaps to the eight-tick octave through the imported phase functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.