Gravity Discrete Vacuum Einstein Incidence Deficit Separating Of Recovering

The recovery condition

In the discrete vacuum Einstein equation, the central object is the deficit angle, the angle by which the flat space around an edge fails to close when you glue tetrahedra together. The vacuum equation demands that this deficit be zero at every edge. A triangulation of space is the discrete stand-in for a smooth manifold, and the equation is the discrete analogue of Einstein's field equations in empty space.

The framework's library, a machine-checked collection of formal theorems, proves a key structural fact about this equation. The declaration incidenceDeficitSeparating_of_recovering establishes that if a triangulation satisfies a certain recovery condition, then the vacuum equation is well-posed: the only way for all variations of the action to vanish is for every edge deficit to be exactly zero. The recovery condition itself is a bookkeeping property: it says that by measuring how edge lengths change when you move a single vertex, you can reconstruct the entire deficit vector. This is a rank condition on the incidence matrix of the triangulation, a real geometric input, not a consequence of local tetrahedron nondegeneracy.

The theorem is the reverse implication in a larger equivalence. The forward direction, that zero deficit implies criticality of the action, follows from a global Schläfli cancellation. The reverse direction, that criticality implies zero deficit, is the nontrivial one, and it is exactly what the recovery condition supplies. Without it, the vacuum equations could have spurious solutions where the action is stationary but the deficit is not zero.

What the theorem does not claim is that every triangulation satisfies the recovery condition. It is a hypothesis on the triangulation, a named input to the discrete Einstein equation, not a proven property of all triangulations. The library records this as a structure, RecoveringIncidenceTriangulation, which is a promise that the recovery condition holds, not a proof that it always does. The theorem also does not claim that the recovery condition is necessary for the equivalence; it only shows that it is sufficient.

The practical consequence is a clean separation of concerns. The discrete vacuum equation can be stated and used once the recovery condition is assumed, and the hard geometric work of proving that condition for specific triangulations is left as a separate, well-defined problem. This is how the framework builds large structures: by isolating the precise input needed for a theorem, rather than pretending the input is free.

theorem incidenceDeficitSeparating_of_recovering
    (K : Triangulation3D)
    (hRecover : IncidenceDeficitRecovering K) :
    IncidenceDeficitSeparating K := by
  rcases hRecover with ⟨recover, hrecover⟩
  intro δ hpair
  funext e
  rw [hrecover δ e]
  apply Finset.sum_eq_zero
  intro i _
  rw [hpair (fun j : Fin K.nV => if j = i then (1 : ℝ) else 0)]
  ring

/-- Concrete recovery/rank certificate for incidence separation.  The scalar
observations are the directional pairings against vertex-basis potentials. -/
def IncidenceDeficitRecovering (K : Triangulation3D) : Prop :=
  ∃ recover : Fin K.nE → Fin K.nV → ℝ,
    ∀ δ : Fin K.nE → ℝ, ∀ e : Fin K.nE,
      δ e =
        ∑ i : Fin K.nV,
          recover e i *
            (∑ e' : Fin K.nE,
              δ e' * directionalLengthCoefficient K
                (fun j : Fin K.nV => if j = i then (1 : ℝ) else 0) e')

theorem zero_deficit_of_flat_configuration
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_flat : FlatConfiguration K hK) :
    ZeroDeficitAtFlat K :=
  h_flat.flat_deficit_zero

theorem zero_deficit_of_critical_of_variationFormula_of_separating
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hFormula : ReggeFirstVariationFormula K hK)
    (hSep : IncidenceDeficitSeparating K)
    (hCrit : CriticalAtFlat K hK) :
    ZeroDeficitAtFlat K := by
  unfold CriticalAtFlat ReggeActionCriticalAtZero at hCrit
  unfold ZeroDeficitAtFlat
  have hdelta :
      (fun e : Fin K.nE => deficitAngle K (zeroPotential K) e) = 0 := by
    apply hSep
    intro η
    have happly := congrArg (fun L : VertexPotential K →L[ℝ] ℝ => L η) hCrit
    have hzero :
        (fderiv ℝ (reggeAction K hK) (zeroPotential K)) η = 0 := by
      simpa using happly
    have hformula := hFormula.variation_formula η
    rw [hformula] at hzero
    simpa using hzero
  intro e
  exact congrFun hdelta e

What this page does not claim

The recovery condition holds for every triangulation. The recovery condition is necessary for the vacuum equivalence. The theorem proves the discrete vacuum equation itself; it only proves a structural implication about it.

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