module module moderate

`IndisputableMonolith.Experimental.GalliumAnomaly`

This module encodes experimental constants for the Gallium anomaly capture rates in Recognition Science. It supplies the SAGE measured value of 57.7 ± 6 SNU together with predicted rates, ratios, deficit bounds, and phi-suppression factors on the ladder. Neutrino physicists or RS modelers would cite these to test consistency with the mass formula. The module is declarative, consisting of definitions and bounds with no proofs.

claimThe measured gallium capture rate is $C_{Ga,meas} = 57.7(6)$ SNU. The RS-predicted rate $C_{Ga,pred}$ and ratio $r = C_{Ga,meas}/C_{Ga,pred}$ are defined with deficit bounds and suppression factor bounded by powers of the golden ratio on the phi-ladder.

background

Recognition Science derives constants from the forcing chain T0-T8, with J-uniqueness fixing the involution $J(x) = (x + x^{-1})/2 - 1$ and phi as the self-similar fixed point. The imported Constants module supplies the fundamental RS time quantum τ₀ = 1 tick. This experimental module situates the Gallium anomaly by introducing measured and predicted capture rates, ratios, real and bounded deficits, the gallium rung on the phi-ladder, and phi-suppression factors.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the experimental benchmark for the Gallium anomaly, enabling direct comparison to RS predictions via phi suppression and the mass formula yardstick * phi^(rung - 8 + gap(Z)). It anchors the experimental domain to the eight-tick octave and D = 3 spatial dimensions. No parent theorems are listed in the used-by edges, but the definitions support future validation of the Recognition Composition Law against solar neutrino data.

scope and limits

Does not derive capture rates from the J-cost or RCL.
Does not include other neutrino experiments or solar models.
Does not compute error propagation beyond the stated ±6 SNU.
Does not resolve the anomaly; only encodes the measured value and RS bounds.

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