spatialNormSq_eq_zero_iff
plain-language theorem explainer
The equivalence states that the squared spatial norm of a four-vector vanishes precisely when its three spatial components are each zero. Analysts separating temporal and spatial contributions in derivative operators or tensor calculus within the Recognition relativity module would cite this result. The proof unfolds the definition and applies non-negativity of squares together with linear arithmetic to conclude each component vanishes.
Claim. For a vector $x : {R}^4$, $x_1^2 + x_2^2 + x_3^2 = 0$ if and only if $x_1 = x_2 = x_3 = 0$.
background
The module develops calculus tools for relativity, including partial derivatives and Laplacians on four-vectors indexed by Fin 4. The spatial norm squared is defined directly as the sum of squares of the three spatial components. The immediate upstream dependency is this definition itself; a radius definition from the cellular automata module is listed among imports but is not used in the argument.
proof idea
The tactic proof unfolds spatialNormSq, then for the forward direction obtains non-negativity of each squared term, applies linarith to force each square to zero, and uses simp with sq_eq_zero_iff to recover the components. The reverse direction applies simp directly to the assumption that all three components vanish.
why it matters
This equivalence supports clean separation of spatial and temporal parts when constructing derivative operators in the relativity calculus layer. It aligns with the framework's derivation of D = 3 spatial dimensions via the forcing chain (T8) and the eight-tick octave. No downstream uses are recorded, leaving its role as a basic isolation lemma for later tensor or derivative results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.