magnetismCert
plain-language theorem explainer
magnetismCert supplies a concrete witness for the MagnetismCert structure by wiring the five-phenomena count directly to its theorem and the two J-cost sign properties to their respective lemmas. A researcher reconstructing classical magnetism as recognition currents would cite it to close the local certification that exactly five behaviors appear with the required zero-field and applied-field signatures. The construction is a direct structure literal performing field-by-field assignment from the upstream results.
Claim. The magnetism certificate is the structure witnessing that the type of magnetic phenomena has cardinality 5, that the recognition cost satisfies $J(1)=0$, and that $J(r)>0$ for every $r>0$ with $r≠1$.
background
The module treats magnetic phenomena as recognition charge currents, with the field B proportional to current density relative to baseline. Five canonical behaviors (ferromagnetism through diamagnetism) are encoded by the finite type MagneticPhenomenon whose cardinality is fixed at 5. The recognition cost function Jcost, imported from the Cost module, vanishes at unit ratio and is strictly positive elsewhere; these sign properties are established by the lemmas zero_field (via Jcost_unit0) and applied_field (via Jcost_pos_of_ne_one).
proof idea
The definition is a direct structure literal. It sets the five_phenomena field to the theorem magneticPhenomenonCount, the zero_field_zero field to the theorem zero_field, and the applied_positive field to the theorem applied_field. No tactics or reductions occur beyond the field assignments.
why it matters
This definition instantiates the local certification that magnetism arises from recognition currents with exactly five observable configurations. It supplies the concrete record required by any downstream claim that the magnetic sector is fully accounted for inside the RS framework, consistent with the configDim=5 assignment and the J-cost properties derived from the forcing chain. No open questions are left inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.