Gravity Seven Gaps Path Sum Probes Unnormalized Torus Weight Suppressed

The suppression bound

In the Recognition Science framework's study of gravity, path sums are built from contributions attached to geometric objects. One family of such objects is a periodic torus, a three-dimensional grid that wraps around on itself like a video game screen. The declaration unnormalized_torus_weight_suppressed is a theorem about how large one such contribution can be. It proves that the modulus of the μ-weighted unitary torus summand is at most 1 / N³, where N is the side length of the torus grid. As N grows, this bound shrinks rapidly: for N = 10, the contribution is at most one thousandth.

The proof works by counting symmetries. The framework's library shows that the translation group Z_N³, which shifts the torus grid by whole steps in each direction, embeds into the automorphism group of the torus image. This means there are at least N³ distinct relabelings of the torus that leave its structure unchanged. A standard argument then bounds the weight of any single contribution by the reciprocal of the number of symmetries. The theorem autCard_ge_translations establishes the count, and freudenthalBoundedComplex turns it into the bound on the weight.

The declaration is explicitly a probe, not a claim about the value of any path sum. It says nothing about measures, limits, or continuum behavior. It does not assert that the contribution is nonvanishing or dominant; in fact, the proof is a warning that any future claim of dominance must account for this suppression, because the contribution could be exactly zero. The library records this as a landmine check: the boolean flag unnormalized_mu_torus_claims_admissible is set to false, meaning such claims are not admissible without further work.

The practical consequence is a constraint on the framework's own future. Any attempt to build a path-sum argument that relies on the unnormalized torus contribution must either work within the 1/N³ bound or explicitly justify why the suppression does not apply. The theorem does not say the contribution is small in any physical sense; it says the contribution is bounded in a way that any honest argument must respect. This is a negative result that clears the ground: it rules out a class of claims before they are made.

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

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

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

What this page does not claim

The theorem does not assert any value for the path sum itself. It does not claim the torus contribution is nonvanishing or dominant. It does not establish any physical measure or limit.

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: