cert
plain-language theorem explainer
Packages three structural facts about the electron-affinity domain cost into one certificate: diagonal vanishing, nonnegativity for positive mass and energy scales, and a strictly positive canonical threshold. Anyone working the phi-ladder affinity scale (F, Cl, O, S) cites this bundle rather than the three lemmas separately. Construction is a pure structure instance wiring sibling equalities and inequalities.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of matching scale $r$ to itself is zero; (ii) for all positive mass and energy scales $m,e$, the domain cost is nonnegative; (iii) the canonical affinity threshold is strictly positive.
background
The module treats electron affinities (F ~ 3.4 eV, Cl ~ 3.6, O ~ 1.46, S ~ 2.07) as a phi-ladder scale problem: affinities should track $\phi^n E_{\mathrm{coh}}$, with an observed F/O ratio near $\phi^{1.6}$. A raw $\phi^9$ rung sits at keV rather than eV, so a negative-power correction is expected; the present file only locks the cost geometry that any such correction must respect.
Domain cost is the local cost functional on mass and energy scales used for the affinity comparison. The certificate structure demands three properties: cost vanishes on the diagonal $m=e$ (away from zero), cost is nonnegative for positive arguments, and a fixed positive threshold separates admissible from inadmissible scale pairs.
Upstream, nonnegativity of recognition cost is already forced in ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity at positive state. The sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos specialize that geometry to the affinity domain.
proof idea
One-line structure instance. The three fields of ElectronAffinityCert are filled by the corresponding sibling lemmas: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No extra algebra or case splits.
why it matters
Gives a single named inhabitant of the electron-affinity certificate so downstream affinity-scale arguments can assume the cost axioms without re-proving them. The module is marked structural (0 sorry, 0 axiom) in the Plan v7 104th pass; this definition is the packaging step that makes that status usable.
It sits under the broader RS cost geometry (T5 $J$-uniqueness and the Recognition Composition Law), specialized to chemical affinity scales on the phi-ladder. No downstream theorems currently depend on it in the graph, so its role is interface closure inside the affinity module rather than a link into mass or alpha chains. The open numerical question (which negative rung restores eV-scale affinities) is deliberately left outside this certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.