module module high

`IndisputableMonolith.Geometry.FourTetSignedDeficit`

Specializes Cayley-Menger and dihedral cofactor machinery to one tetrahedron in the four-tet star: hinge and spokes of squared length 1, rim squared length p, edge data (1,1,1,1,1,p). Records CM value, nondegeneracy, and the 3-4 (and sibling) minors/cofactors used for signed angular deficit. Gravity and Regge analysts matching second-variation coefficients to face areas cite it. Mostly definitional specialization plus determinant identities from the imported CM layer.

claimFix the four-tetrahedron star with hinge squared length $1$, spoke squared lengths $1$, and rim squared length $p$. Each tetrahedron has squared-edge data $(a_0,\ldots,a_5)=(1,1,1,1,1,p)$ with hinge $AB$ as edge $0$. The module defines the associated Cayley-Menger value, nondegeneracy, and the relevant $5\times 5$ Cayley-Menger minors and cofactors (especially the $3$-$4$ block) that enter the dihedral cosine on that edge.

background

Recognition Science geometry work builds tetrahedral volumes and dihedral angles from the Cayley-Menger determinant rather than from ad hoc coordinate charts. The imported polynomial layer supplies the explicit degree-3 Cayley-Menger polynomial cm3 in the six squared edge lengths; the matrix layer identifies that polynomial with the standard $5\times 5$ bordered Gram determinant and exposes minors and cofactors. Dihedral cosines are then read from those cofactors, and angle derivatives follow by the chain rule through $\arccos$.

The four-tet star is the local model for a hinge in a 3D triangulation: four tetrahedra meet along a common edge, with outer rim edges closing the link. This module freezes the squared hinge and spoke lengths to $1$ and leaves a single free rim parameter $p$, so every subsequent deficit or second-variation identity is a function of one real variable. The DOC_COMMENT fixes the edge ordering: hinge $AB$ is edge $0$, and the six-tuple is $(1,1,1,1,1,p)$.

Upstream modules already prove the general cofactor cosine formula and the analytic derivative $d\theta=-(1-\cos^2\theta)^{-1/2},d(\cos\theta)$. Here those tools are instantiated on the star edge data so that signed deficit and mesh geometric-deficit residuals can be computed without re-deriving the matrix algebra.

proof idea

Definition-and-identity module, not a single deep theorem. It introduces the star edge-squared tuple and the associated Cayley-Menger evaluation, states nondegeneracy for admissible $p$, then builds the concrete minor matrices (especially the $3$-$4$ minor) and evaluates their determinants and cofactors by reduction to the general Cayley-Menger matrix API. Sibling lemmas equate those specialized minors and cofactors to the expressions needed by the dihedral cosine formula. No independent analytic argument: the work is specialization, matrix algebra, and reuse of imported determinant identities.

why it matters in Recognition Science

Feeds the gravity analysis module on 4D recognition-mesh geometric deficit, which attacks the Wave B residual that identifies mesh geometricDeficit without an extraneous ratio factor. That downstream file frames the work as closing a QG full-completion gap: the genuine Regge second-variation coefficient matrix built from Cayley-Menger dihedral derivatives must match face areas componentwise. The four-tet star is the minimal hinge configuration where signed angular deficit is well-defined, so cofactors and nondegeneracy on $(1,1,1,1,1,p)$ are the concrete geometric input to that residual. In the broader RS geometry stack this sits under the program begun in the Cayley-Menger polynomial module: replace prose dihedral references by fully expanded CM cofactors, then compare the resulting Hessian to area data. Without this specialization, the mesh-deficit identification would still carry an unexpanded tetrahedron model.

scope and limits

Does not prove global Regge Hessian equals face-area matrix for arbitrary meshes.
Does not treat hinges with unequal spoke lengths or non-unit hinge length.
Does not derive continuum Einstein equations or curvature limits.
Does not fix a numerical value of the rim parameter p; it remains free.
Does not itself close the Wave B geometricDeficit residual; that lives downstream.

used by (1)

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

IndisputableMonolith.Gravity.Analysis.RecognitionMeshGeometricDeficit4D module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMengerMatrix module_import
IndisputableMonolith.Geometry.CayleyMengerPolynomial module_import
IndisputableMonolith.Geometry.DihedralCayleyMenger module_import
IndisputableMonolith.Geometry.DihedralDerivatives module_import

declarations in this module (37)

def starSq L109
def starP L122
theorem star_cm3 L128
theorem fourTet_nondegenerate L143
def starMinor34Matrix L158
theorem det_starMinor34 L164
theorem star_minor_34_eq L171
theorem star_cofactor_34 L179
theorem star_minor_33_eq L186
theorem star_cofactor_33 L194
theorem star_minor_44_eq L200
theorem star_cofactor_44 L208
theorem star_denom L215
theorem fourTet_centralDihedralCosine L231
theorem fourTet_regular_sanity L239
theorem star_q L247
def starDeficit L257
theorem starDeficit_convention_note L266
theorem fourTet_deficit_eq L276
theorem starDeficit_eq_arcsin L282
theorem starDeficit_flat L288
theorem starDeficit_odd L294
theorem fourTet_deficit_sign L304
theorem arcsin_le_pi_div_two_mul L320
theorem abs_arcsin_le_abs L337
theorem starDeficit_abs_le L350
theorem star_mesh_bound L359
theorem fourTet_weak_pair L385
lemma is L432
theorem even_ledger_cannot_match_signed_regge L433
theorem even_cannot_match_starDeficit L452
structure FourTetSignedDeficitStatus L464
def status L474
theorem status_signed_deficit_kernel_checked L480
theorem status_weak_field_pair_constructed L483
theorem status_firewall_no_ledger_imports L486
theorem status_n5_torus_extension_closed L490