IndisputableMonolith.Geometry.FourTetSignedDeficit
Specializes Cayley-Menger matrices, minors, and dihedral cofactors to one tetrahedron in the four-tet star: hinge and spokes of squared length 1, rim squared length p. Records edge data, nondegeneracy, and the 33/34/44 cofactor identities needed for signed hinge deficits. Gravity residual work cites it when identifying mesh geometric deficit in 4D. Mostly definitional specialization plus determinant algebra on the imported CM layer.
claimFor the four-tetrahedron star with hinge squared length $1$, spoke squared lengths $1$, and rim squared length $p$, each tetrahedron has edge-squared data $(a_0,\ldots,a_5)=(1,1,1,1,1,p)$ (hinge as edge $0$). The module defines the associated Cayley-Menger value, nondegeneracy, and the $5\times 5$ CM minors/cofactors (especially the $3$-$4$, $3$-$3$, and $4$-$4$ blocks) used to form dihedral cosines on the hinge.
background
In Regge calculus the local curvature is a signed angular deficit around a hinge, summed from dihedral angles of the tetrahedra incident on that edge. The four-tet star is the standard minimal probe: four tetrahedra around a common hinge, with outer rim edges of common squared length $p$.
Upstream, CayleyMengerPolynomial starts the program of matching the genuine Regge second-variation matrix $M_{ij}$ from CM/dihedral derivatives to face areas. CayleyMengerMatrix connects the explicit tetrahedral polynomial $\mathrm{cm}_3$ to the $5\times 5$ Cayley-Menger determinant and its cofactors. DihedralCayleyMenger defines dihedral cosines from those cofactors; DihedralDerivatives supplies $d\theta=-(1/\sqrt{1-\cos^2\theta}),d(\cos\theta)$.
This module freezes the geometry to unit hinge and spokes and variable rim $p$, so every minor and cofactor becomes a univariate object in $p$, ready for deficit and residual analysis.
proof idea
Definition-and-identity module, not a single deep theorem. It introduces the squared-edge tuple of the star tetrahedron, the rim parameter, the specialized $\mathrm{cm}_3$ value, and a nondegeneracy predicate. It then builds the relevant CM minor matrices (notably the $3$-$4$ block) and proves, by direct expansion against the general cofactor layer from CayleyMengerMatrix, equalities identifying those minors and the $33/34/44$ cofactors with their specialized closed forms. Dihedral cosine and derivative machinery is imported, not re-proved.
why it matters in Recognition Science
Direct import for Gravity.Analysis.RecognitionMeshGeometricDeficit4D, the Wave B attack on the residual that mesh geometricDeficit is identified without an extra ratio factor (TypedResidual_mesh_geometricDeficit_identified). That closes a QG full-completion gap in the recognition-mesh gravity stack.
In the geometry program opened by CayleyMengerPolynomial (matching Regge $M_{ij}$ componentwise to $\mathrm{area}(f_{ij})$), the four-tet star is the concrete configuration on which signed deficit and second-variation coefficients are evaluated. The specialized cofactors here are the algebraic input to dihedral angles around the hinge, hence to discrete curvature feeding 4D recognition-mesh analysis.
scope and limits
- Does not give a closed-form signed deficit angle as a function of p.
- Does not treat unequal hinge, spoke, or rim lengths.
- Does not prove positivity, monotonicity, or bounds on the deficit.
- Does not itself compare the Regge Hessian M_ij to face areas.
- Does not address continuum limits or global mesh topology.
used by (1)
depends on (4)
declarations in this module (37)
-
def
starSq -
def
starP -
theorem
star_cm3 -
theorem
fourTet_nondegenerate -
def
starMinor34Matrix -
theorem
det_starMinor34 -
theorem
star_minor_34_eq -
theorem
star_cofactor_34 -
theorem
star_minor_33_eq -
theorem
star_cofactor_33 -
theorem
star_minor_44_eq -
theorem
star_cofactor_44 -
theorem
star_denom -
theorem
fourTet_centralDihedralCosine -
theorem
fourTet_regular_sanity -
theorem
star_q -
def
starDeficit -
theorem
starDeficit_convention_note -
theorem
fourTet_deficit_eq -
theorem
starDeficit_eq_arcsin -
theorem
starDeficit_flat -
theorem
starDeficit_odd -
theorem
fourTet_deficit_sign -
theorem
arcsin_le_pi_div_two_mul -
theorem
abs_arcsin_le_abs -
theorem
starDeficit_abs_le -
theorem
star_mesh_bound -
theorem
fourTet_weak_pair -
lemma
is -
theorem
even_ledger_cannot_match_signed_regge -
theorem
even_cannot_match_starDeficit -
structure
FourTetSignedDeficitStatus -
def
status -
theorem
status_signed_deficit_kernel_checked -
theorem
status_weak_field_pair_constructed -
theorem
status_firewall_no_ledger_imports -
theorem
status_n5_torus_extension_closed