module module

`IndisputableMonolith.Experimental.GalliumAnomaly`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (17)

def ga_capture_measured L38
def ga_capture_predicted L42
def ga_capture_ratio L46
theorem deficit_real L49
theorem deficit_bounded L55
def gallium_rung L62
def phi_suppression_ga L65
theorem phi_suppression_bounded L69
def sigma_rs L123
theorem rs_matches_measurement L126
theorem correction_factor L131
theorem correction_within_bounds L136
theorem gallium_anomaly_explained L143
theorem no_sterile_needed L149
theorem ssm_plus_rs_equals_obs L153
theorem rs_solar_model_independent L159
def ea003_certificate L168