constructive_interference
plain-language theorem explainer
Constructive interference for two configuration paths holds precisely when there exists an integer n such that the interference amplitude at phase 2πn is positive. Modal geometry work in Recognition Science cites this to mark reinforcement conditions inside possibility spaces. The definition is introduced directly as an existential statement on the amplitude function at integer multiples of 2π.
Claim. For paths $p_1$ and $p_2$ consisting of configurations, the reinforcement property holds if and only if there exists an integer $n$ such that the interference amplitude between $p_1$ and $p_2$ evaluated at phase $2$π$n$ is strictly positive.
background
The ModalGeometry module works with lists of Config structures drawn from the ILG gravity model; each Config bundles the parameters upsilonStar, eps_r, eps_v, eps_t and eps_a. The amplitude function in the same module returns a real value that quantifies reinforcement from a supplied phase difference, relying on the eight-tick phase map that sends each k in Fin 8 to kπ/4 and is periodic with period 2π. The module imports Possibility and Actualization to place these notions inside the modal layer of Recognition Science.
proof idea
The declaration is a direct definition that asserts existence of an integer n for which the amplitude function returns a positive value at the argument 2 * Real.pi * n. It invokes the amplitude function from the same module and the phase periodicity supplied by EightTick.phase; no further lemmas or reductions are applied.
why it matters
The definition is invoked by the lemma constructive_at_zero, which establishes the property at phase zero for nonempty paths by choosing n = 0 and applying positivity of cosine at zero. It supplies a basic modal-geometry predicate that aligns with the eight-tick octave (T7) and the phase relations forced in the unified chain. The supplied data record no open questions attached to this predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.