equivalent_out
plain-language theorem explainer
A chosen representative of a bounded complex's relabeling class is always relabeling-equivalent to the original complex. Anyone evaluating class masses or invariant labeled weights on quotient classes cites this to transfer values between K and out([K]). The proof is a one-line term applying quotient exactness to the out_eq identity.
Claim. For any bound $B$ and any bounded complex $K$ of size at most $B$, if $[K]$ is the class of $K$ under the relabeling setoid and $\mathrm{out}([K])$ is a chosen representative of that class, then $\mathrm{out}([K])$ is relabeling-equivalent to $K$.
background
Gap 2 identifies the discrete gauge volume of a bounded complex with the order of its size-sector relabeling group $S_{n_V}\times S_{n_E}\times S_{n_T}$. Complexes are identified up to relabeling of vertices, edges, and tetrahedra; the relation Equivalent is that setoid, and classes live in the corresponding quotient.
Class-level quantities (class mass, orbit card, erasure pushforwards) are often defined by picking Quotient.out of a class and evaluating a labeled weight there. For that to be well-defined, or to match the weight at a concrete presenter $K$, one needs the out-representative to sit in the same relabeling orbit as $K$.
The module restates the pair-counting premise as: class weight equals labeled presentations of the class divided by sector relabelings, recovering the discrete Faddeev-Popov form $1/|\mathrm{Aut},K|$. This lemma is the elementary bridge that lets invariant weights ignore the choice of representative.
proof idea
One-line term proof. Quotient.out_eq gives equality of quotient elements out(mk K) = mk K. Quotient.exact converts that equality into membership in the setoid relation, which is exactly Equivalent for the relabeling setoid. No case analysis on the complex.
why it matters
This is the standard out-vs-presenter bridge used throughout Gap-2 measure and gluing work. Downstream, classMass_fugacity_mk rewrites the fugacity weight at the out-representative via this equivalence; invariant_weight_gives_measure_iff uses the same move in the uniqueness argument that only the Gibbs weight satisfies gauge counting among relabeling-invariant labeled weights; classMass_sizeWeight, classMass_sizeWeight_dust, and classMass_uniform all invoke it to pull size-blind or uniform weights off the out-representative.
Label-erasure (pushforward_labeledWeight_eq_gauge_divisor) and non-equivariant posting (mu_eq_orbitCard_mul_gibbsWeight) likewise need orbit membership of the chosen representative. Without it, class mass defined via out would not match evaluation at a concrete $K$, and the identification of gauge volume with sector factorial order could not be stated on classes.
It does not itself select the Gibbs measure; it only licenses moving invariant data across the quotient. The open substrate task recorded by MeasureSubstrateBlocker (derive normalized gauge counting from richer ledger structure) still sits above this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.