boundedShellSig
plain-language theorem explainer
Extracts the exact combinatorial signature (vertex, edge, triangle counts) of a B-capped complex, landing in the shell whose index is the complex's true complexity. Cited by the forward carrier map from bounded complexes into the exact-shell quotient. The body packages three Fin witnesses from max inequalities and closes the shell-equality field by rfl.
Claim. Given a bounded complex $K$ at cap $B$ (vertex, edge, and triangle counts each $\le B$), return the exact shell signature of $K$ at shell index $\mathrm{complexity}(K) = \max(n_V,\max(n_E,n_T))$, with each count witnessed as strictly less than $\mathrm{complexity}(K)+1$.
background
Module CapShellBridge builds the missing carrier equivalence behind CapShellCompatibility (Seven Gaps, P2.3). At a fixed cap $B$, a bounded complex carries three natural counts $n_V,n_E,n_T$ each at most $B$, together with incidence data and relabeling witnesses. Its exact complexity is $\max(n_V,\max(n_E,n_T))\le B$.
An exact-shell signature at shell $n$ is the triple of counts packaged as elements of $\mathrm{Fin}(n+1)$, plus a proof that the shell index equals the true complexity. The converse direction reattaches three cap proofs to an exact complex whose shell is $\le B$. Both directions preserve incidence and descend to the two quotient carriers.
No continuum limit, target-sum equality, or physical phase interpretation is assumed here; the object is purely combinatorial.
proof idea
Definitional construction, not a tactic proof. The three Fin components are built by Nat.lt_succ_of_le from the max bounds: $n_V\le\max(n_V,_)$ gives the vertex witness; two applications of le_trans through the nested max give the edge and triangle witnesses. The residual equality field (shell index equals complexity) is closed by rfl.
why it matters
This is the signature half of the forward labeled map boundedToShell, which forgets cap proofs, retains the exact signature and incidence data, and enters the exact relabeling quotient. The inverse-direction identity boundedToShell_exactToBounded also consumes it: forgetting the cap after attaching it recovers the original exact-shell class by proof irrelevance.
Together these maps establish the carrier equivalence that lets an arbitrary exact-shell phase transport to a PhaseModel at every cap, and lets the finite quotient sum reindex to exactComplexityCutoff phase B (shell range $B+1$). That equality is the combinatorial content of CapShellCompatibility. The bridge preserves automorphism cardinality and hence the $1/|\mathrm{Aut}|$ class measure. No gravity continuum claim is discharged here; only the discrete carrier step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.