constructive_interference
plain-language theorem explainer
Two paths through lists of Config structures exhibit constructive interference when their interference amplitude is positive at some phase 2πn for integer n. Modal geometry work in possibility spaces cites this definition to encode phase alignment conditions before proving specific cases. The definition is a direct existential statement over the amplitude predicate at multiples of 2π.
Claim. Paths $p_1, p_2$ in the configuration space satisfy constructive interference when there exists an integer $n$ such that the interference amplitude of $p_1$ and $p_2$ evaluated at phase $2πn$ is strictly positive.
background
The ModalGeometry module imports Possibility and Actualization to work with paths as lists of Config structures. Config, from the ILG gravity model, packages parameters upsilonStar, eps_r, eps_v, eps_t, eps_a. The eight-tick phase supplies discrete values kπ/4. Interference amplitude is the sibling predicate that computes reinforcement from phase difference. Upstream structures include LedgerFactorization.of for J-cost calibration, PhiForcingDerived.of for the same, SpectralEmergence.of for gauge and generation content, and EightTick.phase for the periodic 8-tick phases.
proof idea
This is a definition. It directly encodes the condition as an existential quantifier over the integer n, requiring the interference amplitude at 2πn to be positive.
why it matters
The definition is invoked by the lemma constructive_at_zero in the same module, which establishes the condition at phase zero for nonempty paths. It supplies the phase-coherence predicate needed for modal actualization steps and aligns with the eight-tick octave (T7) and phase definitions in the forcing chain. No open scaffolding is closed here; the definition simply makes the interference distinction available for downstream modal lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.