fullStarDirectional
plain-language theorem explainer
Defines the directional pairing of an arbitrary 15-class edge vector against the type-(1,3) full-star deficit class kernel. Anyone assembling flat Hessian decoy traces or homothety stationarity for the (1,3) hinge cites this linear form. The body is the plain finite sum of class coefficients times kernel values.
Claim. For a real vector $v$ indexed by the fifteen edge-displacement classes, the full-star directional is $\sum_{d=0}^{14} v_d\,K^{(1,3)}_d$, where $K^{(1,3)}$ is the type-$(1,3)$ full-star deficit class kernel (supported on classes $1,3,5,7,9,11,13$ with values $\pm\sqrt{3}$).
background
In the Regge 4D campaign, curvature at a triangle hinge is read from the deficit angle of the Freudenthal star of Kuhn simplices meeting that hinge. Edge lengths are reduced to a 15-class stencil of lattice displacement types; the deficit's first variation at flat geometry collapses to a fixed class kernel $K$ on those fifteen slots.
This module treats the type-$(1,3)$ hinge (absolute masks ${0,1,15}$, local flat squared lengths $(1,3,4)$). Its kernel $K^{(1,3)}$ is nonzero only 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})$. Parallel kernels exist for types $(1,1)$, $(1,2)$, and $(2,2)$.
The directional is the natural pairing of an arbitrary class vector against that kernel: the same pattern used in the seed $(1,1)$ module and the $(1,2)$ sibling.
proof idea
Pure definition: one-line sum $\sum_{d:\mathrm{Fin},15} v_d\cdot K^{(1,3)}_d$. No lemmas, no tactics. Downstream proofs typically restrict the sum to the seven-class support via a zero-off-support lemma, then evaluate the remaining products by decide or direct arithmetic on the $\pm\sqrt{3}$ entries.
why it matters
Supplies the linear form used to state and prove gates for the type-$(1,3)$ star: uniform-scaling decoy vanishing and homothety stationarity (directional of the class-weight vector equals zero). In the flat Hessian assembly it underwrites deficitKernel13_dot_decoyTrace, the $(1,3)$ instance of the decoy-trace orthogonality suite that also covers kernels $(1,1)$, $(1,2)$, and $(2,2)$.
Those orthogonality facts are increments toward a kernel-checked flat Hessian over all hinge types. The module explicitly does not finish that assembly, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, and leaves transport of this kernel to the complementary type $(3,1)$ open. Within the QG full-theory campaign this is the next kernel-checked step after the $(1,1)$ seed orbit and the orbit classification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.