cert
plain-language theorem explainer
Packages the three structural obligations of the cyclotron-frequency certificate into one inhabited record: diagonal domain cost vanishes, domain cost is nonnegative for positive mass and charge, and the canonical threshold is positive. Anyone citing the cyclotron J-cost link (omega_c = J(phi) omega_p) uses this bundle. The body is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There is a certificate record asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive mass $m$ and charge $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module derives cyclotron frequency from the Recognition Science J-cost. Classically $\omega_c = qB/m$; in RS the same frequency is identified with $J(\varphi),\omega_{\mathrm{plasma}}$ in a partially magnetized plasma, and at that matching point the plasma parameter evaluates to $8.47$.
domainCost is the local cost functional on mass/charge pairs; its diagonal vanishing and nonnegativity are the cost axioms needed before any threshold comparison. canonicalThreshold is the positive cutoff against which the cost is measured. Upstream, the foundation lemma cost_nonneg states that every recognition event has nonnegative cost via $J$-cost nonnegativity, which is the global pattern this local certificate mirrors.
Cyclotron5Cert is the structure that packages exactly those three propositions so downstream cyclotron arguments can assume a single inhabited certificate rather than three free-floating lemmas.
proof idea
One-line structure instance. The three fields of Cyclotron5Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra tactics or algebraic work; the definition is pure wiring of already-established facts.
why it matters
Gives a single named witness that the cost side of the cyclotron story is closed: diagonal cost zero, cost nonnegative, threshold positive. That is the structural precondition for treating $\omega_c = J(\varphi),\omega_p$ as a cost-minimizing match rather than an ad hoc fit. The module is marked structural theorem (0 sorry, 0 axiom) in the Plan v7 120th pass; this certificate is the packaging step that makes that status usable.
No downstream consumers are recorded yet in the graph, but the sibling cert_inhabited and any later plasma-parameter or magnetized-plasma theorems would take this record as the cost hypothesis bundle. It sits downstream of the J-uniqueness forcing (T5) only indirectly, through the shared nonnegativity of $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.