Encyclopedia Gravity Gravity Analysis Regge Ttbucket Aggregation Raw Jacobian Coefficient Eq Norm Div

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttbucket Aggregation Raw Jacobian Coefficient Eq Norm Div

A formula that once carried square roots turns out to be a simple table of fractions, and a machine-checked proof confirms it for every case.

Verify this page

The radical-free table

In the Recognition Science framework's study of gravity, a central object is the recognition ledger, a discrete record of events that the framework uses to derive physical structure. Within that ledger, the framework models spacetime geometry through a tetrahedral mesh, and certain calculations of how that mesh responds to changes produce coefficients that initially look messy: they contain square roots of quantities built from the tetrahedron's edge lengths.

The declaration rawJacobianCoefficient_eq_norm_div proves a clean fact about one such coefficient. It states that for any two of the six edges of a tetrahedron, the raw coefficient, which is defined as a Jacobian (a measure of how one geometric quantity changes with respect to another) divided by a square-root factor, is exactly equal to a separate expression that contains no square roots at all. That expression is a rational number divided by a simple product of edge lengths. In plain terms, the theorem shows that a formula that looks like it requires taking square roots can always be rewritten as a fraction involving only whole numbers and simple arithmetic.

The proof is not a numerical approximation. It is a formal, machine-checked derivation that works for every one of the 36 possible pairs of edges. The key step is a proved identity that bridges the square-root form to a polynomial expression, and then the square-root factor in the denominator cancels exactly. The result is that every one of the 36 coefficients evaluates to one of a small set of exact rational values: 0, 1/12, plus or minus 1/8, or plus or minus 1/4. This is a concrete, checkable outcome: the messy geometry reduces to a finite table of simple fractions.

This is a theorem within the framework's machine-checked library, meaning its proof has been verified by a computer to follow from the framework's axioms without gaps. It does not, however, claim anything about physics beyond this algebraic identity. It does not say what these coefficients mean physically, nor does it connect them to any measured quantity. It is a statement about the internal mathematics of the framework's geometric model, not about the observable world.

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
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]

What this page does not claim

This theorem does not claim any physical meaning for the coefficients. This theorem does not connect the coefficients to any measured physical quantity. This theorem does not claim the framework's geometric model is a correct description of real gravity.

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