Encyclopedia Gravity Gravity Seven Gaps Path Sum Probes Freudenthal Bounded Complex Matches Canonical

ARTICLE 4 claims 3 theorems 1 model

Gravity Seven Gaps Path Sum Probes Freudenthal Bounded Complex Matches Canonical

A machine-checked proof attaches the canonical periodic Freudenthal torus to a path-sum state space, preserving its counts and incidence maps while honestly recording what the attachment drops.

Verify this page

The torus embedding

The Freudenthal triangulation is the standard way to slice a cube into tetrahedra, and the periodic version wraps that slicing onto a torus. The declaration freudenthalBoundedComplex_matches_canonical proves, in the framework's machine-checked library of formal theorems, that this torus can be embedded into a bounded complex, a finite combinatorial object that records vertices, edges, and tetrahedra. The embedding preserves the torus's essential structure: the counts of vertices, edges, and tetrahedra, and the incidence maps that say which vertices belong to which edges and tetrahedra.

The proof works for any side length N, where N is a positive integer. The torus has N³ vertices, 7N³ edges, and 6N³ tetrahedra, and the embedding matches these counts exactly. The incidence maps are definitionally equal to those of the canonical periodic triangulation, meaning the combinatorial identity of the torus is not altered by the embedding. This is the core content of the declaration: a precise, verified statement of structural preservation.

The declaration is deliberately narrow. It makes no claim about measures, limits, or continuum behavior, and it does not assign a value to any path sum. The embedding drops two pieces of information: the assignment of edges to tetrahedron slots, and the per-tetrahedron metric geometry. The bounded complex class is equilateral at a fixed scale by convention, so the squared-edge geometry of the torus is lost. The declaration also does not prove that the embedded image is simplicial, meaning the tetrahedra may overlap in ways the torus itself does not.

In Recognition Science, the embedding attaches the torus to a path-sum state space, a step toward probing sums over paths in this geometry. The declaration records an honest landmine check: the translation group of the torus embeds into its relabeling automorphisms, so any future claim that an unnormalized torus contribution is dominant must account for a suppression factor of at least 1/N³. The declaration proves the embedding and the group action, and it explicitly flags what it does not prove.

THEOREM freudenthalBoundedComplex · IndisputableMonolith/Gravity/SevenGaps/PathSumProbes.lean
freudenthalBoundedComplex · IndisputableMonolith/Gravity/SevenGaps/PathSumProbes.lean:112 
/-- **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
THEOREM freudenthalBoundedComplex_edgeVerts · freudenthalBoundedComplex_tetVerts · IndisputableMonolith/Gravity/SevenGaps/PathSumProbes.lean
freudenthalBoundedComplex_edgeVerts · IndisputableMonolith/Gravity/SevenGaps/PathSumProbes.lean:154 
/-- Edge-endpoint incidence is inherited verbatim from the canonical
encoder. -/
theorem freudenthalBoundedComplex_edgeVerts (N : ℕ) [NeZero N] :
    (freudenthalBoundedComplex N).edgeVerts = canonicalEdgeVerts N N N := rfl
freudenthalBoundedComplex_tetVerts · IndisputableMonolith/Gravity/SevenGaps/PathSumProbes.lean:159 
/-- Tetrahedron-corner incidence is inherited verbatim from the canonical
encoder. -/
theorem freudenthalBoundedComplex_tetVerts (N : ℕ) [NeZero N] :
    (freudenthalBoundedComplex N).tetVerts = canonicalTetVerts N N N := rfl
MODEL freudenthalBoundedComplex · IndisputableMonolith/Gravity/SevenGaps/PathSumProbes.lean
freudenthalBoundedComplex · IndisputableMonolith/Gravity/SevenGaps/PathSumProbes.lean:112 
/-- **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
THEOREM translationAut_injective · IndisputableMonolith/Gravity/SevenGaps/PathSumProbes.lean
translationAut_injective · IndisputableMonolith/Gravity/SevenGaps/PathSumProbes.lean:454 
/-- **Injectivity.**  Distinct translations give distinct relabelings: the
image vertex permutation of `t` recovers `t` at the origin. -/
theorem translationAut_injective (N : ℕ) [NeZero N] :
    Function.Injective (translationAut N) := by
  intro t s h
  have hv : (translationAut N t).vEquiv ((vertexFinEquiv N N N).symm 0) =
      (translationAut N s).vEquiv ((vertexFinEquiv N N N).symm 0) := by
    rw [h]
  rw [translationAut_vEquiv, translationAut_vEquiv] at hv
  have hv' : (vertexFinEquiv N N N).symm
      (translateVertex t ((vertexFinEquiv N N N)
        ((vertexFinEquiv N N N).symm 0))) =
    (vertexFinEquiv N N N).symm
      (translateVertex s ((vertexFinEquiv N N N)
        ((vertexFinEquiv N N N).symm 0))) := hv
  rw [Equiv.apply_symm_apply (vertexFinEquiv N N N), translateVertex_apply,
    translateVertex_apply] at hv'
  have h0 : (0 : Vertex N N N) + t = 0 + s :=
    (vertexFinEquiv N N N).symm.injective hv'
  rw [zero_add, zero_add] at h0
  exact h0

What this page does not claim

The declaration does not prove that the embedded torus image is simplicial. The declaration does not assign a value to any path sum or make claims about measures or limits. The declaration 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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND