ea003_certificate
plain-language theorem explainer
The ea003_certificate definition supplies a formatted status string asserting that the gallium neutrino anomaly is resolved by Recognition Science nuclear φ-ladder effects. Experimental physicists working on solar neutrino data would cite it to claim the ~20% deficit requires no sterile neutrinos. It is assembled as a static string concatenation that embeds the outcomes of the module's bounding theorems on ratios and corrections.
Claim. The EA-003 certificate asserts that the gallium capture ratio satisfies $0.70 < r < 0.85$, the RS correction factor is approximately 0.80 from the nuclear φ-ladder at rung 4.5, and the observed deficit is explained without sterile neutrinos.
background
The gallium anomaly is the observed deficit in solar neutrino capture on gallium, with the Standard Solar Model predicting 74 SNU while GALLEX/SAGE measurements give 55-58 SNU. Recognition Science attributes this to the φ-ladder structure of the gallium nucleus, where rung r_Ga ≈ 4.5 produces a suppression φ^(-4.5) modified by gap resonances to an overall factor near 0.80. The module sets the local theoretical setting that three neutrino generations plus this nuclear correction suffice. Upstream results include deficit_real (ratio < 0.85), deficit_bounded (ratio > 0.70), correction_factor (ratio = 57.7/74.0), and gallium_anomaly_explained (|ratio - 0.80| < 0.10).
proof idea
The definition is a direct string concatenation that assembles a header, a sequence of checkmark lines referencing the sibling theorems deficit_real, deficit_bounded, phi_suppression_bounded, rs_matches_measurement, correction_factor, correction_within_bounds, gallium_anomaly_explained, and no_sterile_needed, then a conclusion paragraph.
why it matters
This definition closes the EA-003 experimental module by packaging the resolution of the gallium anomaly as a single certificate. It encapsulates the claim that nuclear φ-ladder structure accounts for the deficit, consistent with the Recognition Science phi-ladder mass formula and the eight-tick octave. No downstream theorems depend on it, but it directly supports the framework verdict that three generations suffice. It touches the open question of distinguishing this nuclear effect from sterile neutrino oscillation patterns via L/E dependence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.