Gravity Analysis Regge Ttbloch Interface Audit Bucket

The bucket and its limits

A bucket is a labeled container: it holds one slot on the left, one slot on the right, and a phase vector, which is a triple of integers describing a wave's momentum shift. In the Recognition Science framework's machine-checked library of formal theorems, the Bucket structure is a definitional choice, not a proven result. It organizes the many terms that appear when a discrete gravity calculation is expanded into a finite sum.

The library proves one concrete fact about these buckets: a specific test case, the row0SmokeBucket, has a rational weight of 1/4. That weight comes from a larger stencil, a 6 by 6 by 6 grid of 216 terms per cell type, which the library expands in full. The expansion is deliberately narrow. The file that defines Bucket keeps its first gate non-tautological, meaning it does not assume the very thing it is meant to audit.

What the library does not claim is more instructive. The full rational bucket aggregation, where all buckets are summed and their weights combined, remains OPEN. The hinge-aware zero-mode cancellation, a step that would remove certain constant terms, also remains OPEN. The spike convention bridge, which would connect this discrete calculation to a continuous limit, is OPEN as well. A same-day diagnostic found that the stencil-only constant block does not vanish, so the ContinuumLimit engine must use a different route, the cosine two-jet approach, after the hinge and diagonal constant block is formally connected.

In Recognition Science, this is a deliberate audit surface. The Bucket declaration establishes a clean, testable object and proves one small weight value, but it does not pretend to close the larger gates. The framework's own status block lists three OPEN gates and names the missing connections. That is the honest boundary: a labeled container, a proven test case, and a clear statement of what remains to be derived.

/-- Bucket representative.  The intended external convention only identifies
`(f,g,u)` with `(g,f,-u)`; this attempt does not yet quotient or aggregate all
fibers. -/
structure Bucket where
  left : Fin 6
  right : Fin 6
  phase : PhaseVector

/-- 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 Bucket declaration does not prove that the full stencil sum vanishes. The Bucket declaration does not establish any connection to a continuous limit. The Bucket declaration does not define the spike convention bridge.

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: