Gravity Analysis Regge Ttbloch Interface Audit A2 Reduced Eq Raw Cell Stencil

The stencil identity

In numerical relativity, the Regge calculus discretizes spacetime into flat tetrahedra, and the second variation of the Einstein-Hilbert action becomes a sum over the edges and diagonals of that mesh. The declaration a2_reduced_eq_rawCellStencil proves, in the framework's machine-checked library of formal theorems, that two ways of writing that sum agree exactly. The first way, canonicalFiniteH, is the compact expression used in the main A2 theorem: a double sum over tetrahedra and slot pairs of a velocity times an angle derivative. The second way, rawCellStencil, expands the inner sum into a literal 6 × 6 × 6 = 216-term triple sum over tetrahedra and ordered slot pairs, with each term written as a product of two plane-wave velocities and a flat-angle Jacobian. The theorem states that these two expressions are equal for any lattice size, any edge metric, and any momentum vector.

The proof is a direct algebraic expansion: it unfolds both definitions, distributes the finite inner sum, and simplifies with ring normalization. No approximation, no numerical integration, no physics input beyond the definitions themselves. The sign convention matches the live A2 theorem, where the reduced second variation is the negative Schlaefli-reduced contraction. This is a narrow but meaningful gate: it confirms that the compact formula used in the main derivation is exactly what the explicit stencil says it is, term by term.

What the declaration does not claim is equally important. It does not claim that the full rational bucket aggregation vanishes, nor that the assembled zero-mode cancels. The same-day symbolic diagnostic found that the stencil-only constant block does not vanish; the ContinuumLimit engine must use the cosine two-jet route after the hinge/diagonal constant block is formally connected. Gate A2-full, Gate A3, and Gate B all remain open. The theorem is a checkpoint on the way to those gates, not a proof that any of them pass.

In Recognition Science, this theorem is a small but concrete instance of the framework's method: take a physical quantity, write it in two different forms, and let a machine check that they are the same. The value here is not a new physical prediction but a reduction of audit risk. A future reader can trust that the compact formula and the explicit stencil are not two different objects that happen to look similar; they are one object written two ways.

/-- Gate A1, honest part: the A2 reduced finite value equals the literal
triple raw stencil.  The proof is finite distribution of the inner
`flatSlotAngleDeriv` sum, not a definitional alias between the two sides.
The panel's `hN` premise is not needed: the incidence identity holds for
every `N` with `[NeZero N]`, which is a strictly stronger statement. -/
theorem a2_reduced_eq_rawCellStencil (N : ℕ) [NeZero N]
    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) :
    canonicalFiniteH N E m = rawCellStencil N E m := by
  unfold canonicalFiniteH rawCellStencil rawCellStencilTerm
  congr 1
  congr 1
  refine Finset.sum_congr rfl fun τ _ => ?_
  refine Finset.sum_congr rfl fun f _ => ?_
  unfold flatSlotSqrtDeriv flatSlotAngleDeriv
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun g _ => ?_
  ring_nf

/-- Gate A1, honest part: the A2 reduced finite value equals the literal
triple raw stencil.  The proof is finite distribution of the inner
`flatSlotAngleDeriv` sum, not a definitional alias between the two sides.
The panel's `hN` premise is not needed: the incidence identity holds for
every `N` with `[NeZero N]`, which is a strictly stronger statement. -/
theorem a2_reduced_eq_rawCellStencil (N : ℕ) [NeZero N]
    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) :
    canonicalFiniteH N E m = rawCellStencil N E m := by
  unfold canonicalFiniteH rawCellStencil rawCellStencilTerm
  congr 1
  congr 1
  refine Finset.sum_congr rfl fun τ _ => ?_
  refine Finset.sum_congr rfl fun f _ => ?_
  unfold flatSlotSqrtDeriv flatSlotAngleDeriv
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun g _ => ?_
  ring_nf

What this page does not claim

The full rational bucket aggregation does not vanish. The assembled zero-mode cancellation is not established here. No ContinuumLimit or spike certificate module is imported or proven in this file.

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: