status_counting_principle_open
plain-language theorem explainer
Records that the gauge-preflight status flag for the counting principle is false: uniform gauge density on labeled representatives remains a named model premise, not a ledger theorem. Gravity auditors tracking honesty of the Seven Gaps 1/|Aut| derivation cite this. Proof is definitional reflexivity on the status record.
Claim. The gauge-preflight status field asserting that the counting principle (uniform gauge density on labeled representatives) is derived from the ledger equals $\mathsf{false}$. Equivalently: that premise is tagged open, not discharged by a ledger theorem.
background
The Seven Gaps gauge-preflight module sits under discrete gravity. PathSumMeasure postulates the symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$. This module instead defines a gauge mass from pure counting: orbit card (labeled complexes equivalent to $K$), pair count (pairs of an orbit copy and a concrete relabeling witness), and gauge-orbit mass as their ratio on the triangulation-class quotient. Those definitions never mention $\mu$ or $\mathrm{Aut}$.
Proved content includes the torsor/orbit-stabilizer factorization $\mathrm{pairCount}, K = \mathrm{gaugeOrbitCard}, K \cdot |\mathrm{Aut}, K|$, representative independence on the quotient, and the identity that the counting-defined mass equals $\mu K = 1/|\mathrm{Aut}, K|$ once the pair-counting principle is granted. The module doc is explicit: what is put in by hand is the choice that gauge volume equals the (copy, witness) pair count; a per-labeled-copy principle would yield the quotient-uniform measure instead.
Status flags tag which pieces are ledger theorems versus open residues. This declaration is the open-residue flag for the counting principle itself.
proof idea
Term-mode one-liner: rfl. The status structure sets counting_principle_derived_from_ledger to false by definition, so equality to false is definitional. No lemmas are applied.
why it matters
Honest bookkeeping for the Seven Gaps gravity stack. Downstream consumers of gauge preflight need a machine-checkable record of what is still a model premise: the uniform gauge density on labeled representatives (pair-count as gauge volume). The module already closes orbit-stabilizer, pair-count factorization, gaugeOrbitMass = mu, and uniqueness of the counting mass; this flag isolates the residual premise so the derivation is not oversold as fully ledger-internal.
No used_by edges yet; the declaration is a status sentinel rather than a lemma in a forcing chain. It does not touch T0–T8, RCL, or the mass ladder directly; it polices the discrete-gravity measure that feeds path-sum gravity. Closing the residue would mean promoting the counting principle to a ledger theorem and flipping the flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.