phasedWeight_pointClass
plain-language theorem explainer
On the explicit B=2 witness phase model, the phased weight of the one-point triangulation class equals −1. Anyone citing the exact pairing cancellation between the empty-complex and one-point classes needs this evaluation. The proof reduces the class phase to π via the nV≠0 branch, then applies exp(iπ)=−1.
Claim. For the witness phase model (phase $0$ on the vertex-free class, phase $\pi$ on every other class), the phased weight of the one-point class equals $-1$: $\exp(i\,\theta([\mathrm{pt}]))=-1$.
background
Lane D3 of the Seven Gaps program equips the quotient-first path sum $Z_q$ with an explicit oscillatory phase model. A PhaseModel is a real phase on labeled configurations that is relabeling-invariant, so it descends to a class phase $\theta$ on TriangulationClass. The phased weight is the unit-modulus complex factor $\exp(i\theta)$.
The witness model used for the $B=2$ non-vacuity argument assigns phase $0$ to the empty (vertex-free) class and phase $\pi$ to every other class. The one-point class is detected by the vertex-count observable $n_V$: for the one-point complex one has $n_V=1\neq 0$, so the model places it on the $\pi$ branch.
This sits inside the fixed-complexity-cap structure theorems: phased $Z_q$ is a finite sum with $|Z_q|\le\mathrm{totalClassMass}\le#(\mathrm{classes})$. Exact cancellation under an opposite-phase pairing hypothesis improves the bound strictly past the triangle inequality; the continuum limit remains open.
proof idea
First establish that the class phase on the one-point class equals $\pi$. Unfolding the witness model, that phase is the conditional if nV(onePoint)=0 then 0 else π. Since $n_V=1$, Nat.one_ne_zero discharges the negative branch and the if collapses to $\pi$.
The goal is then $\exp(i\cdot\theta)=−1$. Substitute the phase, commute the factors so the argument is $\pi,i$, and finish with the standard identity Complex.exp_pi_mul_I ($e^{i\pi}=-1$).
why it matters
This is the concrete evaluation that makes the $B=2$ witness pairing non-vacuous. Downstream, witnessPairing_cancel uses it to prove that unit mass at phase $\pi$ (one-point class) exactly cancels unit mass at phase $0$ (empty-complex class): the paired summands are literal negatives.
That cancellation feeds the kernel chain $|Z_q(2)|\le\mathrm{totalClassMass}(2)-2<\mathrm{totalClassMass}(2)$, showing that a stated pairing hypothesis can be discharged on an explicit finite census and that the improved modulus bound is strict and nonnegative. In the Seven Gaps ledger this is the phase-structure half of the quotient-first no-go / refinement story at fixed cap; it does not yet close the continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.