attenuation_length
plain-language theorem explainer
The declaration fixes the expected attenuation length for EeV cosmic rays in Earth at 10 km. Analysts of ANITA upgoing events cite this constant when comparing planetary radius to propagation distance. The definition is a direct numerical assignment with no derivation or computation.
Claim. The expected attenuation length for ultra-high-energy cosmic rays at EeV energies is defined as $10^{4}$ meters.
background
The ANITA upgoing module examines four anomalous events detected by the balloon experiment at energies 0.5-1 EeV. Standard physics predicts Earth is opaque at these energies because the attenuation length is only a few km while the planetary radius is 6371 km. Upstream results supply structural framing from the simplicial ledger (edge length from psi) and empirical program classes, plus mechanism design and mock theta constructions that set the geometric and statistical context for the RS verdict on systematics versus new physics.
proof idea
The definition is a direct constant assignment of the value 10000. It functions as a one-line wrapper supplying the numerical input to the ratio computation in the downstream theorem.
why it matters
This constant supplies the numerical premise for the parent theorem attenuation_prevents_upgoing, which shows the Earth radius exceeds the length by a factor greater than 600. It fills the EA-004.2 step in the module's RS analysis, confirming that standard attenuation rules out upgoing events and that BSM or rare SM explanations remain unwarranted. The placement aligns with the framework's emphasis on empirical opacity checks before invoking geometric defects or eight-tick structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.