module module moderate

`IndisputableMonolith.Geometry.PeriodicFreudenthalTorus4D`

Defines the typed 4D periodic Freudenthal torus: vertices as 4-tuples of ZMod N, one-step bit translations along each coordinate, and cancellation/injectivity lemmas for those steps. Gravity and seven-gaps authors cite it as the 4D carrier skeleton for period-doubling maps. Content is mostly definitions plus short algebraic lemmas on modular bit flips.

claimThe module introduces the 4D periodic Freudenthal carrier: vertices $V_4(N) = (\mathbb{Z}/N\mathbb{Z})^4$, coordinate bit values in $\{0,1\}$, and one-step translations $\mathrm{addBit}_i$ that add a bit along the $i$-th axis mod $N$. It proves cancellation and injectivity facts for these steps when $1 < N$, including that agreeing one-step images force equal bits.

background

Recognition Science uses discrete toroidal carriers to stage metric refinement and period-doubling between successive lattice levels. The 3D Freudenthal torus already supports the Gap-2 period-doubling track; this module is the matching 4D typed carrier.

Vertices are 4-tuples over $\mathbb{Z}/N\mathbb{Z}$. A bit is a boolean treated as $0$ or $1$ in the ring. The primitive move is adding a bit to one coordinate (mod $N$). Sibling lemmas record how true/false bits compose, that a true step is never the identity when $1 < N$, and that two-step bit paths are nontrivial.

The local cancellation fact (if two one-step bit translations of the same coordinate agree, the bits agree for $1 < N$) is the 4D copy of the corresponding 3D lemma. Together these give a clean skeleton for level-to-level maps without continuum geometry.

proof idea

This is primarily a definition-and-lemmas module, not a single deep theorem. It fixes Vertex4 and the bit/addBit API, then proves a cluster of short facts by modular arithmetic and case splits on booleans: false is a no-op, true is $v \mapsto v+1$ on one axis, true steps are injective and not the identity for $N > 1$, and two successive bit steps cannot be the identity. The cancellation lemma is the 4D analogue of the 3D one-step uniqueness argument: equal images after adding bits on the same coordinate force the bits equal when $1 < N$.

why it matters in Recognition Science

Downstream, Gravity.SevenGaps.Gap2FreudenthalPeriodDoubling4D imports this module as the typed 4D carrier for the Gap-2 period-doubling track. That file is the 4D mirror of the 3D Gap-2 construction and supplies level-to-level maps (including the mod-$N$ vertex projection) that a 4D MetricRefinementFamily needs at the typed skeleton.

In the broader RS geometry stack, the Freudenthal torus is the discrete stage on which octave/period structure and refinement between rungs are made rigorous before continuum limits. The 4D copy keeps the same bit-step algebra while matching the spacetime dimension forced elsewhere in the forcing chain ($D = 3$ spatial plus time, or the 4D carrier used by the gravity gaps). Without these injectivity and cancellation facts, period-doubling maps on vertices would not be well-defined or invertible at the skeleton level.

scope and limits

Does not construct continuum metrics or Riemannian structure on the 4-torus.
Does not prove the full Gap-2 period-doubling theorem; only the carrier API.
Does not force $N$ or identify physical lattice spacing with $\phi$-rungs.
Does not treat dimensions other than 4; 3D lives in a sibling module.
Does not define the MetricRefinementFamily; downstream modules consume this skeleton.

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2FreudenthalPeriodDoubling4D module_import

declarations in this module (69)

def bit L48
def addBit L52
theorem addBit_false L55
theorem addBit_true_eq_mk L60
theorem addBit_false_after_true L65
theorem addBit_true_after_false L69
theorem addBit_true_ne_self L73
theorem addBit_true_injective L89
theorem addBit_injective L120
theorem addBit4_cancel L129
theorem two_bit_steps_ne_id L155
abbrev Vertex4 L187
def addBits4 L190
theorem addBits4_injective L193
theorem addBits4_cancel_offsets L204
def dispBits4 L224
theorem dispBits4_ne_zero L241
theorem dispBits4_injective L246
theorem displacement_classes_are_fifteen L252
def vertexBits4 L263
theorem vertexBits4_injective L281
def addVertexBits4 L285
theorem addVertexBits4_injective L289
structure PeriodicEdge4 L299
theorem card_vertex4 L330
def periodicEdge4EquivProd L336
theorem card_periodicEdge4 L345
def kuhnVerts L361
def edgeSlotPair L486
def kuhnEdgeBase L501
def kuhnEdgeDisp L748
abbrev PeriodicSimplex4 L993
theorem card_periodicSimplex4 L997
theorem kuhn_simplex_count_per_cube L1004
theorem kuhnVerts_zero L1009
theorem kuhnVerts_four L1013
theorem kuhnVerts_label_injective L1017
def localEdgeOf4 L1022
def kuhnCornerAt L1027
theorem localEdgeOf4_endpoints_match_kuhnVerts L1037
theorem kuhn_corners_injective L1050
def pairSlot4 L1071
theorem pairSlot4_spec L1085
def vertexFinEquiv4 L1095
def edgeFinEquiv4 L1100
def simplexFinEquiv4 L1105
def canonicalEdgeVerts4 L1111
def canonicalSimplexVerts4 L1121
def sameUnorderedPair4 L1131
structure Carrier4D L1138
def IsSimplicial4D L1149
def canonicalCarrier4D L1159
theorem canonicalCarrier4D_nV L1167
theorem canonicalCarrier4D_nE L1172
theorem canonicalCarrier4D_nS L1177
theorem canonicalCarrier4D_no_loops L1181
theorem endpoints_injective4 L1192
theorem reverse_impossible4 L1215
theorem canonicalCarrier4D_no_multiedges L1240
theorem canonicalCarrier4D_simplex_injective L1270
theorem canonicalCarrier4D_skeleton L1284
theorem canonicalCarrier4D_isSimplicial L1321
def dispWeight4 L1331
def periodicDispSqEdge4 L1350
theorem dispWeight4_le_four L1353
theorem periodicDispSqEdge4_le_four L1356
def meshVal4D L1364
theorem meshVal4D_pos L1367
theorem meshVal4D_attained L1373