Gravity Analysis Freudenthal Stencil Preflight Canonical Edge Stencil Eq Freuden

The stencil identity

A stencil is a fixed pattern of neighboring points used to approximate a derivative or an energy on a grid. The declaration canonicalEdgeStencil_eq_freudenthalStencil proves, for every grid side length N greater than 2, that the quadratic energy of a particular discrete gravitational action equals exactly a sum over seven displacement classes: three axis directions, three face diagonals, and one body diagonal. The weights are 1 for the three axes, √2 for the three face diagonals, and √3 for the body diagonal. This is a theorem in the machine-checked library of formal theorems, with no unproved assumptions.

The identity is derived, not postulated. The chain starts from the canonical Regge Hessian, a matrix of second derivatives of a discrete gravitational action on a periodic triangulation. The proof shows that the quadratic form of this Hessian equals a graph Dirichlet energy, then reindexes the edges to match the seven-class stencil. The normalization factor is declared before any limit computation, with its dimensional justification, so nothing is fitted after the fact. The result holds for every N greater than 2, not just for the small cases previously certified.

The same module computes the moment tensor of the stencil, which encodes how the energy behaves under small perturbations. The tensor is exactly (1 + √2)·I + (√2 + √3)·J, where I is the identity and J is the all-ones matrix. Its entries are positive, and the tensor is positive semidefinite, meaning the energy is never negative for any perturbation. The off-diagonal entries are strictly positive, so the tensor is not a multiple of the identity: the energy is anisotropic, meaning it treats different directions differently. This is a finding, not a postulate, and it corrects an earlier expectation that the tensor would be rational and symmetric in the usual sense.

In Recognition Science, this stencil identity is a preflight check for a larger campaign: the continuum limit of a frozen quadratic energy on the canonical Freudenthal family. The identity establishes the exact discrete form of the energy and its moment tensor, which a companion module consumes to develop the action-level continuum limit. The path-sum flag for the full theory remains red, meaning the refinement-indexed measure-weighted sum over inequivalent triangulation classes is not yet derived. The stencil identity does not claim that the continuum limit exists, nor that the energy is isotropic, nor that the path-sum flag should be flipped. It establishes the discrete groundwork, and the continuum step remains open.

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

/-- Explicit values of the seven stencil weights:
`√1, √1, √1, √2, √2, √2, √3` for the three axis classes, the three
face-diagonal classes, and the body-diagonal class. -/
theorem stencilWeight_values :
    stencilWeight 0 = 1 ∧ stencilWeight 1 = 1 ∧ stencilWeight 2 = 1 ∧
      stencilWeight 3 = Real.sqrt 2 ∧ stencilWeight 4 = Real.sqrt 2 ∧
      stencilWeight 5 = Real.sqrt 2 ∧ stencilWeight 6 = Real.sqrt 3 := by
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;>
    norm_num [stencilWeight, periodicDispSqEdge, Real.sqrt_one]

/-- 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 continuum limit of the energy is not derived by this declaration. The stencil moment tensor is not isotropic; the proof shows the opposite. The path-sum flag for the full theory is not flipped by this module.

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: