status_gauge_torsor

The Seven Gaps gauge-preflight module derives the standard discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$ from pure counting, rather than postulating it. Two counting quantities are defined without mentioning $\mu$ or Aut: the orbit card (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).

The key algebraic fact is torsor/orbit-stabilizer: for equivalent complexes, the set of relabeling witnesses is a torsor over $\mathrm{Aut}, K$, so $|\mathrm{Relabel}, K, K'| = |\mathrm{Aut}, K|$ and therefore $\mathrm{pairCount}, K = \mathrm{gaugeOrbitCard}, K \cdot |\mathrm{Aut}, K|$. The status record gaugePreflightStatus packages which pieces of that story are theorems versus model premises; its doc states that the torsor, the derivation, and uniqueness are theorems, while the uniform-gauge-density counting principle remains an explicit model premise.

One-line reflexivity. The status structure is defined with gauge_torsor_proved := true, so equating that field to true is definitional (rfl). No lemmas are applied; the theorem is a machine-checkable tag, not a re-proof of the torsor.

Honest status tagging for the gravity side of Recognition Science. The module claims a full derivation of $\mu = 1/|\mathrm{Aut}|$ from gauge counting once the pair-counting principle is granted; this flag certifies that the torsor/orbit-stabilizer block (the factorization pairCount = orbitCard * |Aut|) is closed with zero sorry. Downstream consumers of the preflight record can branch on the flag without re-auditing the torsor proofs. No used-by edges are recorded yet; the flag exists so later measure and uniqueness theorems can advertise a clean dependency surface. It does not touch the forcing chain (T0–T8) or the Recognition Composition Law directly; it sits in the discrete-gravity measure layer that feeds path-sum constructions.