module module high

`IndisputableMonolith.QFT.LambShift`

The QFT.LambShift module supplies the experimental Lamb shift value in MHz together with approximations for alpha and orbital wave behaviors at the origin. Researchers computing QFT corrections inside the Recognition Science framework cite these definitions. The module is organized as a collection of definitions and short lemmas that rest on the imported constants and cost structures.

claimThe experimental Lamb shift frequency expressed in megahertz, together with related approximations to the fine-structure constant and s-wave versus p-wave penetration properties.

background

The module sits inside the QFT domain of Recognition Science and imports the fundamental RS time quantum τ₀ = 1 tick from Constants together with the J-cost machinery from Cost. It therefore inherits the Recognition Composition Law and the phi-ladder conventions already fixed in those upstream modules. The local focus is the Lamb shift as a concrete QFT observable whose numerical value is stated directly in RS-native units.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Lamb shift datum that anchors numerical checks against the alpha band (137.030, 137.039) and the eight-tick octave structure. It therefore feeds any later QFT energy-shift calculations that rely on the same constants and cost functions.

scope and limits

Does not derive the Lamb shift from the J-functional equation.
Does not contain a full QFT Lagrangian or Feynman rules.
Does not compute higher-order radiative corrections beyond the listed approximations.
Does not link the Lamb shift to mass-rung formulas on the phi-ladder.

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