Gravity Analysis Regge Bloch All Orbit Symbol4 D Complement Orbit Deficit Kernel

The complement symmetry

The declaration complement_orbit_deficit_kernels is a theorem in the framework's machine-checked library of formal theorems. It states that for two specific pairs of hinge types in a four-dimensional discrete geometry, the so-called deficit kernels are identical. These kernels are the mathematical objects that encode how much each hinge contributes to the curvature, or deficit angle, in this discrete model of gravity. The theorem proves that the kernel for hinge type (2,1) equals the kernel for hinge type (1,2), and the kernel for hinge type (3,1) equals the kernel for hinge type (1,3).

This is a statement about symmetry under complementation. In this model, a hinge is a two-dimensional triangular face where four tetrahedra meet. The notation (a,b) refers to the number of tetrahedra on each side of the hinge. The theorem says that swapping the two sides, so that a hinge with two tetrahedra on one side and one on the other becomes a hinge with one on the first side and two on the second, does not change the deficit kernel. This is a non-trivial structural property that simplifies the analysis of the gravitational action in this discrete setting.

In Recognition Science, this theorem is part of a larger effort to derive the structure of spacetime from a discrete ledger of recognition events. The framework models spacetime as a complex of tetrahedra, and the gravitational action is built from contributions associated with each hinge. The complement symmetry is one of several proven identities that make the all-orbit Bloch symbol, a key object in this analysis, well-defined and tractable. It is a building block, not the final result.

What this theorem does not claim is equally important. It does not prove that this discrete model recovers the continuum Einstein-Hilbert action of general relativity. It does not establish that the model's predictions match any observed gravitational phenomena. It does not even prove that the all-orbit Bloch symbol has the correct limit as the lattice spacing goes to zero. The theorem is a precise statement about a specific algebraic structure, and its role in the broader framework is a matter of ongoing research.

The practical consequence is that when computing the all-orbit Bloch symbol, one can treat these complement pairs as equivalent, reducing the number of distinct cases to consider. This is a concrete simplification that makes the formal analysis more manageable. The theorem is a small but necessary step in a long chain of formal reasoning.

/-- Complement pairs share deficit kernels (S4+complement four-orbit merge). -/
theorem complement_orbit_deficit_kernels :
    (∀ d : Fin 15, orbitDeficitKernel .t21 d = orbitDeficitKernel .t12 d) ∧
      (∀ d : Fin 15, orbitDeficitKernel .t31 d = orbitDeficitKernel .t13 d) := by
  constructor
  · intro d; rfl
  · intro d; rfl

What this page does not claim

The theorem does not prove recovery of the continuum Einstein-Hilbert action. The theorem does not establish any empirical prediction for gravitational phenomena. The theorem does not address the convergence of the all-orbit Bloch symbol in the continuum limit.

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