arccos_chain_factor_flat
plain-language theorem explainer
At the flat Freudenthal seed, the arccos chain-rule prefactor d(arccos)/d(cos) equals −√2. Anyone differentiating a seed-hinge dihedral along squared-edge coordinates cites this identity. The proof is a two-step rewrite: substitute the flat sine evaluation, then clear the reciprocal.
Claim. At the flat seed squared-edge lengths, $-(1/\sqrt{1-\cos^2\theta})= -\sqrt{2}$, where $\theta$ is the seed-hinge dihedral angle (equivalently $d(\arccos u)/du|_{u=\cos\theta}=-1/\sin\theta=-\sqrt{2}$ on the positive branch).
background
This module develops pathwise Schläfli calculus for the Freudenthal/Kuhn 4-simplex ($n_H=n_E=10$), mirroring the 3D Gate-A2 closed form at six edges. The local objects are squared edge lengths on a 4-simplex, the cosine of a seed-hinge dihedral angle inside one simplex, and the flat seed configuration with fixed squared lengths $(1,2,3,4,1,2,3,1,2,1)$ in local slot order.
Differentiating a dihedral angle written as $\theta=\arccos(\cos\theta)$ produces the chain factor $-1/\sin\theta$. Upstream, the flat sine theorem evaluates the positive branch $\sqrt{1-\cos^2\theta}=1/\sqrt{2}$ at the seed. The angle kernel used throughout the hinge analysis is defined as $\theta'=-(1/\sin\theta)\cdot(\cos\theta)'$ with that flat value $1/\sin=\sqrt{2}$ baked in.
proof idea
One algebraic reduction. Rewrite the left-hand side by the flat sine theorem, which replaces $\sqrt{1-\cos^2\theta}$ by $1/\sqrt{2}$. Then field_simp turns $-(1/(1/\sqrt{2}))$ into $-\sqrt{2}$. No case splits or positivity side goals remain after that substitution.
why it matters
This pins the numerical prefactor in the seed-hinge angle kernel so that coordinate derivatives of the dihedral match angleKernel. The sole downstream consumer is the theorem that the seed-hinge dihedral has derivative angleKernel along every squared-edge coordinate path through the flat seed; that result is a listed THEOREM tier item in the module (pathwise HasDerivAt at flat).
Together with flat hinge areas and the Schläfli summand table, it supplies the Gate A2-style flat directional kill for the 4-simplex. It does not close the OPEN items (full pathwise identity off the flat seed, remapped derivatives on every hinge row, elevation to the continuum candidate, or $S_{RS}\to$ Einstein–Hilbert in 4D).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.