Gravity Analysis Regge Bloch M2 Symbol4 D Class Dot Slot Deficit Ker Gauge

The gauge vanishing

In numerical relativity, a common check is to test a proposed discretization against a configuration that should produce no physical signal. The declaration classDot_slotDeficitKer_gauge establishes exactly such a vanishing result for one piece of a four-dimensional Regge calculus model. Regge calculus approximates spacetime by a network of flat building blocks, here four-dimensional simplices, and this declaration concerns a specific "gauge" configuration, a choice of variables that represents a pure coordinate or redundancy, not a physical change.

The theorem states that for this gauge configuration, a quantity called the slot deficit kernel, which measures the mismatch or deficit around a hinge, has zero overlap with the configuration. In plainer terms, the gauge configuration is invisible to this particular diagnostic. The proof is fully machine-checked, meaning every step is verified by a computer, with no gaps or unproven assumptions. This is a concrete, closed result within a larger research program.

This vanishing is not an accident. The proof works by showing that the gauge configuration lies in the kernel of the slot deficit operator, meaning the operator sends it to zero. This is a structural property, not a numerical coincidence. The result is one of several similar vanishing theorems, including one for a configuration called axisTTPlus, a specific test configuration in the model. Together, these provide evidence that the discretization scheme is well-behaved in these specific cases.

In Recognition Science, this is part of a larger effort to derive gravitational theory from a discrete ledger of recognition events. The framework models spacetime as arising from such a ledger, and this declaration is a technical step in analyzing the resulting discrete geometry. The framework's machine-checked library of formal theorems contains this result as a verified component.

What this declaration does not claim is equally important. It does not prove that the full gravitational action, called the Einstein-Hilbert action, emerges from the discrete model. That remains an open target. It does not establish the behavior for a general configuration, only for the specific gauge and axis cases. And it does not claim to recover any dynamical feature like the gap action. The result is a precise, narrow, and verified fact, not a sweeping conclusion.

theorem classDot_slotDeficitKer_gauge (s : Fin 24) (t : Fin 10) :
    classDot (slotDeficitKer s t) decoyGauge = 0 := by
  rw [classDot_slotDeficit_reindex]
  simp_rw [kernel11_eq_sign, classCoeff_decoyGauge_int]
  have h := congrArg (fun n : ℤ => (n : ℝ)) (slotKerDotZ_gauge s t)
  simpa [slotKerDotZ, Int.cast_sum, Int.cast_mul] using h

theorem classDot_slotDeficitKer_gauge (s : Fin 24) (t : Fin 10) :
    classDot (slotDeficitKer s t) decoyGauge = 0 := by
  rw [classDot_slotDeficit_reindex]
  simp_rw [kernel11_eq_sign, classCoeff_decoyGauge_int]
  have h := congrArg (fun n : ℤ => (n : ℝ)) (slotKerDotZ_gauge s t)
  simpa [slotKerDotZ, Int.cast_sum, Int.cast_mul] using h

theorem classDot_slotDeficitKer_axis (s : Fin 24) (t : Fin 10) :
    classDot (slotDeficitKer s t) axisTTPlus = 0 := by
  rw [classDot_slotDeficit_reindex]
  simp_rw [kernel11_eq_sign, classCoeff_axisTTPlus_int]
  have h := congrArg (fun n : ℤ => (n : ℝ)) (slotKerDotZ_axis s t)
  simpa [slotKerDotZ, Int.cast_sum, Int.cast_mul] using h

What this page does not claim

It does not prove that the full Einstein-Hilbert action emerges from the discrete model. It does not establish the behavior for a general configuration, only for the specific gauge and axis cases. It does not claim to recover any dynamical feature like the gap action.

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/ReggeBlochM2Symbol4D.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: