NucMagicNumbers2Cert
plain-language theorem explainer
A certificate packing three elementary cost properties used for the nuclear magic-number story from J-cost: diagonal domain cost vanishes, domain cost is nonnegative off the axes, and the canonical threshold is positive. Downstream code builds a concrete inhabitant and proves the type is nonempty. The declaration is a pure structure (no proof body).
Claim. A certificate is a triple of facts: (1) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (2) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (3) the canonical threshold is strictly positive.
background
The module treats nuclear magic numbers (2, 8, 20, 28, 50, 82, 126) as a structural comparison against a phi-ladder sequence $N_k \sim \varphi^k \cdot 2$. Status is a structural theorem with no sorry and no axioms; the ladder values 2, 5, 9, 14, 22, 36, 58 sit near but are not identical to the empirical shell closures.
Domain cost is the local cost functional on mass/energy pairs used in this nuclear layer; the certificate only records that it vanishes on the diagonal and stays nonnegative when both arguments are positive. The canonical threshold is the positive cutoff against which shell or rung comparisons are made. Upstream, recognition cost is already known to be nonnegative for any recognition event via the J-cost nonnegativity lemma in ObserverForcing.
proof idea
No proof: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Inhabitation is supplied later by wiring the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos into the concrete cert value.
why it matters
Gives a single named bundle for the cost hypotheses the nuclear magic-number v2 layer needs, so later lemmas can depend on one certificate type rather than three free-floating facts. Immediate consumers are the concrete cert definition and the cert_inhabited theorem proving Nonempty NucMagicNumbers2Cert. In the broader RS picture this sits under the nuclear domain's structural reading of magic numbers against the phi-ladder (T6 self-similar fixed point), not under the forcing chain T0–T8 itself. It does not close the numerical gap between ladder values and empirical shells; it only packages the J-cost hygiene used in that comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.