Pith. sign in
module module moderate

IndisputableMonolith.Physics.Lamb_Shift_RS

show as:
view Lean formalization →

Module packaging the Recognition Science treatment of the hydrogen Lamb shift via a nonnegative domain cost and a canonical positive threshold. It exposes a certificate type witnessing that the RS cost sits at the physical threshold. Spectroscopists and RS auditors cite it when checking the ladder-side Lamb prediction. Structure is definitional: cost, threshold positivity, and an inhabited cert record.

claimDefine a domain cost $C$ on the RS configuration space with $C\ge 0$, a canonical threshold $\theta>0$, and a certificate type asserting that the Lamb-shift domain cost meets $\theta$ in RS-native units (built from $\varphi$-ladder and $J$-cost data).

background

Recognition Science derives spectroscopic shifts from the unique cost $J(x)=(x+x^{-1})/2-1$ fixed by the Recognition Composition Law, together with the $\varphi$-ladder mass and energy rungs. The Lamb shift (the $2S_{1/2}-2P_{1/2}$ splitting) is treated here as a domain-cost excess above a canonical threshold rather than as a loop integral in QED.

The module sits in the Physics layer and imports only Constants (RS time quantum $\tau_0=1$ tick and related units) and Cost (the $J$-cost infrastructure). Sibling definitions introduce domainCost (nonnegative), its evaluation identity, canonicalThreshold (strictly positive), and the record LambShiftCert bundling the numerical claim.

Local convention: energies and thresholds are expressed in RS-native units with $c=1$ and $\hbar=\varphi^{-5}$, so the certificate is a pure dimensionless comparison once the rung offset is fixed.

proof idea

Definition module with light lemmas, not a deep derivation. Nonnegativity of the domain cost and positivity of the canonical threshold are recorded as short facts. The main object is an inhabited certificate record LambShiftCert whose witness cert packages the equality or bound linking domain cost to threshold. No forcing-chain or RCL expansion is proved here; those enter only through the imported Cost and Constants layers.

why it matters in Recognition Science

Gives the Physics-layer handle for the RS Lamb-shift claim so downstream spectroscopy or fine-structure audits can cite a single certificate rather than rebuild the cost comparison. It does not yet feed named parent theorems in the graph (used_by is empty), so it is a leaf packaging node: the place where a numerical or rung-level Lamb prediction is frozen for export. Ties to the broader RS program through $J$-cost uniqueness (T5) and the $\varphi$-ladder mass formula; the eight-tick and $D=3$ landmarks are ambient but not invoked directly. Closes a scaffolding gap only insofar as an inhabited cert removes an ad-hoc constant from later physics modules.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)