axisTTCross
plain-language theorem explainer
Defines the unnormalized cross-polarization matrix on the 4D Freudenthal patch: the unique symmetric Mat4 with H_{23}=H_{32}=1 and zeros elsewhere. Gravity analysts cite it as the second generator of the transverse-traceless plane for linearized edge strain. The body is a one-line piecewise constant matrix.
Claim. Let $H\in M_4(\mathbb{R})$ be the matrix with $H_{23}=H_{32}=1$ and $H_{ij}=0$ for all other index pairs $(i,j)\in\{0,1,2,3\}^2$. This is the symmetric off-diagonal cross witness used in the linearized metric edge image.
background
The module studies the finite linearized metric edge image on the Freudenthal sixteen-site patch. A matrix $F$ lies in MetricEdgeImage when it arises as the strain current of some $4\times 4$ real perturbation; the strain formula and binary patch coordinates match the frozen world-metric null of the Order-Sensitive Gravity plan, reproduced locally so the heavy analysis chain is not imported.
Mat4 is simply $M_4(\mathbb{R})=\mathrm{Matrix}(\mathrm{Fin},4,\mathrm{Fin},4,\mathbb{R})$. Indices $0,1,2,3$ label the four spacetime directions on the unit hypercube. The companion definition in EdgeTTDecomposition4D packages the same matrix by exhaustive pattern match and calls it the cross polarization $H_{23}=H_{32}=1$ (unnormalized). Together with the plus polarization it spans the candidate TT plane for edge-current analysis.
proof idea
Pure definition: the matrix-valued function that returns $1$ on the ordered pairs $(2,3)$ and $(3,2)$ and $0$ on every other entry of $\mathrm{Fin},4\times\mathrm{Fin},4$. No lemmas are applied; the body is the piecewise constant term itself.
why it matters
Supplies the concrete cross generator used throughout the 4D edge-TT decomposition. Downstream, axisTTCross_isTT and axisTTCross_isTT_symbolDir certify that it is transverse-traceless with respect to the axis and symbol directions; axisTTCross_ne_zero rules out the zero matrix; axisTT_independent shows linear independence from the plus polarization. GeometricFoldVsDictionary4D consumes it when comparing geometric fold residuals to the dictionary midpoint (including dict_eq_two_geom_axisTTCross and the convergence package around actually). In the broader RS gravity chain it is the second basis vector for linearized metric perturbations on the Freudenthal cover, feeding the nontriviality and properness theorems of the metric edge image against antisymmetric posting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.