chainT22
plain-language theorem explainer
The arccos chain-rule factor at flat cosine 0 is the constant −1. Anyone linearizing a Regge hinge deficit through cosine data cites it when converting a cosine kernel into a deficit kernel. The body is a one-line numeric definition, not a derived identity.
Claim. The chain-rule factor $\frac{d(\arccos u)}{du}$ evaluated at the flat cosine value $u=0$ equals $-1$.
background
In 4D Regge calculus the hinge deficit is $2\pi$ minus the sum of dihedral angles. Each dihedral angle is recovered as $\arccos$ of a cosine built from the hinge-ordered Gram data of an incident simplex. Differentiating the deficit with respect to edge lengths therefore routes through the scalar factor $d(\arccos)/d(\cos)$.
This module treats the type-(2,2) triangle hinge on the periodic Freudenthal lattice and its full star (four incident Kuhn simplices). All four flat cosines equal 0, so the chain factor is needed only at that single point. Upstream deficit definitions (dihedral and Schläfli) supply the $2\pi-\sum\theta$ shape; the present constant is the local derivative piece that turns a cosine-class kernel into a deficit-class kernel.
proof idea
Pure definition: the real constant $-1$. No lemmas, no tactics. The value is the elementary derivative $\frac{d}{du}\arccos u=-1/\sqrt{1-u^2}$ at $u=0$.
why it matters
Closes the arithmetic link used by the equality that the per-simplex deficit kernel equals $-(\text{chain factor})$ times the cosine kernel, hence equals the cosine kernel itself when the factor is $-1$. That identity is the bridge from the flat cosine multiset (all zeros on the four star members) to the full-star deficit class kernel on the 15 stencil classes. It is a tiny but named step in the QG full-theory campaign for the type-(2,2) orbit; it does not touch Einstein–Hilbert recovery or the global action-convergence gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.