GaugePreflightStatus
plain-language theorem explainer
A four-flag status record for the exact-shell gauge-preflight module: whether the Aut-torsor, the counting-to-mu derivation, and uniqueness are theorems, and whether the pair-counting principle itself is ledger-derived. Gravity authors cite it to read the honest proved-vs-premise split at a glance. It is a plain structure definition with Boolean fields; no proof.
Claim. A status record with four Boolean fields: (1) the gauge-relabeling torsor (orbit-stabilizer) is proved; (2) the class mass equals $1/|\mathrm{Aut}|$ is derived from counting; (3) uniqueness of that mass is proved; (4) the uniform-gauge-density counting principle is derived from the ledger. Field (4) is the named model premise in this module, not a theorem.
background
The parent module sits in the Seven Gaps gravity stack. PathSumMeasure postulates the discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$. This module instead defines pure counting quantities that never mention $\mu$ or $\mathrm{Aut}$: gaugeOrbitCard (size of the relabeling orbit), pairCount (pairs of labeled copy and concrete Relabel witness), and gaugeOrbitMass on triangulation classes as orbit card over pair count.
Module status tiers separate theorems from the model premise. Orbit-stabilizer gives $|\mathrm{Relabel}, K, K'| = |\mathrm{Aut}, K|$ and the factorization pairCount = gaugeOrbitCard * |Aut|. Representative independence lifts the counts to the quotient. The derivation theorem then equates the counting mass to $\mu$, given that gauge volume is the pair count. Uniqueness says any class mass satisfying the counting identity equals that mass.
What remains open is deriving the pair-counting principle from the ledger floor rather than taking it as a model choice (a per-labeled-copy principle would yield the quotient-uniform measure instead).
proof idea
No proof: this is a structure definition with four Bool fields. Downstream, a single value packs the module's honest tags (true for torsor, derivation, and uniqueness; false for ledger-derivation of the counting principle). The mathematical work lives in the sibling theorems (torsorEquiv, pairCount_eq_orbitCard_mul_autCard, gaugeOrbitMass_eq_mu, gaugeCountingMass_unique); this type only records their status.
why it matters
Honest tagging is the point. Downstream gaugePreflightStatus freezes the module verdict: torsor, measure-from-counting, and uniqueness are theorems; the uniform-gauge-density counting principle is the explicit MODEL premise, not ledger-derived. That split matters for the Seven Gaps program, which aims to replace the postulated $1/|\mathrm{Aut}|$ path-sum measure by counting, without smuggling the premise into the theorem list.
In the broader Recognition stack this is gravity-side scaffolding hygiene rather than a T0–T8 forcing step. It does not touch J-uniqueness, $\phi$, the eight-tick octave, or $D=3$. It does pin where the discrete-gravity measure story still depends on a modeling choice versus pure orbit-stabilizer algebra, so later ledger-bridge work has a clear target for closing the remaining false flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.