relabel_nE_eq
plain-language theorem explainer
A relabeling of two size-bounded complexes forces their edge counts to agree. Cited whenever complexity or shell assignment must be shown invariant under combinatorial isomorphism. The proof transports finite cardinalities along the edge bijection carried by the relabeling, then reduces via the standard Fin-card identity.
Claim. Let $K$ and $K'$ be bounded complexes with the same size bound $B$, and let $r$ be a relabeling from $K$ to $K'$. Then the edge count of $K$ equals the edge count of $K'$.
background
This module builds exact (cap-free) complexity shells for the quotient-class path-sum configuration space and proves that the shell-resummed path sum with an explicit Gaussian UV regulator converges for every regulator strength $\rho>0$. Stage 1 is pure shell structure: complexity must be a relabeling invariant before shells and their Fintype instances make sense.
A bounded complex packages finite vertex, edge, and tetrahedron index types together with incidence data, all size-bounded by a natural number $B$. A relabeling is a structure of bijections on those three index types that preserve incidence; in particular it supplies an equivalence between the edge index types. The edge count is the cardinality of that edge index type (the same observable written $n_E$ in the Gap-2 census measure).
Sibling lemmas give the same statement for vertex and tetrahedron counts. Together they feed the complexity congruence used to define exact path classes up to global equivalence.
proof idea
Term-mode, three steps. The relabeling $r$ carries an equivalence eEquiv between the finite edge index types of the two complexes. Apply Fintype.card_congr to obtain equality of those cardinalities. Then simp only [Fintype.card_fin] rewrites both sides to the raw edge-count fields, and the resulting equality is the claim.
why it matters
Stage 1 theorem infrastructure for exact shells. Downstream, complexity_congr (THEOREM S1a) unfolds complexity and rewrites with this lemma plus the vertex and tetrahedron siblings, proving that equivalent bounded complexes have equal complexity. That invariance is what lets exact path classes be well-defined setoid quotients and later receive Fintype and entropy-card bounds.
Also used by boundedToShell_congr in the cap-shell bridge, which needs edge-count agreement to show the forward labeled map respects bounded relabeling.
Framework role is combinatorial bookkeeping inside the Seven Gaps gravity path-sum, not a forcing-chain step (T0–T8) and not a continuum claim. Regulator removal (HasZRSRegulatorRemoval) and the physical continuum limit remain explicitly open; this lemma does not touch them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.