Encyclopedia Gravity Gravity Analysis Freudenthal Stencil Preflight Stencil Moment Tensor Quadratic E

ARTICLE 4 claims 4 theorems

Gravity Analysis Freudenthal Stencil Preflight Stencil Moment Tensor Quadratic E

A machine-checked proof identifies the exact quadratic form of a discrete gravity energy, revealing it is not isotropic.

Verify this page

The stencil's moment tensor

The declaration establishes an exact identity for a 3x3 matrix called the moment tensor, which summarizes how a discrete approximation to a gravitational energy responds to small variations. The identity states that the quadratic form of this matrix, evaluated on any vector v, equals a sum over seven displacement directions. Each term is the square of the dot product between v and that direction, weighted by a coefficient. The coefficients are 1 for the three axis directions, the square root of 2 for the three face-diagonal directions, and the square root of 3 for the body-diagonal direction. This is a theorem, proved in the machine-checked library of formal theorems, not an assumption.

The theorem's content is that the quadratic form of the moment tensor equals this explicit sum of squares. From this identity, the library derives that the moment tensor is positive semidefinite, meaning the energy is never negative, and that it is not isotropic. Isotropy would mean the energy responds identically in all directions, like a perfect sphere. The exact value shows otherwise: the off-diagonal entries are strictly positive, so the energy has a preferred orientation. The matrix is therefore anisotropic, a finding that corrects an earlier expectation that it would be rational and symmetric in the simplest sense.

In Recognition Science, this result is part of a preflight check for a larger campaign. The framework models discrete spacetime as a triangulation, and the energy of a field configuration on that triangulation is a sum over edges. The theorem shows that this discrete energy, after a specific normalization, equals a stencil sum with the seven displacement classes. This is a stepping stone toward a continuum limit, where the discrete energy approaches a smooth quadratic form. The identity is derived for every side length N greater than 2, not just for a few small cases.

What the declaration does not claim is equally important. It does not claim that the continuum limit has been taken, nor that the full path-sum over triangulations is defined. The theorem concerns only the quadratic form of the frozen energy on one fixed triangulation family. It also does not claim that the moment tensor is isotropic; in fact, it proves the opposite. The result is a precise algebraic fact about a discrete energy, not a statement about the physical universe.

THEOREM stencilMomentTensor_quadratic_eq · IndisputableMonolith/Gravity/Analysis/FreudenthalStencilPreflight.lean
stencilMomentTensor_quadratic_eq · IndisputableMonolith/Gravity/Analysis/FreudenthalStencilPreflight.lean:325 
/-- Exact sum-of-squares decomposition of the moment-tensor quadratic form:
`vᵀ A₀ v = Σ_d c_d ⟨d, v⟩²`. This is the kernel-level PSD witness. -/
theorem stencilMomentTensor_quadratic_eq (v : Fin 3 → ℝ) :
    (∑ i : Fin 3, ∑ j : Fin 3, stencilMomentTensor i j * v i * v j) =
      ∑ d : Fin 7,
        stencilWeight d * (∑ i : Fin 3, dispReal d i * v i) ^ (2 : ℕ) := by
  simp only [stencilMomentTensor, Fin.sum_univ_three, Fin.sum_univ_seven,
    dispReal]
  ring
THEOREM stencilMomentTensor_psd · stencilMomentTensor_not_isotropic · IndisputableMonolith/Gravity/Analysis/FreudenthalStencilPreflight.lean
stencilMomentTensor_psd · IndisputableMonolith/Gravity/Analysis/FreudenthalStencilPreflight.lean:335 
/-- KERNEL-PROVED: the moment tensor `A₀` is positive semidefinite. -/
theorem stencilMomentTensor_psd (v : Fin 3 → ℝ) :
    0 ≤ ∑ i : Fin 3, ∑ j : Fin 3, stencilMomentTensor i j * v i * v j := by
  rw [stencilMomentTensor_quadratic_eq]
  refine Finset.sum_nonneg fun d _ => ?_
  exact mul_nonneg (stencilWeight_nonneg d) (by positivity)
stencilMomentTensor_not_isotropic · IndisputableMonolith/Gravity/Analysis/FreudenthalStencilPreflight.lean:366 
/-- 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))
THEOREM freudenthal_stencil_identity · IndisputableMonolith/Gravity/Analysis/FreudenthalStencilPreflight.lean
freudenthal_stencil_identity · IndisputableMonolith/Gravity/Analysis/FreudenthalStencilPreflight.lean:235 
/-- Panel-locked stage-1 observable, for ALL `N > 2` and arbitrary vertex
data `u`:

`ρ(N) · Q_N(u) = h³ · Σ_x Σ_{d ∈ D} c_d · ((u(x+d) − u(x))/h)²`, `h = 1/N`,

where `Q_N` is the canonical Regge-Hessian quadratic form
(`hessianQuadratic (canonicalReggeHessian …)`), `D` is the full
seven-element displacement-class set, the weights `c_d` are the
definitional Hessian dual weights (`stencilWeight`), and
`ρ(N) = stencilNormalization N = 1/N` was declared a priori above. -/
theorem freudenthal_stencil_identity (hN : 2 < N) (u : Vertex N N N → ℝ) :
    stencilNormalization N *
      hessianQuadratic
        (canonicalReggeHessian (canonicalPeriodicTriangulation N N N)
          (canonicalPeriodicIncidenceConsistent N N N))
        (toPotential N u) =
      meshSize N ^ (3 : ℕ) *
        ∑ x : Vertex N N N, ∑ d : Fin 7,
          stencilWeight d *
            ((u (shiftVertex N x d) - u x) / meshSize N) ^ (2 : ℕ) := by
  rw [hessianQuadratic_canonical_eq_freudenthalStencil N hN u]
  unfold freudenthalStencilEnergy stencilNormalization meshSize
  have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  simp_rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun x _ => Finset.sum_congr rfl fun d _ => ?_
  field_simp
THEOREM hessianQuadratic_canonical_eq_freudenthalStencil · IndisputableMonolith/Gravity/Analysis/FreudenthalStencilPreflight.lean
hessianQuadratic_canonical_eq_freudenthalStencil · IndisputableMonolith/Gravity/Analysis/FreudenthalStencilPreflight.lean:193 
/-- General-N stage-1 core identity, DERIVED from the canonical Regge
Hessian (never postulated): the frozen quadratic form
`hessianQuadratic (canonicalReggeHessian …)` of the canonical periodic
Freudenthal triangulation at any side `N > 2` equals the seven-class
stencil energy `Σ_x Σ_d c_d (u(x+d) − u(x))²`.

Derivation chain: `canonicalReggeHessian_quadratic_eq_dirichlet`
(Hessian quadratic form = graph Dirichlet energy), the no-self-loop
edge-stencil reindexing of `ReggeActionConcrete`
(`canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex`), and the
periodic-edge product reindexing above. -/
theorem hessianQuadratic_canonical_eq_freudenthalStencil
    (hN : 2 < N) (u : Vertex N N N → ℝ) :
    hessianQuadratic
        (canonicalReggeHessian (canonicalPeriodicTriangulation N N N)
          (canonicalPeriodicIncidenceConsistent N N N))
        (toPotential N u) =
      freudenthalStencilEnergy N u := by
  rw [canonicalReggeHessian_quadratic_eq_dirichlet]
  rw [canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex
    (canonicalPeriodicTriangulation N N N)
    (canonicalPeriodicIncidenceConsistent N N N)
    (canonicalEdgeStencilSumComm _ _)
    (canonicalEdgePairWeightReindex_of_noSelfLoop _ _
      (canonicalPeriodic_noSelfLoopEdges N hN))
    (toPotential N u)]
  exact canonicalEdgeStencil_eq_freudenthalStencil N u

What this page does not claim

The continuum limit of the discrete energy has been taken and shown to be a smooth quadratic form. The path-sum over all triangulations is defined or evaluated. The moment tensor is isotropic, since the theorem proves it is not.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND