p_systematic
plain-language theorem explainer
This definition assigns the numerical value 0.70 to the estimated probability that ANITA upgoing events arise from systematic effects. Cosmic-ray experimentalists comparing instrumental explanations against rare standard-model or beyond-standard-model scenarios would cite the constant when ranking likelihoods. The definition consists of a direct real-number assignment with no computation or lemmas.
Claim. Let $p$ denote the probability that the ANITA upgoing events originate from systematic effects (instrumental or atmospheric). Then $p = 0.70$.
background
The module examines four anomalous ANITA balloon events at energies 0.5-1 EeV that appear to traverse the Earth, which standard attenuation lengths of order kilometers render impossible. Recognition Science lists three candidate explanations: systematic effects (instrumental, atmospheric, or shower geometry), rare standard-model configurations, and beyond-standard-model physics such as localized curvature defects. The module supplies separate probability estimates for each and concludes that systematic effects dominate.
proof idea
The declaration is a direct constant definition that binds the identifier to the literal real number 0.70. No tactics or upstream lemmas are invoked; the value is supplied as an input estimate for later comparison.
why it matters
The definition supplies the leading numerical input to the downstream theorem systematic_dominant, which proves that this probability exceeds the sum of the rare-SM and BSM estimates. It therefore realizes the module's explicit verdict that ANITA data alone do not justify new physics beyond standard attenuation plus systematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.