Gravity Analysis Freudenthal Energy Limit Witness Field Section Has Deriv At

The witness field's smooth section

The declaration witnessField_section_hasDerivAt establishes a smoothness fact about a specific test function used in a numerical experiment. The function is witnessField, defined on three-dimensional space as f(x,y,z) = sin(2πx). The declaration proves that when you slice this function along the x-axis, holding y and z fixed at zero, the resulting one-dimensional curve has a derivative at every point. The derivative matches the expected formula: 2π cos(2πt) at position t.

This lemma is not an end in itself; it is a tool. The wider experiment, documented in the FreudenthalEnergyLimit module, studies how a discrete lattice approximation to a certain energy functional behaves as the lattice gets finer. The energy functional involves the gradient of the test function. To compute the continuous target value that the lattice should approach, the framework needs to integrate the squared gradient over a unit cube. The derivative lemma supplies the gradient component along the x-axis, which is the only nonzero component for this particular witness field. With that derivative in hand, the integral reduces to a one-dimensional integral of cos²(2πt), which is evaluated exactly.

The lemma is proved for the fixed function sin(2πx) and for the specific section where the other two coordinates are zero. It does not claim that every function has a derivative, nor that this function is differentiable along every possible slice. It says nothing about the y or z components of the gradient, which are zero by definition of the witness field. The declaration is scoped to its exact statement: the derivative of the section exists and equals the given expression.

In the larger context, this lemma is one of several that together establish a convergence result. The lattice energy, normalized appropriately, approaches the continuum integral at a rate proportional to 1/N², where N is the lattice size. The rate constant is explicit. The convergence theorem is proved in the framework's machine-checked library, and this derivative lemma is a necessary step in that proof. The lemma itself, however, is purely about calculus; it does not by itself assert anything about gravity, energy limits, or the physical interpretation of the framework. Those claims live in other declarations that build on this one.

/-- The first gradient component is the honest derivative of the witness
field along the first coordinate axis. -/
theorem witnessField_section_hasDerivAt (t : ℝ) :
    HasDerivAt (fun s : ℝ => witnessField ![s, 0, 0]) (witnessGrad t 0) t := by
  have hg : witnessGrad t 0 = Real.cos (2 * Real.pi * t) * (2 * Real.pi) := by
    show (if (0 : Fin 3) = 0 then 2 * Real.pi * Real.cos (2 * Real.pi * t) else 0) =
      Real.cos (2 * Real.pi * t) * (2 * Real.pi)
    rw [if_pos rfl]
    ring
  rw [hg]
  simp only [witnessField, Matrix.cons_val_zero]
  exact hasDerivAt_sin_const_mul (2 * Real.pi) t

/-- Quantitative distance of the closed form from the continuum target:
`|A₀[0,0]·2N²sin²(π/N) − continuumTarget| ≤ rateConstant/N²`, consuming the
Phase-2a toolkit bound `discrete_sine_eigenvalue_expansion` at wavenumber 1.
The achieved rate is `1/N²`, strictly better than the demanded `1/N`. -/
theorem witness_closed_form_dist (N : ℕ) (hN : 3 ≤ N) :
    |stencilMomentTensor 0 0 *
        (2 * (N : ℝ) ^ (2 : ℕ) * Real.sin (Real.pi / N) ^ (2 : ℕ)) -
      continuumTarget| ≤ rateConstant / (N : ℝ) ^ (2 : ℕ) := by
  have hA : 0 ≤ stencilMomentTensor 0 0 := le_of_lt (stencilMomentTensor_diag_pos 0)
  have hexp := discrete_sine_eigenvalue_expansion 1 N (by omega)
  simp only [Nat.cast_one, mul_one] at hexp
  have hkey : stencilMomentTensor 0 0 *
      (2 * (N : ℝ) ^ (2 : ℕ) * Real.sin (Real.pi / N) ^ (2 : ℕ)) - continuumTarget =
      (stencilMomentTensor 0 0 / 2) *
        (4 * (N : ℝ) ^ 2 * Real.sin (Real.pi / (N : ℝ)) ^ 2 - (2 * Real.pi) ^ 2) := by
    unfold continuumTarget
    ring
  rw [hkey, abs_mul, abs_of_nonneg (div_nonneg hA (by norm_num))]
  calc (stencilMomentTensor 0 0 / 2) *
        |4 * (N : ℝ) ^ 2 * Real.sin (Real.pi / (N : ℝ)) ^ 2 - (2 * Real.pi) ^ 2|
      ≤ (stencilMomentTensor 0 0 / 2) * ((2 * Real.pi) ^ 4 / 12 / (N : ℝ) ^ 2) :=
        mul_le_mul_of_nonneg_left hexp (div_nonneg hA (by norm_num))
    _ = rateConstant / (N : ℝ) ^ (2 : ℕ) := by
        unfold rateConstant
        ring

What this page does not claim

The declaration does not claim differentiability of the witness field along any other slice or in any other direction. It does not assert that the convergence result applies to arbitrary functions, only to the fixed sine wave. It does not by itself establish any physical claim about gravity or energy in the Recognition Science framework.

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/FreudenthalEnergyLimit.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: