ofSector
plain-language theorem explainer
Maps a size-sector relabeling (triple of index permutations) to the corresponding (target complex, witness) pair by pushforward. Anyone proving the pair space equals the gauge group cites this as the inverse direction of that bijection. The body is a one-line constructor pairing the pushforward complex with its canonical relabeling witness.
Claim. Given a bounded complex $K$ and an element $g$ of its size-sector relabeling group $S_{n_V}\times S_{n_E}\times S_{n_T}$, form the pair $(\mathrm{push}_g(K), r_g)$ in the total space of (target, witness) pairs out of $K$, where $\mathrm{push}_g(K)$ is $K$ with indices permuted by $g$ and $r_g$ is the canonical relabeling witness $K\to\mathrm{push}_g(K)$.
background
Gap 2 identifies the gauge volume in the pair-counting premise of exact-shell preflight: pairCount K equals $(n_V)!,(n_E)!,(n_T)!$, the order of the full relabeling group of $K$'s size sector. That group is independent permutations of the vertex, edge, and tetrahedron index sets; nothing about $K$ beyond those three sizes enters.
The sector group is the product of three finite symmetric groups on the index sets. Pushforward along $g$ relabels the data of $K$ while keeping sizes fixed; the companion witness records the three equivalences and the commutation identities for edges and tets.
Pair space is the dependent sum of targets $K'$ with a relabeling witness from $K$ to $K'$. This definition is the canonical section that sends each sector-group element to such a pair.
proof idea
One-line definitional constructor: pack push K g (the relabeled complex) with pushRel K g (the canonical Relabel witness whose three equivalences are the components of $g$). No lemmas or tactics; the pair type is exactly $\Sigma K',,\mathrm{Relabel},K,K'$.
why it matters
Supplies the inverse map of sectorEquiv, the theorem that pair space is definitionally the gauge group: pairs $(K',r)$ out of $K$ biject with triples of index permutations. The left and right inverses ofSector_toSector and toSector_ofSector discharge that equivalence.
Downstream, label-erasure uses it to rebuild a pair from the sector element extracted by toSector, so letterwise relabeling invariance upgrades to full class-function invariance. That step feeds the restatement of the pair-counting premise as unit cross-sector fugacity: class weight equals labeled presentations over sector relabelings, recovering the discrete Faddeev-Popov form $1/|\mathrm{Aut},K|$.
Closes part of the MeasureSubstrateBlocker task (derive normalized gauge counting from ledger structure) without inventing an extra bookkeeping quantity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.