bsm_probability_small
plain-language theorem explainer
BSM probability for ANITA upgoing events falls below ten percent under the Recognition Science assignment. Cosmic-ray experimentalists cite the bound when evaluating whether anomalous EeV events require physics beyond standard attenuation and systematics. The argument reduces directly by unfolding the constant probability definition and normalizing the numerical comparison.
Claim. $p_{BSM} < 0.10$, where $p_{BSM}$ denotes the assigned probability of beyond-standard-model or Recognition Science geometric explanations for the ANITA upgoing events.
background
The module examines ANITA balloon detections of ultra-high-energy cosmic rays that appear to originate below the Earth, events forbidden by standard attenuation lengths of kilometers at EeV energies. Recognition Science considers three channels: dominant systematic effects, rare standard-model configurations, and speculative BSM or curvature-defect contributions. The upstream definition sets $p_{BSM}$ to the constant 0.05 as a speculative estimate for the BSM/RS geometric channel.
proof idea
Term-mode proof that unfolds the definition of $p_{BSM}$ to its numerical value 0.05 and applies norm_num to discharge the inequality against 0.10.
why it matters
Supplies the key inequality for the parent theorem bsm_not_warranted, which concludes BSM physics is not warranted by ANITA data alone, and feeds the ea004_certificate summarizing the full analysis. It corresponds to theorem EA-004.4, reinforcing that small sample size and systematic dominance suffice without new physics. The bound limits the role of speculative curvature defects while aligning with the module verdict that ANITA events do not motivate extensions beyond standard model plus systematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.