below_threshold
plain-language theorem explainer
The theorem establishes that the J-cost is strictly positive for any positive real r not equal to one. Physicists deriving the photoelectric effect in Recognition Science cite it to confirm no electron ejection occurs below the work function threshold. The proof is a direct one-line application of the general J-cost positivity lemma.
Claim. For any real $r > 0$ with $r ≠ 1$, the J-cost satisfies $0 < J(r)$.
background
The module models the photoelectric effect by identifying the work function W with the J-cost evaluated at the ratio W/hν. At exact threshold J equals zero, so no electrons are ejected; below threshold the cost is positive. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 whenever x > 0 and x ≠ 1, proved by rewriting Jcost as a square and using positivity of squares and division.
proof idea
One-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module to the supplied hypotheses on r.
why it matters
This result supplies the below_threshold field of the PhotoelectricCert structure, which also records the five canonical materials and the zero threshold. It completes the basic RS certification of the photoelectric effect and aligns with J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.