refl
plain-language theorem explainer
Identity relabeling of a bounded combinatorial complex: the vertex, edge, and tetrahedron index sets map to themselves by the identity bijections, and incidence is preserved by reflexivity. Anyone building the relabeling setoid or the finite quotient of triangulation classes cites this. The construction is definitional: three identity equivalences plus two `rfl` commutation proofs.
Claim. For any bound $B$ and any bounded complex $K$ with at most $B$ vertices, edges, and tetrahedra, there is a relabeling isomorphism from $K$ to itself whose vertex, edge, and tetrahedron maps are the identity equivalences on the respective finite index sets, and which commutes with the edge- and tetrahedron-incidence maps.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{\mathrm{RS}}$ over a scoped class of combinatorial triangulations. Configurations are modeled by BoundedComplex B: at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps (edge endpoints and tetrahedron vertices) and no metric field. The substrate fixes edge length at the minimum mesh, so the class is CDT-style and equilateral; geometry lives entirely in incidence.
A relabeling isomorphism between two such complexes is a triple of bijections on the vertex, edge, and tetrahedron index sets that intertwine the incidence maps. The module treats this relation as a genuine equivalence (reflexive, symmetric, transitive), then quotients to triangulation classes and defines the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut}(K)|$ for the path sum.
Identity is the first leg of that equivalence: without it the setoid and the finite quotient do not form.
proof idea
Definitional construction, not a tactic proof. The three index equivalences are Equiv.refl on Fin K.nV, Fin K.nE, and Fin K.nT. Edge-incidence commutation reduces to rfl because Prod.map id id is the identity on pairs; tetrahedron-incidence commutation is likewise rfl under the identity vertex map. No external lemmas are invoked.
why it matters
Module status lists relabeling as a proved equivalence relation (relabelSetoid; refl/symm/trans, not asserted) and the quotient of triangulation classes as finite. This definition supplies reflexivity. Together with symmetry and transitivity it underwrites the finite class sum, the automorphism measure $\mu$, and the claim that the path sum is invariant under equivalence-preserving bijections of configurations.
In the broader RS gravity lane this is scaffolding for the honest scoped $Z_{\mathrm{RS}}$: unitary weights $w(K)=\exp(i S(K))$ with $|w|=1$, modulus bounds by the $\mu$-sum and by the cardinality of the bounded class, and discharge of the count-finiteness content previously postulated in the admissible-triangulation growth base. It does not touch the forcing chain (T0–T8) or the Recognition Composition Law directly; it is combinatorial measure theory for the gravity path sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.