axisWaveVector_ne_zero
plain-language theorem explainer
The distinguished axis wave vector used as a non-vacuity witness for the Regge TT continuum-symbol target is nonzero. Anyone instantiating the closed continuum symbol at the axis-plus polarization cites this. The proof evaluates the zero hypothesis at the zeroth component, unfolds the definition, and reduces to the elementary fact that one is not zero.
Claim. The distinguished axis wave vector $k_{\mathrm{axis}}$ (the concrete commensurate momentum used as a TT Bloch witness) satisfies $k_{\mathrm{axis}} \neq 0$.
background
This module is Stage 1 of the Regge TT continuum-symbol program: it defines the true nonlinear 3D Regge action on the periodic Freudenthal torus as a function of an arbitrary edge squared-length field, records its flat point, and builds the TT Bloch symbol object (plane-wave edge fields, second differences, and the continuum-symbol predicate).
The continuum isotropy claim itself remains OPEN (ReggeTTContinuumIsotropyTarget); C10 numerics report isotropic $K(0)=-(1/4)I_{TT}$ but are not proof. To close any concrete instance of that target one needs non-vacuous witnesses: a nonzero wave vector and a genuine TT polarization.
The axis wave vector is the module's fixed commensurate momentum witness. Non-vanishing is the minimal well-formedness condition so that the Bloch symbol is not evaluated at the trivial mode.
proof idea
Tactic proof by contradiction. Assume the axis wave vector equals the zero function. Specialize at index $0$ to obtain that the zeroth component is $0$. Unfold the definition of the axis wave vector at that component; the resulting equality is $1=0$. Discharge with one_ne_zero from the primitive recognition calculus (the standard $1\neq 0$ fact).
why it matters
Non-vacuity receipt for the preflight package. Downstream, axis_plus_continuum_symbol in the continuum closer instantiates the closed target at the axis wave vector and the plus TT polarization, feeding this lemma together with the TT-constraint certificate; the doc there calls it the "non-vacuity receipt" that the continuum symbol at that concrete instance is $-1/4$.
It also grounds the status-flag record ReggeTTSymbolPreflightStatus, which certifies (among other Stage-1 facts) non-vacuity of the TT constraint set while honestly leaving the continuum VALUE flag false. In the QG campaign this is bookkeeping that keeps the OPEN continuum-isotropy target honest: witnesses exist and are nontrivial, even though the continuum limit identity is not yet a theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.