Gravity Analysis Regge Ttbloch Interface Audit Stencil Only Constant Witness Res

A residual that audits

In numerical analysis, a stencil is a fixed pattern of neighboring points used to approximate a derivative or an integral on a grid. The declaration stencilOnlyConstantWitnessResidual names a specific real number: -π(√2 + 4)/8. It is a witness, in the formal sense, to a gap: it is the constant block that remains when only the raw stencil terms are summed, before any further cancellation is applied. The number itself is not a theorem about gravity; it is a measured artifact of the calculation's first pass.

The context is a Regge calculus audit, where spacetime is approximated by flat tetrahedra and the Einstein equations are built from edge-length variations. The framework's machine-checked library of formal theorems defines a 6 × 6 × 6 stencil: for each of 216 ordered triples of tetrahedron type and slot pair, it sums a product of a plane-wave velocity and a Jacobian coefficient. A theorem proves that this triple sum equals the reduced second variation of the action, up to sign. The residual appears when that sum is evaluated at a specific test configuration, the worst-radical bucket, where the Jacobian takes the value -√2/4 and the coefficient becomes -1/8.

What the residual does not claim is the full cancellation. The same-day symbolic diagnostic found that the stencil-only constant block does not vanish; the ContinuumLimit engine must use a different route, the cosine two-jet, after the hinge/diagonal constant block is formally connected. The full rational bucket aggregation and the assembled zero-mode cancellation remain open targets, as do the hinge-aware zero-mode and the spike convention bridge. The declaration is deliberately narrow: it is the first gate of an audit, not the audit's conclusion.

In plain terms, the residual is a checkpoint. It says: here is the exact number the raw stencil leaves behind, so that later stages can be checked against it. It does not say the calculation is complete, nor that the residual is physical. It is a fixed point in a formal development, a number that later machinery must either cancel or explain.

/-- Concrete record of the diagnostic zero-mode obstruction.  The
stencil-only constant block has the displayed nonzero residual for the
reported TT witness; the hinge/diagonal O(1) term is the remaining formal
interface piece needed before a true zero-mode theorem can be stated. -/
def stencilOnlyConstantWitnessResidual : ℝ :=
  -Real.pi * (Real.sqrt 2 + 4) / 8

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

/-- Genuine radical-row audit: at the row-Jacobian layer, individual raw
coefficients ARE irrational here; the panel's rationality claim lives at
bucket-fiber-AGGREGATION level and remains OPEN.  For this selected entry the
Jacobian is `-sqrt 2 / 4`; the current `rawJacobianCoefficient` normalization
then exposes and cancels the same `sqrt 2` denominator. -/
theorem worstRadical_flatAngleJacobian_value :
    ReggeTTDerivativeGate.flatAngleJacobian (1 : Fin 6) (2 : Fin 6) =
      -(Real.sqrt 2) / 4 := by
  rw [ReggeTTDerivativeGate.flatAngleJacobian_cofactor_form]
  rw [Geometry.CofactorDerivatives.dihedralCos3SqClosedFormDeriv_eq_poly]
  norm_num [ReggeTTDerivativeGate.flatArccosFactor,
    Geometry.CofactorDerivatives.dihedralCos3SqPolyClosedFormDeriv,
    Geometry.CofactorDerivatives.dihedralDenom3PolyClosedDerivValue,
    Geometry.CofactorDerivatives.dihedralDenom3Poly,
    Geometry.CofactorPolynomial.cmCofactor3Poly,
    Geometry.CofactorPolynomial.cmCofactorPartial,
    Geometry.DihedralCayleyMenger.oppositeCMVertices,
    freudenthalTetSqEdges]
  rw [show Real.sqrt 32 = 4 * Real.sqrt 2 by
    rw [show (32 : ℝ) = 16 * 2 by norm_num]
    rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 16),
      show Real.sqrt (16 : ℝ) = 4 by norm_num]]
  ring

/-- 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 stencil-only constant block vanishes. The residual is a physical observable. The full rational bucket aggregation or zero-mode cancellation is proved. The declaration establishes anything about the ContinuumLimit engine's correctness.

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: