V
plain-language theorem explainer
Names the vertex set of the two-cube Freudenthal strip as the finite type with twelve elements. Two unit cubes glued on a square face have eight plus eight vertices with four identified, hence twelve. Geometry and incidence lemmas in this module index vertices by this type; anyone citing the multi-cube strip uses it as the ambient vertex universe.
Claim. Write $V$ for the finite set of cardinality $12$, i.e. the vertex set of the two-cube strip (two unit cubes sharing one square face).
background
The module builds the smallest nontrivial multi-cube Freudenthal example: two unit cubes sharing one square face, each cut into six Freudenthal tetrahedra with matching face triangulation. After identifying the shared face, the vertex count is $8+8-4=12$.
This abbreviation is the ambient vertex type for that complex. Sibling abbreviations introduce edges, tetrahedra, and incidence maps (edge endpoints, local-to-global square edges, tetrahedron vertex tuples). The goal of the module is a global local-edge-slot partition after deduplicating the five shared-face edges, the first concrete multi-cube incidence instance beyond the one-cube check.
(The import graph may also surface an unrelated V from the circle-winding chain, the standard $2$-simplex vertex map; that is a name collision, not a dependency of this geometry type.)
proof idea
Definitional abbreviation only: V is definitionally Fin 12. No proof obligations, tactics, or lemmas.
why it matters
Supplies the vertex universe for every incidence statement in the two-cube strip (edges, tetrahedra, local-versus-global square edges, edge-in-tet characterizations). Without a fixed finite vertex type, the global local-edge-slot partition after face deduplication cannot even be stated.
In the broader Recognition geometry stack this is the first multi-cube incidence scaffold beyond the single-cube sanity check, a concrete step toward gluing Freudenthal triangulations across cubes. Downstream Hamiltonian and Noether hits that mention a symbol V are potential-energy maps $\mathbb{R}\to\mathbb{R}$, not this finite type; treat those edges as name collisions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.