module module low

`IndisputableMonolith.QFT.LambShift`

The QFT.LambShift module declares the experimental Lamb shift value in MHz together with alpha approximations and related wave-function facts. Atomic and QFT researchers comparing Recognition Science predictions to hydrogen spectroscopy would reference these constants. The module consists entirely of definitions and numerical approximations with no formal proofs.

claimThe experimental Lamb shift frequency shift for hydrogen, expressed in MHz, together with the fine-structure constant approximations and s/p-wave penetration properties at the origin.

background

Recognition Science places QFT effects inside the J-cost and phi-ladder framework imported from Constants and Cost. Constants supplies the base time quantum τ₀ = 1 tick; Cost supplies the recognition cost function used to quantify defects. The module therefore expresses the Lamb shift, a vacuum-fluctuation splitting between 2S and 2P levels, directly in RS-native units and in the observable MHz scale.

proof idea

This is a definition module, no proofs. It contains only constant declarations, simple numerical approximations for the Lamb shift and alpha, and elementary facts about wave-function behavior at the origin.

why it matters in Recognition Science

The module supplies the experimental Lamb shift benchmark against which RS-derived QFT predictions are compared. It feeds alpha approximations and shift fractions into higher-level QFT calculations in the Recognition framework, closing the loop from the phi-ladder constants to spectroscopic observables.

scope and limits

Does not derive the Lamb shift from the J-functional equation.
Does not include higher-order QED radiative corrections.
Does not specify conversion factors from RS units to SI beyond the MHz label.
Does not attach uncertainty intervals to the experimental value.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (33)

def lambShift_MHz L39
theorem lamb_shift_approx L42
def alpha_approx L48
theorem alpha_value L51
def lambShiftFraction L55
theorem lamb_shift_tiny L58
def s_wave_at_origin_nonzero L67
def p_wave_at_origin_zero L71
def s_wave_l L74
def p_wave_l L77
theorem orbital_angular_momentum L80
theorem s_wave_penetrates_nucleus L86
theorem p_wave_excluded_from_origin L92
def e_2S_eV L100
def e_2P_eV L103
def dirac_degeneracy L106
theorem dirac_prediction L109
def lamb_shift_ueV L112
theorem s_higher_than_p_by_lamb_shift L115
def experimental_uncertainty L123
def theoretical_uncertainty L126
theorem theory_more_precise L129
theorem uncertainties_small L135
def significant_figures L142
theorem precision_agreement L145
def alpha_power_in_formula L154
theorem alpha_fifth_power L157
theorem alpha_fifth_small L161
def rsInterpretation L170
def potentialSmearin L175
structure LambShiftProofs L186
def lambShiftProofs L194
def relatedEffects L204