Encyclopedia Gravity Gravity Freudenthal Axis Stencil Coeff Cert Axis Stencil Residual Coeff Translat

ARTICLE 3 claims 3 theorems

Gravity Freudenthal Axis Stencil Coeff Cert Axis Stencil Residual Coeff Translat

A machine-checked certificate proves that a certain gravity stencil error term is unchanged by shifting the grid, but it does not prove the error is zero.

Verify this page

Translation invariance certificate

In numerical analysis, a stencil is a fixed pattern of neighboring grid points used to approximate a derivative or a differential operator. The Freudenthal axis-stencil is a specific pattern for a three-dimensional grid, and its residual is the difference between the true operator and the stencil approximation. A residual that changes when you translate the grid would be a serious flaw, because the physics should not depend on where you place the grid. The declaration axisStencilResidualCoeffTranslationInvariantCheck_eq_true is a machine-checked proof that, for a 5-by-5-by-5 periodic grid, the coefficient of every unordered pair of vertex potentials in the residual is invariant under translation. In plain terms: shift the entire grid by any amount, and the error term's coefficients stay the same.

The proof works by exact rational arithmetic, not floating-point approximations. The framework's machine-checked library (a collection of formal theorems verified by a computer) computes the coefficient of each unordered monomial xi(u) * xi(v) in the residual and checks that it equals zero after translation. The declaration itself is a theorem that the Boolean check evaluates to true, and it is proved by the native_decide tactic, which runs a verified decision procedure. This is a finite certificate: it covers all 125 vertices and all unordered pairs, so it is exhaustive for this grid size.

What this certificate does not claim is just as important. It does not prove that the residual is zero. It proves only that the residual is translation-invariant, meaning the coefficients do not change when the grid shifts. The actual vanishing of the residual, which would mean the stencil exactly represents the operator, is a separate property. The docstring says this certificate is a step toward a target called CanonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5, but that target is not yet established. The certificate also does not apply to other grid sizes or other stencils; it is specific to N = 5 and to the corrected axis-stencil.

In the Recognition Science framework, this certificate is part of a larger effort to build gravity from discrete structures. The translation invariance is a necessary consistency condition, but it is not sufficient for the full theory. The payoff of this result is that one potential source of grid-dependence in the discrete gravity model is ruled out, at least for this stencil and grid size. That is a concrete step, but the larger claim of a complete discrete gravity theory remains open.

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

What this page does not claim

This certificate does not prove that the residual is zero. It does not apply to grid sizes other than N = 5. It does not establish the full discrete gravity theory.

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