instFiniteRelabel
plain-language theorem explainer
For any two bounded complexes in the discrete-gravity universe, the set of relabeling (gauge) witnesses between them is a finite type. Anyone counting gauge orbits or pair volumes for the 1/|Aut| measure needs this finiteness off the diagonal. The proof injects witnesses into a finite triple of index bijections.
Claim. Fix a bound $B$. For any two bounded complexes $K,K'$ of that bound, the type of relabeling witnesses between $K$ and $K'$ is finite.
background
This module sits in the Seven Gaps gauge-preflight layer. PathSumMeasure postulates the discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$. Here the goal is to derive that factor from pure counting: orbit size (labeled copies gauge-equivalent to $K$) and pair count (pairs of a copy with a concrete relabeling witness), without mentioning $\mu$ or $\mathrm{Aut}$ in the definitions.
A relabeling witness between two bounded complexes is a gauge equivalence of their labeled data. On the diagonal this recovers automorphisms; off the diagonal it is the full set of witnesses used in orbit-stabilizer. The ambient universe of complexes of bound $B$ is finite, so index bijections among the underlying finite index sets form a finite type.
Upstream, injectivity of the map from witnesses into that triple of index bijections is already available (toEquivTriple_injective). The diagonal finiteness instance for automorphisms is the special case this generalizes.
proof idea
One-line wrapper. Apply Finite.of_injective to the map that sends a relabeling witness to its underlying triple of index bijections, using the already-proved injectivity of that map. The codomain is finite because the bound forces finite index sets, so the domain of witnesses is finite.
why it matters
Finiteness of off-diagonal relabeling witnesses is the first hard fact needed before any of the T2 gauge-counting quantities can be treated as natural numbers: orbit cardinality, pair count, and the counting-defined class mass. The module then proves the torsor/orbit-stabilizer factorization (witnesses form a torsor over the automorphism group, so pair count equals orbit size times $|\mathrm{Aut}|$) and finally that the counting mass equals $\mu = 1/|\mathrm{Aut}|$ under the pair-counting principle.
Without this instance, Lean cannot form cardinalities of Relabel K K' for $K \neq K'$, and the derivation of the standard discrete-gravity measure from gauge volume stalls. No downstream edges are recorded yet; sibling lemmas (gaugeOrbitCard, pairCount, torsorEquiv, pairCount_eq_orbitCard_mul_autCard) are the immediate consumers in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.