boundedShellIndex
plain-language theorem explainer
Packages the exact complexity of a size-capped combinatorial triangulation as a shell index in the finite type of rank B+1. Anyone building the capped-to-exact shell carrier map cites this to place a bounded complex into the correct shell slot. The body is a one-line subtype constructor: complexity is the max of the three counts, and the three cap inequalities give the Fin bound.
Claim. Given a natural number $B$ and a bounded complex $K$ at cap $B$ (at most $B$ vertices, edges, and tetrahedra), let $c(K)=\max(n_V,n_E,n_T)$. Then $c(K)\le B$, so $c(K)$ determines a unique element of $\mathrm{Fin}(B+1)$.
background
The module builds the missing carrier equivalence behind CapShellCompatibility in the Seven Gaps gravity stack. At fixed lattice scale the substrate treats configurations as combinatorial equilateral triangulations (CDT-style), so a bounded complex at cap $B$ is abstract incidence data with three size proofs $n_V,n_E,n_T\le B$.
Complexity is the shell coordinate: the largest of those three counts. An exact complex living in shell $n\le B$ becomes bounded by reattaching the three cap proofs; conversely, forgetting the proofs recovers the exact signature. Both directions keep incidence data and relabeling witnesses, so they descend to the quotient carriers.
No continuum limit, convergence claim, or physical phase is assumed here. The only arithmetic needed is that the max of three numbers each at most $B$ is itself at most $B$, hence a legitimate index in ${0,\ldots,B}$.
proof idea
One-line subtype constructor. The value field is complexity K, i.e. $\max(n_V,\max(n_E,n_T))$. The membership proof is Nat.lt_succ_of_le applied to the chained inequality max_le K.hV (max_le K.hE K.hT), which is exactly $c(K)\le B$ and therefore $c(K)<B+1$.
why it matters
This is the shell-slot extractor for the forward labeled map boundedToShell, which forgets cap proofs, retains the exact signature, and enters the exact relabeling quotient. The same index appears in the round-trip identity boundedToShell_exactToBounded: attaching a cap and then forgetting it recovers the original exact-shell class with shell index $n$ packaged as $\langle n, n\le B\rangle$.
In the broader Seven Gaps P2.3 story the bridge preserves automorphism cardinality and the $1/|\mathrm{Aut}|$ class measure, so finite quotient sums reindex cleanly against exactComplexityCutoff phase B whose shell range is $B+1$. Without a canonical $\mathrm{Fin}(B+1)$ index the carrier equivalence cannot even be stated. The construction is pure combinatorial bookkeeping; it does not touch the forcing chain T0–T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.