Gravity Analysis Regge Ttbloch Interface Audit Worst Radical Raw Jacobian Coeffi

A single stencil coefficient

The declaration worstRadical_rawJacobianCoefficient_closedForm is a machine-checked proof of a single arithmetic identity. It shows that a particular coefficient, called rawJacobianCoefficient, which appears in a discrete approximation to a gravity equation, equals exactly negative one eighth, or -1/8, when evaluated at a specific pair of indices. The coefficient itself is defined as a ratio: a term from a geometric derivative divided by two times the square root of an edge-length quantity. The proof establishes that for the chosen indices, this ratio simplifies to a rational number, -1/8, rather than remaining an unevaluated expression involving square roots.

The context is a numerical method for gravity. The framework builds a discrete version of a gravity equation on a tetrahedral mesh, where space is divided into tetrahedra. The calculation involves summing contributions over many tetrahedra and over pairs of slots associated with each tetrahedron. The coefficient in question is one term in that large sum. The proof shows that this one term, which might look complicated because it contains a square root, actually evaluates to a simple rational number. This is a small but concrete step: it confirms that a piece of the larger computation has a clean value, which is useful for checking the correctness of the overall numerical scheme.

In Recognition Science, this identity is part of a broader audit of the interface between a discrete gravity formulation and a continuum limit. The machine-checked library of formal theorems verifies this specific arithmetic fact. The theorem does not, however, establish anything about the full sum of all such coefficients. The documentation explicitly states that the complete rational bucket aggregation and the assembled zero-mode cancellation are not claimed here. A separate diagnostic found that the stencil-only constant block, which would be the sum over all terms, does not vanish. The continuum limit must use a different route, involving a cosine two-jet, after the hinge and diagonal constant block is formally connected.

What this means for the reader is that a single, potentially messy coefficient has been proven to be a simple rational number. This is a verified detail, not a broad conclusion. The proof does not show that the whole gravity calculation is correct, nor does it show that the discrete scheme converges to the continuum theory. It establishes one exact value, which can serve as a check on the larger, still open, computation. The value -1/8 is a concrete anchor point in a much larger and unfinished verification effort.

/-- Exact raw coefficient for the genuine radical-row entry.  The statement
keeps the radical-bearing numerator visible; Lean also proves the normalized
coefficient simplifies to `-1/8`. -/
theorem worstRadical_rawJacobianCoefficient_closedForm :
    rawJacobianCoefficient ⟨1, by decide⟩ ⟨2, by decide⟩ = -(1 / 8 : ℝ) := by
  unfold rawJacobianCoefficient
  change ReggeTTDerivativeGate.flatAngleJacobian (1 : Fin 6) (2 : Fin 6) /
      (2 * Real.sqrt (freudenthalTetSqEdges (1 : Fin 6))) = -(1 / 8 : ℝ)
  rw [worstRadical_flatAngleJacobian_value]
  norm_num [freudenthalTetSqEdges]
  have hsqrt2_ne : Real.sqrt 2 ≠ 0 := by positivity
  field_simp [hsqrt2_ne]
  norm_num

/-- Actual single-entry radical coefficient used by the early bucket
falsifier.  This is not the full fiber aggregation. -/
def rawJacobianCoefficient (f g : Fin 6) : ℝ :=
  ReggeTTDerivativeGate.flatAngleJacobian f g /
    (2 * Real.sqrt (freudenthalTetSqEdges f))

What this page does not claim

The proof does not establish that the full sum of all such coefficients vanishes. The proof does not show that the discrete gravity scheme converges to the continuum limit. The proof does not validate the entire Regge TT Bloch interface audit.

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