Pith. sign in
module module moderate

IndisputableMonolith.Gravity.ReggeComponentTheorem3DProof

show as:
view Lean formalization →

Proof support for the 3D Regge component theorem: independent dual weights on vertex pairs of a triangulation, built from incidence geometry rather than by negating the Regge coefficient matrix. Supplies the geometric data that feed canonical weak-field comparison packages. Anyone citing the 3D Regge Hessian bridge or the weak-field conformal reduction would land here. The module is constructive: weights from edge/vertex incidence, then packaging lemmas into the existing comparison interface.

claimOn a finite 3D triangulation, assign independent dual weights $w_{ij}$ to unordered vertex pairs $(i,j)$, obtained from edge-pair incidence and vertex-pair hinge data, not from $-H_{ij}$ of the Regge Hessian. From incidence-consistent weights one builds a canonical weak-field data package whose bilinear coefficients, row sums, and off-diagonal components match the genuine Regge component comparison interface.

background

Regge calculus discretizes Einstein gravity on a simplicial complex: curvature lives on hinges (codimension-2 faces), and the action is a sum of deficit angles times hinge volumes. In three spatial dimensions the Hessian of that action, under a conformal (length) ansatz, is the discrete object that must match continuum weak-field gravity after a Dirichlet-form reduction.

Upstream, ReggeActionConcrete isolates the analytic second-variation step for a finite 3D triangulation and packages it as ReggeHessianData. The bridge module ReggeComponentTheorem3D turns a genuine component package into the existing ReggeComponentComparison interface used by the weak-field conformal Regge theory.

This module supplies the missing geometric dual weights: edge-pair incidence weights and vertex-pair hinge weights, with symmetry and nonnegativity, then lifts incidence-consistent data to independent dual weights and to canonical weak-field data (bilinear coefficient, row sum, off-diagonal component match).

proof idea

Definition-and-packaging module, not a single deep theorem. It introduces independent dual weights as geometric data on vertex pairs, together with two concrete weight constructions (edge-pair incidence and vertex-pair hinge). Symmetry lemmas for both weights and nonnegativity for the hinge weight are recorded. Two constructors produce independent dual weights from incidence data and from consistency hypotheses. A further constructor builds canonical weak-field data from incidence; three comparison lemmas check that the bilinear coefficient, row sum, and off-diagonal components of that package match the component-theorem interface expected downstream.

why it matters in Recognition Science

Closes the geometric side of the 3D Regge component bridge: without independent dual weights that are not merely $-H_{ij}$, the genuine Hessian package cannot be fed into the weak-field conformal comparison already proved elsewhere. The parent story is the chain Concrete Regge Hessian $\to$ GenuineComponentPackage $\to$ ReggeComponentComparison $\to$ Dirichlet-form reduction in WeakFieldConformalRegge. In the Recognition Science gravity track this is the discrete 3D hinge calculus that must eventually sit under continuum limits and the forced $D=3$ landmark (T8). No downstream consumers are wired in the graph yet; the module is the proof warehouse for the bridge interfaces it imports.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (19)