ElectronAffinityCert
plain-language theorem explainer
A certificate packing three structural axioms for electron-affinity scaling on the phi-ladder: domain cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is positive. Downstream code cites it to inhabit the affinity module without axioms. As a structure, it is pure interface; the proofs live in the field witnesses.
Claim. A certificate consists of three properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical affinity threshold is strictly positive.
background
The module treats electron affinities (F, Cl, O, S) as scales of the form $\phi^n E_{\mathrm{coh}}$ on the Recognition Science phi-ladder, with a structural (sorry-free) certificate rather than a fitted constant. Domain cost is the local cost functional on mass/energy pairs used to score recognition mismatch; the diagonal vanishing condition says matched arguments carry zero cost.
Nonnegativity of cost is the standard RS constraint inherited from the J-cost $J(x)=(x+x^{-1})/2-1$, which is nonnegative for $x>0$ and minimized at the identity $x=1$. Upstream, cost_nonneg records that every recognition event has nonnegative cost via Jcost_nonneg. The canonical threshold is the positive cutoff against which affinity scales are compared in this pass of the plan.
proof idea
No proof body: the declaration is a structure whose three fields are propositions. Inhabitation is deferred to the sibling definition that supplies domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos as the field witnesses. The shape is a pure interface bundle, not a derived lemma.
why it matters
Gives the typed contract for the electron-affinity-from-phi-ladder development. The sibling cert builds a concrete inhabitant, and cert_inhabited records Nonempty of the certificate, closing the structural layer of the module (status: 0 sorry, 0 axiom).
In the broader RS chain this sits under the phi-ladder mass/energy bookkeeping (T6 fixed point $\phi$, coherence energy $E_{\mathrm{coh}}$) rather than under T5–T8 forcing itself. The module note flags the open scale gap: $\phi^9\cdot 0.121,\mathrm{MeV}\sim 14.5,\mathrm{keV}$ versus observed eV affinities, so a $\phi^{-k}$ correction remains to be fixed; the certificate only locks the cost and threshold axioms needed before that numerical step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.