Gravity Analysis Regge4 Dtorus Continuum Limit Dictionary Identifies Fold Of Cel

The dictionary identity

The declaration dictionary_identifies_fold_of_cellSum_scaled is a theorem in the framework's machine-checked library of formal theorems. It concerns a finite periodic action sequence on a 4D torus with side length N and N^4 sites. The theorem states that if a certain cell-sum expression S'' equals the cell-sum factor times the canonical finite Hamiltonian, then multiplying S'' by the second-difference density weight yields exactly the canonical finite Hamiltonian. In plain terms, it proves that a specific bookkeeping factor cancels perfectly, so the finite 4D torus action equals the continuum symbol it approximates.

The theorem is a formal identity about algebraic cancellation. It shows that the product of the density weight (2/N^4) and the cell-sum factor (N^4/2) equals 1, meaning the two factors cancel exactly. This cancellation is what allows the finite 4D torus action to be identified with the continuum symbol. The proof is a direct computation, tagged as a theorem in the library, and it does not rely on any unproven assumptions about the physical interpretation.

What the theorem does not claim is equally important. It does not establish that the 4D cosine cell-sum identity holds in general; that remains an open problem. It also does not address residual star-member offsets for non-t11/t12 orbits on the legacy fold. The theorem does not flip the gap_action_recovery flag, meaning it leaves that separate property untouched. Finally, it does not prove the physical recognition-to-linking bridge for 4D gravity; that bridge is still open.

/-- THEOREM (dictionary reduction): once an independent `S''` equals
`cellSumCosMulCosFactor N * H`, cancellation forces
`(2/N⁴)·S'' = H`.  This is the 3D cancellation step in isolation. -/
theorem dictionary_identifies_fold_of_cellSum_scaled
    (N : ℕ) [NeZero N] (m : IntMode4) (E : Mat4)
    (S'' : ℝ)
    (hS : S'' = cellSumCosMulCosFactor N * canonicalFiniteH4D N m E) :
    ttSecondDifferenceDensityWeight N * S'' = canonicalFiniteH4D N m E := by
  rw [hS]
  have hcancel := density_cellSum_cancellation (N := N)
  calc
    ttSecondDifferenceDensityWeight N *
        (cellSumCosMulCosFactor N * canonicalFiniteH4D N m E)
        = (ttSecondDifferenceDensityWeight N * cellSumCosMulCosFactor N) *
            canonicalFiniteH4D N m E := by ring
    _ = (1 : ℝ) * canonicalFiniteH4D N m E := by rw [hcancel]
    _ = canonicalFiniteH4D N m E := by ring

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

What this page does not claim

The theorem does not prove the general 4D cosine cell-sum identity, which remains an open problem. The theorem does not address residual star-member offsets for non-t11/t12 orbits on the legacy fold. The theorem does not flip the gap_action_recovery flag or prove the physical recognition-to-linking bridge for 4D gravity.

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: