refl_vEquiv
plain-language theorem explainer
The identity relabeling of a bounded complex acts as the identity map on vertices. Anyone building automorphism groups, symmetry factors, or path-sum invariance over labeled triangulations cites this as the reflexive case of the relabeling data. The proof is pure definitional equality (rfl).
Claim. For every bounded combinatorial complex $K$ of size bound $B$, the vertex map of the reflexive relabeling of $K$ equals the identity equivalence on the vertex set of $K$.
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 BoundedComplex B: at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps and no metric field (CDT-style equilateral mesh fixed by the substrate).
Relabelings are structure-preserving reindexings of those incidence data. Each relabeling carries a vertex equivalence (a bijection on the finite vertex type). The reflexive relabeling is the identity reindexing of a fixed labeled complex $K$; this lemma records that its vertex component is literally Equiv.refl.
The module proves that relabeling is a genuine equivalence relation and that the quotient of labeled complexes is finite, so the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ is well-defined and relabeling-invariant. Vertex-map identities are the bookkeeping layer under those results.
proof idea
One-line definitional proof: both sides reduce to the same constructed term, so rfl closes the goal. No lemmas are applied; the simp attribute makes the identity available for rewriting in downstream goals that compare vertex maps of relabelings.
why it matters
Feeds translationAut_zero in PathSumProbes, which identifies the zero translation automorphism with the reflexive relabeling of the Freudenthal bounded complex and rewrites through this identity on vertex equivalences. Without the simp fact, every Aut and $\mu$-invariance argument would re-unfold the reflexive constructor by hand.
In the Lane 2 status list this sits under the proved block that relabeling is a real equivalence relation (refl/symm/trans) and that $Z B w=\sum_K \mu(K),w(K)$ is finite and relabeling-invariant. It is infrastructure, not a physics claim: it does not touch the open exponential-growth semantics of exact simplicial subclasses, nor the forcing chain (T0–T8), but it keeps the combinatorial measure class honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.