equivalent_symm
plain-language theorem explainer
Gauge equivalence of bounded complexes is symmetric: a relabeling witness from K to K' yields an inverse witness from K' to K. Anyone proving that orbit and pair counts are class functions in the Seven Gaps gauge-preflight (the derivation of the 1/|Aut| measure) cites this. The proof is a one-line term: unwrap the Exists-style witness and apply its inverse.
Claim. Let $K,K'$ be bounded complexes in the fixed universe $B$. If $K$ is gauge-equivalent to $K'$ (there exists a concrete relabeling witness $r:K\to K'$), then $K'$ is gauge-equivalent to $K$ (via the inverse witness $r^{-1}$).
background
This module sits in the Seven Gaps gravity stack and derives the discrete-gravity symmetry factor $\mu K=1/|\mathrm{Aut},K|$ from pure gauge counting, rather than postulating it as PathSumMeasure does. The raw objects are labeled bounded complexes in a fixed universe $B$. Two complexes are gauge-equivalent when a concrete relabeling witness exists between them; the module writes that relation as the predicate underlying orbit and pair counts.
The counting quantities never mention $\mu$ or $\mathrm{Aut}$ by name: the orbit card is the number of labeled copies equivalent to $K$, and the pair count is the number of pairs (copy, witness). Symmetry of the gauge relation is the elementary step that makes those counts undirected, so later lifts to the triangulation quotient are well-defined class functions.
Upstream, the module imports the path-sum measure layer that supplies the type of bounded complexes and the postulated $\mu$; the present file rebuilds the same factor from orbit-stabilizer and pair counting.
proof idea
Term-mode, three tokens of substance. The hypothesis is an inductive/Exists-style package of a relabeling witness $r$ from $K$ to $K'$. Eliminate that package, then re-pack the inverse witness $r.symm$ as a gauge equivalence from $K'$ to $K$. No auxiliary lemmas are invoked; invertibility of a single relabeling is enough.
why it matters
This is one leg of the equivalence-relation package (reflexivity, symmetry, transitivity) for gauge relabeling. Downstream, gaugeOrbitCard_congr uses it inside a subtype equivalence: to show the orbit of $K$ equals the orbit of $K'$ as sets, one direction composes the given witness with an orbit member, and the reverse direction needs the inverse witness supplied here.
That class-function property is required before orbit card, pair count, and the counting-defined mass can descend to the triangulation quotient. The module's headline theorem then identifies the quotient mass with $\mu=1/|\mathrm{Aut}|$ via orbit-stabilizer factorization of the pair count. Without symmetry, representative independence fails and the derivation of the standard discrete-gravity measure from gauge volume does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.