Pith. sign in
module module moderate

IndisputableMonolith.Nuclear.Nuclear

show as:
view Lean formalization →

Nuclear domain layer for Recognition Science: a nonnegative domain cost, a positive canonical threshold, and a three-parameter Bethe–Weizsäcker certificate tying bulk nuclear binding to the RS cost calculus. Nuclear-structure or mass-formula workers cite it when lifting semi-empirical binding into the phi-ladder setting. The module is mostly definitions plus elementary nonnegativity and inhabitance proofs over Cost and Constants.

claimThe nuclear module introduces a domain cost $C_{\mathrm{nuc}}$, proves $C_{\mathrm{nuc}}\ge 0$ and an evaluation identity, fixes a canonical threshold $\theta>0$, and packages a three-term Bethe–Weizsäcker certificate (volume, surface, Coulomb-type) as an inhabited nuclear certificate over the RS cost structure.

background

Recognition Science measures mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$ from the Cost layer; Constants supplies the RS-native tick $\tau_0=1$. Nuclear phenomenology is brought in through the classical Bethe–Weizsäcker (semi-empirical mass) decomposition of binding energy into bulk volume, surface, and Coulomb contributions.

This module sits in the Nuclear domain of the monolith. It does not re-derive the forcing chain (T5–T8); it only specializes the cost calculus to a nuclear domain cost, a positive threshold used as a recognition gate, and a certificate type that records a three-parameter BW fit against that cost.

Sibling objects named in the module are exactly those pieces: domainCost with equality-at-evaluation and nonnegativity, canonicalThreshold with positivity, and BetheWeizsacker3Cert / cert with inhabitance.

proof idea

Definition-heavy module, not a deep theorem chain. Domain cost is introduced as a Cost-derived functional; nonnegativity and the pointwise evaluation identity are short algebraic or inheritance lemmas from the Cost import. The canonical threshold is a positive constant (positivity is immediate from the Constants/Cost scaffolding). The Bethe–Weizsäcker certificate is a structure bundling three phenomenological coefficients against the domain cost; inhabitance is a constructive witness that the structure is nonempty. No multi-step tactic scripts beyond those elementary facts.

why it matters in Recognition Science

Gives the monolith a named nuclear landing zone so bulk binding (volume/surface/Coulomb) can be stated in the same cost language as the rest of RS, rather than as an external empirical fit. Downstream nuclear or mass-ladder developments would import this certificate and threshold when comparing BW-type binding to the phi-ladder mass formula (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). The module currently has no recorded used-by edges, so it is an entry point rather than a proved link in T0–T8. It does not claim a first-principles derivation of the BW coefficients from J-uniqueness or the eight-tick octave; it only packages the classical three-term form as an RS certificate.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)