module module moderate

`IndisputableMonolith.Gravity.SevenGaps.PathSumProbes`

Wires the periodic Freudenthal torus into the path-sum BoundedComplex interface at finite side length N. Records exact vertex, edge, and tetrahedron counts (vertices N^3) and a match to the canonical triangulation. Cited by the Seven Gaps torus class-mass gate. Arguments are Fintype cardinalities and structure-preserving equivalences from the periodic model.

claimFor side length $N\in\mathbb{N}$, the periodic Freudenthal vertex set has cardinality $N^3$. The module builds a bounded complex $\mathrm{BC}_N$ from the periodic torus model, records $n_V(\mathrm{BC}_N)=N^3$, $n_E$, $n_T$ with $n_T>0$, and supplies edge and tetrahedron vertex maps that match the canonical triangulation used by the path-sum measure.

background

The Seven Gaps program evaluates a path-sum measure for $Z_{RS}$ on finite incidence data. Upstream, PathSumMeasure introduces the scoped class of bounded complexes: each carries bounded vertex/edge/tetrahedron incidence and is a Fintype via an explicit code equivalence, so configuration sums are well-defined finite sums.

Separately, PeriodicFreudenthalTorus defines the scalable target shape for a periodic Freudenthal tiling. It gives typed periodic vertex, edge, and tetrahedron sets and proves that any finite 3D triangulation encoding this model admits the global incidence-edge-slot partition required by the nonlinear Regge first-variation theorem. It does not yet pin a concrete $N\times N\times N$ mesh.

This module sits between those two layers. It instantiates the torus model at finite side $N$ and packages the result as a bounded complex, so path-sum probes can run on Freudenthal geometry with known cardinalities.

proof idea

Definition-heavy bridge module, not a single deep theorem. It constructs the bounded complex from the periodic torus vertex/edge/tet data, then proves a short stack of cardinality and interface lemmas: vertex count $N^3$ from the product structure of the periodic vertex set; edge and tetrahedron counts via explicit equivalences (including a product form for periodic edges); positivity of the tetrahedron count; and agreement of edge and tet vertex maps with the canonical triangulation. Those facts discharge the BoundedComplex obligations expected by the path-sum measure.

why it matters in Recognition Science

Direct input to FreudenthalTorusClassMass, the Crux-2 consistency gate on torus class mass (labeled versus class) under the locked QUOTIENT_BOOKKEEPING protocol. That gate needs the $N^{-3}$ scaling of the class summand in the pushforward form; the scaling rests on the vertex count $N^3$ and on having the periodic torus packaged as a bounded complex with matching canonical incidence.

In the broader Recognition Gravity lane, the module connects discrete Regge geometry (Freudenthal tiling, incidence partitions) to the proved path-sum measure for $Z_{RS}$. Without these probes, the class-mass comparison has no finite complex on which to evaluate labeled versus quotient sums.

scope and limits

Does not prove the path-sum measure or Fintype instance for general bounded complexes.
Does not establish class-mass suppression of order $N^{-3}$ (downstream gate).
Does not treat non-cubic, aperiodic, or continuum meshes.
Does not derive continuum gravity or Regge equations of motion.
Does not fix a numerical side length $N$; results are parametric in $N$.

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.FreudenthalTorusClassMass module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.PeriodicFreudenthalTorus module_import
IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure module_import

declarations in this module (50)

theorem card_vertex L76
def periodicEdgeEquivProd L84
theorem card_periodicEdge L92
theorem card_periodicTet L99
def freudenthalBoundedComplex L118
theorem freudenthalBoundedComplex_nV L135
theorem freudenthalBoundedComplex_nE L139
theorem freudenthalBoundedComplex_nT L143
theorem freudenthalBoundedComplex_nT_pos L147
theorem freudenthalBoundedComplex_edgeVerts L156
theorem freudenthalBoundedComplex_tetVerts L161
theorem freudenthalBoundedComplex_matches_canonical L169
def translateVertex L192
theorem translateVertex_apply L203
def translateEdge L208
theorem translateEdge_apply L214
def translateTet L220
theorem translateTet_apply L224
theorem addBit_add_right L229
theorem addBits_add_right L237
theorem addVertexBits_add_right L249
theorem translateEdge_endpoints L256
theorem translateVertex_zero L268
theorem translateEdge_zero L276
theorem translateTet_zero L284
theorem translateVertex_trans L292
theorem translateEdge_trans L300
theorem translateTet_trans L308
theorem conj_refl L319
theorem conj_trans L327
def translationAut L341
theorem translationAut_vEquiv L402
theorem translationAut_eEquiv L408
theorem translationAut_tEquiv L414
theorem refl_eEquiv L420
theorem refl_tEquiv L424
theorem translationAut_zero L428
theorem translationAut_add L443
theorem translationAut_injective L456
theorem translations_embed_in_aut L479
theorem translationAut_ne_refl L488
theorem autCard_ge_translations L495
theorem mu_freudenthal_le_inv_cube L503
theorem unnormalized_torus_weight_suppressed L520
theorem translationAut_three_injective L531
theorem autCard_ge_27 L535
theorem nontrivial_aut_three L544
structure ProbeStatus L553
def pathSumProbesStatus L566
theorem pathSumProbesStatus_flags L575