Gravity Seven Gaps Path Sum Probes Freudenthal Bounded Complex N T Pos

A counting fact about a periodic grid

A tetrahedron is the simplest three-dimensional solid: four triangular faces, six edges, four corners. A recognition framework, a discrete record of events, sometimes needs to attach a geometric object to its abstract state space. The declaration freudenthalBoundedComplex_nT_pos proves one small counting fact about such an attachment: for any positive grid size N, the periodic Freudenthal complex contains 6 times N cubed tetrahedra, and that number is always greater than zero.

The Freudenthal complex is a standard way to subdivide a cube into tetrahedra. The framework's library, a machine-checked collection of formal theorems, builds a periodic version on an N by N by N grid. The declaration proves the tetrahedron count is 6N³, which is positive whenever N is at least 1. This is a combinatorial fact, a statement about counting discrete objects, not about geometry or physics.

The proof is fully verified: zero gaps, zero assumptions beyond the standard ones, and the count follows from the definition of the complex itself. The declaration also preserves the vertex and edge counts, N³ and 7N³, and the incidence maps that record which edges and tetrahedra touch which vertices. These match the canonical periodic triangulation exactly.

In Recognition Science, this counting fact acts as a probe. It attaches the periodic Freudenthal torus to the path-sum state space, a space of possible recognition sequences, and records that the attachment is well-defined. The declaration itself makes no claim about measures, limits, or the value of any path sum. It is a landmine check: a way to verify that the attachment does not accidentally collapse to nothing.

The consequence is that the attachment is not vacuous. The complex has a positive number of tetrahedra, so the state space has something in it. This is a necessary precondition for any future claim about the behavior of path sums on this space, though the declaration itself does not establish any such behavior.

/-- The embedded torus is not the empty configuration: it has tetrahedra. -/
theorem freudenthalBoundedComplex_nT_pos (N : ℕ) [NeZero N] :
    0 < (freudenthalBoundedComplex N).nT := by
  rw [freudenthalBoundedComplex_nT]
  have hN : 0 < N := Nat.pos_of_neZero N
  have h3 : 0 < N ^ 3 := pow_pos hN 3
  omega

/-- 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-corner incidence is inherited verbatim from the canonical
encoder. -/
theorem freudenthalBoundedComplex_tetVerts (N : ℕ) [NeZero N] :
    (freudenthalBoundedComplex N).tetVerts = canonicalTetVerts N N N := rfl

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

/-- The embedded torus is not the empty configuration: it has tetrahedra. -/
theorem freudenthalBoundedComplex_nT_pos (N : ℕ) [NeZero N] :
    0 < (freudenthalBoundedComplex N).nT := by
  rw [freudenthalBoundedComplex_nT]
  have hN : 0 < N := Nat.pos_of_neZero N
  have h3 : 0 < N ^ 3 := pow_pos hN 3
  omega

What this page does not claim

The declaration does not prove that the complex is simplicial. The declaration does not establish any property about measures, limits, or the value of any path sum. The declaration does not claim that the attachment is unique or that the complex is the only possible one.

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: