Gravity Seven Gaps Path Sum Probes Translation Aut Three Injective

Translations as relabelings

A torus is a surface shaped like the surface of a doughnut, and a periodic grid on it repeats its pattern endlessly in every direction. The framework's library, a machine-checked collection of formal theorems, builds a specific finite torus at side length N, with N cubed vertices, 7 times N cubed edges, and 6 times N cubed tetrahedra. A translation is a shift: move every vertex, edge, and tetrahedron by the same fixed amount, wrapping around the torus. The declaration translationAut_three_injective proves, for the concrete side length 3, that two different shifts always produce two different relabelings of the grid. No two distinct shifts collapse into the same rearrangement.

The proof is general before it is concrete. The library first proves the injectivity for any side length N, then applies it to N equals 3. This single fact has a sharp consequence: the torus has at least 27 distinct relabelings, one for each of the 27 possible shifts on a 3 by 3 by 3 grid. The proof also shows that the zero shift is the identity relabeling and that composing two shifts corresponds to adding their shifts. These are the standard properties that make the shifts a genuine group of symmetries.

In Recognition Science, this result is a landmine check for a larger program. The framework studies path sums over such grids, sums of complex weights attached to each tetrahedron. A future claim might assert that a particular unnormalized contribution from the torus is nonvanishing or dominant. The injectivity result forbids that claim unless it accounts for a suppression: the contribution's modulus is at most 1 over N cubed, which for N equals 3 is at most 1 over 27. Because the translations embed as distinct relabelings, the averaging over all relabelings can cancel the contribution entirely, potentially reducing it to zero. The honest status flag records this: translations embed, but unnormalized torus claims are not admissible without explicit suppression accounting.

The declaration does not claim that the torus image is simplicial, nor that any measure, limit, or path sum has a particular value. It does not claim that the translations are the only relabelings, only that they are distinct ones. It does not assert anything about the continuum limit or about the behavior of the path sums as N grows. The result is a precise, narrow fact about finite combinatorics, and its value is in the constraint it places on future reasoning.

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

/-- The embedding is injective at the concrete side `N = 3`. -/
theorem translationAut_three_injective :
    Function.Injective (translationAut 3) := translationAut_injective 3

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

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

/-- Projection of `translationAut` onto its tet permutation. -/
theorem translationAut_tEquiv (N : ℕ) [NeZero N] (t : Vertex N N N) :
    (translationAut N t).tEquiv =
      (tetFinEquiv N N N).trans
        ((translateTet t).trans (tetFinEquiv N N N).symm) := rfl

/-- Projection of `translationAut` onto its edge permutation. -/
theorem translationAut_eEquiv (N : ℕ) [NeZero N] (t : Vertex N N N) :
    (translationAut N t).eEquiv =
      (edgeFinEquiv N N N).trans
        ((translateEdge t).trans (edgeFinEquiv N N N).symm) := rfl

What this page does not claim

The torus image is simplicial. Any measure, limit, or path sum has a particular value. The translations are the only relabelings of the torus. The path sums behave in any specific way as N grows.

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: