gaugePreflightStatus
plain-language theorem explainer
Status record for the exact-shell gauge preflight: torsor, counting-to-measure derivation, and uniqueness are marked proved; the uniform-gauge-density counting principle remains an explicit model premise, not a ledger theorem. Gravity residual-DAG and status-binding lemmas cite these four Bools as the honest checklist. The body is a pure structure literal with four boolean constants.
Claim. The gauge-preflight status record sets: gauge torsor proved $=\mathsf{true}$; measure derived from counting $=\mathsf{true}$; uniqueness proved $=\mathsf{true}$; counting principle derived from the ledger $=\mathsf{false}$.
background
In the Seven Gaps gravity stack, PathSumMeasure postulates the discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut},K|$. This module instead builds a gauge mass from pure counting: orbit card (labeled complexes equivalent to $K$), pair count (pairs of an orbit copy with a concrete relabeling witness), and their ratio on the triangulation-class quotient. Those definitions never mention $\mu$ or $\mathrm{Aut}$.
The module proves the torsor/orbit-stabilizer factorization (relabeling witnesses form an $\mathrm{Aut},K$-torsor, so pair count equals orbit card times $|\mathrm{Aut},K|$), representative independence on the quotient, the identity of the counting mass with $\mu$, and uniqueness of any class mass satisfying the counting property. What stays named as a model premise is the choice that gauge volume equals the (copy, witness) pair count (uniform gauge density on labeled representatives).
GaugePreflightStatus is the four-Bool checklist that records which of those layers are theorems and which remain premise.
proof idea
Definitional structure literal: four field assignments to boolean constants, matching the module's proved/open split. No tactics, no lemmas applied at this site. Downstream rfl theorems read the fields back.
why it matters
This is the single honest status object for ExactShellGaugePreflight. In-module parents are the four status theorems that assert each flag by rfl (torsor true, measure-derived true, uniqueness true, counting-principle-from-ledger false). Downstream, Gap2 residual-DAG and measure-status-binding use the open counting-principle flag in retractions and historical status records (R6 measure-side Bools false; ledger roll-up notes on flags 8–9).
It separates closed orbit-stabilizer algebra from the still-named model premise that gauge volume is pair count. That split matters for discrete-gravity path-sum measures: once the premise is granted, $1/|\mathrm{Aut}|$ is derived, not postulated. It does not itself touch T0–T8 or the RCL; it is infrastructure for the Seven Gaps continuum/measure residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.