Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.RecognitionMeshGeometricDeficit4D

show as:
view Lean formalization →

Defines the mesh geometric deficit: the banked signed Regge-convention star deficit as a function of a one-parameter deformation, built only from squared-edge and dihedral data. Gravity and QG closure work cite it as Wave B residual R1. Equalities to the abstract star deficit and arcsin form, plus oddness, flatness, and sign lemmas, pin the identification without logs or edge-length ratios.

claimOn the Recognition mesh four-tet hinge star, the mesh geometric deficit $\Delta_{\mathrm{mesh}}(t)$ is the signed Regge-convention star deficit of the squared-edge configuration at deformation parameter $t$, assembled from squared edge lengths and three-dimensional dihedral angles. It equals the abstract four-tet star deficit, admits an arcsin presentation, is odd in $t$, vanishes at the flat point, and has definite sign in the weak-field regime.

background

The setting is the QG full-theory campaign on a Recognition mesh carrier for the periodic Freudenthal 4-torus. Upstream, the four-tet signed-deficit module supplies an abstract one-parameter family of hinge configurations (squared-edge data for four congruent tetrahedra around a common hinge) whose star-local Regge deficit is strictly positive for one sign of the parameter and strictly negative for the other, with explicit mesh bounds in the weak field.

The Regge 4D star-kernel layer imports Freudenthal incidence, the 15-class stencil, and seed two-simplex dihedral cosine calculus; the exact-J bridge attaches a value-level action whose amplitude Hessian is the Option-C midpoint Bloch symbol on the same torus family. The geometric deficit here is deliberately free of $x$-ratio and $\log$: it is pure squared-edge / dihedral geometry (starSq, dihedral angle from squared data).

proof idea

Definition module plus identification lemmas. The main object is defined from squared-edge star data and 3D dihedral angles in the Regge convention, then equated to the abstract four-tet star deficit and to an arcsin form. Oddness, vanishing at the flat configuration, and weak-field sign are proved from that geometry. Typed-residual closure statements record that the mesh geometric deficit discharges the banked R1 identification; decoy lemmas separate it from even functions and from log-even ratio constructions over hinge kappa.

why it matters in Recognition Science

This module banks Wave B residual R1 (meshGeometricDeficit) in the QG residual DAG. Downstream, dual-entry coupling assembles R1 with hinge kappa (R2) and dual-entry strain (R3) into an inhabited DeficitSourceConstitutiveCoupling. The hinge-kappa module continues the no-$x$Ratio discipline for R2. An audit module requires the closure theorem and decoys to print within [propext, Classical.choice, Quot.sound]. In the broader RS gravity stack it is the geometric deficit side of the Recognition mesh, feeding continuum and constitutive coupling without smuggling logarithmic edge ratios into the deficit definition.

scope and limits

used by (3)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (16)