gallium_anomaly_from_ledger
plain-language theorem explainer
The declaration defines the proposition gallium_anomaly_from_ledger to hold exactly when the self-similar fixed point phi is positive. Neutrino experimentalists analyzing gallium and ANITA data would reference this when embedding their results into the Recognition Science framework. It is introduced as a direct one-line abbreviation with no additional proof steps.
Claim. The gallium anomaly is captured by the proposition that the self-similar fixed point satisfies $0 < phi$.
background
In Recognition Science, phi is the unique positive real satisfying the self-similar fixed point forced at step T6 of the unified forcing chain after J-uniqueness at T5. The gallium anomaly refers to the observed deficit in solar neutrino capture rates on gallium targets. This Experimental.GalliumAnomalyStructure module supplies named propositions that link such anomalies directly to the sign of phi without computing rates or statistics.
proof idea
The definition is a direct abbreviation that sets gallium_anomaly_from_ledger equal to the inequality 0 < phi. No lemmas or tactics are invoked.
why it matters
This definition supplies the structural input for gallium_anomaly_structure and anita_implies_gallium, which connect the gallium anomaly and ANITA upgoing events to the core claim that phi must be positive. It fills the experimental interface after T6 phi fixed point and before mass-ladder applications. The open question it touches is whether the observed anomaly magnitude aligns with the phi-ladder gap predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.