relabelingCount_eq_autCard
plain-language theorem explainer
For equivalent bounded complexes, the number of concrete gauge witnesses (relabelings) equals the order of the source automorphism group. This is orbit-stabilizer in pure cardinal form, used by anyone deriving the discrete-gravity factor 1/|Aut| from gauge counting alone. The proof extracts one witness from equivalence, then transports cardinality along the Aut-torsor equivalence of the witness set.
Claim. Let $K,K'$ be bounded complexes of bound $B$. If $K$ and $K'$ are gauge-equivalent (there exists at least one relabeling $K\to K'$), then the number of relabelings from $K$ to $K'$ equals $|\mathrm{Aut}(K)|$.
background
This module sits in the Seven Gaps gauge-preflight layer. PathSumMeasure postulates the standard discrete-gravity symmetry factor $\mu K=1/|\mathrm{Aut},K|$. Here that factor is derived from pure counting quantities that never mention $\mu$ or $\mathrm{Aut}$ in their definitions: the orbit size (number of labeled complexes equivalent to $K$) and the pair count (number of pairs $(K',r)$ with $K'$ in the orbit and $r$ a concrete relabeling witness).
Equivalence of complexes means the existence of a relabeling witness. The automorphism group is the stabilizer: relabelings of a complex to itself. The companion construction torsorEquiv shows that, once one witness $r_0:K\to K'$ is fixed, the full set of witnesses is a torsor under $\mathrm{Aut},K$ (right action by post-composition with automorphisms). Relabeling count is simply the cardinality of that witness set.
The local goal is the classical orbit-stabilizer identity in finite cardinal form, so that pair count later factorizes as orbit size times $|\mathrm{Aut},K|$.
proof idea
Short term-mode proof. From the equivalence hypothesis, obtain one concrete witness $r_0$. Unfold the definition of relabeling count (cardinality of the witness type). Apply Nat.card_congr to the equivalence of types supplied by torsorEquiv r0, which identifies the witness set with $\mathrm{Aut},K$ as an $\mathrm{Aut},K$-torsor; take the symmetric direction to get witness count $=|\mathrm{Aut},K|$.
why it matters
This is the cardinal half of the torsor/orbit-stabilizer block listed as proved (zero sorry, zero new axioms) in the module header. It feeds directly into the pair-count factorization (pair count $=$ orbit card $\times|\mathrm{Aut}|$) and into the grounding theorem gaugePreflight_grounded, whose first conjunct is exactly the universal quantification of this identity.
Together with representative-independence of the counting quantities, it lets the counting-defined class mass equal $\mu=1/|\mathrm{Aut}|$ under the model premise that gauge volume is the $(copy,witness)$ pair count. That closes the gap between a postulated symmetry factor and a derived one inside the discrete path-sum measure used for the gravity side of Recognition Science. It does not itself touch the forcing chain T0–T8; it is infrastructure for the gauge measure on bounded complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.