exactCodeEquiv
plain-language theorem explainer
Canonical bijection between exact-size labeled complexes of signature $(v,e,t)$ and the raw product of edge-incidence maps with tetrahedron-incidence maps. Cited by anyone installing a Fintype instance or counting labeled complexes at fixed signature. Both directions unpack or repack the two structure fields; the inverse laws hold by reflexivity.
Claim. For natural numbers $v,e,t$, the set of exact combinatorial complexes with exactly $v$ vertices, $e$ edges and $t$ tetrahedra is in bijection with $(\mathrm{Fin}\,e\to\mathrm{Fin}\,v\times\mathrm{Fin}\,v)\times(\mathrm{Fin}\,t\to\mathrm{Fin}\,4\to\mathrm{Fin}\,v)$: each complex is identified with its pair of incidence maps (one vertex-pair per edge, one $4$-tuple of vertices per tetrahedron).
background
This module organizes the quotient-class path-sum configuration space into exact complexity shells (no size caps in the shell definition) and studies a Gaussian-UV-regularized path sum. Honesty constraints: the regulator $\exp(-\rho n^2)$ is inserted by hand; the action/phase is a free parameter on classes; regulator removal $\rho\to 0^+$ remains a named open.
An exact complex of signature $(v,e,t)$ is the cap-free configuration type: exactly $v$ vertices, $e$ edges, $t$ tetrahedra, with abstract incidence data edgeVerts : Fin e → Fin v × Fin v and tetVerts : Fin t → Fin 4 → Fin v. Because there is no cap, the cross-cap identification problem of bounded complexes cannot arise. The present declaration simply exposes that incidence pair as a product type (the "finite code" of the complex).
proof idea
Definitional equivalence, not a deep argument. The forward map sends a complex $K$ to the pair $(K.\mathrm{edgeVerts}, K.\mathrm{tetVerts})$. The inverse rebuilds the structure constructor from the two product components. Left and right inverse identities are both rfl: packing then unpacking (and conversely) is definitionally the identity on the structure and on the product.
why it matters
Stage-1 shell infrastructure in the Seven Gaps gravity path-sum development. Downstream, the Fintype instance on exact complexes is obtained by transporting along the inverse of this equivalence, and the labeled count theorem rewrites cardinality through it to get $$|\mathrm{ExactComplex}(v,e,t)|=(v\cdot v)^e\cdot(v^4)^t.$$ That count feeds the labeled entropy bound used when every shell index is at most $n+1$, which in turn supports finiteness of exact path classes and the modulus bound on regulated shell terms. Nothing here touches continuum limits, physical actions, or regulator removal; those stay open or RED per the module protocol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.