ea004_certificate
plain-language theorem explainer
ea004_certificate defines a formatted string that consolidates the Recognition Science verdict on ANITA upgoing events. Experimental physicists working on ultra-high-energy cosmic rays cite it to record that the four detected events are most likely systematic or rare standard-model configurations. The definition assembles the string by direct concatenation of verdict lines drawn from sibling theorems on sample size, attenuation, and probability bounds.
Claim. The EA-004 certificate is the string that states: ANITA upgoing events (N≈4, energies 0.5–1 EeV) are statistically limited, Earth attenuation prevents upgoing paths at these energies, systematic probability dominates at ~70%, BSM probability is ~5%, curvature defects must be smaller than 10^{-5}, and ANITA data alone are inconclusive for new physics.
background
The module analyzes ANITA balloon detections of ultra-high-energy cosmic rays that appear to originate below the Earth. Standard physics predicts Earth is opaque at EeV energies because the attenuation length is only kilometers while the planetary radius is 6371 km. Recognition Science considers three explanations: instrumental or atmospheric systematics, beyond-standard-model processes, or rare standard-model configurations; the geometric-defect route (localized ledger curvature anomalies) is listed as speculative and requires specific defect sites. Upstream results include attenuation_prevents_upgoing (Earth radius / attenuation_length > 600) and anita_inconclusive (sample size < 10).
proof idea
The definition is a direct string literal formed by concatenating eight verdict lines. Each line is taken verbatim from the conclusions of the sibling theorems upgoing_statistically_limited, attenuation_prevents_upgoing, systematic_dominant, bsm_probability_small, defect_must_be_small, bsm_not_warranted, and anita_inconclusive.
why it matters
This definition supplies the single consolidated certificate for the EA-004 ANITA analysis inside the Recognition Science experimental module. It records the framework’s conclusion that the data do not warrant new physics and points to the falsifier given in the module doc-comment: detection of 100+ upgoing events above EeV without systematic explanation would reopen the case for BSM or RS geometric effects. The certificate closes the local analysis chain that begins with the forcing sequence T0–T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.