mu_out_emptyClass
plain-language theorem explainer
The empty-complex triangulation class has representative symmetry factor exactly 1. Anyone citing the B=2 phase-pairing witness (unit mass on empty and one-point classes) needs this identity. The proof is a two-step term: transport mu along the out/mk equality for emptyComplex 2, then apply the empty-complex measure lemma.
Claim. If $\mathrm{emptyClass}$ denotes the triangulation class of the empty complex at complexity cap $2$, then the symmetry factor $\mu$ of its chosen representative satisfies $\mu(\mathrm{out}(\mathrm{emptyClass})) = 1$.
background
Lane D3 of the Seven Gaps program equips the quotient-first path sum $Z_q$ with an explicit oscillatory phase model on labeled configurations that descends to triangulation classes. Each class $q$ contributes a real mass given by the symmetry factor $\mu$ of a chosen representative $\mathrm{out}(q)$; the total class mass is the sum of these factors over classes at a fixed complexity cap $B$.
The empty complex is the unique vertex-free configuration at cap $B=2$. Its class $\mathrm{emptyClass}$ is one of two unit-mass witnesses used later for exact phase pairing (phase $0$ on the empty class, phase $\pi$ elsewhere). Upstream, MeasureInvarianceNoGo.mu_emptyComplex already records that the empty complex itself has $\mu=1$; the present statement lifts that fact to the quotient representative.
The module works at fixed finite cap: continuum limits remain open. Cancellation is not derived from first principles here; it is supplied by a pairing hypothesis and discharged concretely at $B=2$.
proof idea
Term-mode, two steps. First rewrite with mu_out_eq_of_mk_eq at $K:=\mathrm{emptyComplex},2$, using that $\mathrm{emptyClass}$ is the class of that complex (rfl on the mk equality). This replaces $\mu(\mathrm{out}(\mathrm{emptyClass}))$ by $\mu(\mathrm{emptyComplex},2)$. Second, apply MeasureInvarianceNoGo.mu_emptyComplex 2, which states that the empty complex at cap 2 has symmetry factor 1.
why it matters
This is the empty-class half of the unit-mass pair that makes the $B=2$ phase-pairing witness non-vacuous. Downstream, witnessPairing_cancel uses unit mass at phase $0$ against unit mass at phase $\pi$ on the one-point class; witnessPaired_mass sums those two unit contributions to exactly 2; and two_le_totalClassMass_two cites both unit masses to prove $\mathrm{totalClassMass},2\ge 2$, so the improved bound $\mathrm{totalClassMass},2-2$ is nonnegative.
Together they close the kernel chain $|Z_q,2|\le\mathrm{totalClassMass},2-2<\mathrm{totalClassMass},2$ under the explicit witness phase model. In the Seven Gaps gravity lane this is structural evidence that phase pairing can beat the triangle inequality at fixed cap; the continuum limit and a first-principles derivation of the pairing remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.