upgoing_statistically_limited
plain-language theorem explainer
The theorem shows that the number of anomalous upgoing events recorded by ANITA is strictly less than ten, so the sample lacks statistical power to support new-physics claims. Cosmic-ray experimentalists would cite it when assessing balloon-borne EeV data against standard attenuation. The proof is a one-line wrapper that unfolds the event-count definition and applies norm_num to confirm the numerical inequality.
Claim. Let $N$ be the number of anomalous upgoing events detected by ANITA. Then $N < 10$, where $N = 4$.
background
The module examines ANITA balloon observations of ultra-high-energy cosmic rays that appear to originate below the Earth. Standard physics predicts Earth is opaque at EeV energies because the attenuation length is only a few kilometers while the planetary radius is thousands of kilometers. The key definition is anita_upgoing_count, which records the observed count of such events as the natural number 4. The upstream radius definition supplies the neighborhood size for cellular-automaton models of defect propagation, though it is not invoked in this particular statement.
proof idea
The term proof first unfolds anita_upgoing_count to its literal value 4, then invokes norm_num to discharge the inequality 4 < 10 by direct arithmetic normalization.
why it matters
This result is the first step in the EA-004 certificate and is invoked directly by anita_inconclusive to conclude that ANITA data alone cannot establish new physics. It reinforces the module verdict that systematic effects or rare atmospheric configurations remain the most probable explanation, consistent with the Recognition Science emphasis on statistical limits before invoking geometric defects or BSM channels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.