Gravity Analysis Recognition Mesh Exact Jbridge4 D Wave Norm Sq Preflight Eq Ide

The preflight identity

In the Recognition Science framework, a wave on a discrete mesh carries a number called its squared norm, a measure of the wave's size. The declaration waveNormSq_preflight_eq_identity is a machine-checked proof that two definitions of that number, one written for a continuum preflight check and one written for an exact midpoint identity, are the same for every wave. The proof is a direct computation, a definitional equality, so it needs no auxiliary assumptions. It is a bookkeeping step: it verifies that two notations in the library refer to the same object.

The identity sits inside a larger campaign. The framework models gravity on a periodic four-dimensional mesh, a lattice of points on a torus, and it attaches an action to that mesh. The action's second derivative, its amplitude Hessian, is built to match a known continuum object, the exact midpoint Bloch symbol. The preflight identity is the kind of check that makes the larger construction trustworthy: before the framework claims that its discrete action converges to a continuum limit, it first proves that the elementary pieces, like the squared norm of a wave, are named consistently across the library.

What the identity does not do is as important as what it does. It does not establish that the discrete action reproduces general relativity, nor that the continuum limit exists. Those are separate claims, tracked elsewhere in the library. The identity is a local consistency statement about notation, not a physical result. In the framework's own status ledger, the convergence of the iterated limit is marked closed, but the elevation of the model action to a literal Regge action via Schläfli remains open. The preflight identity is a small, exact, and deliberately narrow step that keeps the larger edifice honest.

private theorem waveNormSq_preflight_eq_identity (k : Wave4) :
    Regge4DContinuumPreflight.waveNormSq k =
      ReggeExactMidpointM2TTIdentity4D.waveNormSq k :=
  rfl

private theorem waveNormSq_preflight_eq_identity (k : Wave4) :
    Regge4DContinuumPreflight.waveNormSq k =
      ReggeExactMidpointM2TTIdentity4D.waveNormSq k :=
  rfl

What this page does not claim

The identity does not prove that the discrete action reproduces general relativity. The identity does not establish the existence of a continuum limit for the action. The identity does not claim that the model action is the literal Regge action, only that its amplitude Hessian matches by construction.

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