zero_field
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 in Recognition Science
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.
scope and limits
- Does not derive the explicit form of J for arguments other than 1.
- Does not compute magnetic field strength from current density.
- Does not enumerate or classify the five magnetic phenomena.
- Does not link to the phi-ladder or forcing chain steps T0-T8.
Lean usage
example : Jcost 1 = 0 := zero_fieldformal statement (Lean)
31theorem zero_field : Jcost 1 = 0 := Jcost_unit0
proof body
Term-mode proof.
32
33/-- Applied field: J > 0. -/