simplex3d_edge_card_ne_4d
plain-language theorem explainer
The finite type of six labels is not equicardinal with the finite type of ten labels: 6 ≠ 10. Gravity and discrete-geometry workers cite it as a domain-mismatch witness separating 3-simplex edge tuples from 4-simplex edge tuples. The proof is a one-line decidability check.
Claim. The number of elements of $\{0,\ldots,5\}$ is not equal to the number of elements of $\{0,\ldots,9\}$; equivalently $6 \neq 10$. In context, 3D edge data are maps $\mathrm{Fin}\,6 \to \mathbb{R}$ while 4D edge data are maps $\mathrm{Fin}\,10 \to \mathbb{R}$.
background
A $d$-simplex has $\binom{d+1}{2}$ edges. In three spatial dimensions the elementary cell is a tetrahedron (3-simplex), so edge data are 6-tuples; in four dimensions the 4-simplex carries 10 edges. The module packages Gap-6 lookalike separation certificates: positive theorems that a 3D Lorentzian continuation (or other decoy) holds on its own domain, together with a witness that it does not discharge the 4D Wick action continuation.
Recognition Science forces spatial dimension $D=3$ (T8/T9). Edge-tuple algebra on the 3-simplex is therefore the native discrete geometry for the gravity ledger, while 4D edge data live on a strictly larger index set. The sibling vertex-cardinality inequality plays the same role for vertices ($4 \neq 5$).
This declaration is pure finite-type arithmetic; it does not invoke the J-cost, the Recognition Composition Law, or the phi ladder. It only records that the two edge-index types are inequivalent.
proof idea
One-line wrapper: decide closes the goal because both sides are concrete natural numbers (Fintype.card (Fin n) = n), and inequality of numerals is decidable. No lemmas from the gravity stack are applied.
why it matters
Feeds the structure lorentzianContinuation3DNotAction4DCertificate, which packages the banked 3D Lorentzian continuation together with vertex- and edge-cardinality mismatches and a reflexivity witness. That certificate is the post-close separation proof that the 3D lookalike does not discharge wick_action_continuation_4d_v2 (domain mismatch on edge tuples).
In the Wave C4 Gap-6 residual DAG, lookalikes must be retained as positive mathematics while being certified not to close the 4D action-level claim. Edge-count separation is the elementary combinatorial half of that argument; it aligns with the framework landmark that spatial dimension is forced to $D=3$, so 3-simplex edge data cannot silently stand in for 4-simplex data.
No open scaffolding remains here: the theorem is fully proved with no sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.