Pith. sign in
module module moderate

IndisputableMonolith.Gravity.ReggeComponentTheorem3DProof

show as:
view Lean formalization →

Constructs independent dual weights on vertex pairs of a 3D triangulation and packages them as canonical weak-field data for the Regge component comparison. Gravity workers cite it when matching geometric hinge weights to the bilinear coefficient matrix without defining duals by matrix negation. The argument builds incidence and hinge weights, proves symmetry and nonnegativity, then feeds the existing weak-field interface.

claimOn a finite 3D triangulation, assign independent dual weights $w_{ij}$ to vertex pairs from edge-pair incidence and vertex-pair hinge data. These weights are geometric (not $-A_{ij}$ from the Regge coefficient matrix). From consistent incidence one obtains canonical weak-field data whose bilinear coefficient, row sums, and off-diagonal components match the Regge component comparison interface.

background

Recognition Science gravity work reduces weak-field conformal dynamics on a triangulation to a Dirichlet form via a Regge Hessian. Upstream, ReggeActionConcrete isolates the final analytic Hessian step: a concrete action package supplies the Regge action under the conformal ansatz and proves its second variation, exposing a ReggeHessianData interface.

ReggeComponentTheorem3D then bridges a genuine 3D Regge Hessian package to the weak-field conformal Regge bridge: geometric computation yields a GenuineComponentPackage, turned into ReggeComponentComparison and hence into the Dirichlet-form reduction already proved in WeakFieldConformalRegge.

This module supplies the missing geometric dual side. Independent dual weights on vertex pairs are geometric data attached to the triangulation; they are not defined by negating the Regge coefficient matrix. Edge-pair incidence weights and vertex-pair hinge weights are the elementary building blocks, with symmetry and nonnegativity lemmas.

proof idea

Definition-heavy module with short algebraic lemmas, not a single monolithic theorem. It introduces independent dual weights, edge-pair incidence weight, and vertex-pair hinge weight. Symmetry of both weights and nonnegativity of the hinge weight are recorded as elementary facts.

From incidence (or a consistency hypothesis) one builds an independent dual-weight package, then a canonical weak-field data object. Three comparison lemmas check that this canonical data reproduces the bilinear coefficient, the row-sum condition, and the off-diagonal component match required by the Regge component interface. The structure is: geometric weights → dual package → canonical weak-field data → component identities.

why it matters in Recognition Science

Closes the geometric half of the 3D Regge component bridge. Without independent dual weights that are not mere matrix negations, the genuine Hessian package cannot be fed honestly into ReggeComponentComparison and the Dirichlet-form reduction in WeakFieldConformalRegge.

Parent chain: concrete Hessian (ReggeActionConcrete) → component bridge (ReggeComponentTheorem3D) → this dual-weight and canonical-data construction. In the broader RS gravity story this is the discrete geometric input that lets the weak-field conformal ansatz sit on a real 3D triangulation rather than a formal bilinear form. No downstream consumers are wired in the graph yet; the module is the proof-side filler for the 3D component theorem interface.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (19)