Gravity Seven Gaps Path Sum Probes Freudenthal Bounded Complex N E

The torus edge count

The declaration freudenthalBoundedComplex_nE is a proved theorem about a specific finite object: the canonical periodic Freudenthal torus at side length N, a standard three-dimensional grid wrapped around on itself. The theorem states that this torus, viewed as a bounded complex with a fixed number of vertices, edges, and tetrahedra, has exactly 7 * N^3 edges. The proof is machine-checked in the framework's library of formal theorems, with no gaps and no extra axioms beyond the ambient type theory's standard three.

The number itself has a concrete combinatorial meaning. The torus has N^3 vertices, arranged as a cube of N cells in each direction. Each vertex is the corner of several tetrahedra, and the edges connect these vertices along the grid lines. The factor 7 reflects the local geometry: in the periodic Freudenthal triangulation, each vertex is incident to 7 distinct edge directions, and the total count follows by multiplying the vertex count by this local degree and dividing by 2, since each edge has two endpoints. The theorem freudenthalBoundedComplex_nE proves this count directly, alongside companion theorems fixing the vertex count as N^3 and the tetrahedron count as 6 * N^3.

What the theorem does not claim is as important as what it proves. It does not assert anything about measures, limits, or the value of any path sum. It does not claim that the torus image is simplicial, meaning that its tetrahedra meet only along shared faces; that property is explicitly left unproved. It does not preserve the edge-slot-in-tetrahedron assignment of the original triangulation, because the bounded complex structure lacks a field for it, and it drops the per-tetrahedron metric geometry, modeling the complex as equilateral at a fixed scale by convention. The declaration is a provenance record: it attaches the torus to a larger state space and records the exact counts, nothing more.

In Recognition Science, this theorem is a probe in a larger investigation of path sums over gravitational configurations. The honest limitation matters because a later claim that a particular torus contribution dominates a path sum would need to account for the fact that the torus has many symmetries: the translation group of size N^3 embeds into its relabeling automorphisms, which suppresses any unnormalized contribution by at least 1/N^3. The edge count itself does not address that suppression; it is a building block, not a conclusion about the path sum's value.

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

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

/-- 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 prove any property of path sums, measures, or limits. The theorem does not establish that the torus image is simplicial. The theorem does not preserve the edge-slot-in-tetrahedron assignment or the per-tetrahedron metric geometry.

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: