Pith. sign in
module module moderate

IndisputableMonolith.Gravity.DiscreteVacuumEinstein

show as:
view Lean formalization →

Discrete vacuum Einstein package for Regge gravity: flat edge-length data has zero deficit on every global edge, and the Regge action is critical there. The module defines vertex-to-edge incidence derivatives, separating/recovering predicates for deficit reconstruction from vertex probes, and the first-variation formula matching hinge derivatives to incidence. Downstream restricted recovery cites it as the unrestricted (too strong) bulk target.

claimFor a triangulation with edge lengths $\ell$, the flat configuration has Regge deficit $\delta_e=0$ at every global edge $e$, and the Regge action $S_{\mathrm{Regge}}$ is critical at that point. Vertex length probes induce an incidence map on edge-deficit vectors; separating and recovering predicates record injectivity and surjectivity of that map, with a first-variation identity equating hinge derivatives to incidence coefficients.

background

Regge calculus replaces smooth curvature by deficit angles on hinges (edges in 3D) of a simplicial complex. Edge lengths $\ell$ are the dynamical variables; the Regge action is a sum of hinge volumes times deficits. The vacuum Einstein condition is vanishing deficit everywhere, so flat length assignments are the discrete Ricci-flat backgrounds.

This module sits under Gravity and imports the second-variation scaffolding from ReggeActionSecondVariation, whose doc states nonlinear second-variation and cubic-remainder targets while the full Cayley-Menger/arccos expansion remains named input structure. Local objects include zero-deficit-at-flat, criticality-at-flat, vertex-edge incidence derivatives, directional length coefficients, and matching lemmas between hinge derivatives and incidence.

Incidence predicates (separating, recovering) formalize when vertex probes can distinguish or reconstruct an arbitrary edge-deficit vector. That unrestricted recovery demand is the mathematical ideal; bulk 3D lattices typically have more edges than vertices, so a later module weakens it.

proof idea

Definition-and-lemma module, not a single theorem. Core facts: zero deficit of the flat configuration (and the named ZeroDeficitAtFlat structure), criticality of the Regge action at flat data, and a first-variation formula identifying hinge derivatives with incidence coefficients (HingeDerivativeMatchesIncidence and its simplified form). Separating and recovering incidence predicates are introduced as Props on triangulations; a short implication shows recovering implies separating. RecoveringIncidenceTriangulation packages the geometric hypothesis that vertex probes suffice. Arguments are mostly algebraic identities and one-line wrappers over the imported Regge second-variation interface, not a full Cayley-Menger expansion.

why it matters in Recognition Science

Supplies the unrestricted discrete vacuum Einstein layer that RestrictedIncidenceRecovery imports and deliberately weakens. Downstream doc: "The unrestricted recovery predicate in DiscreteVacuumEinstein asks vertex probes to recover an arbitrary edge-deficit vector. That is too strong for bulk 3D lattices, where there are generally more edge variables than vertex probes." So this module states the ideal vacuum and incidence targets; the restricted sibling proves the version valid for bulk 3D.

In the broader RS gravity stack it anchors the discrete Ricci-flat background against which second variation and cubic remainder (from the imported ReggeActionSecondVariation module) are measured. It does not yet close the full nonlinear expansion; it freezes the vacuum and first-variation interface those expansions need.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (17)