IndisputableMonolith.Geometry.FreudenthalTwoCubeStrip
Defines the combinatorial skeleton of the two-cube Freudenthal strip: two unit cubes glued along a face, each split into six tetrahedra by the standard body-diagonal triangulation. It fixes the vertex set, the 33 unique global edges, the tetrahedra, and the local-to-global edge incidence maps. Discrete geometers and anyone wiring lattice bookkeeping for Recognition geometry would cite it. Content is definitional incidence data plus short equivalence lemmas, extending the single-cube Freudenthal module.
claimLet the two-cube Freudenthal strip be two unit cubes identified along a common face, each decomposed into six tetrahedra by the Freudenthal triangulation along the body diagonal from vertex $0$ to vertex $7$. The module introduces the vertex set $V$, the set $E$ of $33$ distinct global edges, the tetrahedron collection $T$, and incidence data relating each tetrahedron's local edges to $E$.
background
The upstream single-cube module supplies the Freudenthal six-tetrahedron triangulation of the unit cube. Cube vertices are labeled by binary coordinates; the decomposition uses the body diagonal from vertex $0$ to vertex $7$ and packages the incidence bookkeeping (vertices, edges, tetrahedra) as a reusable combinatorial layer.
This module doubles that cell complex into a strip of two cubes glued along a face. Sibling definitions name the global vertex set $V$, edge set $E$, tetrahedron set $T$, edge endpoint maps, global square-edge labels, tetrahedron vertex lists, and the local-to-global edge correspondence. The doc line flags the main count: thirty-three unique global edges on the strip.
The setting is pure discrete geometry: finite labeled complexes and incidence predicates, not metric embedding or continuum limits. Notation stays combinatorial (edge membership in a tetrahedron, equality of local and global edge labels).
proof idea
This is largely a definition module. It introduces the strip's finite sets and incidence maps by extending the single-cube Freudenthal data across two cubes, then records a handful of short lemmas: membership of an edge in a tetrahedron is equivalent to the local-edge encoding; local square edges match the corresponding global labels; and edge-in-tetrahedron implies the expected vertex endpoints. No deep tactic proof is required beyond unfolding definitions and finite case checks on the labeled complex.
why it matters in Recognition Science
In the Recognition geometry stack the strip is the next combinatorial layer after the single-cube Freudenthal triangulation: it supplies a two-cell window on which edge and tetrahedron incidence can be stated uniformly. Downstream use is not yet wired in the graph (no recorded consumers), so the module presently closes the local bookkeeping gap rather than discharging a named forcing-chain theorem. It sits in the geometry domain that underpins discrete models of spatial structure (related at framework scale to the $D=3$ landmark), giving a concrete finite complex on which later recognition or defect-counting arguments can be stated without re-deriving cube gluing by hand.
scope and limits
- Does not prove metric or curvature properties of the strip.
- Does not embed the complex in continuum $\mathbb{R}^3$ with lengths.
- Does not treat strips longer than two cubes or periodic boundary conditions.
- Does not connect edge counts to physical constants or the forcing chain T0–T8.
- Does not claim completeness of any downstream Recognition theorem.
depends on (1)
declarations in this module (16)
-
abbrev
V -
abbrev
E -
abbrev
T -
def
edgeVerts -
def
globalSqEdge -
def
tetVerts -
def
localEdgeOf -
def
edgeInTet -
def
twoCubeStrip -
theorem
edgeInTet_iff_localEdgeOf -
theorem
local_sqEdge_eq_global -
theorem
edgeInTet_vertices -
theorem
localEdge_complete -
def
twoCubeStrip_incidenceConsistent -
def
twoCubeStrip_edgeSlotPartition -
def
twoCubeStrip_edgeSlotBookkeeping