gaugeOrbitCard
plain-language theorem explainer
The gauge orbit card of a bounded complex K counts how many labeled complexes in the finite universe are gauge-equivalent to K. Discrete-gravity and path-sum workers cite it as the pure counting input to the 1/|Aut| measure, before any automorphism group is named. It is the subtype cardinality of the relabeling equivalence class, finite because the ambient universe is a Fintype.
Claim. For a bounded complex $K$ in the finite universe of bound $B$, write $\mathrm{card}_{\mathrm{orbit}}(K) := \lvert\{K' : K'\sim K\}\rvert$, the number of labeled complexes gauge-equivalent to $K$ under relabeling.
background
This module sits in the Seven Gaps gravity stack. PathSumMeasure postulates the discrete-gravity symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$. ExactShellGaugePreflight instead derives that factor from pure gauge counting, never mentioning $\mu$ or $\mathrm{Aut}$ in the mass definition.
A bounded complex is a labeled triangulation (or complex) inside a finite universe fixed by a bound $B$. Two complexes are equivalent when a concrete relabeling witness identifies them; the equivalence relation is the gauge relation generated by those witnesses. The ambient type is a Fintype, so every subtype is finite and Nat.card is well-defined.
The companion count is the pair count: number of pairs $(K',r)$ with $K'$ in the orbit of $K$ and $r$ a relabeling witness from $K$ to $K'$. Orbit card is the pure copy count; pair count is the gauge volume of the orbit.
proof idea
Definitional, not a proof. The value is Nat.card of the subtype of bounded complexes $K'$ such that $K$ is gauge-equivalent to $K'$. Finiteness is inherited from the ambient Fintype structure on the bounded universe; no separate cardinality argument is needed at the definition site.
why it matters
This is the first of the two raw counting quantities from which the module builds the gauge mass. Downstream, positivity (gaugeOrbitCard_pos) follows because the orbit contains $K$ itself. Class-functionality (gaugeOrbitCard_congr) lets the count descend to triangulation classes as orbitCardClass.
Together with the torsor/orbit-stabilizer theorem, it yields the factorization pairCount K = gaugeOrbitCard K * |Aut K|. That identity is the load-bearing step in the derivation theorem gaugeOrbitMass_eq_mu: the counting-defined class mass equals the postulated $\mu(K)=1/|\mathrm{Aut},K|$. The grounding theorem gaugePreflight_grounded packages this as status-backed evidence that the $1/|\mathrm{Aut}|$ path-sum weight is forced by gauge volume counting rather than written in by hand.
In the Recognition gravity program this closes the gap between a postulated discrete measure and a counting principle on labeled complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.