constructive_at_zero
plain-language theorem explainer
Lemma establishing constructive interference for any two nonempty configuration paths at zero phase. Modal geometry researchers cite it when verifying positive amplitudes in possibility spaces. The term proof instantiates phase zero, simplifies the amplitude expression via cosine and multiplication identities, then confirms positivity through square-root and product rules.
Claim. Let $p_1,p_2$ be nonempty lists of configurations. Then the interference amplitude of $p_1$ and $p_2$ at phase zero is positive.
background
ModalGeometry works inside the space of configurations equipped with modal_distance and possibility_curvature, forming a two-dimensional manifold whose boundary behavior is governed by the J-cost function. Paths are represented as nonempty lists of Config, each carrying a positive weight. The lemma imports arithmetic facts such as mul_one from ArithmeticFromLogic, which asserts that multiplication by the successor of zero leaves a LogicNat unchanged.
proof idea
Term-mode proof. Instantiate the phase argument with 0, simplify interference_amplitude using Real.cos_zero together with mul_one, then apply mul_pos; the first factor is obtained by Real.sqrt_pos_of_pos applied to the product of two path_weight_pos terms, while the second factor is discharged by norm_num.
why it matters
The lemma supplies a base case for interference calculations inside the modal manifold, whose metric and curvature are defined in sibling declarations such as modal_distance and possibility_curvature. It aligns with the Recognition Science treatment of possibility and actualization modules, feeding the broader forcing chain that recovers spatial dimension D=3. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.