lorentz_invariance
plain-language theorem explainer
The theorem states that the J-cost function satisfies J(r) = J(r^{-1}) for every positive real r, supplying the Lorentz invariance axiom W0 on the Recognition Science Hilbert space H_RS. Axiomatic QFT researchers and RS foundation auditors cite it to confirm that inversion symmetry of the cost function yields the required invariance. The proof is a direct one-line wrapper applying the Jcost_symm lemma from the Cost module.
Claim. For every positive real number $r > 0$, the J-cost satisfies $J(r) = J(r^{-1})$, where $J$ is the J-cost function.
background
The module WightmanAxiomsStatus summarises the status of the five Wightman axioms on the RS Hilbert space H_RS. W0 is defined as Lorentz invariance and is obtained directly from J-cost symmetry. The J-cost function itself is introduced in the Cost module, where Jcost_symm establishes the required inversion invariance by algebraic reduction: unfolding the definition, clearing denominators via field_simp, and confirming equality by ring normalisation.
proof idea
This is a one-line wrapper that applies the Jcost_symm lemma (from both Cost and Cost.JcostCore). The lemma reduces the claim by rewriting Jcost as a squared expression, invoking ne_of_gt to obtain nonzero denominators, then simplifying with field_simp and ring.
why it matters
The declaration supplies the lorentz field inside wightmanStatusCert, which certifies that the five Wightman axioms hold on H_RS. It closes the W0 slot in the axiom count, linking J-cost symmetry (T5 J-uniqueness in the forcing chain) to the overall axiom status. The module notes that W4 remains sector-dependent and the continuum limit is open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.