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 pure function of the deformation parameter, built only from squared-edge and dihedral geometry. Gravity and QG continuum-closure workers 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; decoys rule out even and log-ratio impostors.

claimOn the Recognition mesh, the geometric deficit $\delta_{\mathrm{mesh}}(\varepsilon)$ is the signed Regge-convention star deficit of the four-tetrahedron hinge, expressed solely through squared edge lengths and three-dimensional dihedral angles. It equals the abstract star deficit, admits an arcsin closed form, is odd in the deformation, vanishes in the flat limit, and carries the correct weak-field sign; no edge-length ratio or logarithm enters the definition.

background

Recognition Science gravity work packages the continuum limit of a periodic Freudenthal 4-torus mesh. Local curvature is carried by Regge hinge deficits: at each interior edge (hinge), four congruent tetrahedra meet, and the deficit is $2\pi$ minus the sum of dihedral angles around that hinge. The signed version distinguishes positive and negative weak-field curvature.

Upstream, FourTetSignedDeficit supplies the first kernel-checked signed Regge-convention deficits on an abstract four-tet star (squared-edge data, certified nondegenerate), strictly positive for one deformation sign and strictly negative for the other. ReggeHinge4DStarKernel lifts that calculus to the full periodic-lattice star class on the Freudenthal incidence layer. RecognitionMeshExactJBridge4D attaches the Recognition mesh carrier and the exact-$J$ action whose Hessian is the Option-C midpoint Bloch symbol.

This module banks the geometric half of that story: a deficit functional of the deformation alone, free of $x$-ratio and $\log$, so later constitutive coupling can treat geometry and source strain as separate residual slots.

proof idea

Definition-first module. The main object is introduced from squared-edge star data and the three-simplex dihedral cosine calculus already certified upstream; no new geometric primitives. Companion lemmas identify it with the abstract star deficit and with an arcsin expression, record the Regge sign convention, and prove oddness, flat vanishing, and weak-field sign. Two decoy inequalities show that even functions of the deformation, and log-even ratio-over-kappa expressions, cannot equal the star deficit. Closure lemmas package the identification as a typed residual discharge for the Wave B DAG.

why it matters in Recognition Science

This is Wave B residual R1 in the QG full-completion campaign: the geometric deficit source that later constitutive coupling must consume. Downstream, RecognitionMeshDualEntryCoupling4D assembles banked R1 (this deficit), R2 (hinge kappa with source-dominated admissibility), and R3 (dual-entry strain state) into an inhabited DeficitSourceConstitutiveCoupling. RecognitionMeshHingeKappa4D is the parallel R2 track, deliberately also free of $x$-ratio. The audit module requires the closure theorem and decoys to print inside {propext, Classical.choice, Quot.sound} only.

In the broader RS chain the object sits on the gravity side of the Recognition mesh, after the exact-$J$ bridge and before dual-entry coupling closes the continuum residual DAG. It does not itself force $D=3$ or the eight-tick octave; those are upstream forcing landmarks. It does enforce that curvature bookkeeping on the mesh is pure geometry, which is the separation the dual-entry residual needs.

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)