Gravity Seven Gaps Path Sum Probes

Path-sum probes

A path-sum probe is a deliberately small, honest check inside a larger research program. The program studies gravity by summing over discrete geometries, and the probe asks a narrow question: when you attach a periodic grid to the state space of those sums, what symmetries survive, and what do they forbid? The answer, proved in a machine-checked library of formal theorems, is that the grid's translations embed into its relabeling automorphisms, and that embedding forces any unnormalized contribution from the grid to shrink at least as fast as 1/N³.

The object at the center is the canonical periodic Freudenthal torus, a standard triangulation of a 3-torus built from N³ vertices. The library packages it as a bounded complex, a finite cell complex with 7N³ edges and 6N³ tetrahedra, preserving the vertex, edge, and tetrahedron counts and their incidence maps. What it does not preserve is recorded honestly: the edge-in-tetrahedron slots and per-tetrahedron metrics are dropped because the scoped class does not carry them, and simpliciality of the image is not proved. Those are limitations, not hidden assumptions.

The substantive result concerns the translation group Z_N³. Each translation by a grid vector acts on vertices, edges, and tetrahedra, and the library proves this action is a relabeling automorphism of the torus image. The map from translations to automorphisms is injective, sends zero to the identity, and sends sums to composites. Consequently the automorphism group has at least N³ elements, and the measure of the torus in the path-sum state space is at most 1/N³. For any action, the modulus of the unnormalized unitary torus summand is bounded by 1/N³.

The punchline is a landmine record. Because the translations embed, any future claim that the unnormalized torus contribution is nonvanishing or dominant must be rejected as potentially 0 = 0 unless it explicitly accounts for the 1/N³ suppression. The status flags are rfl-forced: translations embed is true, and unnormalized mu torus claims admissible is false. The module makes no claim about measures, limits, continuum behavior, or the value of any path sum. It is a provenance record and a guardrail, not a result about gravity itself.

What the module changes is the vocabulary of future work. Researchers can no longer assert a torus contribution without facing the suppression bound. The proof is axiom-clean, with zero sorry and zero admit, and uses decide exactly once for a concrete finite inequality at N = 3. The general case is fully symbolic. For a reader, the lesson is that symmetry counting is not optional bookkeeping: it can kill a claim before any physics enters.

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

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

/-- `|Aut(T_3)| ≥ 27`. -/
theorem autCard_ge_27 :
    27 ≤ Nat.card (Aut (freudenthalBoundedComplex 3)) := by
  have h := autCard_ge_translations 3
  norm_num at h
  exact h

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

This module does not prove any value for a path sum, nor any statement about measures or limits. This module does not claim the torus image is simplicial. This module does not derive gravity from the path-sum state space; it only records a symmetry constraint on future claims.

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: