sigEmbed
plain-language theorem explainer
Canonical injection from the global-equivalence quotient of exact complexes of a fixed shell signature into the exact path class of complexity n. Anyone counting signature fibers or Burnside masses on ExactPathClass cites it. The map is the sigma-pair constructor; injectivity is immediate from equality of dependent pairs.
Claim. For each shell level $n$ and shell signature $s=(v,e,t)$ (with $\max(v,e,t)=n$), there is a canonical embedding $$\mathrm{ExactComplex}(v,e,t)/\sim \hookrightarrow \mathrm{ExactPathClass}(n)$$ sending each global-equivalence class $q$ to the pair $(s,q)$, where $\sim$ is global relabeling equivalence and $\mathrm{ExactPathClass}(n)$ is the disjoint union of those quotients over all signatures at level $n$.
background
ExactPathClass at complexity $n$ is the set of combinatorially distinct exact complexes of exact complexity $n$: the dependent sum over shell signatures $s$ of the quotient of labeled exact complexes by global equivalence. No bounded-complexity cap appears in the type.
A shell signature at level $n$ is a triple $(v,e,t)$ of vertex, edge, and tetrahedron counts, each at most $n$, with maximum exactly $n$, packaged in finite types so the signature space is finite. The projections $\mathrm{sigV}$, $\mathrm{sigE}$, $\mathrm{sigT}$ recover those three counts. On each fixed $(v,e,t)$, global equivalence (via explicit relabelings) is a setoid, so the quotient is well-defined.
This module is the Wave C1 R4 terminal attack on the SignatureFin8OscillatoryTailBlocker. The blocker Prop itself is not proved; the landed theorems package signature and Burnside masses and reformulate the blocker as an explicit sequence statement.
proof idea
Definition of an embedding (Function.Embedding). The forward map sends a quotient class $q$ to the dependent pair $\langle s, q\rangle$ in ExactPathClass $n$. Injectivity is a one-tactic argument: if two such pairs are equal, cases on the equality of sigma types forces the second components equal, then rfl. No external lemmas are required beyond the structure of $\Sigma$-types and Quotient.
why it matters
This embedding is the bridge from per-signature quotients into the global shell type used by the mass lemmas. Downstream, signatureFiber_eq_map identifies the signature fiber as the image of the finite universe under this embedding, and signatureMass_eq_burnside rewrites fiber mass as the Burnside quotient mass via sum_map along the embedding.
Those identities support shellMass_eq_sum_signatureMass and the fiberwise 8th-root grouping exactShellAmplitude_signature_fiberwise. In the Recognition gravity gap program they are the bookkeeping layer for the Fin-8 oscillatory-tail blocker attack: they make precise that single-signature mass concentration fails as a uniform large-$n$ strategy (cube dominance only mesoscopically), without flipping gap2_continuum_and_measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.