Gravity Analysis Regge4 Dtorus Continuum Limit Dictionary Does Not Inhabit Eh Or

The dictionary's boundary

In the Recognition Science framework, a ledger is a discrete record of events, and here the record is a four-dimensional torus of lattice points, with side length N and N⁴ total sites. The framework's machine-checked library of formal theorems builds a dictionary between this finite lattice action and its continuum limit, the smooth theory it approximates as N grows. The dictionary's central bookkeeping fact is an algebraic cancellation: the second-difference weight (2/N⁴) multiplied by the cell-sum factor (N⁴/2) equals exactly 1. That single identity, proved as survivingDictionaryFactor4D_eq_cancellation, is what lets the finite action match the continuum symbol without leftover scale factors.

The dictionary's scope is deliberately narrow. It proves that the surviving factor is 1, that the density weight is N⁻⁴ and not a wrong power, and that the finite Hessian equals the distinct-hinge fold for all orbits. These are formal theorems. What the dictionary does not do is inhabit the Einstein-Hilbert action. A separate declaration, distinctHinge_pinned_ne_eh, proves that the pinned distinct-hinge moment, -1/16, is not equal to the Einstein-Hilbert coefficient. The dictionary identifies the fold of the cell-sum-scaled action; it does not claim that this fold is the Einstein-Hilbert action.

The gap to Einstein-Hilbert remains open. The declaration SchlafliElevationToDistinctHingeOpen names the missing step: a second-variation term S'' such that the density-weighted product equals the canonical finite Hessian. The 4D cosine cell-sum identity is also open, and residual offsets remain for non-t11/t12 orbits on the legacy fold. The dictionary does not flip gap_action_recovery; that recovery remains a target, not a result.

theorem survivingDictionaryFactor4D_eq_cancellation (N : ℕ) [NeZero N] :
    survivingDictionaryFactor4D =
      ttSecondDifferenceDensityWeight N * cellSumCosMulCosFactor N := by
  rw [survivingDictionaryFactor4D_eq_one, density_cellSum_cancellation]

theorem distinctHinge_pinned_ne_eh :
    DistinctHingePinnedMomentVsEH := by
  unfold DistinctHingePinnedMomentVsEH
  rw [einsteinHilbertTTCoefficient4D_eq]
  norm_num

What this page does not claim

The dictionary does not claim that the lattice action equals the Einstein-Hilbert action. The dictionary does not claim that the continuum limit has been fully constructed; the Tendsto statements bind to a specific midpoint trig-poly mesh sequence. The dictionary does not claim that the Einstein-Hilbert gap is closed; it names the missing steps as open targets.

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