foldOrbitAlong_zero
plain-language theorem explainer
Ray fold of a factorized Bloch orbit symbol along any wave direction, evaluated at scale μ = 0, recovers the committed zero-momentum orbit quadratic. Gravity analysts working the Regge 4D Hessian assembly cite this when specializing finite-momentum folds to the static sector. The proof is a short term reduction: scale the direction by zero, apply the zero-smul identity, and invoke the existing zero-momentum consistency gate.
Claim. For every hinge orbit type $\mathrm{ty}$, every $4\times 4$ matrix $H$, and every wave direction $\mathrm{dir}:\{0,1,2,3\}\to\mathbb{R}$, the factorized Bloch fold of that orbit along the ray $\mu\cdot\mathrm{dir}$ at $\mu=0$ equals the committed zero-momentum orbit quadratic of $(\mathrm{ty},H)$.
background
This module builds the Regge 4D Bloch symbol as an all-orbit factorized fold over the six $S_4$ hinge types $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$, grouped into four orbits under $S_4$ plus complement. It consumes committed Heron area covectors and deficit kernels from the flat 4D Hessian assembly. Scope is factorized (orbit-constant) kernels only; it does not replace the transported $(1,1)$ fold elsewhere in the stack.
The ray fold scales a fixed wave direction: $\mathrm{foldOrbitAlong}(\mathrm{ty},H,\mathrm{dir},\mu)$ is the factorized Bloch orbit fold at momentum $m_i=\mu,\mathrm{dir}_i$. The zero-momentum orbit quadratic is the static specialization $(\mathrm{orbit\ cell\ count})\cdot(\mathrm{area\ cov}\cdot H)\cdot(\mathrm{deficit\ kernel}\cdot H)$.
Upstream, the consistency gate already states that the unscaled factorized orbit fold at the zero momentum map equals that quadratic. A private zero-smul lemma records that $0\cdot\mathrm{dir}$ is the constant-zero momentum map.
proof idea
Term-mode, three steps. Unfold the ray fold definition to expose the factorized orbit fold at $m_i=\mu,\mathrm{dir}_i$. Rewrite with the zero-smul identity so the momentum map becomes the constant-zero function. Finish by the existing zero-momentum consistency gate, which equates that fold to the committed orbit quadratic.
why it matters
Closes a THEOREM-tier zero-momentum reduction for the ray fold, as flagged in the module doc (orbit-count identity, zero-momentum reductions, evenness of the ray fold). Downstream, the axis and gauge specializations rewrite through this identity and then kill the quadratic by deficit-kernel orthogonality: the axis-$TT^+$ and decoy-gauge matrices give vanishing deficit dots, so the ray fold at $\mu=0$ is zero on those backgrounds.
Those vanishings are the static-sector checks before the open cosine two-jet / Tendsto props for arbitrary directions. The result stays inside the factorized-kernel program; it does not claim continuum Einstein–Hilbert recovery or flip the gap-action flag. In the broader RS gravity stack it is bookkeeping that keeps finite-momentum symbols continuous with the committed Hessian assembly at vanishing momentum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.