ArbitraryDirectionCosineTwoJet
plain-language theorem explainer
Packages the open per-orbit claim that the ray fold over μ, divided by μ², tends to the m² moment polynomial in every nonzero direction in R⁴. Gravity analysts working the Regge–Bloch continuum limit cite it as the arbitrary-direction cosine two-jet hypothesis for one hinge orbit. The body is pure universal quantification of the punctured Tendsto predicate over nonzero directions; no proof content.
Claim. For a hinge orbit type $\tau$ and a $4\times 4$ real matrix $H$, the property that every nonzero direction $d\in\mathbb{R}^4$ satisfies: the one-orbit ray fold along $d$, divided by $\mu^2$, tends as $\mu\to 0$ in the punctured neighborhood to the orbit $m^2$ moment polynomial at $(\tau,H,d)$.
background
The module builds the factorized all-orbit Bloch symbol for 4D Regge calculus. Hinge edges fall into six lattice orbit types under coordinate permutation (and four orbits once complement is included): $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$. The assembly consumes committed Heron area covectors and deficit kernels from the flat 4D Hessian assembly.
The cosine two-jet is the second-order small-momentum expansion of the Bloch fold. Upstream, OrbitFoldAlongM2Tendsto is the open punctured Tendsto statement for a single orbit and a fixed direction: fold along the ray divided by $\mu^2$ approaches the orbit $m^2$ moment polynomial. The shifted cost $H(x)=J(x)+1=\frac12(x+x^{-1})$ appears in the broader cost algebra but is not the matrix $H$ here; the matrix argument is the 4D Hessian/symbol input.
Module tier tags mark this family of Props as OPEN (status false): the Tendsto is named, not proved. Scope is factorized (orbit-constant) kernels only.
proof idea
Definition, not a theorem. The body is the single universal quantifier
$\forall, d:\mathrm{Fin},4\to\mathbb{R},; d\neq 0;\Rightarrow;\mathrm{OrbitFoldAlongM2Tendsto}(\tau,H,d)$.
No tactics, no lemmas applied. It simply lifts the fixed-direction open Tendsto predicate to every nonzero direction, packaging the arbitrary-direction cosine two-jet claim as a named Prop.
why it matters
Sits in the OPEN tier of the Regge 4D Bloch-symbol program: the per-orbit arbitrary-direction cosine two-jet that must hold before an all-orbit sum version can be stated cleanly. The module explicitly does not claim continuum Einstein–Hilbert recovery and does not flip gap_action_recovery; a one-orbit symbol is flagged as a decoy relative to the continuum target.
No downstream consumers are wired yet (used_by empty). Once discharged, the Prop would feed the all-orbit arbitrary-direction Tendsto and the formal $m^2$ moment polynomial used as the cosine two-jet coefficient. In the broader Recognition stack this is analysis scaffolding for the gravity sector, not a forcing-chain (T0–T8) step; it constrains the discrete-to-continuum symbol, not $\phi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.