symbolDir
plain-language theorem explainer
Fixed probe direction (1,1,0,0) in Euclidean 4-space for the (1,1)-orbit Bloch fold. Gravity analysts cite it whenever the small-momentum m² symbol is restricted to a single ray. The body is a four-case pattern match on Fin 4; no proof content.
Claim. The direction $d \in \mathbb{R}^{4}$ with components $d_{0}=1$, $d_{1}=1$, and $d_{2}=d_{3}=0$ (indices in $\{0,1,2,3\}$).
background
The module studies the (1,1)-orbit piece of the small-momentum symbol of the 4D Regge Bloch fold blochFold11. It never redefines Hessians, kernels, or stencils; those come from ReggeBlochFold4D.
Along a fixed ray one sets foldAlong H μ := blochFold11 H (μ · d) and extracts the quadratic coefficient of the fold in μ. The chosen ray is this direction d = (1,1,0,0). Downstream work checks that banked TT polarizations (axisTTPlus, axisTTCross) are transverse to d, so the 1,208-row identity applies on this ray rather than only on a unit axis wave.
Scope is deliberately narrow: (1,1) orbit only. The module does not claim full Hessian-symbol recovery or close the global EH convergence gap.
proof idea
Pure definition by cases on Fin 4: index 0 and 1 map to 1, all other indices map to 0. No lemmas, tactics, or proof obligations.
why it matters
This direction is the standard probe for the landed (1,1) m² analysis: evenness of the fold, vanishing at zero on TT and gauge axes, and the closed-form coefficient m2Symbol (−3 on TT, 0 on gauge). The open Prop FoldAlongM2Tendsto is stated along the same ray.
Downstream, GeometricFoldVsDictionary4D uses it to certify IsTT symbolDir axisTTPlus and IsTT symbolDir axisTTCross, enabling coefficient comparisons between geometric fold and dictionary moments. FoldMomentNamingLink4D evaluates exactMidpointBlochM2 and hybrid moments at (axisTTPlus, symbolDir) when separating witness-level factor-two equalities from definitional naming links. It is infrastructure for the Regge–Bloch gravity stack, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.