Encyclopedia Gravity Gravity Freudenthal Axis Stencil Coeff Cert Canonical Periodic Mixed Hinge Defic

ARTICLE 3 claims 3 theorems

Gravity Freudenthal Axis Stencil Coeff Cert Canonical Periodic Mixed Hinge Defic

A machine-checked certificate verifies that a discrete approximation to gravity's equations leaves no spurious terms, using exact rational arithmetic.

Verify this page

The coefficient certificate

A stencil is a fixed pattern of neighboring points used to approximate a differential equation on a grid. The declaration in question is a machine-checked certificate, a formal proof that a particular corrected stencil for a five-point periodic grid has a specific property: every unwanted coefficient in its residual expression is exactly zero. The residual is the difference between the true equation and the stencil's approximation; if any coefficient were nonzero, the stencil would introduce errors that do not vanish as the grid refines.

The certificate works with rational numbers, not floating-point approximations. It checks the coefficient of every unordered monomial, a product of two potential values at distinct grid points, in the corrected residual. The proof covers all pairs of vertices on the five-by-five-by-five periodic torus, a grid with 125 points wrapped around in all three directions. The statement FullResidualCoeffCert asserts that for every pair of vertices, the mixed-axis residual coefficient equals zero, and the theorem axisStencilCoeffSoundnessAtN5 establishes that the axis-stencil residual equals its unordered coefficient expansion for any potential function on the grid.

This is a finite, exact audit. It does not use floating-point arithmetic, so there are no rounding errors to hide behind. The proof relies on native_decide, a computation that evaluates the finite statement directly. This is a recognition event, a discrete record of a check performed, in the framework's sense: the cost of verifying the certificate is forced by the structure of the grid itself.

The certificate does not claim that the stencil is the unique correct one, nor that it converges to the continuum equations in any limit. It does not assert that the physical theory of gravity is correct or that this grid approximates reality. It is a purely combinatorial statement about a specific algebraic expression. The declaration establishes that a particular corrected stencil has no spurious coefficients in its residual, nothing more and nothing less.

THEOREM FullResidualCoeffCert · IndisputableMonolith/Gravity/FreudenthalAxisStencilCoeffCert.lean
FullResidualCoeffCert · IndisputableMonolith/Gravity/FreudenthalAxisStencilCoeffCert.lean:334 
/-- Full coefficient-vanishing statement for the corrected `N = 5` axis-stencil
residual.  This is the finite certificate still needed before converting the
coefficient audit into `CanonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5`. -/
def FullResidualCoeffCert : Prop :=
  ∀ u v : Vertex5, mixedAxisResidualCoeff u v = 0
THEOREM axisStencilCoeffSoundnessAtN5 · IndisputableMonolith/Gravity/FreudenthalAxisStencilCoeffCert.lean
axisStencilCoeffSoundnessAtN5 · IndisputableMonolith/Gravity/FreudenthalAxisStencilCoeffCert.lean:1389 
/-- The corrected three-axis stencil is sound with respect to the unordered
coefficient expansion.  This closes the RHS half of
`ExplicitFiberAxisStencilCoeffSoundnessAtN5`; the remaining packaging work is
the explicit-fiber LHS expansion. -/
theorem axisStencilCoeffSoundnessAtN5 :
    AxisStencilCoeffSoundnessAtN5 := by
  intro ξ
  let atom := fun (base : Vertex5) (d : Fin 3) (u v : Vertex5) =>
    let edge : PeriodicEdge5 := { base := base, disp := periodicAxisDisp d }
    let ep := edge.endpoints
    (if ep.1 = u && ep.1 = v then (-2 : Rat) else 0) +
      (if ep.2 = u && ep.2 = v then (-2 : Rat) else 0) +
        (if sameUnordered ep.1 ep.2 u v then (4 : Rat) else 0)
  let F := fun (u v base : Vertex5) (d : Fin 3) =>
    if vertex5CanonLE u v then ((atom base d u v : Rat) : ℝ) *
      potentialAtVertex5 ξ u * potentialAtVertex5 ξ v else 0
  have hdist : unorderedAxisCoeffExpansionAtN5 ξ =
      ∑ u : Vertex5, ∑ v : Vertex5, ∑ base : Vertex5, ∑ d : Fin 3,
        F u v base d := by
    unfold unorderedAxisCoeffExpansionAtN5 axisStencilResidualCoeff
    refine Finset.sum_congr rfl ?_
    intro u _
    refine Finset.sum_congr rfl ?_
    intro v _
    by_cases huv : vertex5CanonLE u v
    · simp only [huv, if_true, F]
      simp [atom, Finset.sum_mul]
    · simp [F, huv]
  have hreorder :
      (∑ u : Vertex5, ∑ v : Vertex5, ∑ base : Vertex5, ∑ d : Fin 3,
        F u v base d) =
      ∑ base : Vertex5, ∑ d : Fin 3, ∑ u : Vertex5, ∑ v : Vertex5,
        F u v base d := by
    calc
      (∑ u : Vertex5, ∑ v : Vertex5, ∑ base : Vertex5, ∑ d : Fin 3,
        F u v base d) =
          ∑ u : Vertex5, ∑ base : Vertex5, ∑ v : Vertex5, ∑ d : Fin 3,
            F u v base d := by
            refine Finset.sum_congr rfl ?_
            intro u _
            rw [@Finset.sum_comm Vertex5 ℝ Vertex5 _
              (s := Finset.univ) (t := Finset.univ)
              (f := fun v base => ∑ d : Fin 3, F u v base d)]
      _ = ∑ base : Vertex5, ∑ u : Vertex5, ∑ v : Vertex5, ∑ d : Fin 3,
            F u v base d := by
            rw [@Finset.sum_comm Vertex5 ℝ Vertex5 _
              (s := Finset.univ) (t := Finset.univ)
              (f := fun u base => ∑ v : Vertex5, ∑ d : Fin 3, F u v base d)]
      _ = ∑ base : Vertex5, ∑ d : Fin 3, ∑ u : Vertex5, ∑ v : Vertex5,
            F u v base d := by
            refine Finset.sum_congr rfl ?_
            intro base _
            calc
              (∑ u : Vertex5, ∑ v : Vertex5, ∑ d : Fin 3,
                F u v base d) =
                  ∑ u : Vertex5, ∑ d : Fin 3, ∑ v : Vertex5,
                    F u v base d := by
                    refine Finset.sum_congr rfl ?_
                    intro u _
                    rw [@Finset.sum_comm (Fin 3) ℝ Vertex5 _
                      (s := Finset.univ) (t := Finset.univ)
                      (f := fun v d => F u v base d)]
              _ = ∑ d : Fin 3, ∑ u : Vertex5, ∑ v : Vertex5,
                    F u v base d := by
                    rw [@Finset.sum_comm (Fin 3) ℝ Vertex5 _
                      (s := Finset.univ) (t := Finset.univ)
                      (f := fun u d => ∑ v : Vertex5, F u v base d)]
  have hpairSum :
      (∑ base : Vertex5, ∑ d : Fin 3, ∑ u : Vertex5, ∑ v : Vertex5,
        F u v base d) =
      ∑ base : Vertex5, ∑ d : Fin 3,
        -2 * (potentialAtVertex5 ξ
            ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.1 -
          potentialAtVertex5 ξ
            ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.2) ^ (2 : ℕ) := by
    refine Finset.sum_congr rfl ?_
    intro base _
    refine Finset.sum_congr rfl ?_
    intro d _
    let edge : PeriodicEdge5 := { base := base, disp := periodicAxisDisp d }
    have hne : edge.endpoints.1 ≠ edge.endpoints.2 :=
      PeriodicEdge.endpoints_ne (by decide) (by decide) (by decide) edge
    simpa [F, atom, edge] using
      pairAxisCoeffExpansionAtN5 ξ edge.endpoints.1 edge.endpoints.2 hne
  have hcoeff : unorderedAxisCoeffExpansionAtN5 ξ =
      ∑ base : Vertex5, ∑ d : Fin 3,
        -2 * (potentialAtVertex5 ξ
            ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.1 -
          potentialAtVertex5 ξ
            ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.2) ^ (2 : ℕ) := by
    rw [hdist, hreorder, hpairSum]
  have haxis : axisStencilResidualAtN5 ξ =
      ∑ base : Vertex5, ∑ d : Fin 3,
        -2 * (potentialAtVertex5 ξ
            ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.1 -
          potentialAtVertex5 ξ
            ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.2) ^ (2 : ℕ) := by
    unfold axisStencilResidualAtN5 canonicalPeriodicMixedAxisStencilAction potentialAtVertex5
    rw [← Finset.sum_neg_distrib]
    refine Finset.sum_congr rfl ?_
    intro base _
    rw [← Finset.sum_neg_distrib]
    refine Finset.sum_congr rfl ?_
    intro d _
    ring
  rw [haxis, hcoeff]
THEOREM snormRat · IndisputableMonolith/Gravity/FreudenthalAxisStencilCoeffCert.lean
snormRat · IndisputableMonolith/Gravity/FreudenthalAxisStencilCoeffCert.lean:173 
def snormRat : Fin 6 → Fin 6 → Rat
  | 0, 0 => 0
  | 0, 1 => 0
  | 0, 2 => 0
  | 0, 3 => 0
  | 0, 4 => -1
  | 0, 5 => 2
  | 1, 0 => 0
  | 1, 1 => 2
  | 1, 2 => -2
  | 1, 3 => -4
  | 1, 4 => 4
  | 1, 5 => -2
  | 2, 0 => 0
  | 2, 1 => -3
  | 2, 2 => 2
  | 2, 3 => 6
  | 2, 4 => -3
  | 2, 5 => 0
  | 3, 0 => 0
  | 3, 1 => -2
  | 3, 2 => 2
  | 3, 3 => 2
  | 3, 4 => -2
  | 3, 5 => 0
  | 4, 0 => -2
  | 4, 1 => 4
  | 4, 2 => -2
  | 4, 3 => -4
  | 4, 4 => 2
  | 4, 5 => 0
  | 5, 0 => 2
  | 5, 1 => -1
  | 5, 2 => 0
  | 5, 3 => 0
  | 5, 4 => 0
  | 5, 5 => 0

What this page does not claim

The certificate does not prove that the stencil converges to the continuum equations. The certificate does not assert that the physical theory of gravity is correct. The certificate does not claim uniqueness of the corrected stencil.

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