Encyclopedia Gravity Gravity Freudenthal Axis Stencil Coeff Cert Selected Cell5 Eq Freudenthal Explic

ARTICLE 3 claims 3 theorems

Gravity Freudenthal Axis Stencil Coeff Cert Selected Cell5 Eq Freudenthal Explic

A machine-checked audit shows that a corrected five-point gravity stencil leaves no residual error, without relying on floating-point arithmetic.

Verify this page

The coefficient certificate

The declaration selectedCell5_eq_freudenthalExplicitFiberPairSelectedCell, found in the framework's machine-checked library of formal theorems, establishes a precise algebraic identity. It states that a particular selected cell in a five-point stencil, called the explicit-fiber pair selected cell, satisfies an equality that makes a certain residual coefficient vanish. In plain terms, the declaration certifies that a corrected numerical scheme for a gravity-related discretization has no leftover error term for that cell, when computed with exact rational arithmetic rather than floating-point approximations.

This certificate is part of a larger audit in the module FreudenthalAxisStencilCoeffCert. The audit checks the coefficient of every unordered monomial xi(u) * xi(v) in the corrected N = 5 mixed explicit-fiber axis-stencil residual. The key theorem axisStencilCoeffSoundnessAtN5 proves that for every potential function xi, the axis-stencil residual equals its unordered coefficient expansion, meaning all residual coefficients are zero. The declaration in question is a specific instance of this broader soundness result, applied to a particular selected cell within the five-point stencil.

The audit deliberately avoids floating-point arithmetic. Instead, it works with rational numbers, using definitions like snormRat and sqEdgeRat to represent squared edge lengths as exact fractions. The certificate verifies the coefficient of every unordered monomial in the residual, for all pairs of vertices in a 5x5x5 periodic torus. The theorem originResidualCoeffsZero_eq_true and rowResidualCoeffsZero_100_eq_true provide additional checks that specific rows and the origin have zero residual coefficients, all confirmed by native_decide, a computational proof method.

What the declaration does not claim is equally important. It does not assert that the stencil scheme is physically correct or that it matches any observed gravitational behavior. It only certifies the algebraic consistency of the residual coefficients for this specific N = 5 case. The certificate does not extend to other stencil sizes or to the full physical derivation of gravity from recognition principles. It is a finite, computational check, not a general theorem about the nature of gravity or the structure of spacetime.

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

What this page does not claim

The declaration does not claim the stencil scheme is physically correct or matches observed gravitational behavior. It does not extend the certificate to other stencil sizes or to a general theorem about gravity. It does not assert the full physical derivation of gravity from recognition principles.

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