foldAlong_neg
plain-language theorem explainer
The (1,1)-orbit Bloch fold along the fixed symbol direction is even in the momentum scale μ: flipping the sign of μ leaves the value unchanged. Anyone extracting the small-momentum m² symbol of the Regge fold cites this to kill odd powers before taking μ→0. The proof is a double Finset sum congruence that reduces T11 hinges to cos(−θ)=cos(θ) on the phased class dots.
Claim. For every $4\times 4$ real matrix $H$ and every real scale $\mu$, the (1,1)-orbit Bloch fold of $H$ at momentum $-\mu$ along the fixed symbol direction equals the same fold at $+\mu$: $\mathrm{foldAlong}(H,-\mu)=\mathrm{foldAlong}(H,\mu)$.
background
This module studies the small-momentum ($m^2$) symbol of the honest transported (1,1) Bloch fold on the Regge 4D complex. It never redefines Hessians, kernels, or stencils; it only restricts the already-built fold along one momentum ray.
blochFold11 H m sums transported slot terms over 24 hinges and 10 triangle slots. The ray restriction is foldAlong H μ := blochFold11 H (μ · symbolDir) with symbolDir = (1,1,0,0). Only slots of orbit type T11 contribute nontrivial phased terms; others drop out of the fold.
Each T11 contribution is built from phasedClassDot, a plane-wave weighted class perturbation of $H$ at a hinge base point. The phase factors involve cosines of momentum dotted into lattice directions, so sign flips of μ act through Real.cos_neg.
proof idea
Unfold foldAlong, blochFold11, and transportedSlotTerm, then apply double Finset.sum_congr. On each pair $(s,t)$ case-split on isT11 s t.
If the slot is T11, a local lemma shows phasedClassDot v H (fun i => (-μ)·symbolDir) (hingeBase s t) equals the same expression with $+μ$, by rewriting both sides via phasedClassDot_symbolDir and using neg_mul with Real.cos_neg inside the class-dot sum. Apply that identity to both the area-covariance vector and the deficit kernel. If the slot is not T11, both sides simplify to the same zero contribution.
why it matters
Evenness is the first landed item in the module's m²-symbol checklist: it feeds foldAlong_even (the Function.Even packaging) and foldAlong_odd_deriv_at_zero (evenness plus the pointwise sign-flip identity). Downstream work uses that package to conclude the first derivative at the origin vanishes wherever the fold is differentiable, clearing the linear term before the quadratic coefficient m2Symbol is read off.
In the broader Recognition gravity stack this is local analytic hygiene for the (1,1) orbit only. It does not close the open FoldAlongM2Tendsto glue, nor the global EH recovery goals flagged in the module doc. It is the concrete reason odd powers drop from the small-momentum expansion along symbolDir.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.