spectral_positivity
plain-language theorem explainer
Off-vacuum states satisfy strict positivity of the J-cost for every positive real r different from 1. Researchers embedding the Wightman axioms in Recognition Science cite the result to secure the spectral positivity condition W1. The proof is a direct one-line application of the core J-cost positivity lemma.
Claim. For every real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $0 < J(r)$.
background
The module records the status of the five Wightman axioms W0-W4 on the RS Hilbert space H_RS. W1 is realised as the spectral condition that off-vacuum states carry positive J-cost. The J-cost function is imported from the Cost module, where it is defined via the square identity Jcost r = (r-1)^2 / r for r ≠ 0 and shown positive away from the vacuum point r = 1.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module, passing the hypotheses 0 < r and r ≠ 1.
why it matters
The theorem supplies the spectral field of the wightmanStatusCert record that aggregates the status of W0-W4. It closes the W1 entry that follows from J-uniqueness in the forcing chain and leaves only the W4 sector-dependence gap noted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.