Gravity Analysis Regge Ttbucket Aggregation Rational Stencil Weight Swap

Symmetry of the stencil table

The declaration rationalStencilWeight_swap proves a symmetry property of a specific 36-entry table of rational numbers. This table, called rationalStencilWeight, assigns a value to each ordered pair of slots (f, g) from a set of six, along with an integer phase key. The theorem states that swapping the two slots, and negating the phase key, leaves the table value unchanged. In plainer terms, the table is symmetric: the entry for (f, g) with phase u equals the entry for (g, f) with phase -u.

The table itself arises in a specific, technical context: a discrete model of spacetime geometry built from tetrahedra. A separate, more substantial theorem (aggregate_raw_weight_eq_rational) shows that a certain radical-bearing coefficient, derived from the geometry, is exactly equal to this rational table for all 36 slot pairs. The swap theorem is a consistency check on that table. It confirms that the table's values are well-defined under a natural reversal operation, which is a prerequisite for a later step that would identify certain configurations as equivalent.

The proof of rationalStencilWeight_swap is a direct computation: it checks all 36 possible slot pairs by explicit case analysis, and each case reduces to a definitional equality. The proof does not rely on the deeper geometric theorem that links the table to the coefficients. It is a standalone fact about the table's internal structure. The declaration is part of a larger, machine-checked library of formal theorems, and its proof uses only the standard axioms of the underlying logic.

What this declaration does not claim is important. It does not, by itself, assert anything about the physical meaning of the table or the coefficients. It does not say that the table represents a valid discretization of gravity, nor that the symmetry property has any direct physical consequence. It is purely a mathematical statement about a defined object. The physical interpretation, if any, is a separate question that this theorem does not address.

/-- 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

/-- 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

/-- 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

What this page does not claim

This theorem does not assert any physical meaning for the table or the coefficients. This theorem does not claim the table is a valid discretization of gravity. This theorem does not claim the symmetry property has a direct physical consequence.

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: