Gravity Analysis Regge Exact Flat Hessian Bloch Symbol4 D Coupling Phase Idx Smu

Scaling a wave

A wave in four dimensions is a list of four numbers, one for each direction in spacetime. The declaration couplingPhaseIdx_smul is a theorem about what happens to a certain phase when you scale such a wave by a factor t. It states that the phase of the scaled wave equals t times the phase of the original wave. This is a linearity property: scaling the input scales the output by the same amount.

The phase in question is not a physical phase in the usual quantum mechanical sense. It is a bookkeeping device inside a larger construction. The construction starts with a discrete ledger, a record of 1208 coupling terms between points on a lattice. Each term has a weight and a phase. The phase is a sum over the four directions of the wave number times a displacement vector. The theorem says that if you multiply all four wave numbers by t, the phase multiplies by t as well.

This lemma is used in a proof that a certain trigonometric polynomial, built from these phases and weights, behaves like a quadratic form near zero. The polynomial is called the exact midpoint Bloch symbol. The proof shows that as the scale t approaches zero, the symbol minus its value at zero, divided by t squared, converges to a specific quadratic expression. The linearity of the phase is what allows the scaling argument to go through cleanly.

The broader goal is to show that this discrete ledger converges to the Einstein-Hilbert action of general relativity in the continuum limit. That goal is not met. The machine-checked library records that the convergence of the ledger to the continuum is open, and that the recovery of the gap action is false. The theorem about scaling the phase is a proved step inside a larger structure whose central claims remain targets, not achievements.

theorem couplingPhaseIdx_smul (t : ℝ) (dir : Wave4) (i : CouplingIdx) :
    couplingPhaseIdx (fun j => t * dir j) i =
      t * couplingPhaseIdx dir i := by
  unfold couplingPhaseIdx
  exact couplingPhase_smul t dir _

theorem couplingPhaseIdx_smul (t : ℝ) (dir : Wave4) (i : CouplingIdx) :
    couplingPhaseIdx (fun j => t * dir j) i =
      t * couplingPhaseIdx dir i := by
  unfold couplingPhaseIdx
  exact couplingPhase_smul t dir _

theorem exactBlochSymbolStatus_flags :
    exactBlochSymbolStatus.trigPolyNamed = true ∧
      exactBlochSymbolStatus.abstractTendstoProved = true ∧
        exactBlochSymbolStatus.specializedTendstoProved = true ∧
          exactBlochSymbolStatus.normalizationGatePass = true ∧
            exactBlochSymbolStatus.srsInhabited = false ∧
              exactBlochSymbolStatus.gapActionRecovery = false :=
  ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩

What this page does not claim

The theorem does not establish that the ledger converges to general relativity. The theorem does not establish that the exact midpoint Bloch symbol is a quadratic form for all scales, only in the limit as scale approaches zero. The theorem does not assign a physical meaning to the phase it scales.

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