IndisputableMonolith.Geometry.DihedralCofactorFormula
Coordinate-level formulas for the dihedral cosine of a tetrahedron edge from adjacent face normals. Opposite-vertex bookkeeping, edge vectors, cross-product normals, and the resulting numerator, squared denominator, and cosine are defined here. Downstream Regge-interior and dihedral-derivative modules import these identities. Mostly definitions plus elementary vector equalities linking dots and crosses to the geometric cosine.
claimFor a realized tetrahedron and edge $(i,j)$ with opposite vertices $(p,q)$, the two adjacent face normals are built as cross products of coordinate edge vectors from a base vertex. The geometric dihedral cosine is $\cos\theta = N/\sqrt{D}$ where $N$ is the inner product of the two normals and $D$ is the product of their squared norms (equivalently the normalized face-normal inner product).
background
Recognition Science geometry tracks tetrahedral dihedral angles both algebraically (Cayley-Menger cofactors) and metrically (realized edge vectors in Euclidean space). This module sits on the metric side. Upstream GramCayleyMenger isolates the bridge from the Euclidean Gram determinant of a realized tetrahedron to its Cayley-Menger determinant. Upstream DihedralCayleyMenger defines the tetrahedral dihedral cosine from Cayley-Menger cofactors for an edge $e=(i,j)$ with opposite vertices $(p,q)$.
Here the same edge is treated in coordinates. adjacentFaceOppositeVertices names the two remaining vertices opposite edge $(i,j)$. Coordinate edge vectors are differences of vertex positions; face normals are their cross products. Dot-product lemmas identify those vectors with the ambient inner product so that the geometric numerator, squared denominator, and cosine are ordinary Euclidean quantities.
The local setting is classical 3D vector geometry of a labeled tetrahedron, not yet the discrete curvature or Regge action. The module imports Mathlib cross and dot products and the two Cayley-Menger geometry modules above.
proof idea
Definition-heavy module, not a single theorem. It introduces opposite-vertex pairs for each edge, coordinate edge vectors (with equalities to base-point differences), and face normals as cross products. Lemmas then relate normal-normal and normal-self dots to the geometric numerator and squared denominator, and package the ratio as geometricDihedralCos. Cross-product forms of the numerator close the vector identities. No deep analytic argument: the content is bookkeeping plus standard $\mathbb{R}^3$ algebra so later modules can quote a named cosine.
why it matters in Recognition Science
Supplies the concrete face-normal cosine that the cofactor story must match and that analytic steps differentiate. Downstream AffineIndepInterior needs strict interior dihedral angles for the Regge closure program: its analytic core is that two linearly independent adjacent face normals have normalized dot product strictly in $(-1,1)$, and the remaining work is to prove those normals arise from the tetrahedron; this module is the source of those normals and their cosine. Downstream DihedralDerivatives isolates $d\theta=-(1/\sqrt{1-\cos^2\theta}),d(\cos\theta)$ once the Cayley-Menger cofactor cosine is differentiable; the geometric cosine defined here is the matching metric object.
In the broader RS geometry stack this is infrastructure between pure Cayley-Menger algebra and Regge-type curvature bookkeeping in $D=3$, not a forcing-chain landmark itself.
scope and limits
- Does not prove equality of geometric cosine with the Cayley-Menger cofactor cosine.
- Does not establish affine independence or strict interior bounds on the angle.
- Does not differentiate the cosine or the angle; that lives in DihedralDerivatives.
- Does not treat non-Euclidean or degenerate tetrahedra with vanishing face areas.
- Does not define Regge action, deficit angles, or curvature closure.
used by (2)
depends on (2)
declarations in this module (80)
-
def
adjacentFaceOppositeVertices -
def
coordEdgeVector -
theorem
coordEdgeVector_dot_eq_inner -
theorem
coordEdgeVector_eq_base_sub -
theorem
coordEdgeVector_dot_base_sub -
def
faceNormal -
theorem
faceNormal_dot_faceNormal -
theorem
faceNormal_dot_self -
def
geometricDihedralNumerator -
def
geometricDihedralDenomSq -
def
geometricDihedralCos -
theorem
geometricDihedralNumerator_cross -
theorem
geometricDihedralNumerator_edge0_gram -
theorem
cmCofactor3_edge0_eq_four_geometricNumerator -
theorem
faceNormal_edge0_left_self_gram -
theorem
faceNormal_edge0_right_self_gram -
theorem
cmCofactor3_edge0_left_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge0_right_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge0_diag_product_eq_sixteen_denomSq -
theorem
dotProduct_self_nonneg -
theorem
geometricDihedralDenomSq_nonneg -
theorem
abs_dot_div_sqrt_self_mul_self_le_one -
theorem
geometricDihedralCos_range -
theorem
geometricDihedralCos_interior_of_ne_endpoints -
theorem
cmCofactor3_edge0_sqrt_diag_product -
theorem
geometricDihedralCos_edge0_eq_cofactorRatio_of_sqrt -
theorem
geometricDihedralCos_edge0_eq_cmCofactorRatio -
theorem
geometricDihedralNumerator_edge1_gram -
theorem
cmCofactor3_edge1_eq_four_geometricNumerator -
theorem
faceNormal_edge1_left_self_gram -
theorem
faceNormal_edge1_right_self_gram -
theorem
cmCofactor3_edge1_left_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge1_right_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge1_diag_product_eq_sixteen_denomSq -
theorem
cmCofactor3_edge1_sqrt_diag_product -
theorem
geometricDihedralCos_edge1_eq_cmCofactorRatio -
theorem
geometricDihedralNumerator_edge2_gram -
theorem
cmCofactor3_edge2_eq_four_geometricNumerator -
theorem
faceNormal_edge2_left_self_gram -
theorem
faceNormal_edge2_right_self_gram -
theorem
cmCofactor3_edge2_left_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge2_right_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge2_diag_product_eq_sixteen_denomSq -
theorem
cmCofactor3_edge2_sqrt_diag_product -
theorem
geometricDihedralCos_edge2_eq_cmCofactorRatio -
theorem
geometricDihedralNumerator_edge3_gram -
theorem
cmCofactor3_edge3_eq_four_geometricNumerator -
theorem
faceNormal_edge3_left_self_gram -
theorem
faceNormal_edge3_right_self_gram -
theorem
cmCofactor3_edge3_left_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge3_right_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge3_diag_product_eq_sixteen_denomSq -
theorem
cmCofactor3_edge3_sqrt_diag_product -
theorem
geometricDihedralCos_edge3_eq_cmCofactorRatio -
theorem
geometricDihedralNumerator_edge4_gram -
theorem
cmCofactor3_edge4_eq_four_geometricNumerator -
theorem
faceNormal_edge4_left_self_gram -
theorem
faceNormal_edge4_right_self_gram -
theorem
cmCofactor3_edge4_left_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge4_right_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge4_diag_product_eq_sixteen_denomSq -
theorem
cmCofactor3_edge4_sqrt_diag_product -
theorem
geometricDihedralCos_edge4_eq_cmCofactorRatio -
theorem
geometricDihedralNumerator_edge5_gram -
theorem
cmCofactor3_edge5_eq_four_geometricNumerator -
theorem
faceNormal_edge5_left_self_gram -
theorem
faceNormal_edge5_right_self_gram -
theorem
cmCofactor3_edge5_left_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge5_right_diag_eq_neg_four_normalSq -
theorem
cmCofactor3_edge5_diag_product_eq_sixteen_denomSq -
theorem
cmCofactor3_edge5_sqrt_diag_product -
theorem
geometricDihedralCos_edge5_eq_cmCofactorRatio -
def
BergerCofactorFormula3 -
theorem
geometricDihedralCos_eq_cmCofactorRatio -
theorem
bergerCofactorFormula3 -
theorem
dihedralCos3Sq_sqEdgeOfPoints_range -
theorem
dihedralCos3Sq_sqEdgeOfPoints_interior_of_ne_endpoints -
theorem
dihedralCos3_range_of_realization -
def
dihedralAngleData3_of_realization -
theorem
dihedralCos3_interior_of_realization_ne_endpoints