equivalent_refl

This module derives the discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$ from pure gauge counting, rather than postulating it. The raw data are labeled bounded complexes inside a fixed bound $B$. Two complexes are related by the gauge relation when a concrete relabeling witness exists between them; the identity map is the trivial such witness.

Orbit size is the number of labeled copies gauge-equivalent to a given $K$. Pair count is the number of (copy, witness) pairs along that orbit. The counting-defined class mass is orbit size over pair count; orbit-stabilizer then forces that mass to equal $1/|\mathrm{Aut}|$.

Reflexivity is the first algebraic property of the gauge relation: without it the orbit of $K$ need not contain $K$, and the orbit cardinality is not guaranteed positive.

One-line term proof. The equivalence type is inhabited by a relabeling witness; supply the identity relabeling of $K$ to itself. No tactics, no side conditions.

Feeds gaugeOrbitCard_pos, which builds a nonempty subtype of complexes equivalent to $K$ by pairing $K$ with this reflexivity witness, then concludes the orbit cardinality is positive. That positivity is prerequisite infrastructure for the torsor/orbit-stabilizer block (relabeling witnesses form an $\mathrm{Aut}$ torsor, pair count factors as orbit size times $|\mathrm{Aut}|$) and for the main derivation that the counting-defined gauge mass equals $1/|\mathrm{Aut}|$.

In the Seven Gaps gravity stack this is pure preflight algebra: it does not touch the Recognition forcing chain (T5–T8) or the mass ladder, but it closes the discrete-gauge bookkeeping that justifies the standard $1/|\mathrm{Aut}|$ measure from counting alone.