autEquivToExact
plain-language theorem explainer
Bounded-complex automorphisms are in canonical bijection with exact automorphisms of the cap-forgotten complex: both packages are the same triple of vertex/edge/tet bijections commuting with incidence. Anyone tracking the 1/|Aut| class measure under cap forgetting cites this equivalence. The construction copies the three equivalences both ways and discharges the round-trips by structure extensionality.
Claim. For any cap $B\in\mathbb{N}$ and any bounded complex $K$ of cap $B$, there is a type equivalence $\mathrm{Aut}(K)\simeq\mathrm{ExactAut}(\mathrm{toExact}(K))$ identifying bounded automorphisms of $K$ with exact automorphisms of the cap-forgotten complex. Both sides are the same data: bijections of the vertex, edge, and tet index sets that commute with the incidence maps.
background
Module P2.3 builds the carrier bridge behind CapShellCompatibility. At cap $B$, a bounded complex carries incidence data together with proofs that its vertex/edge/tet counts are at most $B$. Forgetting those cap proofs yields an exact complex of the same signature (via toExact); the target type no longer mentions $B$.
An automorphism of a bounded complex is a self-relabeling: three equivalences on the finite index sets that commute with edge and tet incidence. ExactAut is the analogous self-relabeling for an exact complex, defined independently of any capped class (ExactRelabel with identical source and target). The module's point is that these two automorphism packages carry identical combinatorial data once the cap is forgotten.
Upstream, ExactRelabel packages vEquiv, eEquiv, tEquiv plus the two commutation laws; toExact simply reuses edgeVerts and tetVerts. The bridge is needed so that finite quotient sums and $1/|\mathrm{Aut}|$ measures can be reindexed between the capped and exact-shell carriers.
proof idea
Both directions of the equivalence are pure data copies. The forward map sends a bounded automorphism $r$ to the ExactRelabel whose three equivalences and two commutation proofs are exactly those of $r$. The inverse map does the same in reverse: an exact automorphism is re-wrapped as a bounded Relabel with the same fields.
Left inverse is Relabel.ext applied to three reflexivity proofs (the copied equivalences are definitionally identical). Right inverse is ExactRelabel.ext on the same three rfls. No combinatorial content is rewritten; the equivalence is definitional identity of the relabeling payload.
why it matters
This equivalence is the sole ingredient of autCard_toExact, which states Nat.card(Aut K) = Nat.card(ExactAut(toExact K)) by Nat.card_congr. That cardinality equality is what the module doc means by "the bridge preserves automorphism cardinality and hence the 1/|Aut| class measure."
Without it, reindexing the finite quotient sum from the capped carrier to exactComplexityCutoff phase B would lose the symmetry factors. The construction is local scaffolding for Seven Gaps P2.3: it closes the automorphism half of the capped-quotient to exact-shell carrier bridge, so that an arbitrary exact-shell phase can transport to a PhaseModel at every cap. No continuum limit, convergence claim, or physical interpretation is involved; only discrete carrier equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.