zero_field
plain-language theorem explainer
Zero-field equilibrium in the recognition cost model is established by showing the J-cost vanishes at argument 1. Researchers modeling magnetic phenomena from recognition currents would reference this to set the baseline for applied-field deviations. The result follows immediately from the unit lemma in the cost core.
Claim. $J(1) = 0$ where $J$ is the recognition cost function.
background
In the Magnetism from RS module, magnetic fields arise from recognition charge currents, with B expressed as current density relative to baseline. The J-cost function quantifies deviation from equilibrium via the squared ratio formula (x-1)^2/(2x). This zero-field result builds directly on the upstream Jcost_unit0 lemma, which proves the cost vanishes at unit scale by simplification.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module.
why it matters
It supplies the zero_field_zero component in the magnetismCert definition, which certifies the five canonical magnetic phenomena under the Recognition Science axioms. This anchors the equilibrium case where recognition current is absent, consistent with the module statement that at zero field J equals zero. It closes the baseline for the magnetism model without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.