pushforwardClass
plain-language theorem explainer
Defines the pushforward of a 15-component class covector under a covering permutation of the 4D hinge lattice. Anyone assembling transported orbit deficits, areas, or phased star contractions cites it. The body is a one-line reindex sum: mass at source class d0 is moved to the image class under the covering perm.
Claim. Given a class covector $v:\{0,\ldots,14\}\to\mathbb{R}$ and a covering permutation $p\in\{0,\ldots,23\}$, the pushforward is the covector $(P_p v)(d)=\sum_{d_0} v(d_0)\,\mathbf{1}_{\pi_p(d_0)=d}$, where $\pi_p$ is the induced action of $p$ on the 15 nonzero coordinate masks.
background
This module builds the continuum-facing multi-orbit Bloch fold in 4D Regge calculus. Each hinge orbit type carries a seed area covector and star deficit kernel; transport to a lattice slot is by the first $S_4$ covering permutation of the orbit representative, not by the factorized transport used only for type $(1,1)$.
Class indices run over the 15 nonzero 4-bit masks (edges of the 4-cube). A covering permutation $p\in\mathrm{Fin},24$ acts on masks by permuting coordinates; the upstream map permClass sends each class index to the class of its permuted mask. The present definition is the corresponding pushforward on covectors: it relocates the value at each source class to the image class.
The local setting is the transported all-orbit fold that recovers the $(1,1)$ Bloch fold on the nose and feeds exact-action and $m^2$ symbol evaluations.
proof idea
Pure definition, no proof obligations. The body is the standard pushforward sum: for each target class $d$, sum $v(d_0)$ over those $d_0$ with $\mathrm{permClass}(p,d_0)=d$, else zero. It is the linear dual of the class reindexing induced by the covering permutation.
why it matters
Every transported orbit object in this module is built by applying this pushforward to a seed kernel: transported orbit deficit and area, slot-orbit kernels, and the full Bloch fold. Downstream, the exact-action symbol module uses it inside resolved deficit contractions for types $(1,1)$ and $(1,2)$ (phased star-member dots pushed by the covering perm), and the zero-momentum specializations reduce those to ordinary class dots of the pushed assemblies. Local-incidence theorems unfold through it when equating mean local kernels to scaled slot deficits.
It is the uniform transport mechanism that lets the all-orbit fold recover the $(1,1)$ slice and produce the measured raw $m^2=-5/2$ on the axis/symbol direction. Open items it supports but does not close: all-orbit $m^2$ Tendsto and continuum Einstein-Hilbert isotropy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.