RelabelInvariant
plain-language theorem explainer
Defines letterwise relabeling invariance for a real weight on serially named bounded complexes of budget B: the weight is unchanged under any permutation of vertex, edge, and triangle serial indices. Gap-2 measure work cites it as the G1 hypothesis that never names Aut, orbits, or gauge classes. The body is a plain universal equality over the rename action.
Claim. Fix a natural number $B$ and a weight $w$ assigning a real number to every $B$-bounded complex. Call $w$ letterwise relabeling-invariant when, for every such complex $K$ and every permutations $\sigma_V,\sigma_E,\sigma_T$ of its vertex, edge, and triangle serial names, $w(\mathrm{rename}(K;\sigma_V,\sigma_E,\sigma_T))=w(K)$.
background
Gap 2 (A18, lane C4) treats the continuum measure $\mu$ on isomorphism classes of bounded complexes as the pushforward of a local weight on serially named carriers. Serial names are the Fin-indexed labels on vertices, edges, and triangles; the rename action permutes those indices while preserving incidence (the same action underlying the gauge-volume push).
A labeled weight is simply a map from $B$-bounded complexes to $\mathbb{R}$, with no Gibbs factor built in. The module insists that the invariance hypothesis be stated letterwise: only the rename action appears, never $\mathrm{Aut}$, orbit, stabilizer, gauge class, or a canonical representative. That is the statability gate G1 for the erasure Jacobian identity.
Upstream, the rename/push infrastructure and the equivalence relation on complexes supply the action; orbit-stabilizer later converts letterwise invariance into the factor $(n_V!,n_E!,n_T!)/|\mathrm{Aut},K|$ on the quotient.
proof idea
Definitional: the predicate is the Prop that for all $K$ and all three serial-name permutations, $w$ of the renamed complex equals $w(K)$. No lemmas are applied; inhabitation is shown downstream (constant one, Boltzmann numerators of equivariant letter costs).
why it matters
This is the G1 hypothesis for D1 in the label-erasure module. The parent theorem pushforward_labeledWeight_eq_gauge_divisor uses it to prove that the erasure pushforward equals $w(K)$ times the gauge divisor $(n_V!,n_E!,n_T!)/|\mathrm{Aut},K|$, with $|\mathrm{Aut}|$ appearing only in the conclusion. Sibling lemmas upgrade it to full equivalence-class invariance, show the constant weight $1$ and $\exp(-\mathrm{historyCost})$ for equivariant letter costs satisfy it, and feed the LabelErasureIndex structure (d1_stated_letterwise). Hostile-probe checks confirm the hypothesis wording avoids Aut. Flag 8 / gap2_measure_derived remains unmoved: G1 alone does not close the measure gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.