Gravity Analysis Freudenthal Stencil Preflight Stencil Moment Tensor Not Isotrop

The anisotropic finding

In classical continuum mechanics, a moment tensor summarizes how a material responds to bending or twisting. The second moment of a distribution, it is the matrix you get by summing, over every direction, the product of the direction with itself, weighted by how much stiffness that direction carries. When that matrix is proportional to the identity, the material is isotropic: it behaves the same in every orientation. When it is not, the material has preferred axes, like wood grain or a crystal lattice.

The Recognition Science framework studies a discrete, periodic lattice called the Freudenthal triangulation, a standard way to divide a cube into tetrahedra. On this lattice, the framework defines a stencil: a fixed set of seven displacement directions, each with a weight read off from the lattice's edge lengths. The framework's machine-checked library of formal theorems proves, for every side length N greater than 2, that the energy of a small displacement field on this lattice is exactly a sum over these seven directions. That exact identity is the preflight check before any continuum limit is taken.

The theorem named stencilMomentTensor_not_isotropic establishes a specific fact about the stencil's moment tensor. It proves that this 3 by 3 matrix is not proportional to the identity matrix, for any real number c. The off-diagonal entries are strictly positive, equal to the square root of 2 plus the square root of 3, so the matrix cannot be a scalar multiple of the identity. The theorem's proof is direct: it shows the off-diagonal entry is positive, then derives a contradiction from assuming the matrix were isotropic. The framework's library also proves the matrix is positive semidefinite, meaning its quadratic form never takes negative values, and that its diagonal entries are positive.

In Recognition Science, this result is a finding, not a postulate. The anisotropy is derived from the lattice geometry, not assumed. The framework's library states this explicitly: the stencil's frozen quadratic energy carries an anisotropic continuum quadratic form. The spectrum is also computed exactly: one eigenvalue with multiplicity two, and a larger one along the body diagonal. This means the discrete lattice, before any continuum limit, already distinguishes directions.

What this theorem does not claim is just as important. It does not claim that the continuum limit of this energy is anisotropic, because that limit is a separate, later stage of the framework's program. It does not claim that this anisotropy is physically observed in gravity; the framework treats this as a structural property of a candidate discrete model, not a measurement. It does not claim that isotropy is impossible in general, only that this particular stencil, on this particular lattice, is not isotropic. The theorem is a precise, scoped statement about a specific mathematical object, and its scope is exactly that object.

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

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

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

/-- The canonical status inhabitant (documentation record, not a proof
obligation). -/
def stencilPreflightStatus : StencilPreflightStatus where
  general_N_identity_derived := true
  normalization_a_priori := true
  moment_tensor_psd_nonzero := true
  moment_tensor_anisotropic_finding := true

What this page does not claim

The continuum limit of this energy is anisotropic. This anisotropy is a measured property of physical gravity. No discrete lattice can have an isotropic moment tensor.

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: