Gravity Analysis Freudenthal Stencil Preflight Stencil Moment Tensor Off Diag Po

The off-diagonal entry

The declaration stencilMomentTensor_offDiag_pos is a theorem in a machine-checked library of formal theorems. It concerns a stencil, a fixed pattern of neighboring points used to approximate a derivative or an energy on a grid. The theorem states that, for the canonical Freudenthal triangulation of a three-dimensional grid with side length N greater than 2, a certain 3 by 3 matrix called the moment tensor has strictly positive off-diagonal entries. In plainer terms, the matrix that summarizes how the discrete energy responds to small displacements is not diagonal, and its off-diagonal parts are not zero but positive.

To see why this matters, consider the moment tensor itself. It is defined as a sum over seven displacement classes: the three axis directions, the three face diagonals, and the one body diagonal. The weights in that sum are the square roots of the squared edge lengths, which are 1, 1, 1, 2, 2, 2, and 3. The theorem stencilMomentTensor_eq computes the result exactly: every diagonal entry is 1 + 2√2 + √3, and every off-diagonal entry is √2 + √3. The off-diagonal positivity follows immediately from the fact that √2 + √3 is greater than zero, a fact proved separately as sqrt_two_add_sqrt_three_pos.

This positivity has a direct consequence, proved as stencilMomentTensor_not_isotropic: the moment tensor is not a multiple of the identity matrix. That is, the discrete energy is anisotropic: it does not treat all directions equally. The spectrum of the tensor is 1 + √2 with multiplicity two and 1 + 4√2 + 3√3 along the body diagonal. This finding corrects an earlier expectation that the moment tensor might be rational and symmetric in a simpler sense; the exact entries live in the field ℚ[√2, √3], not in ℚ.

Within the Recognition Science framework, this theorem is part of a larger campaign to derive the continuum limit of a discrete gravitational action. The theorem itself does not claim that the continuum limit exists, nor that the discrete energy is isotropic, nor that the off-diagonal entries have any particular physical interpretation beyond being strictly positive. It establishes a precise algebraic fact about a specific discrete construction, and that fact constrains what the continuum limit can look like: it cannot be a simple Laplacian, which would be isotropic. The path-sum flag for the full theory remains red, meaning the sum over inequivalent triangulation classes is not yet defined.

/-- Off-diagonal entries of `A₀` are strictly positive (`√2 + √3`). -/
theorem stencilMomentTensor_offDiag_pos (i j : Fin 3) (hij : i ≠ j) :
    0 < stencilMomentTensor i j := by
  rw [stencilMomentTensor_eq, if_neg hij]
  simpa using sqrt_two_add_sqrt_three_pos

/-- EXACT value of the moment tensor:
`A₀ = (1 + √2)·I + (√2 + √3)·J` with `J` the all-ones matrix. Every
diagonal entry is `1 + 2√2 + √3`; every off-diagonal entry is `√2 + √3`.
The entries are irrational (in `ℚ[√2,√3]`); this is the exact
kernel-checked value. -/
theorem stencilMomentTensor_eq (i j : Fin 3) :
    stencilMomentTensor i j =
      (if i = j then 1 + Real.sqrt 2 else 0) + (Real.sqrt 2 + Real.sqrt 3) := by
  fin_cases i <;> fin_cases j <;>
    · norm_num [stencilMomentTensor, Fin.sum_univ_seven, dispReal,
        stencilWeight, periodicDispSqEdge, Real.sqrt_one]
      try ring

/-- FINDING (kernel-checked): the moment tensor is ANISOTROPIC. The
off-diagonal entry is `√2 + √3 > 0`, so `A₀ ≠ c·I` for every scalar `c`.
Isotropy is NOT claimed; the exact anisotropic value is
`stencilMomentTensor_eq`. -/
theorem stencilMomentTensor_not_isotropic (c : ℝ) :
    stencilMomentTensor ≠ fun i j => if i = j then c else 0 := by
  intro h
  have hne : (0 : Fin 3) ≠ 1 := by decide
  have h01 := congrFun (congrFun h 0) 1
  rw [if_neg hne] at h01
  exact absurd h01 (ne_of_gt (stencilMomentTensor_offDiag_pos 0 1 hne))

What this page does not claim

The theorem does not claim that the continuum limit of the discrete energy exists. The theorem does not claim that the off-diagonal entries have a specific physical meaning beyond being strictly positive. The theorem does not claim that the discrete energy is isotropic.

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/Analysis/FreudenthalStencilPreflight.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: