Gravity Seven Gaps Path Sum Probes Freudenthal Bounded Complex Edge Verts

The edge incidence fact

A triangulation of a three-dimensional grid is a way of chopping a cube into tetrahedra, the simplest three-dimensional solids. The canonical periodic Freudenthal triangulation is a specific, standard way to do this chopping on a torus, a space that wraps around on itself. It has N³ vertices, 7N³ edges, and 6N³ tetrahedra for a grid of side length N, and each edge connects exactly two vertices. The declaration freudenthalBoundedComplex_edgeVerts is a machine-checked theorem stating that when this triangulation is placed into a coarser state space called BoundedComplex, a discrete record of geometric objects with limited structure, the edge-to-vertex incidence map is preserved exactly. In plain terms, every edge in the torus triangulation still connects the same two vertices after the embedding, with no ambiguity or loss.

This preservation matters because the coarser state space is designed for a different purpose: it carries path sums, which are weighted counts of geometric configurations. The theorem is one of two "probes" that attach the torus to this state space. The other probe shows that the torus's translation symmetries, the shifts that move the grid by whole steps, embed into the relabeling automorphisms of the embedded complex. This embedding is injective, meaning distinct translations give distinct relabelings, and it forces a concrete bound: the number of automorphisms is at least N³, and the normalized weight of the torus contribution is at most 1/N³. The edge incidence theorem is the structural backbone that makes these symmetry arguments coherent, because a relabeling must respect which vertices each edge touches.

The declaration is deliberately narrow. It does not claim that the embedded complex is simplicial, meaning that its tetrahedra meet only along shared faces. That property is not proved here and is not asserted. The coarser state space also drops information: it has no record of which edge slots belong to which tetrahedron, and it treats each tetrahedron as equilateral by convention, discarding the original squared-edge geometry. The theorem does not compute any path sum, does not assign a measure or limit to any configuration, and does not say anything about the value of any contribution. Its role is purely structural: it certifies that the edge incidence data survives the embedding, so that later work on path sums can rely on that fact without rechecking it.

What the theorem changes is the trust boundary of the framework's library. Because the edge incidence fact is machine-checked, any future claim that uses the embedded torus's edge structure can cite it as a proven foundation. The honest limits are equally explicit: the lack of simpliciality proof and the dropped tetrahedron data are recorded as known gaps, not hidden. This is the framework's method in miniature: prove what can be proved exactly, state what cannot be proved yet, and let the boundary between the two be visible.

/-- Edge-endpoint incidence is inherited verbatim from the canonical
encoder. -/
theorem freudenthalBoundedComplex_edgeVerts (N : ℕ) [NeZero N] :
    (freudenthalBoundedComplex N).edgeVerts = canonicalEdgeVerts N N N := rfl

/-- Vertex count of the embedded torus: `N ^ 3`. -/
theorem freudenthalBoundedComplex_nV (N : ℕ) [NeZero N] :
    (freudenthalBoundedComplex N).nV = N ^ 3 := card_vertex N

/-- Edge count of the embedded torus: `7 * N ^ 3` (the cap is met exactly). -/
theorem freudenthalBoundedComplex_nE (N : ℕ) [NeZero N] :
    (freudenthalBoundedComplex N).nE = 7 * N ^ 3 := card_periodicEdge N

/-- Tetrahedron count of the embedded torus: `6 * N ^ 3`. -/
theorem freudenthalBoundedComplex_nT (N : ℕ) [NeZero N] :
    (freudenthalBoundedComplex N).nT = 6 * N ^ 3 := card_periodicTet N

/-- **LANDMINE, count form.**  `|Aut(T_N)| ≥ N ^ 3`. -/
theorem autCard_ge_translations (N : ℕ) [NeZero N] :
    N ^ 3 ≤ Nat.card (Aut (freudenthalBoundedComplex N)) := by
  have h := Nat.card_le_card_of_injective (translationAut N)
    (translationAut_injective N)
  rwa [Nat.card_eq_fintype_card, card_vertex] at h

/-- **PROBE C3.**  The canonical periodic Freudenthal torus at side `N` as
an element of the path-sum state space at cap `B = 7 * N ^ 3`.  Counts and
both incidence maps are inherited verbatim from
`canonicalPeriodicTriangulation N N N`; the `edgeInTet` slot assignment and
the per-tet metric are dropped (shape mismatch, recorded in the module
docstring and `pathSumProbesStatus`). -/
noncomputable def freudenthalBoundedComplex (N : ℕ) [NeZero N] :
    BoundedComplex (7 * N ^ 3) where
  nV := Fintype.card (Vertex N N N)
  nE := Fintype.card (PeriodicEdge N N N)
  nT := Fintype.card (PeriodicTet N N N)
  hV := by
    rw [card_vertex]
    calc N ^ 3 = 1 * N ^ 3 := (one_mul _).symm
      _ ≤ 7 * N ^ 3 := Nat.mul_le_mul (by norm_num) (le_refl _)
  hE := le_of_eq (card_periodicEdge N)
  hT := by
    rw [card_periodicTet]
    exact Nat.mul_le_mul (by norm_num) (le_refl _)
  edgeVerts := canonicalEdgeVerts N N N
  tetVerts := canonicalTetVerts N N N

/-- Outcome record for probes C3 and C6.  No `True` shells; every flag is
forced by `rfl` below. -/
structure ProbeStatus where
  torus_attached_to_state_space : Bool
  counts_and_incidence_preserved : Bool
  edge_in_tet_slots_preserved : Bool
  per_tet_metric_preserved : Bool
  simpliciality_of_image_proved : Bool
  translations_embed : Bool
  unnormalized_mu_torus_claims_admissible : Bool

What this page does not claim

The theorem does not compute or bound the value of any path sum. The theorem does not assert that the embedded complex is simplicial. The theorem does not preserve the per-tetrahedron metric or edge-in-tetrahedron slot data.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/PathSumProbes.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: