`correction_factor`

proved

show as: view math explainer →

module: IndisputableMonolith.Experimental.GalliumAnomaly
domain: Experimental
line: 131 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Experimental.GalliumAnomaly on GitHub at line 131.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 128  norm_num [abs_of_pos]
 129
 130/-- **THEOREM EA-003.5**: The correction factor is ~0.8. -/
 131theorem correction_factor : sigma_rs / ga_capture_predicted = (57.7 / 74.0) := by
 132  unfold sigma_rs ga_capture_predicted
 133  norm_num
 134
 135/-- **THEOREM EA-003.6**: The correction is within φ-suppression bounds. -/
 136theorem correction_within_bounds : sigma_rs / ga_capture_predicted > 0.75 := by
 137  rw [correction_factor]
 138  norm_num
 139
 140/-! ## IV. The Anomaly Resolution -/
 141
 142/-- **THEOREM EA-003.7**: The Gallium anomaly is explained in RS. -/
 143theorem gallium_anomaly_explained : |ga_capture_ratio - 0.80| < 0.10 := by
 144  unfold ga_capture_ratio ga_capture_measured ga_capture_predicted
 145  norm_num [abs_of_pos]
 146
 147/-- **THEOREM EA-003.8**: No sterile neutrinos are needed.
 148    3 generations suffice with nuclear correction. -/
 149theorem no_sterile_needed : phi_suppression_ga > 0 := phi_suppression_bounded.1
 150
 151/-- **THEOREM EA-003.9**: Standard Solar Model + RS = observed.
 152    SSM predicts 74 SNU; RS correction gives ~59 SNU. -/
 153theorem ssm_plus_rs_equals_obs : sigma_rs > 55 ∧ sigma_rs < 65 := by
 154  unfold sigma_rs ga_capture_predicted
 155  norm_num
 156
 157/-- **THEOREM EA-003.10**: RS predicts solar model independent check.
 158    The RS sigma value is in [55, 65], independent of solar model details. -/
 159theorem rs_solar_model_independent : sigma_rs > 55 ∧ sigma_rs < 65 :=
 160  ssm_plus_rs_equals_obs
 161

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.