pairCount
plain-language theorem explainer
Defines the gauge volume of a labeled complex as the number of pairs (orbit representative, concrete relabeling witness). Pure counting: only equivalence and relabel data enter. Downstream orbit-stabilizer and class-mass theorems cite it to derive the discrete-gravity factor 1/|Aut| from pair counting, without naming Aut or mu in the definition itself.
Claim. For a bounded complex $K$, the gauge volume $\mathrm{pairCount}(K)$ is the cardinality of the set of pairs $(K', r)$ where $K'$ ranges over labeled complexes equivalent to $K$ and $r$ is a concrete relabeling witness from $K$ to $K'$.
background
The Seven Gaps gauge-preflight module starts from PathSumMeasure, which postulates the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut},K|$ as the standard discrete-gravity convention. The goal here is to derive that factor from pure gauge counting, so that the mass definition never mentions $\mu$ or Aut.
Two counting quantities are introduced on labeled complexes inside a bounded universe. The orbit card counts labeled complexes equivalent to $K$. The pair count (this definition) counts pairs $(K',r)$ with $K'$ in that orbit and $r$ a concrete relabeling $K\to K'$. The module doc states: DEFINITION mentions only Equivalent and Relabel (pure counting; no mu, no Aut).
On the quotient by equivalence, the ratio of orbit card to pair count becomes the gauge-counting mass of a triangulation class: labeled copies per unit of gauge volume. Orbit-stabilizer then identifies that ratio with $1/|\mathrm{Aut}|$.
proof idea
One-line definition: noncomputable natural-number cardinality of the dependent sum (sigma type) whose first component is a subtype of complexes equivalent to $K$ and whose second component is a relabeling witness from $K$ to that complex. No lemmas are applied; the body is pure Nat.card of that sigma type.
why it matters
This is the gauge-volume half of the counting principle that replaces the postulated $\mu$. Downstream, pairCount_eq_orbitCard_mul_autCard factorizes it as orbit card times $|\mathrm{Aut}|$ via the torsor structure of relabeling witnesses. Congruence (pairCount_congr) and the class lift (pairCountClass) make it a well-defined class function, so gaugeOrbitMass (orbit card over pair count on classes) is independent of representative.
The derivation theorem then equates that counting mass with $\mu=1/|\mathrm{Aut}|$, given the modeling choice that gauge volume equals the (copy, witness) pair count. Existence (gaugeOrbitMass_mul_pairCount) and the grounding theorem package the factorization as part of the preflight status. In the gravity stack this closes the gap between a hand-inserted symmetry factor and a count-only definition of discrete gauge measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.