nonclassical_state
plain-language theorem explainer
The theorem asserts that the J-cost is strictly positive for any positive real number r different from 1. Researchers deriving quantum optical states from Recognition Science would cite this to establish the positivity of J for nonclassical states. The proof consists of a direct application of the general positivity lemma for the J-cost function.
Claim. Let $r$ be a positive real number not equal to 1. Then the J-cost of $r$ is positive: $0 < J(r)$.
background
The J-cost function measures the recognition cost associated with a scaling factor r in the Recognition Science framework. In the Quantum Optics from RS module, photon states are modeled on the EM recognition lattice with five canonical states: Fock, coherent, squeezed, thermal, and entangled. Coherent states satisfy J = 0 corresponding to classical light at recognition equilibrium, while nonclassical states such as Fock states with positive photon number have J > 0. The key upstream result is the lemma Jcost_pos_of_ne_one, which states that J(x) > 0 whenever x > 0 and x ≠ 1, proved by expressing Jcost as a square divided by a positive term.
proof idea
The proof is a one-line wrapper that invokes the lemma Jcost_pos_of_ne_one with the given hypotheses on r.
why it matters
This theorem supplies the nonclassical_pos component of the QuantumOpticsCert structure, which certifies the five quantum optical states with coherent states having zero J-cost and nonclassical states having positive J-cost. It reinforces the RS distinction between classical and quantum light states. The result aligns with the framework's treatment of J-uniqueness in deriving quantum optics properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.