attenuation_prevents_upgoing
plain-language theorem explainer
The theorem establishes that Earth's radius divided by the EeV attenuation length exceeds 600, confirming that upgoing particles at these energies are fully absorbed under standard physics. Experimental physicists evaluating ANITA cosmic-ray data would cite this result to exclude standard-model traversal through the planet. The proof is a direct numerical reduction after unfolding the attenuation length constant to its 10 km value.
Claim. Let $R_⊕ = 6.371×10^6$ m be Earth's radius and let $ℓ_{att}$ be the expected attenuation length in Earth at EeV energies. Then $R_⊕ / ℓ_{att} > 600$.
background
The ANITA upgoing events module examines four anomalous detections at 0.5-1 EeV and contrasts standard attenuation with possible Recognition Science curvature defects. The attenuation length is defined noncomputably as 10 km, so that the planetary radius of 6371 km yields an optical depth far greater than unity. The modal operator Possible is imported from the Possibility module to frame alternative explanations as reachable at finite cost, though the present theorem uses only the numerical definition.
proof idea
The proof is a one-line wrapper that unfolds attenuation_length to its 10 km constant and applies norm_num to verify the concrete inequality 6371000 / 10000 > 600.
why it matters
This result supplies the second numbered claim in the EA-004 certificate, which concludes that ANITA upgoing events are most likely systematic or rare atmospheric effects. It anchors the experimental analysis by quantifying Earth opacity at EeV energies, thereby limiting the scope for speculative RS geometric effects or BSM propagation in the broader verdict. The theorem directly feeds the certificate string that lists attenuation_prevents_upgoing as a verified component.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.