Encyclopedia Gravity Gravity Freudenthal Axis Stencil Coeff Cert Scaled Pair Local Vertex Coeff Endpo

ARTICLE 3 claims 3 theorems

Gravity Freudenthal Axis Stencil Coeff Cert Scaled Pair Local Vertex Coeff Endpo

A machine-checked audit that a five-point gravity stencil leaves no residual error, carried out entirely in exact rational arithmetic.

Verify this page

The coefficient certificate

A stencil is a fixed pattern of points used to approximate a derivative or a differential operator on a grid. In numerical gravity, the Freudenthal axis stencil is a specific pattern on a triangular lattice, and its residual is the difference between what the stencil's weighted sum produces and the true operator value it is meant to approximate. The declaration scaledPairLocalVertexCoeffEndpointSumExpansionAtN5_value is a machine-checked certificate that this residual vanishes for the N = 5 case: every coefficient of every unordered monomial xi(u) * xi(v) in the corrected mixed explicit-fiber axis-stencil residual is exactly zero.

The certificate is not a numerical approximation. It uses exact rational arithmetic throughout, with no floating-point rounding, and it checks the coefficient of every unordered monomial at every vertex pair on a 5 x 5 x 5 periodic torus. The central theorem, axisStencilCoeffSoundnessAtN5, states that the axis-stencil residual equals its unordered coefficient expansion for every potential field on the torus. Supporting lemmas verify translation invariance and endpoint comparability for the periodic edges, and the full residual coefficient certificate asserts that the mixed-axis residual coefficient is zero for all vertex pairs.

What this does not claim is broader physical significance. The certificate is a finite algebraic check for one specific grid size, N = 5. It does not prove that the stencil works for other grid sizes, nor does it establish any connection to the framework's forcing chain, the golden ratio, or the derivation of three spatial dimensions. The declaration is a prerequisite step: the docstring notes it is the finite certificate still needed before converting the coefficient audit into a target statement for the canonical periodic mixed hinge deficit. It is a piece of bookkeeping that confirms a particular numerical construction is internally consistent, not a law of physics.

The value of this certificate is practical. When a stencil is used in a simulation, a nonzero residual means the approximation introduces systematic error that does not shrink with grid refinement. By proving the residual is exactly zero for this N = 5 case, the framework's library rules out that source of error for this specific configuration. The result is a guarantee about arithmetic, not about the physical world: it says the stencil's coefficients balance precisely on a 5-periodic lattice, nothing more and nothing less.

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:1385 
def AxisStencilCoeffSoundnessAtN5 : Prop :=
  ∀ ξ : VertexPotential5,
    axisStencilResidualAtN5 ξ = unorderedAxisCoeffExpansionAtN5 ξ
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

The certificate does not prove the stencil works for grid sizes other than N = 5. The certificate does not establish any connection between the stencil and the framework's forcing chain or derived constants. The certificate does not claim physical significance beyond the algebraic consistency of the N = 5 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