Gravity Analysis Regge Ttbloch Interface Audit

The audit surface

Gravity analysis in the Recognition Science framework works with a discrete approximation of spacetime called Regge calculus, where space is chopped into flat tetrahedra instead of smooth curves. The ledger, a discrete record of events, tracks how these tetrahedra respond to small deformations. The stencil is the local pattern of these responses: a fixed 6 by 6 by 6 grid of 216 terms per periodic cell, each term combining a tetrahedron type with an ordered pair of slots. The audit module checks whether this stencil, written out literally, matches the reduced second variation of the Regge action, the quantity that controls whether the discrete geometry is stable.

The central proved result is that the reduced second variation equals the raw stencil sum. The theorem a2_reduced_eq_rawCellStencil shows this by expanding the finite inner sum and distributing it, so the equality is not assumed but computed. The sign convention follows the live A2 theorem: the reduced second variation is the negative Schlaefli-reduced contraction. A second proved result pins down one stencil weight: for the zero-row slot pair, the raw Jacobian coefficient is exactly one quarter, matching the rational bucket table entry. A third theorem gives a closed form for the worst radical bucket: the coefficient for slot pair (1,2) is negative one eighth, derived from the flat angle Jacobian value of minus the square root of two over four.

What the module does not claim is as important as what it proves. The full rational bucket aggregation over all buckets is open, as is the hinge-aware zero-mode cancellation. The same-day diagnostic found that the stencil-only constant block does not vanish; the continuum limit engine must use a different route, the cosine two-jet, after the hinge and diagonal constant block is formally connected. The spike convention bridge is also open, with a target state named but not reached. No continuum limit or spike certificate module is imported here.

In plain terms, the audit establishes that the local stencil, written as a literal sum over tetrahedra and slot pairs, is the correct expansion of the reduced second variation. It proves three concrete numerical facts about the stencil weights. It leaves the global aggregation and zero-mode cancellation as open targets, which means the module is a checkpoint, not a completion. The reader can now see exactly which pieces of the gravity calculation are kernel-checked and which are still being assembled.

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

/-- Row-0 smoke test: the radical-trivial coefficient
`J_05 / (2 * sqrt a*_0)` is the literal rational `1/4`. -/
theorem row0Smoke_raw_weight_eq_rational :
    rawJacobianCoefficient ⟨0, by decide⟩ ⟨5, by decide⟩ = (1 / 4 : ℝ) := by
  unfold rawJacobianCoefficient
  change ReggeTTDerivativeGate.flatAngleJacobian (0 : Fin 6) ⟨5, by decide⟩ /
      (2 * Real.sqrt (freudenthalTetSqEdges (0 : Fin 6))) = (1 / 4 : ℝ)
  rw [ReggeTTDerivativeGate.flatAngleJacobian_row0_eval ⟨5, by decide⟩]
  norm_num [ReggeTTDerivativeGate.flatAngleJacobianRow0,
    freudenthalTetSqEdges, Real.sqrt_one]

/-- Exact raw coefficient for the genuine radical-row entry.  The statement
keeps the radical-bearing numerator visible; Lean also proves the normalized
coefficient simplifies to `-1/8`. -/
theorem worstRadical_rawJacobianCoefficient_closedForm :
    rawJacobianCoefficient ⟨1, by decide⟩ ⟨2, by decide⟩ = -(1 / 8 : ℝ) := by
  unfold rawJacobianCoefficient
  change ReggeTTDerivativeGate.flatAngleJacobian (1 : Fin 6) (2 : Fin 6) /
      (2 * Real.sqrt (freudenthalTetSqEdges (1 : Fin 6))) = -(1 / 8 : ℝ)
  rw [worstRadical_flatAngleJacobian_value]
  norm_num [freudenthalTetSqEdges]
  have hsqrt2_ne : Real.sqrt 2 ≠ 0 := by positivity
  field_simp [hsqrt2_ne]
  norm_num

What this page does not claim

The full rational bucket aggregation is not proved here; it remains open. The hinge-aware zero-mode cancellation is not established in this module. The spike convention bridge is not reached; only its target state is named.

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: