orbitCard
plain-language theorem explainer
Counts the relabeling orbit of an exact combinatorial complex K of fixed signature (v,e,t): how many exact complexes are globally equivalent to K. Gravity and combinatorial-gauge arguments cite it as the orbit factor in orbit-stabilizer. The body is a direct cardinality of the GlobalEquivalent subtype, not a derived identity.
Claim. For an exact complex $K$ with $v$ vertices, $e$ edges and $t$ tetrahedra, the orbit size of $K$ is the number of exact complexes $K'$ of the same signature for which a relabeling isomorphism $K\simeq K'$ exists (global equivalence).
background
The ambient module is the zero-phase regulator-removal no-go for the Gaussian-regulated quotient path sum on exact shells. Exact complexes are cap-free combinatorial data: exactly $v$ vertices, $e$ edges, $t$ tetrahedra, with incidence maps and no bound inequalities. Global equivalence on a fixed signature means a nonempty exact relabeling: bijections of the three index sets that commute with incidence.
The shell-mass identity (Burnside / orbit-stabilizer route) equates the sum of per-class measures $1/|\mathrm{Aut}|$ over the quotient to the labeled count divided by the full relabeling volume $v!\cdot e!\cdot t!$. That identity needs a named orbit size for each labeled representative before fibers and stabilizers can be split.
Upstream, ExactComplex supplies the configuration type and GlobalEquivalent is the setoid relation (nonempty exact relabeling) used to form the orbit subtype.
proof idea
Pure definition: noncomputable natural-number cardinality of the subtype of exact complexes $K'$ of the same signature that are globally equivalent to the given $K$. No lemmas are applied; finiteness is inherited from the ambient finite exact class when later theorems invoke Nat.card.
why it matters
This is the orbit factor in the exact-form orbit-stabilizer theorem: orbit size times automorphism count equals $v!\cdot e!\cdot t!$ for every labeled complex. Downstream, fiber cardinality over a quotient class equals the orbit size of a representative; summing witness counts factorizes as orbit times aut; summing orbit sizes over the quotient closes the shell-mass identity sum_classMuOn_eq_card_div_factorials.
That identity feeds the shell-mass lower bound on signatures $(n,n,n)$, which diverges and kills absolute/positive-term regulator removal at zero phase. Preflight code reuses the same counting idea for gauge-orbit mass (labeled copies per unit gauge volume). The oscillatory-phase removal question stays open; this definition only supports the zero-phase kernel no-go.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.