Pith. sign in
module module moderate

IndisputableMonolith.Nuclear.AlphaDecayGeiger2FromJCost

show as:
view Lean formalization →

Module packages a Recognition-Science derivation of a second Geiger–Nuttall relation for alpha decay from the J-cost. It defines a domain cost on the decay channel, a positive canonical threshold, and a certificate type that packages the inequality. Nuclear and RS auditors cite it when linking half-life scaling to the cost functional rather than to a phenomenological fit. Structure is definitional plus nonnegativity and positivity lemmas, then an inhabited certificate.

claimOn the alpha-decay channel one defines a domain cost $C$ built from the Recognition $J$-cost, proves $C \ge 0$ and an evaluation identity, and introduces a positive canonical threshold $\theta > 0$. A certificate type asserts the second Geiger–Nuttall-type bound relating decay observables to $C$ and $\theta$; the module supplies an inhabited instance of that certificate.

background

Recognition Science takes the unique cost $J(x) = \frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$) forced by the Recognition Composition Law. Nuclear observables are read off as costs and thresholds on dimensionless ratios built from that $J$, in RS-native units where the tick $\tau_0$ is the fundamental time quantum.

This module sits in the nuclear layer. It imports the constants and cost libraries and introduces a domain-specific cost on the alpha-decay channel, together with a canonical threshold meant to mark the barrier scale that controls tunneling lifetime. The classical Geiger–Nuttall law correlates $\log$ half-life with $Q^{-1/2}$ (or related energy proxies); the RS claim is that an analogous second form follows once the channel is scored by $J$ rather than by an ad hoc Gamow integral.

Sibling definitions name the domain cost, its pointwise evaluation, nonnegativity, the canonical threshold and its positivity, and a certificate bundle that packages the resulting inequality.

proof idea

Definitional spine: introduce domainCost from the imported $J$-cost, record the evaluation identity, and prove nonnegativity by reduction to known $J \ge 0$. Define canonicalThreshold and prove it is positive from the constant layer. Package the Geiger–Nuttall-type inequality as a certificate structure and exhibit an inhabited instance, so downstream nuclear theorems can assume the bound by type rather than by a free hypothesis. No deep tactic proof of the full empirical law is claimed here; the module is the cost-to-certificate bridge.

why it matters in Recognition Science

Gives the nuclear layer a J-native handle on alpha-decay scaling, so half-life versus energy relations are not free phenomenology but consequences of the same cost that forces $\phi$, the eight-tick octave, and $D=3$ upstream. Downstream use is currently empty in the graph; the inhabited certificate is the export surface for later decay-chain or abundance arguments. Ties the classical Geiger–Nuttall pattern to T5 J-uniqueness and the RS cost calculus rather than to a separate tunneling model.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)