witnessBase
plain-language theorem explainer
Constant zero base point on the four axis coordinates of the 4-torus. Gravity analysts cite it as the concrete evaluation site when checking that a transverse-traceless plane-wave edge loading is nonzero. The body is the zero function on Fin 4; no proof content.
Claim. Define the constant zero base map $b:\{0,1,2,3\}\to\mathbb{R}$ by $b(i)=0$ for every axis index $i$.
background
The module attaches the Euclidean $4\times 4$ TT/gauge/transverse-trace split to plane-wave EDGE loadings on axis edges of the 4-torus, continuing the algebraic EdgeTTDecomposition4D layer. Edge loading of a matrix $H$ along an axis displacement is the quadratic form $H_{aa}$; the midpoint plane-wave perturbation multiplies that load by $\cos(m\cdot x+m_a/2)$.
A base point on the four axis coordinates is needed to evaluate the plane-wave edge perturbation at a concrete lattice site. The zero map is the simplest such site: every coordinate vanishes, so the phase factor reduces to the pure half-step cosine along the chosen axis.
No upstream lemmas are required; the definition stands alone as a fixed witness configuration.
proof idea
Pure definition: the constant function sending every element of $\mathrm{Fin},4$ to $0\in\mathbb{R}$. No tactics, no lemmas.
why it matters
Supplies the evaluation base for witness_tt_edge_ne_zero, which asserts that the plane-wave axis-edge perturbation of the TT projection of a fixed witness matrix and wave covector is nonzero at this base on axis 2. That nonvanishing check is the concrete witness that the TT sector can load an axis edge under the plane-wave convention of the W4-1 campaign.
It does not advance continuum Einstein-Hilbert recovery or close gap_action_recovery; it only anchors the discrete nondegeneracy sample inside the Regge edge TT attachment layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.