Gravity Analysis Srsconverges Eh4 D Typed Residual M2 Rayleigh Eq Algebraic Face

The algebraic face

In the Recognition Science framework, gravity is studied by starting with a discrete ledger, a record of events on a grid, and asking whether that grid can behave like the smooth continuum of Einstein's theory. The declaration typedResidual_m2_rayleigh_eq_algebraic_face_closed is a machine-checked theorem that settles one precise piece of that question. It proves that a certain ratio, computed from the discrete grid, equals a specific constant. The ratio is the midpoint Bloch symbol, a quantity that measures how a wave of a given momentum interacts with a small perturbation of the grid, divided by the squared norm of the wave's momentum. The constant is exactHessianM2UnitFrobeniusTTCoeff, a number that appears in the discrete action and is designed to match the coefficient of the Einstein-Hilbert action in the weak-field limit.

The theorem states that for any transverse-traceless wave and any small perturbation with unit Frobenius norm, this ratio is exactly that constant. It also states a second identity: for a pure gauge wave, a wave that represents a coordinate change rather than physical curvature, the same ratio equals a different constant, exactHessianM2GaugeCoeff. The proof is a formal derivation in the framework's machine-checked library of formal theorems, meaning every step is verified by a computer. This is not an approximation or a numerical fit; it is an exact algebraic identity that holds for all allowed inputs.

The purpose of this theorem is to serve as one of several "faces" that together establish a larger result. The framework's goal is to show that the discrete action, when refined to smaller and smaller grids, converges to the Einstein-Hilbert action of general relativity. This particular face shows that the algebraic core of the discrete action, the part that does not depend on the grid spacing, already has the correct form. It is a necessary ingredient, but not the whole story. The full convergence result, named S_RS_converges_EH_4d, requires additional faces, such as the vanishing of certain residual terms and the behavior of the discrete torus family as the grid size grows.

What this theorem does not claim is just as important as what it does. It does not prove that the full Einstein equation emerges from the discrete ledger. That would require showing that the continuum limit of the discrete action is the Einstein-Hilbert action for all configurations, not just for the specific algebraic faces. It does not claim that the discrete ledger is a complete theory of quantum gravity. The convergence result is about the weak-field, quadratic action, not about horizons, singularities, or the full nonlinear theory. The framework's own documentation is explicit: the convergence is only for the weak-field quadratic action, and the full theory remains an open target.

The value of this theorem is that it pins down a precise algebraic fact that can be checked and reused. It gives the framework a solid foundation for the next step, which is to prove the convergence of the full action. Without this face, the larger claim would rest on an unverified assumption. With it, the framework has one more piece of the puzzle in place, and the path to the full result is clearer.

/-- **THEOREM (R3):** cosine two-jet Rayleigh equals algebraic m² faces
(`-1/8` on unit-F TT; `0` on pure gauge). -/
theorem typedResidual_m2_rayleigh_eq_algebraic_face_closed :
    TypedResidual_m2_rayleigh_eq_algebraic_face :=
  ReggeExactFlatHessianBlochM2Rayleigh4D.typedResidual_m2_rayleigh_eq_algebraic_face

/-- **THEOREM (R3):** cosine two-jet Rayleigh equals algebraic m² faces
(`-1/8` on unit-F TT; `0` on pure gauge). -/
theorem typedResidual_m2_rayleigh_eq_algebraic_face_closed :
    TypedResidual_m2_rayleigh_eq_algebraic_face :=
  ReggeExactFlatHessianBlochM2Rayleigh4D.typedResidual_m2_rayleigh_eq_algebraic_face

/-- Packaged: bridge closed; S_RS inhabit reduces to Option-C m² faces. -/
theorem srs_converges_eh_4d_of_m2_optionC_faces
    (hFaces : TypedResidual_m2_optionC_faces) :
    S_RS_converges_EH_4d :=
  ⟨continuumEHTarget_of_bridge_and_m2_faces hFaces,
    continuumGaugeZeroTarget_of_bridge_and_m2_faces hFaces⟩

What this page does not claim

This theorem does not prove that the full Einstein equation emerges from the discrete ledger. This theorem does not claim that the discrete ledger is a complete theory of quantum gravity. This theorem does not cover horizons, singularities, or the full nonlinear theory of general relativity.

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