Gravity Analysis Regge Hinge4 Dflat Kernel Seed Orbit Assembly Decoy Area

The seed orbit and its decoys

In a discrete approach to quantum gravity, spacetime is chopped into flat pieces, and curvature is concentrated along shared lower-dimensional faces. In four dimensions the natural pieces are 4-simplices, the four-dimensional generalization of a triangle. This declaration concerns a specific building block: the Freudenthal or Kuhn 4-cube cell, which is a standard way to divide a 4-cube into 24 such 4-simplices. The declaration's subject is a particular triangle inside that cell, called the seed hinge, and the question of which of the cell's fifteen edge types actually touch that triangle.

The answer is exact and combinatorial. Exactly two of the 24 simplices contain the seed hinge. Those two simplices, together, contain ten of the fifteen edge types. The remaining five edge types split into two groups: three are absent entirely from the two simplices that contain the seed hinge, and two more are present only as boundary edges of the hinge itself. The three absent types are the decoys: they look like they could participate in the curvature calculation, but the incidence structure rules them out. The declaration proves this by explicit enumeration, and it also proves a symmetry: swapping the third and fourth coordinate axes leaves the incidence pattern unchanged.

The purpose of this combinatorial bookkeeping is to support a later, physical calculation. The flat Hessian of the Regge action, the second variation of the action at a flat configuration, is a sum over hinges of an area weight times a deficit angle kernel. The declaration provides the assembly skeleton for that sum: a formula that contracts per-hinge area weights against per-hinge deficit kernels, and forces the result to vanish on the decoy edge types. The actual numeric values of those weights and kernels are not derived here; they remain an open target. The declaration does not complete the flat Hessian, does not prove convergence to the Einstein-Hilbert action, and does not reverse-engineer weights from classical gravity.

Within the framework, this is a step in a longer campaign to derive the Einstein-Hilbert action from a discrete ledger of recognition events. The combinatorial support is a proved theorem, machine-checked with no gaps. The physical bridge, from this incidence table to the actual deficit-angle calculus, is the part that remains open. The declaration's honesty lies in separating those two: what is proved is the incidence structure, and what is not proved is any claim about the true curvature weights.

/-- 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 (decoy): three explicit edge classes have zero seed-hinge
incidence. -/
theorem seedHingeIncidence_decoy_zero :
    seedHingeIncidenceNat decoyClass4 = 0 ∧
      seedHingeIncidenceNat decoyClass8 = 0 ∧
        seedHingeIncidenceNat decoyClass12 = 0 := by
  decide

/-- THEOREM: every seed-hinge boundary class has positive incidence. -/
theorem hingeBoundary_incidence_pos (i : Fin 3) :
    0 < seedHingeIncidenceNat (hingeBoundaryClass i) := by
  fin_cases i <;> 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 true numeric values of the area weights and deficit kernels are not derived here. The flat Hessian of the 4D Regge action is not completed by this declaration. No claim is made that the decoy edge types have zero physical curvature contribution; they are absent from the seed orbit's incidence support only.

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: