zero_eval
plain-language theorem explainer
The zero scalar field evaluates to zero at every spacetime point. Researchers building scalar field models in Recognition Science cite this when verifying linearity or the zero element in the algebra. The proof is a one-line reflexivity that follows directly from the definition of evaluation.
Claim. Let $0$ be the zero scalar field. For every spacetime point $x : Fin 4 → ℝ$, the evaluation satisfies $eval(0, x) = 0$.
background
A scalar field assigns a real value to each spacetime point via its ψ component. Evaluation is defined by applying this component at the input point, reducing to the field's internal function. The upstream LinearLogicBridge.eval supplies the general mechanism for resource expressions, where constants reduce directly to their numeric value.
proof idea
The proof is a one-line term-mode reflexivity. It unfolds the definition of eval on the zero field, which is constructed to return the constant zero, yielding equality by construction.
why it matters
This identity establishes the zero element for scalar field operations such as addition and scalar multiplication in the module. It supports the Recognition Science foundation where constant fields arise from the functional equation and the forcing chain to T8. No downstream uses are recorded yet, leaving its role as a basic algebraic fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.