seedDihedralAngle
plain-language theorem explainer
Defines the seed-hinge dihedral angle of a 4-simplex as the arccos of the Gram-projection cosine of squared edge lengths. Anyone proving pathwise Schläfli identities or flat second-variation formulas for Freudenthal 4-simplices cites this. The body is a one-line composition of Real.arccos with the existing cosine kernel.
Claim. For squared edge lengths $a \in \mathbb{R}^{10}$ of a 4-simplex, the seed-hinge dihedral angle is $\theta(a) := \arccos\bigl(\cos_{\mathrm{dih}}(a)\bigr)$, where $\cos_{\mathrm{dih}}$ is the Gram-projection cosine of the seed hinge.
background
The ambient module develops pathwise Schläfli calculus for the Freudenthal (Kuhn) 4-simplex, the 4D analogue of the closed-form tetrahedron identity with $n_H = n_E = 10$ rather than 6. Squared edge data live in $\mathrm{SqEdges4} \simeq \mathbb{R}^{10}$, ordered by the local incidence slots of the hinge layer.
Upstream, cosDihedral supplies the cosine of the seed-hinge dihedral angle inside one 4-simplex via the normalized apex Gram projection: $\mathrm{apexDot}/\sqrt{\mathrm{apex3NormSq}\cdot\mathrm{apex4NormSq}}$. The present definition simply recovers the geometric angle from that cosine.
Flat seed lengths and the associated angle kernel (directional derivatives at flat) are already fixed in the hinge-dihedral and orbit-classification layers; this angle is the scalar whose flat derivatives feed the Schläfli summands.
proof idea
Pure definition: apply Real.arccos to cosDihedral a. No proof obligations. Downstream derivative theorems compose the chain rule for arccos with the already-proved HasDerivAt of the cosine along each squared-edge coordinate path through the flat seed.
why it matters
This is the geometric angle that appears in the seed-hinge row of the flat Schläfli table. Downstream, hasDerivAt_seedDihedralAngle_coord and its wrapper flat_freudenthal_seed_angle_hasDerivAt establish that along every coordinate path through the flat seed the derivative equals the angle kernel, which is the Gate-A2-style input needed for directional Schläfli kill at flat. remapped_seed_dihedral_eq records invariance under the zero remapping of squared edges.
In the module tier list this underwrites the THEOREM that the seed-hinge dihedral has HasDerivAt along every squared-edge coordinate path through flat. It does not close the OPEN items (full pathwise identity off the flat seed, remapped derivatives for every hinge row, elevation to the EH candidate, or $S_{RS}$ convergence in 4D), and it does not touch gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.