module module moderate

`IndisputableMonolith.QFT.LambShift`

The QFT.LambShift module states the experimental Lamb shift value in MHz together with related wave-function and alpha approximations inside the Recognition Science framework. QED phenomenologists comparing RS predictions to precision spectroscopy would reference these declarations. The module is a pure collection of definitions and numerical constants with no proofs.

claimThe principal object is the experimental Lamb shift $\Delta\nu_{\rm Lamb}$ expressed in MHz, accompanied by the fine-structure constant $\alpha$ and s/p-wave origin values.

background

The module sits in the QFT domain and imports the RS time quantum $\tau_0=1$ tick from Constants together with the cost structure from Cost. It assembles sibling declarations for lambShift_MHz, lamb_shift_approx, alpha_value, s_wave_at_origin_nonzero, p_wave_at_origin_zero and orbital_angular_momentum. The local setting is Recognition Science applied to QED observables, using RS-native units.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the experimental Lamb shift benchmark that any RS-derived QFT result would be tested against. It closes the comparison loop for the alpha band and phi-ladder predictions referenced in the broader framework.

scope and limits

Does not derive the Lamb shift from the J-cost or phi-ladder.
Does not contain a theorem equating the RS prediction to the experimental value.
Does not supply uncertainty intervals or higher-order corrections.
Does not import or reference the eight-tick octave or D=3 forcing steps.

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