applied_field
plain-language theorem explainer
The theorem establishes that the J-cost is strictly positive for any positive real r not equal to 1. Physicists modeling magnetic phenomena as recognition currents in the Recognition Science framework cite it to confirm nonzero current under applied fields. The proof is a direct one-line application of the upstream positivity lemma for J-cost.
Claim. For any real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $0 < J(r)$.
background
The MagnetismFromRS module treats magnetic phenomena as recognition charge currents, identifying the magnetic field B with recognition current density. The J-cost function quantifies deviation from equilibrium recognition states, with J(r) = 0 at baseline and J(r) > 0 under applied fields. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x ≠ 1 and x > 0, proved by rewriting Jcost as a square over a positive denominator.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module.
why it matters
This result supplies the applied_positive component in the magnetismCert definition, which certifies the five canonical magnetic phenomena. It fills the applied-field case in the module's contrast between zero-field equilibrium (J = 0) and nonzero current under external fields, consistent with the Recognition Science treatment of magnetic phenomena as configDim D = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.