Gravity Analysis Regge Ttbloch Interface Audit Row0 Smoke Table Value

A single table entry

A table of numbers is only as trustworthy as its entries. Recognition Science, a framework that derives physics from a discrete record of events, is building a machine-checked library of formal theorems to audit a complicated calculation in gravity. The declaration row0Smoke_table_value is one such audit: it proves that a specific weight in that calculation equals the simple fraction 1/4.

The weight belongs to a stencil, a small pattern of points used to approximate a derivative on a grid. In this case the stencil models a piece of a curved spacetime, and the weight describes how one particular pair of tetrahedra, the building blocks of the grid, contributes to the second variation of the action. The theorem states that this contribution is exactly one quarter, a rational number, rather than a complicated expression involving square roots or pi.

The proof is a direct computation. The declaration expands the definition of the weight, which is a quotient of a Jacobian matrix entry by a square root of an edge length, and simplifies it. The result is a clean, checkable fact: the value is 1/4. This is the kind of small, verifiable step that gives confidence in a larger edifice.

What the theorem does not claim is just as important. It does not prove that the entire stencil sums to zero, which would be needed to show that the discretized gravity theory has the correct continuous limit. The same-day diagnostic found that the stencil-only constant block does not vanish. The full aggregation over all buckets, the zero-mode cancellation, and the bridge to a different convention are all marked as open targets in the library's status block. This theorem is a single verified cell in a table, not the proof of the table's bottom line.

/-- The independent table agrees with the row-0 smoke rational after casting
to real.  This is intentionally only the isolated smoke-test bucket, not the
full `aggregate_raw_weight_eq_rational` gate. -/
theorem row0Smoke_table_value :
    ((rationalStencilWeight row0SmokeBucket : ℚ) : ℝ) = (1 / 4 : ℝ) := by
  norm_num [rationalStencilWeight, row0SmokeBucket]

What this page does not claim

The theorem does not prove that the full stencil sum vanishes. The theorem does not establish the continuous limit of the discretized theory. The theorem 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: