irreducible_input_is_orbit_stabilizer
plain-language theorem explainer
The gauge-orbit size of a bounded complex times the order of its automorphism group equals the full label count nV!·nE!·nT!. Gravity and gauge-counting authors cite it so orbit accounting is a library theorem, not a free premise of the measure. The proof is a one-line re-export of the existing Gap2GaugeVolume orbit-stabilizer identity.
Claim. For every natural bound $B$ and every bounded complex $K$ of that bound, $\mathrm{gaugeOrbitCard}(K)\cdot|\mathrm{Aut}(K)|=n_V(K)!\cdot(n_E(K)!\cdot n_T(K)!)$.
background
Gap 2 asks whether the Gauge Counting Principle can be derived from substrate structure richer than counting at the posting layer. The module's answer is no: on the pinned carrier, counted histories are one per complex, invariant enrichments are forced to the Gibbs weight, and equivariant costs contribute no factor. What remains as premise is label indifference.
Orbit-stabilizer is the classical partition of the label space. Labels are permutations of vertices, edges, and triangles, so the total label count is $n_V!\cdot n_E!\cdot n_T!$. The gauge action partitions that space into orbits; the stabilizer of a complex is its automorphism group. The product of orbit size and stabilizer order recovers the label count.
The doc-comment records the identity here so "the accounting the measure relies on is visible as a theorem of the library, not a premise." Both the label count and the orbit count are computed; selection among them is the named premise of §6.
proof idea
One-line term proof: apply the upstream lemma Gap2GaugeVolume.orbitCard_mul_autCard to the bounded complex. That lemma already proves the orbit-stabilizer relation for the gauge action on labeled complexes. This declaration re-exports it under the posting-layer floor's name so the arc's index and the inevitable-reasons list can cite a local theorem.
why it matters
Feeds two parents. R11_orbit_stabilizer in GaugeCountingInevitableReasons is a one-line wrapper whose doc states "Orbit-stabilizer accounting is theorem, not premise," and is listed among the REFUTED derivation routes' supporting reasons. Locally, index_audit conjoins five floor flags; this identity underwrites the accounting half of that audit.
In Track A1.2 of the QG completion plan, the committed answer is that richer posting-layer structure does not derive the counting principle. Making orbit-stabilizer a proved library fact keeps the premise list honest: the §6 five-part verdict explicitly leaves label indifference as the remaining premise and disclaims completeness beyond the weight-based classes quantified. No T0–T8 or RCL step is at stake; this is gauge-counting infrastructure for the gravity gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.