Encyclopedia Gravity Gravity Analysis Regge Ttlocal Symbol Existence Tendsto Centered Second Differen

ARTICLE 2 claims 2 theorems

Gravity Analysis Regge Ttlocal Symbol Existence Tendsto Centered Second Differen

A small lemma about smooth functions that lets physicists extract a number from a curve without knowing the curve's formula.

Verify this page

The centered second difference

In calculus, the second derivative of a function measures how its slope changes. For a smooth function f, the centered second difference (f(t) - 2f(0) + f(-t))/t² is a numerical approximation of f''(0) that gets better as t shrinks. The theorem tendsto_centeredSecondDifference_of_contDiffAt states that if f is twice continuously differentiable at 0, then this difference converges to the second derivative f''(0) as t approaches 0 from either side. This is a standard result, proved here by one application of L'Hôpital's rule, and it is reusable for any real-valued function meeting the smoothness condition.

In Recognition Science, this lemma is the bridge that lets a discrete lattice calculation connect to a continuum limit. The framework models spacetime as a discrete ledger, a record of events, and studies how a plane wave of amplitude t deforms a regular tetrahedral lattice. The action S(t) of this deformation is a smooth function of t, so the lemma applies. The centered second difference of S at t = 0 is exactly the second variation of the action, the quantity that determines whether a configuration is stable. The theorem proves this difference converges to the true second derivative S''(0), so the discrete calculation has a well-defined continuum meaning at each fixed lattice spacing.

The theorem does not compute the value of S''(0). It only proves that the limit exists and equals the second derivative. In the framework's gravity program, this establishes that a certain symbol, the fixed-N TT Bloch symbol, exists for every polarization and wave vector, and that it equals (2/N³)·S''(0). The numerical value of this symbol, and its limit as the lattice spacing N grows, remain open targets. The theorem is a statement about smooth functions, not a physical law; it does not claim that gravity behaves this way, only that if the action is smooth, this limit is well-defined.

THEOREM tendsto_centeredSecondDifference_of_contDiffAt · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean
tendsto_centeredSecondDifference_of_contDiffAt · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean:248 
/-- (d) THEOREM, THE REUSABLE LOCAL BRIDGE: if `f : ℝ → ℝ` is `C²` at `0`,
the centered second difference `(f(t) − 2f(0) + f(−t))/t²` converges along
the punctured neighborhood filter to `iteratedDeriv 2 f 0`.

Route (LOCAL Taylor / L'Hôpital, panel-approved): one pass of L'Hôpital's
rule for `0/0` forms on the punctured neighborhood
(`HasDerivAt.lhopital_zero_nhdsNE`) with numerator `g(t) = f(t) − 2f(0) +
f(−t)` and denominator `t²` reduces the limit to
`(f'(t) − f'(−t))/(2t) → f''(0)`, which is the average of the two slope
quotients of `deriv f` at `0` and converges by
`hasDerivAt_iff_tendsto_slope` applied to `deriv f` (differentiable at `0`
with derivative `deriv (deriv f) 0` since `f` is `C²` on a neighborhood).
The forbidden global lemma (`continuum_limit_second_order`, global
`ContDiff ℝ 4`) is not used. -/
theorem tendsto_centeredSecondDifference_of_contDiffAt (f : ℝ → ℝ)
    (hf : ContDiffAt ℝ 2 f 0) :
    Filter.Tendsto
      (fun t : ℝ => (f t - 2 * f 0 + f (-t)) / t ^ (2 : ℕ))
      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds (iteratedDeriv 2 f 0)) := by
  -- Extract a symmetric open ball on which f is C².
  obtain ⟨u, hu_mem, hu⟩ := hf.contDiffOn (le_refl 2) (by simp)
  obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.mp hu_mem
  have hfC2 : ContDiffOn ℝ 2 f (Metric.ball (0 : ℝ) ε) := hu.mono hball
  have hopen : IsOpen (Metric.ball (0 : ℝ) ε) := Metric.isOpen_ball
  have h0mem : (0 : ℝ) ∈ Metric.ball (0 : ℝ) ε := Metric.mem_ball_self hε
  -- deriv f is C¹ on the ball, hence differentiable at 0 with the second derivative.
  have hderivC1 : ContDiffOn ℝ 1 (deriv f) (Metric.ball (0 : ℝ) ε) :=
    hfC2.deriv_of_isOpen hopen (by norm_num)
  have hderiv_diffAt : DifferentiableAt ℝ (deriv f) 0 :=
    ((hderivC1.contDiffAt (hopen.mem_nhds h0mem)).differentiableAt (by norm_num))
  have hD : HasDerivAt (deriv f) (deriv (deriv f) 0) 0 := hderiv_diffAt.hasDerivAt
  set D : ℝ := deriv (deriv f) 0 with hD_def
  -- Membership of ±t in the ball, eventually on the punctured filter.
  have hmem_event : ∀ᶠ t in nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ,
      t ∈ Metric.ball (0 : ℝ) ε ∧ -t ∈ Metric.ball (0 : ℝ) ε := by
    have hball_event : ∀ᶠ t in nhds (0 : ℝ),
        t ∈ Metric.ball (0 : ℝ) ε ∧ -t ∈ Metric.ball (0 : ℝ) ε := by
      have h1 : ∀ᶠ t in nhds (0 : ℝ), t ∈ Metric.ball (0 : ℝ) ε :=
        hopen.mem_nhds h0mem
      have hneg_cont : Filter.Tendsto (fun t : ℝ => -t) (nhds 0) (nhds 0) := by
        simpa using (continuous_neg (G := ℝ)).tendsto (0 : ℝ)
      have h2 : ∀ᶠ t in nhds (0 : ℝ), -t ∈ Metric.ball (0 : ℝ) ε :=
        hneg_cont.eventually h1
      exact h1.and h2
    exact hball_event.filter_mono nhdsWithin_le_nhds
  -- f is differentiable at every point of the ball, with derivative deriv f.
  have hfd : ∀ x ∈ Metric.ball (0 : ℝ) ε, HasDerivAt f (deriv f x) x := by
    intro x hx
    exact ((hfC2.contDiffAt (hopen.mem_nhds hx)).differentiableAt
      (by norm_num)).hasDerivAt
  -- The numerator g and its derivative on the punctured ball.
  have hgg' : ∀ᶠ t in nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ,
      HasDerivAt (fun s : ℝ => f s - 2 * f 0 + f (-s))
        (deriv f t - deriv f (-t)) t := by
    filter_upwards [hmem_event] with t hmem
    have hft : HasDerivAt f (deriv f t) t := hfd t hmem.1
    have hfnt : HasDerivAt f (deriv f (-t)) (-t) := hfd (-t) hmem.2
    have hneg : HasDerivAt (fun s : ℝ => -s) (-1 : ℝ) t := hasDerivAt_neg' t
    have hcomp : HasDerivAt (fun s : ℝ => f (-s)) (deriv f (-t) * (-1)) t :=
      HasDerivAt.comp t hfnt hneg
    have hsum := ((hft.sub_const (2 * f 0)).add hcomp)
    have hval : deriv f t + deriv f (-t) * (-1) = deriv f t - deriv f (-t) := by
      ring
    rw [hval] at hsum
    exact hsum
  -- The denominator t² and its derivative 2t.
  have hhh' : ∀ᶠ t in nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ,
      HasDerivAt (fun s : ℝ => s ^ (2 : ℕ)) (2 * t) t := by
    filter_upwards with t
    simpa using hasDerivAt_pow 2 t
  have hden_ne : ∀ᶠ t in nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ, 2 * t ≠ 0 := by
    filter_upwards [self_mem_nhdsWithin] with t ht
    exact mul_ne_zero two_ne_zero ht
  -- Both numerator and denominator tend to 0.
  have hf_cont : ContinuousAt f 0 := hf.continuousAt
  have hnum_tendsto : Filter.Tendsto (fun s : ℝ => f s - 2 * f 0 + f (-s))
      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds 0) := by
    have hneg_cont : Filter.Tendsto (fun t : ℝ => -t) (nhds (0 : ℝ)) (nhds 0) := by
      simpa using (continuous_neg (G := ℝ)).tendsto (0 : ℝ)
    have hcompneg : Filter.Tendsto (fun s : ℝ => f (-s)) (nhds 0) (nhds (f 0)) := by
      simpa [Function.comp_def] using hf_cont.tendsto.comp hneg_cont
    have h1 : Filter.Tendsto (fun s : ℝ => f s - 2 * f 0 + f (-s))
        (nhds 0) (nhds (f 0 - 2 * f 0 + f 0)) :=
      (hf_cont.tendsto.sub tendsto_const_nhds).add hcompneg
    have hval : f 0 - 2 * f 0 + f 0 = 0 := by ring
    rw [hval] at h1
    exact h1.mono_left nhdsWithin_le_nhds
  have hden_tendsto : Filter.Tendsto (fun s : ℝ => s ^ (2 : ℕ))
      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds 0) := by
    have h1 : Filter.Tendsto (fun s : ℝ => s ^ (2 : ℕ)) (nhds 0)
        (nhds ((0 : ℝ) ^ (2 : ℕ))) :=
      (continuous_pow 2).tendsto (0 : ℝ)
    rw [show ((0 : ℝ) ^ (2 : ℕ)) = 0 by norm_num] at h1
    exact h1.mono_left nhdsWithin_le_nhds
  -- The derivative quotient tends to D by slope averaging.
  have hslope : Filter.Tendsto (slope (deriv f) 0)
      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds D) :=
    hasDerivAt_iff_tendsto_slope.mp hD
  have hnegmap : Filter.Tendsto (fun t : ℝ => -t)
      (nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ) (nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ) := by
    have h1 : Filter.Tendsto (fun t : ℝ => -t) (nhds 0) (nhds 0) := by
      simpa using (continuous_neg (G := ℝ)).tendsto (0 : ℝ)
    refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      (h1.mono_left nhdsWithin_le_nhds) ?_
    filter_upwards [self_mem_nhdsWithin] with t ht
    exact neg_ne_zero.mpr ht
  have hslope_neg : Filter.Tendsto (fun t : ℝ => slope (deriv f) 0 (-t))
      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds D) :=
    hslope.comp hnegmap
  have havg : Filter.Tendsto
      (fun t : ℝ =>
        (slope (deriv f) 0 t + slope (deriv f) 0 (-t)) / 2)
      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds ((D + D) / 2)) :=
    (hslope.add hslope_neg).div_const 2
  rw [show (D + D) / 2 = D by ring] at havg
  have hdiv : Filter.Tendsto
      (fun t : ℝ => (deriv f t - deriv f (-t)) / (2 * t))
      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds D) := by
    refine havg.congr' ?_
    filter_upwards [self_mem_nhdsWithin] with t ht
    exact (slope_average_eq (deriv f) ht).symm
  -- One L'Hôpital pass assembles the limit.
  have hlim := HasDerivAt.lhopital_zero_nhdsNE hgg' hhh' hden_ne
    hnum_tendsto hden_tendsto hdiv
  have hiter : iteratedDeriv 2 f 0 = D := by
    rw [show (2 : ℕ) = 1 + 1 from rfl, iteratedDeriv_succ, iteratedDeriv_one]
  rw [hiter]
  exact hlim
THEOREM planeWave_TTBlochSymbolIs_secondVariation · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean
planeWave_TTBlochSymbolIs_secondVariation · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean:379 
/-- (e) HEADLINE THEOREM (first existence theorem of the program): for
every side `N`, every polarization matrix `E`, and every integer wave
vector `m`, the fixed-`N` TT Bloch symbol EXISTS and equals
`(2/N³) · S''(0)` where `S` is the plane-wave action profile of the TRUE
nonlinear Regge action.  Exact bookkeeping: the preflight's
`ttSecondDifference` is `(2/N³) · [(S(t) − 2S(0) + S(−t))/t²]` and the
bracket converges to `iteratedDeriv 2 S 0` by the local bridge (d) — no
stray `1/2` anywhere.  NOTE: this identifies the LIMIT, not its value; the
continuum `-(1/4)` target remains OPEN. -/
theorem planeWave_TTBlochSymbolIs_secondVariation (E : Fin 3 → Fin 3 → ℝ)
    (m : Fin 3 → ℤ) :
    TTBlochSymbolIs N E m
      ((2 / (N : ℝ) ^ (3 : ℕ)) *
        iteratedDeriv 2 (planeWaveActionProfile N E (commensurateMomentum N m)) 0) := by
  set k : Fin 3 → ℝ := commensurateMomentum N m with hk
  set S : ℝ → ℝ := planeWaveActionProfile N E k with hS
  have hC2 : ContDiffAt ℝ 2 S 0 := planeWaveActionProfile_contDiffAt N E k 2
  have hbridge := tendsto_centeredSecondDifference_of_contDiffAt S hC2
  unfold TTBlochSymbolIs
  have hconst := hbridge.const_mul (2 / (N : ℝ) ^ (3 : ℕ))
  refine hconst.congr' ?_
  filter_upwards with t
  unfold ttSecondDifference
  rw [← hk, ← hS, mul_div_assoc]

What this page does not claim

The theorem does not evaluate the second derivative S''(0) or the TT Bloch symbol. The theorem does not establish a continuum limit as N grows; all results are at fixed N. The theorem does not claim that the physical action is smooth; it only applies if it is.

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