seedCosDihedral
plain-language theorem explainer
Alias for the cosine of the seed-hinge dihedral angle on a 4-simplex, given ten squared edge lengths. Gravity and Regge-calculus readers cite it when assembling flat Schläfli summands or directional derivatives at the Freudenthal seed. The body is a one-line rename of the hinge-kernel cosine.
Claim. For squared edge lengths $a \in \mathbb{R}^{10}$ of a 4-simplex, $\mathrm{seedCosDihedral}(a)$ equals the cosine of the seed-hinge dihedral angle: $\mathrm{apexDot}(a)/\sqrt{\mathrm{apex3NormSq}(a)\,\mathrm{apex4NormSq}(a)}$.
background
This module lifts the 3D Gate-A2 Schläfli closed form (six edges, six hinges) to the Freudenthal/Kuhn 4-simplex ($n_H = n_E = 10$). Squared edge data live in SqEdges4, an abbreviation for maps $\mathrm{Fin},10 \to \mathbb{R}$ in the local incidence slot order.
Upstream, the hinge kernel defines the cosine of the seed-hinge dihedral inside one 4-simplex as the normalized apex inner product: $\mathrm{apexDot}/\sqrt{\mathrm{apex3NormSq},\mathrm{apex4NormSq}}$. Flat Freudenthal squared lengths are shared by both seed simplices; the present name simply marks that cosine as the seed-hinge quantity used in pathwise Schläfli bookkeeping.
Local theorems already cover flat hinge areas, the flat Schläfli summand table (column sums vanish), and seed-hinge $\mathrm{HasDerivAt}$ along every squared-edge coordinate path through the flat seed.
proof idea
Pure definitional wrapper: the right-hand side is exactly the upstream hinge-kernel cosine on the same ten squared lengths. No algebraic simplification or tactic proof; it is a seed-scoped name for that formula.
why it matters
Gives a stable local name for the seed-hinge dihedral cosine inside the 4D pathwise Schläfli stack, matching the module's THEOREM tier that the seed-hinge row equals hinge area times the angle kernel from the dihedral kernel. That cosine is the angular factor in flat directional Schläfli kill (Gate A2-style input at flat) and in seed-hinge derivative statements along affine edge velocities.
It does not close the OPEN items: full pathwise identity off the flat seed on nondegenerate 4-simplices, remapped $\mathrm{HasDerivAt}$ for every hinge row, elevation to a Regge candidate, or $S_{RS}$ convergence to Einstein-Hilbert in 4D. No downstream uses are wired yet; the def is scaffolding nomenclature for those later rows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.