mu_onePointComplex
plain-language theorem explainer
The one-point complex at complexity cap 2 (one vertex, no edges or triangles) has path-sum measure exactly 1. Anyone citing the B=2 phase-pairing witness or the one-point class symmetry factor needs this unit value. The proof unfolds the 1/|Aut| definition, uses uniqueness of the automorphism group, and evaluates 1/1.
Claim. Let $K$ be the bounded complex of cap $B=2$ with one vertex and no edges or triangles. Its path-sum measure equals one: $\mu(K)=1/|\mathrm{Aut}(K)|=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. At fixed complexity cap $B$, every class carries a path-sum measure $\mu(K)=1/|\mathrm{Aut}(K)|$, the standard symmetry factor (uniform convention; a substrate-derived nonuniform measure remains open).
The one-point configuration at cap 2 is the bounded complex with $n_V=1$, $n_E=0$, $n_T=0$. It is the concrete representative of the one-point triangulation class used later in the $B=2$ pairing witness. Because a single unlabeled vertex admits only the identity relabeling, its automorphism group is a singleton, so the measure collapses to 1.
This sits inside the module's structure theorems at fixed cap: phased weights have unit modulus, $Z_q$ is a finite sum bounded by total class mass, and conditional exact-opposite pairings improve the triangle inequality. The continuum limit stays open.
proof idea
Term-mode proof in three steps. Unfold $\mu$ to $1/|\mathrm{Aut}(K)|$. Rewrite the cardinality by Nat.card_unique, which applies because the automorphism type of the one-point complex is a unique-element type (only the identity). Finish with norm_num to evaluate $1/1=1$.
why it matters
Feeds directly into mu_out_pointClass, which lifts the unit measure from the concrete one-point complex to any quotient representative of the one-point class. That unit factor is one of the two discharged legs of the $B=2$ non-vacuity witness: the explicit phase model (phase 0 on the vertex-free class, phase $\pi$ elsewhere) pairs the empty-complex and one-point classes, both of unit symmetry factor, yielding the kernel chain $|Z_q(2)|\le\mathrm{totalClassMass}(2)-2<\mathrm{totalClassMass}(2)$.
In the Seven Gaps gravity lane this is the concrete arithmetic that makes conditional cancellation non-vacuous at the smallest nontrivial cap. It does not derive the pairing mechanism from first principles; it supplies the measure input that the stated pairing hypothesis needs. Continuum-limit and substrate-derived measure questions remain open upstream of this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.