Gravity Analysis Regge Bloch M2 Tendsto4 D M2 Slot Coeff Eq Area Ker M2

The second-order slot coefficient

Regge calculus approximates general relativity by replacing smooth spacetime with a piecewise-flat simplicial complex, and the action becomes a sum over hinges, the shared edges of tetrahedra. In the framework's analysis of the continuum limit, one studies how this discrete action behaves as the mesh is refined. The relevant object is the slot coefficient, a number that controls the second-order term in the expansion of a transported slot term, which is a building block of the discretized action, as a function of a small perturbation parameter.

The theorem m2SlotCoeff_eq_area_kerM2 states that this slot coefficient equals the product of two simpler quantities, but only when the slot is of a special type called T11. The first factor is the area along the slot at zero perturbation, and the second is a coefficient derived from the deficit kernel, which measures the failure of the discrete geometry to close flatly. For all other slot types, the coefficient is zero. The proof is a direct computation that unfolds the definition and uses the fact that the area term has no linear part in the perturbation.

The theorem is a formal statement in the framework's machine-checked library of formal theorems. It does not by itself prove that the continuum limit exists, nor that the second-order term is finite for arbitrary perturbations. It establishes an algebraic identity for the slot coefficient, and the convergence results that use it require additional hypotheses, such as the vanishing of the deficit kernel at zero perturbation. The theorem is a component in a larger argument about the behavior of the discrete action near flat space, not a standalone physical prediction.

theorem m2SlotCoeff_eq_area_kerM2 (H : Mat4) (s : Fin 24) (t : Fin 10) :
    m2SlotCoeff H s t =
      (if isT11 s t then areaAlong H s t 0 * kerM2Coeff H s t else 0) := by
  unfold m2SlotCoeff kerM2Coeff
  by_cases ht : isT11 s t
  · simp [ht, areaAlong_zero]
  · simp [ht]

theorem m2SlotCoeff_eq_area_kerM2 (H : Mat4) (s : Fin 24) (t : Fin 10) :
    m2SlotCoeff H s t =
      (if isT11 s t then areaAlong H s t 0 * kerM2Coeff H s t else 0) := by
  unfold m2SlotCoeff kerM2Coeff
  by_cases ht : isT11 s t
  · simp [ht, areaAlong_zero]
  · simp [ht]

What this page does not claim

This theorem does not prove the existence of a continuum limit for the discrete action. This theorem does not establish convergence for arbitrary perturbations without additional hypotheses. This theorem does not make a physical prediction about gravity; it is an algebraic identity within the 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/ReggeBlochM2Tendsto4D.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: