hasDerivAt_t13_coord
plain-language theorem explainer
For each of the ten edge-coordinate directions on a type-(1,3) Regge hinge, the dihedral cosine along the one-parameter squared-edge path is differentiable at the flat point, with derivative equal to the tabulated cosine-kernel entry. Anyone assembling the full-star deficit class kernel on classes (1,3,5,7,9,11,13) cites this. The proof is a Fin-10 case split that hands each slot to a pre-proved cleared-denominator derivative lemma.
Claim. For every coordinate index $k\in\{0,\ldots,9\}$, the real map $t\mapsto\cos\theta$ of the seed-hinge dihedral angle along the type-$(1,3)$ squared-edge path in direction $k$ admits a derivative at the flat squared-length configuration, and that derivative equals the $k$-th entry of the type-$(1,3)$ cosine kernel.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the type-(1,1) star kernel and the orbit classification. It treats the type-(1,3) triangle hinge with absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$) and its full periodic Freudenthal star inside the origin unit cube.
The dihedral cosine of a seed hinge inside one 4-simplex is the Gram-projection ratio of apex dot product over the product of apex 3- and 4-norms. Coordinate paths stretch one of the ten independent squared-edge slots while holding the others at the flat values; the flat Gram data give cosine $1/2$ on every simplex of the star.
Upstream, each individual slot already has a HasDerivAt statement obtained from a cleared-denominator master lemma evaluated at flat $(N,P,Q)=(8,8,8)$. The present theorem packages those ten facts under a single index.
proof idea
Term-mode proof by exhaustive case analysis on $k:\mathrm{Fin},10$. The tactic fin_cases k produces ten goals; each is discharged by exact of the corresponding pre-proved slot lemma (hasDerivAt_t13_slot0 through hasDerivAt_t13_slot9). Those slot lemmas themselves invoke the cleared-denominator master derivative at the flat point and convert the resulting scalar. No new analytic work occurs here: the theorem is pure index packaging.
why it matters
Deliverable A of the module explicitly lists "all ten coordinate derivatives" as a required gate before the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$ with values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$. Downstream, hinge4DStarKernel13Status_flags records that the full-star class kernel is closed precisely when these derivatives (together with star enumeration and the flatness gate $6\cdot\arccos(1/2)=2\pi$) are in hand.
In the broader Recognition gravity stack this is a discrete curvature building block toward Regge action matching Einstein–Hilbert in 4D, not a continuum limit theorem. Transport of the same kernel to the complementary type $(3,1)$ remains open, as does flat Hessian assembly over all hinges and the gap-action recovery flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.