Gravity Analysis Regge4 Dcontinuum Preflight Regge4 Dcontinuum Preflight Status

The preflight status flags

The declaration regge4DContinuumPreflightStatus_flags is a status board for a specific step in a research program. It records, in a machine-checked library of formal theorems, which pieces of a four-dimensional gravity calculation have been fixed in place and which have been deliberately set aside. The word preflight means the check happens before the main flight: the module pins down the target, the mesh, the data, and the decoys before any further computation begins. The flags themselves are the binding record of that freeze.

The classical object here is the Einstein-Hilbert action, the standard starting point for general relativity. The module defines a quadratic version of it in four dimensions, with a coefficient κ that is not a free lattice normalization but a fixed constant. The target is that this quadratic functional, evaluated on a specific family of gravitational wave polarizations, matches a discrete lattice expression in the continuum limit. The polarizations are transverse-traceless (TT), meaning they are purely spatial, divergence-free, and trace-free, the physical degrees of freedom of a gravitational wave. The mesh is a periodic four-torus with side length at least three, built from a Freudenthal triangulation, a standard way to subdivide a torus into simplices.

The flags establish three things as theorems. First, the continuum symbol, the lattice expression that should converge to the Einstein-Hilbert coefficient, is unique: if two limits exist, they are equal. Second, the wrong mesh power, N⁻² instead of the correct N⁻⁴, is provably different from the right one. Third, the transverse-traceless decomposition of any symmetric matrix into a TT part, a pure gauge part, and a residual trace part is stated as a definition, with the normalized TT polarizations named explicitly. These are the honest, checkable facts the module banks.

What the flags do not claim is the central recovery itself. The module explicitly says nothing here proves continuum recovery. The convergence of the discrete action to the Einstein-Hilbert action is a closed target, meaning it is a named goal with a date and a ledger entry, not a proved theorem in this file. The exact flat cross-term symbol that would complete the match is an open target, not yet derived. The module also rejects several decoys: a provisional weight-1 aggregate that fails gauge, a one-orbit symbol that is not the continuum object, and arbitrary pullbacks that are excluded from the action theorem. The flags freeze the battlefield, they do not declare victory.

The point of the flags is discipline. By recording what is fixed and what is not, the module prevents a later step from quietly fitting a scale to make the numbers match. The Einstein-Hilbert quadratic is frozen independently of the lattice symbol; the later algebraic closer must observe equality, never fit it. A reader can now see exactly which claims are load-bearing and which are placeholders, and that separation is the value the flags provide.

/-- Limits of the concrete exact-action continuum sequence are unique. -/
theorem continuumSymbolIs_unique {m : IntMode4} {E : Mat4} {Λ₁ Λ₂ : ℝ}
    (h1 : Regge4DContinuumSymbolIs m E Λ₁)
    (h2 : Regge4DContinuumSymbolIs m E Λ₂) : Λ₁ = Λ₂ :=
  tendsto_nhds_unique h1 h2

theorem decoy_wrong_mesh_power {N : ℕ} (hN : 2 ≤ N) :
    wrongMeshPowerWeight N ≠ correctTorusDensityWeight N := by
  unfold wrongMeshPowerWeight correctTorusDensityWeight
  have hNne : (N : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt (lt_of_lt_of_le (by norm_num : 0 < 2) hN))
  intro h
  have hclear :
      ((N : ℝ)⁻¹) ^ 2 * (N : ℝ) ^ 4 = ((N : ℝ)⁻¹) ^ 4 * (N : ℝ) ^ 4 :=
    congrArg (fun t : ℝ => t * (N : ℝ) ^ 4) h
  have hNsq : (N : ℝ) ^ 2 = 1 := by
    field_simp [hNne] at hclear
    exact hclear
  have hcast : (2 : ℝ) ≤ (N : ℝ) := by exact_mod_cast hN
  nlinarith [sq_nonneg ((N : ℝ) - 1)]

/-- Independently defined continuum EH quadratic on a Frobenius-normalized
TT polarization.  At this preflight stage the functional is the constant
coefficient times the Frobenius pin (already 1 on `IsTTPolarization4D`).
The coupling `kappa_einstein` is recorded as the Recognition field-equation
scale; weak-field quadratic recovery identifies the *symbol* coefficient
with `einsteinHilbertTTCoefficient4D`, not a free lattice normalization. -/
def einsteinHilbertQuadratic4D (E : Mat4) : ℝ :=
  kappa_einstein * einsteinHilbertTTCoefficient4D * frobeniusNormSq E

/-- Packaged OPEN name for the ledger closer.  Weak-field quadratic action
convergence only; not nonlinear strong-field GR and not sourced EFE. -/
def S_RS_converges_EH_4d : Prop :=
  Regge4DContinuumEHTarget ∧ Regge4DContinuumGaugeZeroTarget

What this page does not claim

The module does not prove that the discrete action converges to the Einstein-Hilbert action in the continuum limit. The module does not claim that the exact flat cross-term symbol has been derived or that it equals the Einstein-Hilbert coefficient. The module does not claim that the legacy distinct-hinge fold is the continuum object; it is retained for comparison only.

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