Pith. sign in
module module moderate

IndisputableMonolith.Physics.NeutronGFactorScoreCard

show as:
view Lean formalization →

Scorecard module that packages CODATA/PDG targets and residual checks for the neutron g-factor and magnetic moment against the RS nuclear prediction. Experimentalists and RS auditors cite it when verifying that the structural neutron-moment theorem lands inside the accepted band. The module is mostly certificate rows and nonnegativity/sign lemmas, not a deep derivation.

claimA certificate bundle for the neutron $g$-factor and $\mu_n/\mu_N$ against CODATA/PDG values: residual of the RS magnetic cost, sign constraints ($g_n<0$, $\mu_n<0$), nonnegativity of the cost, positivity of the threshold, and a named residual identity, culminating in a single scorecard certificate that holds.

background

Recognition Science treats nuclear magnetic moments as structural consequences of the J-cost on the golden ratio ladder. Upstream, the neutron magnetic moment module states the empirical anchor $\mu_n \approx -1.9130,\mu_N$ and records the RS structural ratio involving $J(\phi)$ and $\phi$, marked as a structural theorem with no sorry and no axioms.

This physics scorecard sits one layer above that nuclear result. It does not re-derive $\mu_n$; it freezes CODATA/PDG target rows for $g_n$ and $\mu_n/\mu_N$, defines a residual between the RS magnetic cost and those targets, and packages sign, matching, and threshold lemmas that a certificate can discharge in one place.

The local setting is audit-facing: named rows and a holds lemma so downstream reports can point at a single certificate rather than scatter CODATA constants through the nuclear layer.

proof idea

Definition-and-certificate module rather than a single deep proof. CODATA target rows are introduced as data. Residual and named-residual objects compare the RS magnetic cost to those targets. Separate lemmas record negativity of the CODATA $g$ and $\mu$ rows, nonnegativity of the magnetic cost, positivity of the threshold, and cost matching. The scorecard certificate aggregates those rows; its holds lemma is the top-level discharge that the packaged inequalities and residual identities are satisfied.

why it matters in Recognition Science

Gives the physics layer a single, citable CODATA/PDG scorecard for the neutron $g$-factor so the structural neutron-moment theorem can be audited without reopening nuclear definitions. Upstream status is structural (zero sorry, zero axiom) on $\mu_n$; this module turns that into residual and sign checks suitable for a report card. No downstream consumers are wired yet in the graph, so the module is presently a terminal audit artifact rather than an intermediate lemma factory. It touches the broader RS program of matching dimensionless nuclear observables to $\phi$-ladder structure without introducing free nuclear parameters.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)