pith. machine review for the scientific record. sign in
def definition def or abbrev high

rs_counter_term

show as:
view Lean formalization →

The RS counter-term is defined as the product of the fine-structure constant over pi, phi raised to the negative muon rung, and the gap-1332 resonance factor. Researchers modeling the muon g-2 anomaly within Recognition Science would cite this term when constructing predictions that deviate from the Standard Model. The definition is a direct algebraic composition of the pre-established constants for alpha_em, muon_rung, and gap_1332_factor.

claim$c = (a / p) * f^{-m} * g$ where $a$ is the fine-structure constant, $p$ is pi, $f$ is the golden ratio, $m$ is the muon rung on the phi-ladder, and $g$ is the gap-1332 resonance factor.

background

The module derives the muon g-2 anomaly resolution through phi-ladder calibration in Recognition Science, addressing the reported 4.2 sigma discrepancy with the Standard Model. The fine-structure constant is fixed at approximately 1/137.036, the muon rung is placed at 13 on the ladder, and the gap-1332 factor is set to 1 over 1332 times phi. Upstream constants establish these quantities as positive real numbers in the framework.

proof idea

The definition is a one-line algebraic composition that multiplies the fine-structure constant divided by pi, by phi to the power of the negative muon rung, and by the gap-1332 factor. No additional lemmas or tactics are invoked beyond direct substitution of the constituent definitions.

why it matters in Recognition Science

This term is added to the SM reference value to produce the RS prediction for the muon anomalous magnetic moment. It supports the downstream claim that the RS prediction exceeds the Standard Model result, filling the phi-ladder step in the Recognition Science resolution of the anomaly. The parent theorem establishes positivity of the counter-term itself.

scope and limits

Lean usage

noncomputable def a_mu_rs_prediction : ℝ := sm_reference + rs_counter_term

formal statement (Lean)

  53noncomputable def rs_counter_term : ℝ :=

proof body

Definition body.

  54  (alpha_em / Real.pi) * (phi ^ (-muon_rung)) * gap_1332_factor
  55
  56/-- **THEOREM EA-001.4**: The RS counter-term is positive. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.