Pith. sign in
module module moderate

IndisputableMonolith.Physics.Hydrogen_Ground_State_RS

show as:
view Lean formalization →

Hydrogen ground-state package in Recognition Science units. Defines a domain cost on the hydrogen scale, a positive canonical threshold from the RS cost layer, and an inhabited certificate HydrogenGSRS bundling nonnegativity and threshold positivity. Cite when matching RS ladder/yardstick predictions to the Bohr ground state. Structure is definitional with elementary positivity lemmas, not a forcing-chain derivation.

claimModule defining a domain cost $C_{\mathrm{dom}}$, a canonical threshold $\theta>0$, and a certificate structure for the hydrogen ground state in RS-native units, with lemmas $C_{\mathrm{dom}}\ge 0$, $\theta>0$, and inhabitation of the certificate.

background

Recognition Science works in native units imported from Constants (time quantum $\tau_0=1$ tick, and the usual $c=1$ convention) and the cost layer from Cost. The underlying cost is the J-functional $J(x)=(x+x^{-1})/2-1$ fixed by the Recognition Composition Law; scales sit on the $\varphi$-ladder.

This module specializes that cost language to hydrogen. domainCost is the RS cost assigned to a hydrogen domain (radial or energy configuration). canonicalThreshold is the positive cutoff used as a comparison scale for the ground state. HydrogenGSRS is the bundled certificate that the cost is nonnegative and the threshold is positive.

Sibling lemmas record equality at evaluation points, nonnegativity of the domain cost, and positivity of the threshold, so downstream physics can treat the ground-state package as a single inhabited object.

proof idea

Definition-and-certificate module, not a deep proof development. Core objects (domainCost, canonicalThreshold, HydrogenGSRS) are introduced by definition. Supporting facts are elementary: domainCost_nonneg and canonicalThreshold_pos discharge sign conditions; domainCost_at_eq records evaluation identities; cert and cert_inhabited show the certificate type is inhabited. No appeal to the T0–T8 forcing chain beyond what Constants and Cost already supply.

why it matters in Recognition Science

Supplies the hydrogen ground-state interface in the RS physics layer so later ladder, mass, or spectroscopy results can import a single certified package rather than re-proving cost nonnegativity. The graph currently lists no downstream users, so it functions as a leaf interface ready for Bohr-level or Rydberg matching against the $\varphi$-ladder mass formula (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). It does not itself close any open forcing step; it only packages Cost/Constants infrastructure for hydrogen.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)