constructive_at_zero
plain-language theorem explainer
The lemma shows that any two non-empty lists of configurations produce constructive interference when the relative phase is set to zero. Modal geometry work in Recognition Science cites it to guarantee positive amplitude contributions inside the possibility manifold. The term proof substitutes phase zero into the amplitude expression, reduces via cosine and multiplication identities, then applies positivity of square roots on path weights.
Claim. Let $p_1$ and $p_2$ be non-empty lists of configurations. Then the interference amplitude of $p_1$ and $p_2$ at phase zero is strictly positive.
background
The ModalGeometry module treats the space of configurations as a two-dimensional manifold whose metric is modal_distance and whose curvature is possibility_curvature. Paths are finite lists of configurations; interference_amplitude combines their weights with a cosine of relative phase. The supplied upstream result mul_one supplies the arithmetic identity $n * 1 = n$ used in the reduction. Broader module imports supply dimension signatures and structural lists that contextualize the configuration space.
proof idea
Term proof that instantiates the phase argument to zero. It rewrites interference_amplitude using Real.cos_zero and mul_one, then applies mul_pos to the product of two square-root terms. The first square root is shown positive by Real.sqrt_pos_of_pos applied to the product of path_weight_pos on each list; the second factor is discharged by norm_num.
why it matters
The result anchors positivity of interference inside the modal manifold section, supporting the metric and curvature definitions that follow. It supplies a basic case for the possibility space in the Recognition framework, consistent with the dimension-forcing and eight-tick structures referenced in upstream dimension and arithmetic modules. No downstream theorems are recorded, leaving its precise placement in larger modal constructions open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.