hasDerivAt_arccos_comp
plain-language theorem explainer
If a real map f is differentiable at x and f(x) stays strictly inside (-1,1), then arccos∘f is differentiable there with the classical chain-rule derivative. Analysts working dihedral or Regge angle variations cite it as the calculus interface between a cosine path and the angle path. The proof is a short composition of Mathlib's arccos derivative with the given HasDerivAt hypothesis.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be differentiable at $x$ with derivative $f'$. If $f(x)\neq -1$ and $f(x)\neq 1$, then $t\mapsto \arccos(f(t))$ is differentiable at $x$ with derivative $-\frac{1}{\sqrt{1-(f(x))^2}}\,f'$.
background
The module isolates the analytic half of dihedral differentiation: once a Cayley–Menger cofactor cosine is known to be differentiable along a path, the geometric angle $\theta=\arccos(\cos\theta)$ inherits the standard formula $d\theta=-(1/\sqrt{1-\cos^2}),d(\cos\theta)$. Algebraic work that produces the cosine derivative lives in the cofactor layer; this file only supplies the calculus interface that layer must feed.
Mathlib already records the pointwise derivative of $\arccos$ on $(-1,1)$. The present statement packages the chain rule for an arbitrary outer path $f$, under the two endpoint exclusions that keep the radicand positive and the arccos derivative defined. Downstream dihedral and Euclidean-angle lemmas invoke exactly this packaging rather than reopening the inverse-trig calculus each time.
proof idea
Term-mode one-liner. Instantiate Mathlib's Real.hasDerivAt_arccos at the two endpoint hypotheses $f(x)\neq\pm 1$, then compose that derivative with the given HasDerivAt f f' x. A simpa pass normalizes the multiplicative association and commutation so the composite derivative matches the displayed scalar $-1/\sqrt{1-(f x)^2}\cdot f'$.
why it matters
This is the reusable calculus bridge for every pathwise dihedral derivative in the geometry stack. Immediate parent is hasDerivAt_dihedralAngle3Sq_along, which feeds a known cofactor-cosine derivative into the angle map under the same endpoint exclusions. Gravity consumers reuse it directly: hasDerivAt_seedDihedralAngle_coord in the Regge 4D Schläfli pathwise analysis, and hasDerivAt_euclidAngle in the Wick/Euclidean Schläfli action (where the doc states "Euclidean angle derivative via arccos ∘ euclidCos on the causal range").
In the Recognition geometry program the hard content is algebraic (cofactor minors of squared-edge data). Keeping the arccos chain rule as a proved, zero-sorry lemma means those geometric layers can quote a single interface rather than re-proving inverse-trig calculus. It does not itself touch T0–T8 or the RCL; it is infrastructure for the Schläfli and dihedral variation identities those gravity modules need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.