exactComplex_ext
plain-language theorem explainer
Two exact complexes of fixed signature (v,e,t) are equal once their edge-vertex and tetrahedron-vertex incidence tables agree. Anyone building the Burnside shell-mass identity or the relabeling torsor cites this. The proof is pure structure extensionality: case-split both complexes and apply constructor injectivity.
Claim. Let $K$ and $K'$ be exact complexes of the same signature $(v,e,t)$. If the edge-vertex incidence of $K$ equals that of $K'$ and the tetrahedron-vertex incidence of $K$ equals that of $K'$, then $K = K'$.
background
This module is the kernel no-go for regulator removal at zero phase: the Gaussian-regulated quotient path sum $Z_{\mathrm{RS},\mathrm{uv}}$ has no $\rho\to 0^+$ limit when the action phase vanishes. The quantitative engine is a shell-mass identity obtained by Burnside/orbit-stabilizer on the relabeling gauge group of exact complexes.
An exact complex packages the incidence data of a labeled shell of signature $(v,e,t)$: which vertices bound each edge, and which vertices bound each tetrahedron. Equality of complexes is therefore equality of those two tables. The surrounding development treats the full relabeling triple group as a torsor over the sigma-type of all relabelings out of a fixed base complex, then splits fibers by orbit-stabilizer to relate $\sum 1/|\mathrm{Aut}|$ to the labeled count over $v!,e!,t!$.
Upstream geometry supplies concrete edge and tet vertex tables (Freudenthal-style triangulations); here only the abstract incidence fields matter.
proof idea
Tactic proof by double case analysis. Destructure $K$ and $K'$ as constructor applications of their two fields (edge incidence, tet incidence). Simplify with the injectivity equation for that constructor, then discharge the resulting pair of equalities by the two hypotheses. No external lemmas; pure inductive structure of the complex type.
why it matters
Feeds sigma_relabel_ext immediately: once incidence determines the complex, a pair (target, witness) in the total relabeling sigma is fixed by the witness's three index bijections alone, because the target is forced by the commutation equations. That extensionality is a step in realizing the relabeling triple group as a torsor (relabelSigmaEquiv), which underwrites the shell-mass identity sum_classMuOn_eq_card_div_factorials and the lower bound shellMass n \ge n^{3n}.
Those bounds kill absolute/positive-term regulator removal at zero phase (not_hasZRSRegulatorRemoval_zeroPhase). Oscillatory phases remain open; this lemma is phase-independent bookkeeping inside the labeled gauge counting, not a cancellation statement. It sits in the Gravity/SevenGaps stack rather than the T0–T8 forcing chain, but it is load-bearing for the kernel no-go that closes one named OPEN.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.