p_bsm
plain-language theorem explainer
p_bsm supplies the Recognition Science estimate of 0.05 for the probability that ANITA upgoing events arise from BSM or geometric-defect effects. Experimentalists working on ultra-high-energy cosmic rays would cite the value when deciding whether four anomalous events justify new physics. The definition is a direct constant assignment that encodes the speculative status of localized ledger curvature anomalies.
Claim. $p_{BSM} = 0.05$, where $p_{BSM}$ is the assigned probability that the ANITA upgoing events originate from beyond-standard-model physics or Recognition-Science geometric effects rather than systematics or rare standard-model processes.
background
The ANITA balloon experiment recorded roughly four ultra-high-energy cosmic-ray events at 0.5-1 EeV that appear to traverse the Earth, where standard attenuation lengths are only kilometers. Recognition Science frames the events under three headings: instrumental or atmospheric systematics, rare standard-model shower configurations, and speculative BSM contributions from localized ledger curvature anomalies (topological defects). The module concludes that systematics dominate and that ANITA data alone supply insufficient evidence for new physics.
proof idea
The declaration is a direct constant definition that sets the identifier to the numerical value 0.05. No lemmas or tactics are invoked; the assignment simply records the speculative low probability attached to the geometric-defect hypothesis.
why it matters
The definition supplies the numerical input used by systematic_dominant (p_systematic > p_rare_sm + p_bsm) and by bsm_probability_small (p_bsm < 0.10). It therefore supports the downstream claim bsm_not_warranted that ANITA events do not justify invoking new physics. The value aligns with the framework's emphasis on the eight-tick octave and standard attenuation while leaving open whether defect sites at other locations would produce observable signals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.