Gravity Analysis Regge Hinge4 Dstar Kernel Full Star Uniform Scale Decoy

The uniform scale decoy

In four-dimensional geometry, a Regge calculus builds curved space from flat triangular pieces, the way a paper model builds a dome from flat panels. The angle where panels meet is the hinge. In a flat space, the angles around any hinge add to exactly 2π. Curvature appears when that sum is not 2π, and the difference is called the deficit angle.

The machine-checked library of formal theorems proves a fact about one hinge in a repeating four-dimensional lattice. Around this hinge sit exactly six four-simplex pieces, the four-dimensional analog of triangles. The proof shows that in the flat configuration, four of those pieces meet with a cosine of 1/√2 and two with a cosine of 0, and the six angles sum to exactly 2π. This is the flatness gate: the hinge is flat before any weights are applied.

In Recognition Science, the framework models gravity by assigning a weight to each of fifteen symmetry classes of edge in the lattice. The declaration fullStar_uniformScale_decoy is a gate on that weight assignment. It proves that if you multiply every edge length by the same factor, a uniform scaling, the weighted sum called the deficit class kernel remains exactly zero. The theorem is named a decoy because a uniform scaling is a change that looks like it might matter but provably does not. The framework's library checks this by direct computation: the statement fullStar_homothety_stationary proves that the directional sum along the uniform-scale direction is zero.

The gate is one of several checks on a candidate weight assignment. The same library proves the assignment is nonvacuous, meaning it is not identically zero, and that it respects a swap symmetry between two of the fifteen classes. The uniform-scale decoy closes a loophole: a weight assignment that produced a nonzero response to uniform scaling would be suspect, because pure scaling should not create curvature from a flat configuration.

What the declaration does not claim is broader. It does not prove that the full flat Hessian, the second variation of the action over all hinges, is assembled. It does not prove that the Recognition Science action converges to the Einstein–Hilbert action of general relativity. It does not derive the weights from Einstein's equations, and it does not prove that any other hinge orbit in the lattice behaves this way. The proof covers exactly one hinge and its six surrounding pieces, and the other orbits remain open targets.

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

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

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

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

theorem fullStarClassKernel_swap23 (d : Fin 15) :
    fullStarClassKernel (swap23Class d) = fullStarClassKernel d := by
  have hinv : ∀ x : Fin 15, swap23Class (swap23Class x) = x := by decide
  have hs2 : swap23Class (2 : Fin 15) = 2 := by decide
  have hs3 : swap23Class (3 : Fin 15) = 7 := by decide
  have hs6 : swap23Class (6 : Fin 15) = 10 := by decide
  have hs7 : swap23Class (7 : Fin 15) = 3 := by decide
  have hs10 : swap23Class (10 : Fin 15) = 6 := by decide
  have hs11 : swap23Class (11 : Fin 15) = 11 := by decide
  have hs14 : swap23Class (14 : Fin 15) = 14 := by decide
  by_cases h2 : d = 2
  · subst h2; rw [hs2]
  by_cases h3 : d = 3
  · subst h3; rw [hs3]; rfl
  by_cases h6 : d = 6
  · subst h6; rw [hs6]; rfl
  by_cases h7 : d = 7
  · subst h7; rw [hs7]; rfl
  by_cases h10 : d = 10
  · subst h10; rw [hs10]; rfl
  by_cases h11 : d = 11
  · subst h11; rw [hs11]
  by_cases h14 : d = 14
  · subst h14; rw [hs14]
  have g2 : swap23Class d ≠ 2 := fun h => h2 (by rw [← hinv d, h, hs2])
  have g3 : swap23Class d ≠ 3 := fun h => h7 (by rw [← hinv d, h, hs3])
  have g6 : swap23Class d ≠ 6 := fun h => h10 (by rw [← hinv d, h, hs6])
  have g7 : swap23Class d ≠ 7 := fun h => h3 (by rw [← hinv d, h, hs7])
  have g10 : swap23Class d ≠ 10 := fun h => h6 (by rw [← hinv d, h, hs10])
  have g11 : swap23Class d ≠ 11 := fun h => h11 (by rw [← hinv d, h, hs11])
  have g14 : swap23Class d ≠ 14 := fun h => h14 (by rw [← hinv d, h, hs14])
  rw [fullStarClassKernel_zero_off _ g2 g3 g6 g7 g10 g11 g14,
    fullStarClassKernel_zero_off _ h2 h3 h6 h7 h10 h11 h14]

What this page does not claim

The declaration does not prove the full flat Hessian assembly over all hinges. The declaration does not prove convergence to the Einstein–Hilbert action. The declaration does not prove the behavior of any other hinge orbit in the lattice.

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: