opposite_phase_exp
plain-language theorem explainer
Advancing a real phase by π multiplies the complex unitary weight by −1: exp(i(θ+π)) = −exp(iθ). Gravity and path-sum authors cite it when pairing opposite-phase summands on the quotient-first Zq. The proof is a short rewrite chain through ofReal_add, exp_add, and exp(iπ) = −1.
Claim. For every real phase $\theta$, $\exp\bigl(i(\theta+\pi)\bigr) = -\exp(i\theta)$ as complex numbers.
background
Lane D3 equips the quotient-first path sum Zq with an explicit oscillatory phase model: a real phase on labeled configurations that is relabeling-invariant, hence descends to triangulation classes, and yields unitary weights exp(i·phase) of modulus one. At fixed complexity cap the phased sum is a finite complex combination of class masses times these weights.
Exact cancellation of two equal-mass contributions requires that their phases differ by π, so the corresponding unitaries are negatives of each other. The present identity is the pure complex-analytic fact that implements that sign flip; it does not yet mention masses or the path sum.
The surrounding module keeps the continuum limit open and treats pairing as a stated hypothesis discharged only by concrete finite witnesses (notably at cap B = 2).
proof idea
Rewrite-only proof. Expand the real sum inside the complex embedding (ofReal_add), distribute I over the sum (mul_add), factor the exponential (exp_add), commute I past the real π, apply the standard identity exp(I·π) = −1, and finish with multiplication by −1. No induction or case split.
why it matters
Feeds the two-term exact cancellation theorem: equal real masses at phases θ and θ+π sum to zero in ℂ, which is the arithmetic engine behind the conditional pairing decomposition of phased Zq. That decomposition improves the modulus bound from the triangle inequality to totalClassMass − pairedMass whenever a nonempty opposite-phase pairing exists, and supplies the B = 2 non-vacuity witness that beats the triangle bound by 2.
In the Seven Gaps gravity program this is the elementary phase step that turns a pairing hypothesis into strict cancellation on the quotient-first object. It does not itself derive why opposite phases appear; it only certifies the unitary sign flip once they do. The continuum limit of the phased sum remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.