status_uniqueness
plain-language theorem explainer
The gauge-preflight status record marks uniqueness as proved. Auditors of the Seven Gaps derivation of the discrete-gravity path-sum measure 1/|Aut| can cite this as a machine-checked certificate that the counting-defined class mass is the unique solution of the orbit-volume relation. Proof is reflexivity on the status structure literal.
Claim. In the gauge-preflight status record for the Seven Gaps module, the uniqueness flag equals $\mathrm{true}$: uniqueness of the counting-defined class mass among solutions of the orbit-volume relation has been established as a theorem.
background
This module sits in the Seven Gaps gravity stack. PathSumMeasure postulates the symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$. Here that factor is derived from pure gauge counting: gaugeOrbitCard counts labeled complexes equivalent to $K$, pairCount counts pairs $(K', r)$ of an orbit copy with a concrete relabeling witness, and gaugeOrbitMass is their ratio on the triangulation-class quotient (labeled copies per unit of gauge volume).
Orbit-stabilizer is proved as a torsor statement: for equivalent complexes the relabeling set is a torsor over $\mathrm{Aut}, K$, so pairCount factorizes as orbit cardinality times $|\mathrm{Aut}|$. The counting mass then equals $1/|\mathrm{Aut}|$. Uniqueness means any class mass $\nu$ satisfying $\nu(c)\cdot\mathrm{pairCount}(c)=\mathrm{orbitCard}(c)$ coincides with that mass.
The status record packages four booleans. Three (torsor, derivation, uniqueness) are set true; the uniform-gauge-density counting principle itself remains an explicit model premise, not a ledger theorem.
proof idea
One-line term proof by rfl. The status definition hard-codes uniqueness_proved := true, so equality to true is definitional. No lemmas are applied; the certificate simply reifies that the uniqueness theorems in this module have been completed.
why it matters
Closes the uniqueness tier of the gauge-preflight checklist for Seven Gaps. Together with the torsor and the derivation gaugeOrbitMass_eq_mu, it certifies that the counting-defined mass is not merely one solution of the orbit-volume relation but the only class function that does so. That pins the discrete-gravity convention $\mu = 1/|\mathrm{Aut}|$ once the pair-counting principle is granted.
The open residue remains honest: the counting principle (uniform gauge density on labeled representatives) is still a named model premise, not derived from the Recognition ledger. Downstream path-sum and curvature work that imports this preflight can rely on uniqueness without re-proving it, while still seeing the ledger gap flagged false on the same record.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.