Encyclopedia Gravity Gravity Analysis Regge Ttbucket Aggregation Rational Stencil Weight

ARTICLE 4 claims 3 theorems 1 model

Gravity Analysis Regge Ttbucket Aggregation Rational Stencil Weight

A table of 36 rational numbers that exactly reproduces a set of radical-bearing coefficients from a gravity calculation, with every entry machine-checked.

Verify this page

The rational stencil table

In the Recognition Science framework's analysis of Regge calculus, a stencil is a fixed set of weights used to approximate a derivative or other local quantity from values on a discrete grid. The declaration rationalStencilWeight defines a literal table of 36 rational numbers, one for each ordered pair of slots in a six-slot bucket. The table's entries are simple fractions: 0, 1/12, +1/8, -1/8, and +1/4.

The table is not plucked from thin air. It is an independent, explicitly written-out object. The framework's library of machine-checked theorems then proves that this bare table exactly equals a separate, more complicated coefficient that arises from the geometry: the raw Jacobian coefficient, which carries square roots. The theorem aggregate_raw_weight_eq_rational states that for every bucket, every slot pair, and every integer phase key, the radical-bearing coefficient equals the corresponding rational table entry. The proof route is a bridge that rationalizes the square roots, turning each entry into a fraction divided by a fixed integer, and then closes all 36 cases by exact arithmetic. No numerical approximation is involved.

The table also respects a symmetry: reversing the order of the two slots and negating the phase leaves the table value unchanged. This is the theorem rationalStencilWeight_swap. Two previously recorded values from an earlier audit are reproduced exactly: the row-0 smoke value of 1/4 and the worst-radical value of -1/8. The value set is slightly larger than what was preregistered, with +1/8 and +1/12 appearing on diagonals.

What the declaration does not claim is broader physical significance. It establishes an algebraic identity between two defined objects within the framework's formal system. It does not assert that this stencil is the unique or optimal one for any numerical scheme, nor that the table's values have been compared against any measured gravitational quantity. The theorem is about internal consistency of the framework's own derivative machinery, not about the physical world.

MODEL rationalStencilWeight · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean
rationalStencilWeight · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean:68 
/-- THE FULL LITERAL RATIONAL TABLE (all 36 slot pairs).  This is an
independent literal table in the sense demanded by the panel: a bare match
with literal rational values, phase-independent, never defined through any
fiber sum or through `rawJacobianCoefficient`.  Derived offline from the
closed forms of `flatAngleJacobian` and `freudenthalTetSqEdges` and then
kernel-verified entry by entry in `aggregate_raw_weight_eq_rational`. -/
def rationalStencilWeight (b : Bucket) : ℚ :=
  match b.left, b.right with
  | 0, 0 => 0        | 0, 1 => 0        | 0, 2 => 0
  | 0, 3 => 0        | 0, 4 => -(1 / 8) | 0, 5 => 1 / 4
  | 1, 0 => 0        | 1, 1 => 1 / 8    | 1, 2 => -(1 / 8)
  | 1, 3 => -(1 / 4) | 1, 4 => 1 / 4    | 1, 5 => -(1 / 8)
  | 2, 0 => 0        | 2, 1 => -(1 / 8) | 2, 2 => 1 / 12
  | 2, 3 => 1 / 4    | 2, 4 => -(1 / 8) | 2, 5 => 0
  | 3, 0 => 0        | 3, 1 => -(1 / 4) | 3, 2 => 1 / 4
  | 3, 3 => 1 / 4    | 3, 4 => -(1 / 4) | 3, 5 => 0
  | 4, 0 => -(1 / 8) | 4, 1 => 1 / 4    | 4, 2 => -(1 / 8)
  | 4, 3 => -(1 / 4) | 4, 4 => 1 / 8    | 4, 5 => 0
  | 5, 0 => 1 / 4    | 5, 1 => -(1 / 8) | 5, 2 => 0
  | 5, 3 => 0        | 5, 4 => 0        | 5, 5 => 0
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 rationalStencilWeight_swap · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean
rationalStencilWeight_swap · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean:184 
/-- The literal table is invariant under the bucket reversal
`(f, g, u) ~ (g, f, -u)`: the underlying 6x6 rational matrix is symmetric,
so the intended external quotient is well-defined on table values. -/
theorem rationalStencilWeight_swap (b : Bucket) :
    rationalStencilWeight b.swap = rationalStencilWeight b := by
  rcases b with ⟨l, r, u⟩
  fin_cases l <;> fin_cases r <;> rfl
THEOREM table_matches_row0Smoke · table_matches_worstRadical · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean
table_matches_row0Smoke · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean:194 
/-- The table reproduces the interface audit's row-0 smoke value
(`rawJacobianCoefficient (0,5) = 1/4`, kernel-recorded there). -/
theorem table_matches_row0Smoke :
    ((rationalStencilWeight row0SmokeBucket : ℚ) : ℝ) =
      rawJacobianCoefficient ⟨0, by decide⟩ ⟨5, by decide⟩ :=
  (aggregate_raw_weight_eq_rational row0SmokeBucket).symm
table_matches_worstRadical · IndisputableMonolith/Gravity/Analysis/ReggeTTBucketAggregation.lean:201 
/-- The table reproduces the interface audit's worst-radical value
(`rawJacobianCoefficient (1,2) = -1/8`, kernel-recorded there through the
`-sqrt 2 / 4` Jacobian entry). -/
theorem table_matches_worstRadical :
    ((rationalStencilWeight worstRadicalBucket : ℚ) : ℝ) = -(1 / 8 : ℝ) := by
  rw [← aggregate_raw_weight_eq_rational worstRadicalBucket]
  exact ReggeTTBlochInterfaceAudit.worstRadical_rawJacobianCoefficient_closedForm

What this page does not claim

This declaration does not assert that the stencil is unique or optimal for any numerical approximation scheme. No measured gravitational quantity is compared against these table values. The theorem does not establish any physical law; it establishes an algebraic identity between two framework-internal objects.

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