Gravity Analysis Regge4 Dexact Action Symbol Discrete Bookkeeping Factor Eq

The discrete bookkeeping factor

In numerical relativity, the Regge action approximates Einstein's theory of gravity by dividing spacetime into flat four-dimensional blocks, or simplices, and summing contributions from their hinges. The framework's analysis of this action studies a Hessian, the matrix of second derivatives, on a flat background where the usual deficit angles vanish. That Hessian leaves a cross term, a product of area and deficit variations, which the framework calls the exact flat cross-term fold. The declaration discreteBookkeepingFactor_eq establishes that a certain bookkeeping factor, named discreteBookkeepingFactor, is exactly 2. This factor appears when the framework writes the discrete version of the Regge action symbol: it multiplies the geometric fold to produce the discrete symbol.

The declaration is a definitional identity, proved by reflexivity in the framework's machine-checked library of formal theorems. It states that the discrete bookkeeping factor equals the real number 2, and as a consequence the discrete exact Regge symbol is exactly twice the finite exact Regge symbol. The factor 2 is not derived from deeper principles; it is chosen as a definitional convenience, and the declaration merely records that choice. The framework's documentation notes a parallel in three dimensions, where a second-difference operator also carries a factor of 2, but the four-dimensional factor is not forced by that analogy.

What the declaration does not claim is more interesting than what it proves. It does not establish that the discrete symbol equals the continuum symbol; the framework's own status flags mark that comparison as open. It does not show that the factor 2 is physically necessary, only that the discrete symbol is defined with it. The declaration also does not resolve whether the geometric fold itself is the correct continuum object; the framework treats the dictionary sequence as ground truth for that question, and a separate measured comparison shows the geometric fold differs from that dictionary by exactly the factor of 2 at two test points. The factor is a definitional bridge, not a physical discovery.

theorem discreteBookkeepingFactor_eq : discreteBookkeepingFactor = (2 : ℝ) :=
  rfl

theorem discreteBookkeepingFactor_eq : discreteBookkeepingFactor = (2 : ℝ) :=
  rfl

/-- Discrete bookkeeping factor carrying the bare hinge fold to the Regge
action's second variation, from the 3D `ttSecondDifference = (2/N³)·S''`
convention (EH audit §2.3).  Not a fitted lattice rescale.

**One of two definitions in this tree with this name, and they do different
jobs** (arc 2 step 8, `GeometricFoldVsDictionary4D`).  This one is the
fold-to-action factor.  `ReggeExactFlatHessianNormGate4D.discreteBookkeepingFactor`
is also 2 but is `1/ρ`, Regge's normalization, carrying the action to the
Einstein-Hilbert integral; that one is derived in `ReggeNormalizationDerived4D`
(arc 2 step 7).  Their product is the residual factor 4 that
`Regge4DTorusContinuumLimit` records as unclosed between the fold's
`-(1/16)` and the Einstein-Hilbert `-(1/4)`.  Measured corroboration for the
value here: at both banked transverse-traceless witnesses on `symbolDir` the
dictionary's m² is exactly twice the geometric hinge moment, and the factor is
pinned against 1 and against 4
(`GeometricFoldVsDictionary4D.factor_pinned_axisTTPlus`).  The factor here is
still a convention rather than a derivation; the derivation is arc 2's next
target. -/
def discreteBookkeepingFactor : ℝ := 2

/-- Local status flags remain open; geometric ContinuumSymbolIs Tendsto
is the Preflight ledger gate.  Edge-origin m² decide-certs are banked
elsewhere and do not inhabit `S_RS`. -/
theorem exact_action_srs_still_open :
    exactActionSymbolStatus.srsInhabited = false ∧
      exactActionSymbolStatus.gapActionRecovery = false := by
  decide

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

The declaration does not prove the discrete symbol equals the continuum symbol. The factor of 2 is not derived from the framework's forcing chain or any deeper principle. The declaration does not establish that the geometric fold is the correct continuum object.

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: