Gravity Analysis Freudenthal Stencil Preflight Stencil Weight Eq Sqrt Global Sq

The stencil weight identity

In the Recognition Science framework's study of gravity, space is often modeled as a discrete triangulated network, a mesh of points connected by edges. The declaration stencilWeight_eq_sqrt_globalSqEdge is a proved theorem that establishes a precise relationship for this kind of mesh. It states that for every edge in a canonical periodic Freudenthal triangulation, the square root of the edge's squared length, as recorded in the framework's global incidence data, is exactly equal to a pre-defined stencil weight associated with that edge's displacement class. In plainer terms, it confirms that the weight used in a local stencil sum, a pattern of coefficients for neighboring points, is not an arbitrary choice but is directly derived from the geometry of the mesh itself.

The theorem is a key component of a larger, panel-scoped preflight check. This check aims to show that the discrete energy of the mesh, defined by a Hessian matrix, can be rewritten exactly as a sum over local stencil contributions. The identity stencilWeight_eq_sqrt_globalSqEdge is the bridge that connects these two descriptions. It is proved for every side length N greater than 2, not just for a single test case. The proof is axiom-clean, meaning it relies only on the standard axioms of the underlying logic system and contains no unproven assumptions or shortcuts. This makes the connection between the global edge data and the local stencil weights a rigorous, machine-checked fact, not a heuristic approximation.

This identity is the foundation for the next stage of the preflight, which computes the moment tensor of the stencil. The moment tensor is a matrix that summarizes the directional properties of the stencil weights. The identity ensures that this tensor is computed from the correct, geometrically derived weights. The framework's library of formal theorems proves that this moment tensor is positive semidefinite and, importantly, not isotropic, meaning it does not treat all directions equally. This anisotropy is a significant finding for the continuum limit, suggesting the discrete energy does not become a simple, direction-independent form.

What the declaration does not claim is just as important. It does not claim that the continuum limit of the gravity action has been fully derived or that the path-sum over triangulations is complete; that remains an open target. It does not claim that the stencil weights are the only possible weights or that they are fitted to match any experimental data. The theorem is a precise, internal consistency check within the framework's model of discrete gravity, establishing a necessary link in a larger chain of reasoning, not a complete physical theory of gravity.

/-- The stencil weight is exactly the Hessian dual-weight length factor of
any canonical periodic edge in displacement class `d`: definitional
transparency of `stencilWeight` (proof is `rfl`). -/
theorem stencilWeight_eq_sqrt_globalSqEdge
    (e : Fin (canonicalPeriodicTriangulation N N N).nE) :
    Real.sqrt ((canonicalPeriodicIncidenceConsistent N N N).globalSqEdge e) =
      stencilWeight ((edgeFinEquiv N N N e).disp) := rfl

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

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

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

/-- 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 declaration does not claim that the full continuum limit of the gravity action has been derived. The theorem does not claim that the stencil weights are fitted to experimental data.

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: