Gravity Analysis Regge Ttgate Bbridge Core Weight Eq Raw

A check against transcription

In a large formal proof, one constant risk is that a table of numbers written out by hand, for speed or clarity, silently disagrees with the formula it is meant to represent. The declaration coreWeight_eq_raw is a guard against exactly that failure. It states, as a proved theorem, that a table called coreWeight, used in a computation about a tetrahedral grid, is equal to a quantity called rawJacobianCoefficient, which is computed directly from the underlying geometry. The equality is checked for every possible pair of slots in the grid, not just for a few sample values.

The purpose of the check is to make sure that no step of the larger argument rests on a number that was copied by hand rather than derived. The proof works by expanding both sides for each of the 36 possible slot pairs and simplifying, so the equality is not an assumption but a verified fact. This matters because the table is used later in a long chain of reasoning about a gravitational wave signal; if the table were wrong, everything built on it would be suspect. The theorem closes that gap by tying the table to the formula it claims to encode.

What the declaration does not claim is just as important. It does not say anything about the physical meaning of the numbers, about whether the gravitational wave computation is correct, or about whether the underlying model of gravity is right. It is a purely internal consistency check: a statement that two ways of writing down the same mathematical object agree. The theorem is a piece of bookkeeping, not a discovery about nature, and its value is that it makes the bookkeeping trustworthy.

In the framework's own account, this kind of check is part of how the library earns confidence. The machine-checked library of formal theorems does not take a table on faith; it proves that the table matches the definition. The result is that a reader can trust the numbers in the table as much as they trust the formula, and can follow the later argument without wondering whether a transcription error has crept in.

/-- The core weight table IS the actual raw Jacobian coefficient (via
the Gate C-A2f kernel evaluation; nothing is transcribed on trust). -/
theorem coreWeight_eq_raw (f g : Fin 6) :
    coreWeight f g = rawJacobianCoefficient f g := by
  rw [rawJacobianCoefficient_eval f g]
  fin_cases f <;> fin_cases g <;>
    norm_num [coreWeight, ReggeTTBucketAggregation.rationalStencilWeight]

What this page does not claim

The declaration says nothing about the physical meaning of the numbers or the correctness of the gravitational wave model. The declaration does not assert that the table is the only way to compute the coefficient, only that it agrees with the direct formula. The declaration does not validate any other table or formula in the framework, only the specific pair it names.

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