area22Z
plain-language theorem explainer
Integer area-weight mask on the 15 class indices for the t22 hinge orbit: value 1 at indices 2 and 11, else 0. Downstream t22 slot certificates and the real areaCov22 normalization cite it as the exact integer numerator. Defined by a two-branch pattern match on Fin 15.
Claim. For each class index $d\in\{0,\ldots,14\}$, the integer area weight $a_{22}(d)$ equals $1$ when $d\in\{2,11\}$ and equals $0$ otherwise.
background
This module certifies transported all-orbit $m^2$ moments for 4D Regge–Bloch analysis on axes such as axisTTPlus and directions such as symbolDir. The target identities include the raw all-orbit moment equaling $-5/2$ and the distinct-hinge weighted moment equaling $-1/4$, assembled from per-orbit integer certificates that sum over six orbit types (t11, t12, t13, t21, t31, t22).
Symmetric $4\times 4$ curvature data are packaged as fifteen real class coefficients. For each orbit type one needs a sparse integer area mask on those fifteen slots; the real covariant area is that mask divided by a fixed denominator. Sibling masks area12Z, area21Z, area13Z, area31Z play the same role for the other orbits. The t22 orbit slice on plus is the zero contribution in the module theorem list (t11 $=-3$, t12 $=+2$, t13 $=-3/2$, and t21 $=$ t31 $=$ t22 $=0$).
proof idea
Definition by exhaustive match on Fin 15: return the integer 1 on the constructors for indices 2 and 11, and 0 on every other index. No lemmas, no tactics.
why it matters
Supplies the integer numerator for the t22 area channel. areaCov22_eq_z lifts it to reals via areaCov22 d = (area22Z d : ℝ)/4. slotAZ22 folds it against permuted class coefficients to build the integer slot certificate for orbit t22. That certificate is the backbone of m2TransportedOrbitSlotCoeff_t22_eq_cert (and the e0-direction variant), which state that the transported t22 slot coefficient equals the integer certificate over 32. An edge-origins twin, m2OrbitSlotCoeffEdgeOrigins_t22_eq_cert, uses the same mask family. Together these close the t22 $=0$ orbit slice in the all-orbit sum that yields the module’s $-5/2$ and $-1/4$ moment theorems. They do not repair the open e0 plus/cross anisotropy or flip gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.