meshGeometricDeficit_eq_arcsin
plain-language theorem explainer
The mesh geometric deficit equals four times arcsin of the deformation parameter. Gravity analysts cite this when they need a closed, ratio-free expression for the signed Regge hinge deficit on the recognition mesh. The proof is a one-line transfer of the banked star-deficit arcsin identity through the definitional alias.
Claim. For every real deformation parameter $h$, the mesh geometric deficit at $h$ equals $4\arcsin(h)$.
background
Wave B residual R1 identifies the mesh geometric deficit on the recognition Freudenthal mesh without ratio fields. The deformation carrier is a real parameter $h$; the geometric object is the signed Regge-convention star deficit built from squared-edge data and dihedral angles, not from $x$-ratios or logarithms.
meshGeometricDeficit is defined to be exactly starDeficit. The latter is the four-tetrahedron star deficit in Regge convention: a signed angle defect assembled from dihedral angles of squared-edge geometry (dihedralAngle3Sq). Upstream, starDeficit_eq_arcsin already records the closed form starDeficit h = 4 arcsin h, obtained by rewriting the four-tet deficit through the arccos–arcsin identity and simplifying.
The local setting deliberately stops short of a full triangulation lift onto ReggeActionConcrete.deficitAngle; the binding is the abstract star convention plus the exact-$J$/true-Regge Hessian context on the canonical recognition mesh.
proof idea
One-line term proof: apply starDeficit_eq_arcsin at $h$. Because meshGeometricDeficit is definitionally starDeficit, the arcsin closed form transfers verbatim. No extra algebraic work occurs at this layer; the ring and arccos-to-arcsin rewrite live in the upstream geometry lemma.
why it matters
Gives the geometry-first closed form demanded by Wave B residual R1: a signed Regge hinge deficit free of xRatio and log xRatio. Downstream, meshGeometricDeficit_abs_le_two_pi rewrites through this identity and uses |arcsin h| ≤ π/2 to bank the uniform bound $|δ| ≤ 2π` needed for hinge-kappa control.
In the Recognition gravity stack this is the clean analytic handle on the mesh deficit before constitutive coupling or ratio-derived claims. It does not flip gap1_bridge_derived, inhabit DeficitSourceConstitutiveCoupling, or claim recognition_ratio_derived. The recorded open remainder is lifting starDeficit onto an encoded triangulation of the recognition Freudenthal mesh (encodedFreudenthalLiftOpen).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.