orbitSeedKernel
plain-language theorem explainer
Assigns to each of the six lattice hinge orbit types its committed seed star deficit kernel in R^15. Gravity analysts cite it as the single assembly entry point before covering transport and all-orbit Bloch folds. The body is pure case dispatch onto the star-class kernels (with (2,1) and (3,1) identity-transported from (1,2) and (1,3)).
Claim. For each hinge orbit type $\tau\in\{t_{11},t_{12},t_{21},t_{13},t_{31},t_{22}\}$ under coordinate permutation, the seed star deficit kernel is the committed full-star class covector in $\mathbb{R}^{15}$ for that type. Types $(2,1)$ and $(3,1)$ reuse the $(1,2)$ and $(1,3)$ kernels by identity transport.
background
The module builds a continuum-facing multi-orbit 4D Bloch fold: each slot transports its orbit's seed area covector and star deficit kernel by the first $S_4$ covering permutation of the orbit representative. The six orbit types are the lattice classes of hinges under coordinate permutation ($t_{11},t_{12},t_{21},t_{13},t_{31},t_{22}$).
A star deficit kernel is a fixed 15-component real vector on the edge/defect basis encoding the full-star class contribution for one orbit. The $(1,1)$, $(1,2)$, $(1,3)$, and $(2,2)$ kernels are committed in the dedicated star-kernel modules (sparse signed entries, with $\sqrt{2}$ and $\sqrt{3}$ factors on the non-diagonal types). Assembly defines the $(2,1)$ and $(3,1)$ kernels as identical copies of $(1,2)$ and $(1,3)$ under identity transport.
This definition is the assembly commitment that later pushforwards and mean-local constructions read from, rather than reaching into each star-kernel module separately.
proof idea
Definition by exhaustive pattern match on HingeOrbitType. The four primary cases point at the corresponding fullStarClassKernel from the star-kernel modules; the $(2,1)$ and $(3,1)$ cases point at the assembly aliases kernel21 and kernel31, which are themselves definitional equalities to the $(1,2)$ and $(1,3)$ kernels. No tactics or lemmas.
why it matters
Single seed table for the transported all-orbit 4D Bloch fold. Downstream, transportedOrbitDeficit pushforwards this kernel by a covering permutation; orbitMeanLocalKernel scales it by $1/r_\tau$ (orbit star size) for distinct-hinge continuum weighting; and the M2Eval siblings read the transported slot coefficients for raw all-orbit $m^2$ checks (measured $-5/2$ on axisTTPlus/symbolDir).
The equality theorem orbitSeedKernel_eq_assembly locks this table to the assembly deficit kernels, and the $t_{11}$ specialization recovers the classical star kernel used by the single-orbit fold. That recovery is part of the module status: $(1,1)$ slice of $m^2$ matches m2Symbol, while non-$(1,1)$ orbits must use covering transport rather than the factorized transportPermOfDiff (lesson L-p1).
Does not close the open all-orbit $m^2$ Tendsto or continuum EH isotropy questions; those still need the residual $2/N^4$ cell-sum dictionary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.