Pith. sign in
module module high

IndisputableMonolith.Gravity.ReggeComponentTheorem3D

show as:
view Lean formalization →

Packages the genuine geometric component of the 3D Regge action under the conformal weak-field ansatz, built from Cayley-Menger volumes, dihedral angles, and the Hessian. Gravity theorists matching discrete curvature to continuum Newton cite this package. Structure is definitional: it exposes the component record and comparison maps that the companion proof module discharges.

claimDefines the genuine geometric component package from the Cayley-Menger/dihedral/Hessian computation on a finite 3D triangulation, and the comparison that identifies it with the weak-field coefficient matrix of the conformal Regge action $S=\frac{1}{\kappa}\sum_h A_h\delta_h$ under the edge ansatz $\ell_{ij}=\ell_0\exp((\xi_i+\xi_j)/2)$.

background

Regge calculus replaces continuum curvature by deficit angles on a triangulation: the action is $S=\frac{1}{\kappa}\sum_h A_h\delta_h$, with hinge areas $A_h$ and deficits $\delta_h$. The upstream weak-field conformal module fixes the edge lengths by the ansatz $\ell_{ij}=\ell_0\exp((\xi_i+\xi_j)/2)$ and expands $S$ to second order in the conformal potentials $\xi$.

The Hessian module supplies the analytic interface for that quadratic form on a finite 3D complex: an explicit action, its Hessian matrix, and the theorem that the second-order Taylor coefficient is that matrix. Cayley-Menger determinants give volumes from edge lengths; dihedral angles give the deficits; their joint second variation is the geometric input.

This module sits between those two layers. It records the genuine component package (the geometric quadratic form produced by that computation) and the maps that compare it to the algebraic weak-field coefficient matrix, without yet proving the final identification theorem.

proof idea

Definition and packaging module, not a single end-to-end proof. It introduces the genuine component package as the geometric object coming out of the Cayley-Menger/dihedral/Hessian pipeline, then states comparison and Dirichlet-reduction lemmas that relate that package to the weak-field coefficient matrix. Heavy lifting (Hessian representation, conformal expansion identities) is imported from the Hessian and weak-field modules; the companion proof module closes the comparison target.

why it matters in Recognition Science

In the Recognition gravity stack this is the geometric half of the 3D Regge component theorem: the place where discrete curvature data become a concrete quadratic form ready for continuum comparison. Downstream, ReggeComponentTheorem3DProof "separates the independent dual-weight construction from the weak-field coefficient matrix and records the theorem that turns that geometric computation into ReggeComponentComparison." Without this package the final comparison has nothing geometric to match against. It is the bridge from T8-style three-dimensional structure (finite 3D triangulation, conformal edges) into the weak-field Newtonian limit of the discrete action.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (3)