Gravity Analysis Regge Hinge4 Dflat Kernel Hinge4 Dflat Kernel Status Flags

Status flags for a gravity kernel

In numerical relativity, the Regge calculus approximates spacetime by a grid of flat simplices, and the second variation of the action gives the linearized dynamics. The declaration hinge4DFlatKernelStatus_flags is a record of five boolean fields that summarize the state of a particular construction: the Freudenthal 24-simplex cell has been enumerated, the seed hinge incidence is closed, the true deficit kernel is open, convergence to Einstein–Hilbert is not proved, and gap action recovery is not achieved. The flags are a compact ledger, a discrete record of what has been established and what has not.

The first two flags record genuine theorems. The Freudenthal cell, a standard subdivision of the 4-cube, has all 24 monotone 4-simplices explicitly listed, and each simplex's ten edges are classified into one of 15 types. For the chosen seed hinge, a triangle with vertices at the origin and two unit axes, exactly two of the 24 simplices contain it, and the incidence counts for the 15 edge classes are computed and proved invariant under a symmetry that swaps two axes. The machine-checked library of formal theorems confirms these combinatorial facts with no gaps in reasoning.

The remaining three flags are honest markers of what is not done. The true per-hinge deficit kernels, the dihedral and Cayley–Menger calculus that would supply numeric weights, remain open. The construction does not complete the flat Hessian of the 4D Regge action, does not prove convergence to the Einstein–Hilbert action, and does not recover the gap action. The assembly formula that contracts these open weights is a definitional model, not a derived result.

What the flags change is the working vocabulary of the campaign: instead of a vague sense of progress, researchers have a precise checklist. A future step can flip a flag from false to true only by supplying a kernel-checked proof or a new definition. The flags make the boundary between the proved and the open explicit, so the next increment knows exactly which gap it must close.

/-- Lexicographic enumeration of the 24 permutations of `Fin 4`:
`permAxes s = (σ(0), σ(1), σ(2), σ(3))`. -/
def permAxes : Fin 24 → Fin 4 × Fin 4 × Fin 4 × Fin 4
  | 0 => (0, 1, 2, 3)
  | 1 => (0, 1, 3, 2)
  | 2 => (0, 2, 1, 3)
  | 3 => (0, 2, 3, 1)
  | 4 => (0, 3, 1, 2)
  | 5 => (0, 3, 2, 1)
  | 6 => (1, 0, 2, 3)
  | 7 => (1, 0, 3, 2)
  | 8 => (1, 2, 0, 3)
  | 9 => (1, 2, 3, 0)
  | 10 => (1, 3, 0, 2)
  | 11 => (1, 3, 2, 0)
  | 12 => (2, 0, 1, 3)
  | 13 => (2, 0, 3, 1)
  | 14 => (2, 1, 0, 3)
  | 15 => (2, 1, 3, 0)
  | 16 => (2, 3, 0, 1)
  | 17 => (2, 3, 1, 0)
  | 18 => (3, 0, 1, 2)
  | 19 => (3, 0, 2, 1)
  | 20 => (3, 1, 0, 2)
  | 21 => (3, 1, 2, 0)
  | 22 => (3, 2, 0, 1)
  | 23 => (3, 2, 1, 0)
  | ⟨n + 24, h⟩ => absurd h (by omega)

/-- THEOREM: exactly two of the 24 Freudenthal simplices contain the
seed hinge. -/
theorem seedHinge_simplex_count :
    (Finset.univ.filter (fun s : Fin 24 => containsSeedHinge s = true)).card =
      2 := by
  decide

/-- THEOREM (symmetry): seed-hinge incidence is invariant under the
lattice symmetry that swaps axes `2` and `3` and fixes the hinge. -/
theorem seedHingeIncidence_swap23 (d : Fin 15) :
    seedHingeIncidenceNat (swap23Class d) = seedHingeIncidenceNat d := by
  fin_cases d <;> decide

/-- MODEL: flat second-variation class form for one hinge orbit,
`Σ_{e,f} Aweight_e · Kdeficit_{e f} · c_e · c_f`.

This is the 4D skeleton of the 3D Schläfli-reduced contraction
`−Σ_τ Σ_f L' · θ'` in `ReggeTTFlatSecondVariation`: here `Aweight`
plays the role of the area / hinge-volume first derivative and
`Kdeficit` the outer product of deficit gradients.  Both maps are OPEN. -/
def flatHessianOrbitForm
    (Aweight : Fin 15 → ℝ)
    (Kdeficit : Fin 15 → Fin 15 → ℝ)
    (c : Fin 15 → ℝ) : ℝ :=
  ∑ e : Fin 15, ∑ f : Fin 15, Aweight e * Kdeficit e f * c e * c f

What this page does not claim

The flat Hessian of the 4D Regge action is not completed by this declaration. Convergence to the Einstein–Hilbert action is not proved. The gap action recovery is not achieved.

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