Gravity Analysis Regge Hinge4 Dstar Kernel Hinge4 Dstar Kernel Status Flags

The four-dimensional hinge kernel

In four-dimensional geometry, a hinge is a shared edge where several higher-dimensional simplices meet. Around any such edge, the angles contributed by the surrounding simplices can be summed. In a flat, uncurved space, that sum is exactly 2π, the full circle. The declaration hinge4DStarKernelStatus_flags in the Recognition Science library establishes, by machine-checked proof, that this flatness condition holds for a specific hinge in the integer lattice: the seed triangle hinge {0, e₀, e₀+e₁}.

The proof enumerates the entire periodic star around that hinge. Exactly six pairs of a unit cube translate and a Kuhn simplex contain the hinge. Four of those six simplices contribute a flat cosine of 1/√2, corresponding to a 45-degree angle; the remaining two contribute a cosine of 0, a 90-degree angle. The sum is 4 × (π/4) + 2 × (π/2) = 2π, proved exactly. This is the flatness gate: the star angle sum equals 2π and no more.

Beyond the angle sum, the declaration defines a signed weight kernel on the fifteen symmetry classes of the star's edges. The kernel assigns values to classes (2,3,6,7,10,11,14) as (-1,-1,+1,-1,+1,+1,-1). It is nonvacuous, meaning the kernel is not identically zero. It respects a swap symmetry between classes 2 and 3, and it is stationary under uniform scaling and homothety: scaling the entire configuration leaves the kernel's directional sum at zero. These are the gates that qualify the kernel as a candidate for a discrete gravity action.

In Recognition Science, this is one increment in a campaign toward a full theory of quantum gravity. The declaration does not complete the flat Hessian assembly over all hinges in the lattice. It does not prove the convergence of the RS action to the Einstein–Hilbert action in four dimensions. It does not flip the gap action recovery flag, and it does not reverse-engineer weights from Einstein–Hilbert. Other hinge orbits in the lattice remain open targets. The proof's axiom footprint is the standard three: propositional extensionality, choice, and quotient soundness.

theorem star_cardinality :
    (Finset.univ.filter (fun p : CubeTranslate × Fin 24 =>
      containsHinge p.1 p.2 = true)).card = 6 := by
  decide

def starFlatCosines : Fin 6 → ℝ
  | ⟨0, _⟩ | ⟨1, _⟩ => 1 / Real.sqrt 2
  | ⟨2, _⟩ | ⟨3, _⟩ => 0
  | ⟨4, _⟩ | ⟨5, _⟩ => 1 / Real.sqrt 2

theorem star_flat_angle_sum_two_pi : starFlatAngleSum = 2 * Real.pi := by
  simp only [starFlatAngleSum, flatAngleSeedOpp_eq, flatAngleOrth_eq]
  ring

theorem fullStarClassKernel_nonvacuous : fullStarClassKernel 11 ≠ 0 := by
  norm_num [fullStarClassKernel]

theorem fullStar_homothety_stationary :
    fullStarDirectional (fun d => (classWeightNat d : ℝ)) = 0 := by
  simp only [fullStarDirectional]
  rw [sum15_support _ (fun d h2 h3 h6 h7 h10 h11 h14 => by
    rw [fullStarClassKernel_zero_off d h2 h3 h6 h7 h10 h11 h14, mul_zero])]
  have w2 : classWeightNat 2 = 2 := by decide
  have w3 : classWeightNat 3 = 1 := by decide
  have w6 : classWeightNat 6 = 3 := by decide
  have w7 : classWeightNat 7 = 1 := by decide
  have w10 : classWeightNat 10 = 3 := by decide
  have w11 : classWeightNat 11 = 2 := by decide
  have w14 : classWeightNat 14 = 4 := by decide
  simp [fullStarClassKernel, w2, w3, w6, w7, w10, w11, w14]
  norm_num

What this page does not claim

The declaration does not prove convergence of the RS action to the Einstein–Hilbert action in four dimensions. The declaration does not complete the flat Hessian assembly over all hinges in the lattice. The declaration does not reverse-engineer weights from Einstein–Hilbert.

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