Gravity Analysis Regge Exact Flat Hessian Bloch Symbol4 D

The exact Bloch symbol

In numerical relativity, the Regge calculus discretizes spacetime into flat building blocks, and the Einstein-Hilbert action becomes a sum over edges. The subject here is the exact Hessian, the matrix of second derivatives of that action, for a flat four-dimensional Regge geometry. This Hessian is named as a finite trigonometric polynomial over a table of 1208 couplings, each coupling carrying a weight and a phase that depends on the wavevector. The central object is the exact midpoint Bloch symbol, which evaluates the Hessian's response to a plane-wave perturbation with wavevector k.

The main theorem is a limit statement. As the wavevector magnitude t tends to zero, the centered symbol divided by t squared converges to a specific quadratic form, the exact midpoint Bloch M2. This is the discrete analog of the continuum dispersion relation: at long wavelengths, the discrete lattice dynamics must reproduce the continuum physics. The proof works by specializing a general theorem about centered trigonometric polynomials through irreducible wrappers, avoiding a combinatorial explosion in the 1208-element array. A second theorem generalizes the limit to division by t squared times any nonzero integer n.

Two supporting theorems establish the basic properties of the phase: it is zero at the zero wavevector and scales linearly with t. A normalization gate checks that the discrete bookkeeping, multiplied by a factor of two, recovers the frozen preflight Einstein-Hilbert coefficient of negative one quarter. The status record shows the trigonometric naming, the abstract and specialized limit proofs, and the normalization gate all pass. Two flags remain false: the ledger S_RS_converges_EH_4d and the gap action recovery are open, meaning the full continuum limit of the discrete action is not yet established.

In Recognition Science, this work is a step toward showing that the discrete Regge calculus, built from the framework's forced recognition costs, reproduces general relativity in the long-wavelength limit. The exact Bloch symbol is the tool that connects the discrete ledger to the continuum. What is established is precise: the discrete Hessian has the correct continuum limit at the level of its quadratic form. What is not established is the full convergence of the action itself, which remains an open target.

/-- Exact midpoint Bloch symbol: finite trig polynomial over the unit-cell
coupling table. -/
def exactMidpointBlochSymbol (H : Mat4) (k : Wave4) : ℝ :=
  ∑ i : CouplingIdx,
    couplingWeightIdx H i * Real.cos (couplingPhaseIdx k i)

/-- **THEOREM:** centered exact midpoint Bloch `/ t²` tends to its cosine
two-jet.  Specialized through irreducible wrappers (no Fin-1208 whnf). -/
theorem tendsto_exactMidpointBloch_centered_div_sq
    (H : Mat4) (dir : Wave4) :
    Tendsto
      (fun t : ℝ =>
        (exactMidpointBlochSymbol H (fun j => t * dir j) -
            exactMidpointBlochSymbolZero H) / t ^ 2)
      (𝓝[≠] (0 : ℝ)) (nhds (exactMidpointBlochM2 H dir)) := by
  have habs :=
    tendsto_centeredTrigPoly_div_sq (weightFn H) (phaseFn dir) couplingUniv
  have htarget :
      centeredTrigPolyM2 (weightFn H) (phaseFn dir) couplingUniv =
        exactMidpointBlochM2 H dir := (m2_eq_irred H dir).symm
  rw [← htarget]
  refine (tendsto_congr' ?_).mpr habs
  filter_upwards with t
  rw [centered_eq_irred]

theorem couplingPhase_zero (c : Coupling) :
    couplingPhase c (fun _ => (0 : ℝ)) = 0 := by
  unfold couplingPhase
  simp only [zero_mul, Finset.sum_const_zero]

theorem couplingPhase_smul (t : ℝ) (dir : Wave4) (c : Coupling) :
    couplingPhase c (fun j => t * dir j) = t * couplingPhase c dir := by
  unfold couplingPhase
  simp_rw [mul_assoc]
  exact Eq.symm (Finset.mul_sum _ (fun i => dir i * c.delta i) t)

theorem gate_passes_with_discrete_bookkeeping :
    NormalizationGatePass = true ∧
      discreteBookkeepingFactor * exactUnitFrobeniusTTCoefficient =
        frozenPreflightEHCoefficient ∧
          continuumEHDiscreteFace (1 : ℝ) = frozenPreflightEHCoefficient :=
  ⟨normalizationGatePass_true, frozen_EH_is_discrete_bookkeeping_times_unitF.symm,
    continuumEHDiscreteFace_on_unitF⟩

What this page does not claim

The full continuum limit of the discrete action is not proved, only its quadratic form. The module does not establish the ledger S_RS_converges_EH_4d, which remains open. The 1208 couplings are a definitional choice, not a derived result.

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