Gravity Seven Gaps Path Sum Probes Freudenthal Bounded Complex N T

The torus embedding

The declaration freudenthalBoundedComplex_nT is a theorem in the framework's machine-checked library of formal theorems. It states that the number of tetrahedra in a certain periodic triangulation, packaged as a bounded complex, equals 6 times the cube of the side length N. For a torus built from N subdivisions along each axis, this is the expected count: each cube of the grid splits into 6 tetrahedra, and there are N³ cubes. The proof is symbolic for any positive N and uses no unproved assumptions.

This theorem is one of three counting facts that together attach the canonical periodic Freudenthal torus to the path-sum state space. The other two establish the vertex count N³ and the edge count 7N³. The embedding preserves the incidence maps that record which edges meet which vertices and which tetrahedra meet which corners. These maps are definitionally equal to those of the canonical triangulation, so the combinatorial skeleton of the torus survives the packaging.

In Recognition Science, this packaging is a probe, not a physical claim. The path-sum state space, a discrete record of possible geometric configurations, receives the torus as an element. The probe records that the torus fits into this space and that its translations embed as relabeling automorphisms. That embedding implies the automorphism group has at least N³ elements, which in turn bounds any unnormalized torus contribution by 1/N³. This is a landmine check: future claims that a torus summand dominates must account for this suppression.

The declaration does not claim that the image is simplicial, that any measure or limit exists, or that any path sum has a particular value. The bounded complex drops the edge-in-tetrahedron assignment and the per-tetrahedron metric, so the equilateral geometry is a modeling convention, not a proved property. The probe status flags record these omissions honestly: translations embed, but unnormalized torus claims are inadmissible without explicit suppression accounting.

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

/-- 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

/-- **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

What this page does not claim

The image of the torus is simplicial. Any measure, limit, or path sum value is established. The per-tetrahedron metric is preserved by the embedding.

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: