arccos_endpoint_hypotheses_of_interior

The module isolates the calculus step for dihedral angles: once a Cayley–Menger cofactor cosine is differentiable, the angle $\theta = \arccos(\cos\theta)$ has the classical derivative $d\theta = -(1/\sqrt{1-\cos^2\theta}),d(\cos\theta)$. Mathlib’s derivative of $\arccos$ requires the argument to avoid the endpoints $\pm 1$, where the derivative blows up.

Sibling lemmas such as hasDerivAt_arccos_comp therefore take hypotheses $c \neq -1$ and $c \neq 1$. In geometric settings one usually obtains the stronger open-interval statement $-1 < c < 1$ (nondegenerate tetrahedra, causal Euclidean range). This lemma is the trivial bridge from that interior range to the endpoint form the arccos API expects.

Downstream, Euclidean angle derivatives on the causal band and local analytic flat charts for Regge triangulations both need exactly this conversion before they can invoke the chain rule through arccos.

Term-mode proof by constructor on the conjunction. Each conjunct is discharged by assuming equality to the forbidden endpoint and applying linarith against the corresponding strict inequality. No external lemmas are required.

Feeds the Euclidean angle derivative hasDerivAt_euclidAngle in the Wick/Schläfli gap stack: that proof obtains $-1 < \mathrm{euclidCos},\alpha < 1$ on the causal range $\alpha > 7/12$, converts via this lemma, then applies hasDerivAt_arccos_comp. It is also part of the endpoint-avoidance story behind LocalAnalyticFlatChart for Regge action smoothness, where every realized nondegenerate tetrahedron must keep cofactor cosines off $\pm 1$ so the dihedral chart stays analytic.

In the broader Recognition geometry layer this is scaffolding for smooth Regge–TT hinge analysis, not a forcing-chain landmark. It closes a tiny but mandatory interface gap between geometric interior bounds and Mathlib’s arccos derivative hypotheses.