relabelInvariant_implies_classFun
plain-language theorem explainer
Letterwise relabeling invariance of a labeled weight upgrades to constancy on full relabeling-equivalence classes of bounded complexes. Anyone proving the erasure pushforward formula (D1) cites this bridge: Aut and orbit data stay out of the hypothesis. The proof turns an equivalence witness into a sector-group element and applies the letterwise hypothesis through the gauge push map.
Claim. Let $w$ be a labeled weight on bounded complexes of bound $B$. If $w$ is letterwise relabeling-invariant (unchanged under every serial-name permutation of vertices, edges, and triangles), then $w(K)=w(K')$ whenever $K$ and $K'$ are relabeling-equivalent.
background
Gap 2 / A18 (lane C4) treats label erasure: the measure $\mu$ is the pushforward of a local relabeling-invariant labeled weight, and $1/|\mathrm{Aut}|$ is the erasure Jacobian. The module proves the Jacobian reading (D1) without closing flag 8.
A labeledWeight assigns a real value to each serially named bounded complex and carries no Gibbs factor. Letterwise invariance (RelabelInvariant) says $w$ is unchanged when serial names are permuted via the rename action; its statement names neither Aut, orbit, stabilizer, nor gauge class. Equivalence of two complexes means there exists an incidence-preserving index bijection between them.
The gauge-volume layer supplies the sector group of a complex $K$, the push map that applies a sector element as a relabeling, and the round-trip ofSector_toSector identifying pair-space elements with sector elements. Those tools convert a global equivalence witness into a concrete letterwise rename.
proof idea
Unpack the equivalence $K\sim K'$ to a relabeling witness $r$. Package $\langle K',r\rangle$ as a sector-group element $g$ of $K$ via toSector. The identity ofSector_toSector yields ofSector K g = \langle K',r\rangle, so projecting to the first component gives push K g = K'. Letterwise invariance applied to the three permutation components of $g$ says $w(\mathrm{push},K,g)=w(K)$. Rewrite along the push equality to conclude $w(K')=w(K)$.
why it matters
This is the upgrade step from letterwise invariance to class-function behavior on the relabeling setoid. Downstream, pushforward_labeledWeight_eq_gauge_divisor (D1) invokes it as hinv: for any letterwise-invariant labeled weight, the erasure pushforward on the class of $K$ equals $w(K)$ times the gauge divisor $(n_V!,n_E!,n_T!)/|\mathrm{Aut},K|$, with $|\mathrm{Aut}|$ appearing only in the conclusion.
That Jacobian reading is the scoped headline of the module: $\mu$ is the pushforward of a local relabeling-invariant labeled weight, and $1/|\mathrm{Aut}|$ is the erasure factor. The sibling index_flag_unmoved records that flag 8 stays false here; full measure closure still needs G1$\wedge$G2 plus fugacity elimination and numerator triviality. No T0–T8 forcing step is claimed; this is pure gauge bookkeeping inside the gravity seven-gaps stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.