phasedWeight_emptyClass
plain-language theorem explainer
Under the B=2 witness phase model, the empty-complex triangulation class carries phased weight +1. Anyone citing the non-vacuous pairing witness or the exact cancellation of the empty/one-point pair needs this evaluation. The proof is a short tactic reduction: the class phase is the zero branch of the nV-test, so exp(i·0)=1.
Claim. For the witness phase model on the $B=2$ quotient-first path sum, the phased weight of the empty-complex class equals $+1$: $\mathrm{phased\,weight}=e^{i\theta}=1$ when $\theta$ is the class phase of the empty complex.
background
Lane D3 equips the quotient-first object $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 on TriangulationClass. The phased weight is the unit-modulus complex number $\exp(i\cdot\mathrm{classPhase})$.
The witness model used for the non-vacuity argument at complexity cap $B=2$ assigns phase $0$ to the vertex-free (empty) class and phase $\pi$ to every other class. The empty complex is the concrete zero-vertex, zero-edge, zero-triangle inhabitant of every BoundedComplex B; its class is the empty class.
This evaluation is the phase-$0$ half of the two-term pairing that later cancels unit mass at $0$ against unit mass at $\pi$.
proof idea
First establish that the class phase of the empty class under the witness model is $0$. Unfolding the witness definition, that phase is the conditional if nV(emptyComplex 2)=0 then 0 else π. The empty complex has nV=0 by definition (rfl), so if_pos selects the zero branch.
The goal is then $\exp(i\cdot\mathrm{classPhase})=1$. Rewrite by the phase fact just proved, coerce $0:\mathbb{R}$ to $\mathbb{C}$, apply mul_zero and Complex.exp_zero.
why it matters
Feeds directly into witnessPairing_cancel, which states that the witness pairing cancels exactly: unit mass at phase $\pi$ against unit mass at phase $0$. Together with the companion evaluation that the one-point class has weight $-1$, this discharges the exact-opposite hypothesis of the general pairing theorems (Zq_pairing_decomposition, Zq_pairing_bound, Zq_pairing_beats_triangle) at $B=2$.
That discharge is the concrete kernel of the non-vacuity witness chain: $|Z_q(2)|\le\mathrm{totalClassMass}(2)-2<\mathrm{totalClassMass}(2)$. Module status remains theorem-at-fixed-cap; the continuum limit stays open. No forcing-chain landmark (T5–T8) is touched here; this is pure finite-sum phase arithmetic inside the Seven Gaps gravity lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.