Gravity Analysis Regge4 Dexact Action Symbol Exact Flat Cross Term Fold Smul

Scaling law for a discrete gravity symbol

In numerical relativity, the Regge action is a discrete version of Einstein's general relativity, built from flat four-dimensional blocks called simplices. The action's second derivative, its Hessian, controls how the theory responds to small perturbations. A central question is whether this discrete object converges to the continuous Einstein-Hilbert action as the blocks shrink. The declaration exactFlatCrossTermFold_smul proves a precise scaling property of one piece of that Hessian, called the flat cross-term.

The theorem states that if you multiply the metric perturbation matrix H by a constant c, the value of the cross-term symbol scales as c squared. In symbols: exactFlatCrossTermFold (c • H) m = c^2 * exactFlatCrossTermFold H m. This is the expected behavior for a quantity that is quadratic in the perturbation, a hallmark of an action-like object. The proof is a direct computation in the machine-checked library of formal theorems, with no gaps or unverified steps.

This scaling law is a necessary consistency check for the discrete gravity program. It confirms that the cross-term, which arises from the variation of both the area and the deficit angle in the Regge action, has the correct algebraic structure. It also provides a building block for proving similar scaling properties for the full finite symbol and its discrete counterpart, which includes a bookkeeping factor of two. These results are stepping stones toward the larger goal of showing the discrete theory reproduces the continuous Einstein-Hilbert action in the continuum limit.

In Recognition Science, this theorem is part of a broader effort to derive physical laws from a discrete ledger of recognition events. The framework models spacetime as a discrete structure and seeks to show that its dynamics reduce to general relativity at large scales. This particular theorem does not claim that the continuum limit has been achieved, nor does it establish the full equivalence between the discrete and continuous actions. It proves a specific algebraic property of one term, leaving the convergence question open.

What this means for the reader is that a critical piece of the discrete gravity machinery behaves as it should under scaling. The result is a formal guarantee, verified by a computer, that this part of the calculation is consistent. It is not a physical measurement or a derivation of a new constant; it is a structural theorem about a mathematical object. The theorem's value lies in the confidence it provides that the discrete framework is on the right track, one verified step at a time.

theorem exactFlatCrossTermFold_smul (c : ℝ) (H : Mat4) (m : Wave4) :
    exactFlatCrossTermFold (c • H) m =
      c ^ 2 * exactFlatCrossTermFold H m := by
  unfold exactFlatCrossTermFold exactFlatCrossTermOrbit
  simp_rw [exactFlatCrossTermSlot_smul]
  -- ∑ ty, w_ty * ∑∑ c² f = c² * ∑ ty, w_ty * ∑∑ f
  have hty : ∀ ty : HingeOrbitType,
      (orbitStarSize ty)⁻¹ *
          ∑ s : Fin 24, ∑ t : Fin 10,
            c ^ 2 * exactFlatCrossTermSlot ty H m s t =
        c ^ 2 *
          ((orbitStarSize ty)⁻¹ *
            ∑ s : Fin 24, ∑ t : Fin 10, exactFlatCrossTermSlot ty H m s t) := by
    intro ty
    simp_rw [Finset.mul_sum]
    ring_nf
  simp_rw [hty, ← Finset.mul_sum]

theorem exactFlatCrossTermFold_smul (c : ℝ) (H : Mat4) (m : Wave4) :
    exactFlatCrossTermFold (c • H) m =
      c ^ 2 * exactFlatCrossTermFold H m := by
  unfold exactFlatCrossTermFold exactFlatCrossTermOrbit
  simp_rw [exactFlatCrossTermSlot_smul]
  -- ∑ ty, w_ty * ∑∑ c² f = c² * ∑ ty, w_ty * ∑∑ f
  have hty : ∀ ty : HingeOrbitType,
      (orbitStarSize ty)⁻¹ *
          ∑ s : Fin 24, ∑ t : Fin 10,
            c ^ 2 * exactFlatCrossTermSlot ty H m s t =
        c ^ 2 *
          ((orbitStarSize ty)⁻¹ *
            ∑ s : Fin 24, ∑ t : Fin 10, exactFlatCrossTermSlot ty H m s t) := by
    intro ty
    simp_rw [Finset.mul_sum]
    ring_nf
  simp_rw [hty, ← Finset.mul_sum]

What this page does not claim

This theorem does not establish the continuum limit of the Regge action. This theorem does not prove the full equivalence between the discrete and continuous gravity actions. This theorem does not derive any new physical constant or measurement.

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