Encyclopedia Gravity Gravity Analysis Regge Ttbucket Aggregation

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttbucket Aggregation

A machine-checked proof shows that a radical-laden gravity coefficient collapses to a simple table of rational numbers, with no approximations.

Verify this page

The rational stencil table

Regge calculus is a discrete approach to general relativity where spacetime is approximated by flat tetrahedral pieces, and the curvature is concentrated along their shared edges. In this framework, the Regge action is a sum over these edges of the edge length times the deficit angle, the amount by which the surrounding flat pieces fail to close flat. The derivative of this action with respect to the edge lengths gives the gravitational field equations, and the second derivatives, the Jacobian, control the linearized dynamics around a solution.

The bucket-fiber aggregation, a discrete record of how these derivatives combine across the 36 possible pairs of edges in a single tetrahedron, had a known problem. The raw coefficients, built from the flat angle Jacobian and a flat tuple of squared edge lengths, contained square roots. These radicals made the coefficients awkward to work with and obscured the underlying structure. The module ReggeTTBucketAggregation closes this gate by proving that every one of these 36 radical-bearing coefficients is exactly equal to a value from a simple, independent table of rational numbers.

The proof is not a numerical approximation. It uses a previously proved bridge, the Schlaefli radical bridge, which connects the square-root expression to a rationalized polynomial summand. At the flat tuple, a key constant simplifies from sqrt(2 * cm3) to exactly 4, and the square roots cancel. The headline theorem, aggregate_raw_weight_eq_rational, states that for every bucket, the actual radical-bearing coefficient equals the real cast of the literal table entry. The table's values are only {0, 1/12, ±1/8, ±1/4}, a strictly larger set than the panel had preregistered, and it correctly reproduces the two previously recorded entries as corollaries.

In Recognition Science, this result matters because it shows a complex, radical-laden expression from the derivative machinery is actually a clean, rational stencil. This is a step toward a fully discrete, algebraic formulation of gravity where the fundamental quantities are exact rational numbers, not floating-point approximations. The module also proves the table is symmetric under a natural reversal of the edge pair, which is necessary for a well-defined quotient. The proof is pure algebra, verified by a machine-checked library of formal theorems, with an axiom footprint of only the standard trio [propext, Classical.choice, Quot.sound].

The practical consequence is that the linearized gravity equations on a flat tetrahedral lattice can be written down with exact rational coefficients. This removes a source of numerical error and opens the door to exact, symbolic analysis of the discrete field equations. The framework's library proves that the apparent complexity of the square roots was an artifact of the representation, not a property of the underlying geometry.

THEOREM aggregate_raw_weight_eq_rational · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean
aggregate_raw_weight_eq_rational · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean:167 
/-- **GATE C-A2f HEADLINE (THEOREM): on EVERY bucket (every slot pair,
every integer phase key), the actual radical-bearing raw stencil
coefficient `J_{fg} / (2 * sqrt a*_f)` equals the real cast of the
independent literal rational table.**  The left side is
`rawJacobianCoefficient` of the interface audit (built from the
kernel-proved flat angle Jacobian and the flat tuple); the right side is
the bare literal table of §1.  The two sides are independently defined;
their equality is 36 kernel-checked radical cancellations. -/
theorem aggregate_raw_weight_eq_rational (b : Bucket) :
    rawJacobianCoefficient b.left b.right =
      ((rationalStencilWeight b : ℚ) : ℝ) := by
  have h := rawJacobianCoefficient_eval b.left b.right
  have htbl : rationalStencilWeight ⟨b.left, b.right, fun _ => 0⟩ =
      rationalStencilWeight b := rfl
  rw [htbl] at h
  exact h
THEOREM rawJacobianCoefficient_eval · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean
rawJacobianCoefficient_eval · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean:151 
/-- All 36 raw coefficients evaluated to exact rationals.  Each entry is
the radical-free normal form of `rawJacobianCoefficient_eq_norm_div`
evaluated by kernel rational arithmetic on the flat integer tuple. -/
theorem rawJacobianCoefficient_eval (f g : Fin 6) :
    rawJacobianCoefficient f g =
      ((rationalStencilWeight ⟨f, g, fun _ => 0⟩ : ℚ) : ℝ) := by
  rw [rawJacobianCoefficient_eq_norm_div]
  fin_cases f <;> fin_cases g <;>
    norm_num [rationalStencilWeight,
      Geometry.SchlaefliTetrahedronProof.schlaefliPolySummandNorm,
      Geometry.CofactorPolynomial.cmCofactor3Poly,
      Geometry.CofactorPolynomial.cmCofactorPartial,
      freudenthalTetSqEdges]
THEOREM rawJacobianCoefficient_eq_norm_div · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean
rawJacobianCoefficient_eq_norm_div · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean:91 
/-- Every raw coefficient is the rationalized Schlaefli summand divided by
`8 * a*_f`: `J_fg / (2 * sqrt a*_f) = schlaefliPolySummandNorm(a*, f, g) /
(8 * a*_f)`.  Route: the proved radical bridge
`sqrt(a_f) * (dtheta_f/da_g) = (1/sqrt(2*cm3)) * norm` with
`sqrt(2 * cm3 a*) = sqrt 16 = 4` at the flat tuple, then
`sqrt(a_f) * sqrt(a_f) = a_f`.  No radical survives on the right. -/
theorem rawJacobianCoefficient_eq_norm_div (f g : Fin 6) :
    rawJacobianCoefficient f g =
      Geometry.SchlaefliTetrahedronProof.schlaefliPolySummandNorm
          freudenthalTetSqEdges f g /
        (8 * freudenthalTetSqEdges f) := by
  have hb := Geometry.SchlaefliTetrahedronProof.schlaefliSummandBridge
    freudenthalTet f g
  have h4 : Real.sqrt (2 * Geometry.CayleyMengerPolynomial.cm3
      freudenthalTet.sqEdge) = 4 := by
    have hcm : Geometry.CayleyMengerPolynomial.cm3 freudenthalTet.sqEdge = 8 :=
      Geometry.FreudenthalCubeTriangulation.cm3_freudenthalTetSqEdges
    rw [hcm, show (2 : ℝ) * 8 = 4 ^ 2 by norm_num,
      Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)]
  rw [h4] at hb
  have hJ : ReggeTTDerivativeGate.flatAngleJacobian f g =
      Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSqPoly
        freudenthalTet f g := by
    rw [ReggeTTDerivativeGate.flatAngleJacobian_eq_dihedralClosedDerivSq]
    exact Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSq_eq_poly
      freudenthalTet f g
  have hpos : (0 : ℝ) < freudenthalTetSqEdges f := freudenthalTet.sqEdge_pos f
  have hsqrt_ne : Real.sqrt (freudenthalTetSqEdges f) ≠ 0 :=
    ne_of_gt (Real.sqrt_pos.mpr hpos)
  have hsq : Real.sqrt (freudenthalTetSqEdges f) *
      Real.sqrt (freudenthalTetSqEdges f) = freudenthalTetSqEdges f :=
    Real.mul_self_sqrt hpos.le
  unfold rawJacobianCoefficient
  rw [hJ]
  rw [show freudenthalTet.sqEdge = freudenthalTetSqEdges from rfl] at hb
  rw [div_eq_div_iff
    (by positivity : (2 : ℝ) * Real.sqrt (freudenthalTetSqEdges f) ≠ 0)
    (by positivity : (8 : ℝ) * freudenthalTetSqEdges f ≠ 0)]
  calc
    Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSqPoly
          freudenthalTet f g * (8 * freudenthalTetSqEdges f)
        = 8 * (Real.sqrt (freudenthalTetSqEdges f) *
            Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSqPoly
              freudenthalTet f g) * Real.sqrt (freudenthalTetSqEdges f) := by
          rw [show Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSqPoly
                freudenthalTet f g * (8 * freudenthalTetSqEdges f) =
              8 * (Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSqPoly
                freudenthalTet f g *
                (Real.sqrt (freudenthalTetSqEdges f) *
                  Real.sqrt (freudenthalTetSqEdges f))) by rw [hsq]; ring]
          ring
    _ = 8 * (1 / 4 *
          Geometry.SchlaefliTetrahedronProof.schlaefliPolySummandNorm
            freudenthalTetSqEdges f g) * Real.sqrt (freudenthalTetSqEdges f) := by
          rw [hb]
    _ = Geometry.SchlaefliTetrahedronProof.schlaefliPolySummandNorm
          freudenthalTetSqEdges f g *
            (2 * Real.sqrt (freudenthalTetSqEdges f)) := by
          ring

What this page does not claim

This module does not derive the full quantum gravity theory or make contact with experimental data. The rational table applies only to the flat tuple of squared edge lengths, not to a general tetrahedron. The proof does not use any numerical approximation or floating-point arithmetic.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND