module module high

`IndisputableMonolith.Geometry.PeriodicFreudenthalTorus`

Defines the vertex set and bit-arithmetic of the periodic cubic lattice that carries the Freudenthal six-tetrahedron triangulation. Gravity continuum-limit, Dirichlet-instance, path-sum, and tensor-shear modules import this scaffold for exact stencil bookkeeping on the torus. Content is combinatorial: vertices as bit patterns, unit displacements by bit flips, and elementary identities for those operations.

claimThe module equips a periodic cubic lattice with vertices labeled by bit-strings and with displacement maps that add unit edge bits (modulo the torus identification), so that the Freudenthal six-tetrahedron decomposition of the unit cube extends by periodicity.

background

Recognition Science gravity work needs an exact discrete geometry on which continuum limits of quadratic actions can be stated without mesh ambiguity. The upstream Freudenthal module fixes the standard six-tetrahedron split of one unit cube along the body diagonal from binary vertex $0$ to vertex $7$, with cube corners labeled by three-bit coordinates.

This module lifts that single-cube incidence data to a periodic cubic torus: vertices remain bit-labeled lattice points, and translation by a cube edge is realized by flipping or adding the corresponding bit. Sibling definitions package single-bit and multi-bit displacements, together with elementary equalities (adding false is identity, true after false, non-fixed-point of a true flip, and so on).

The local setting is pure combinatorial geometry. No metric, measure, or continuum claim is made here; the torus is only the carrier for later stencil and path-sum constructions.

proof idea

This is primarily a definition module. It introduces the vertex type and bit-level displacement operations, then proves short algebraic identities (identity under false bits, commutation patterns of true/false flips, self-inequality after a true flip, and multi-bit variants) by direct case analysis on booleans and constructors. There is no deep geometric argument; the lemmas are bookkeeping facts that downstream stencil code can rewrite against.

why it matters in Recognition Science

The module is the shared periodic carrier for several gravity tracks. FreudenthalStencilPreflight uses it for exact general-$N$ stencil identities and moment tensors in the QG Phase 2b continuum-limit campaign. PhysicalSixTetCubicDirichletInstance packages theorem obligations that instantiate the physical six-tet Dirichlet model on this torus. SevenGaps.PathSumProbes records cheap honest facts linking the canonical periodic Freudenthal torus to scoped path-sum state spaces (probes only). TensorShearSector needs the same vertex lattice when extending beyond the conformal scalar ansatz toward shear and transverse-traceless modes.

In the broader RS geometry stack it sits above the single-cube Freudenthal triangulation and below action-level and path-sum gravity modules; it does not itself touch the T0–T8 forcing chain or the J-cost functional.

scope and limits

Does not assert any continuum limit, measure, or path-sum value.
Does not prove physical Dirichlet equality; only supplies the periodic vertex scaffold.
Does not encode metric edge lengths, shear modes, or weak-field gravity dynamics.
Does not extend the Freudenthal split beyond cubic periodicity and bit displacements.
Does not claim uniqueness of the six-tet decomposition among all triangulations.

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight module_import
IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance module_import
IndisputableMonolith.Gravity.SevenGaps.PathSumProbes module_import
IndisputableMonolith.Gravity.TensorShearSector module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.FreudenthalCubeTriangulation module_import

declarations in this module (59)

abbrev Vertex L28
def bit L30
def addBit L34
theorem addBit_false L37
theorem addBit_true_eq_mk L42
theorem addBit_false_after_true L47
theorem addBit_true_after_false L51
theorem addBit_true_ne_self L55
def addBits L71
def dispBits L76
def vertexBits L86
def addVertexBits L96
theorem addBit_true_injective L101
theorem addBit_injective L132
theorem addBits_injective L139
theorem addVertexBits_injective L150
theorem addVertexBits_surjective L158
theorem existsUnique_addVertexBits_eq L164
theorem sum_ite_eq_of_addVertexBits L175
structure PeriodicEdge L195
def cubeEdgeBase L241
def cubeEdgeDisp L264
def localEdgeOf L287
abbrev PeriodicTet L295
def vertexFinEquiv L300
def edgeFinEquiv L306
def tetFinEquiv L312
def canonicalEdgeSlot L318
theorem canonicalEdgeSlot_eq_some_implies L330
theorem canonicalEdgeSlot_eq_some_of_noDup L354
def canonicalEdgeVerts L387
def canonicalTetVerts L399
def canonicalEdgeInTet L408
theorem canonicalEdgeInTet_eq_some_implies L415
def CanonicalPeriodicLocalEdgeNoDup L427
theorem canonicalPeriodicLocalEdgeNoDup L432
theorem canonicalEdgeInTet_iff_of_noDup L440
def periodicDispSqEdge L459
def canonicalGlobalSqEdge L468
theorem freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf L473
theorem canonicalLocalSqEdge_eq_global L484
theorem canonicalLocalEdge_complete L497
def canonicalPeriodicTriangulation L515
def canonicalPeriodicEdgeEquiv L526
def canonicalPeriodicTetEquiv L532
def CanonicalPeriodicEndpointIncidence L542
theorem localEdgeOf_endpoints_match_tetVerts L552
theorem canonicalPeriodicEndpointIncidence L569
def canonicalPeriodicIncidenceConsistent_of_endpoint L590
def canonicalPeriodicIncidenceConsistent L610
structure EncodedPeriodicFreudenthalTorus L620
def canonicalEncodedPeriodicFreudenthalTorus_of_incidence L635
def canonicalEncodedPeriodicFreudenthalTorus_of_endpoint L652
def canonicalEncodedPeriodicFreudenthalTorus L661
theorem canonicalEncodedPeriodic_K_tetVerts_eq L668
theorem canonicalEncodedPeriodic_tetEquiv_eq L677
theorem canonicalEncodedPeriodic_tetVerts_addVertexBits L685
def edgeSlotPartition_of_encodedPeriodicFreudenthalTorus L700
def edgeSlotBookkeeping_of_encodedPeriodicFreudenthalTorus L717