status_measure_derived

The Seven Gaps gauge-preflight module sits downstream of PathSumMeasure, which postulates the discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$. This module instead defines two pure counting quantities that never mention $\mu$ or $\mathrm{Aut}$: the orbit size (number of labeled complexes equivalent to $K$) and the pair count (number of pairs of an orbit copy with a concrete relabeling witness). Their ratio on the triangulation-class quotient is the counting-defined gauge mass.

Orbit-stabilizer for the relabeling torsor yields $\mathrm{pairCount}, K = \mathrm{orbitCard}, K \cdot |\mathrm{Aut}, K|$, so the counting mass equals $1/|\mathrm{Aut}, K|$. The status record packages which pieces of that story are theorems versus model premises. Its doc-comment states: "the torsor, the derivation, and uniqueness are theorems; the uniform-gauge-density counting principle is the explicit MODEL premise, not derived from the ledger."

One-line reflexivity. The status structure is defined with measure_derived_from_counting := true, so equating that field to true is definitional and discharged by rfl. No lemmas are applied.

Bookkeeping, not physics content. It freezes the claim that the $1/|\mathrm{Aut}|$ factor is no longer a bare postulate but follows from orbit-stabilizer plus the pair-counting principle inside this module. Downstream consumers of the Seven Gaps gravity stack can pattern-match on the status record rather than re-audit the torsor and mass-equality theorems. The companion flags mark torsor and uniqueness as proved while leaving counting_principle_derived_from_ledger false: the remaining open hinge is whether the ledger forces the pair-count gauge-volume convention itself. No forcing-chain landmark (T5--T8) is touched; this is discrete-gravity measure hygiene.