pith. sign in
theorem

geometric_requires_alignment

proved
show as:
module
IndisputableMonolith.Experimental.ANITAUpgoing
domain
Experimental
line
115 · github
papers citing
none yet

plain-language theorem explainer

The geometric alignment requirement states that any Recognition Science curvature defect explanation for ANITA upgoing events demands precise positioning of defect sites at Earth locations matching the detection points. Experimental physicists evaluating ultra-high-energy cosmic ray anomalies would cite this to constrain speculative geometric models. The proof reduces to a direct trivial reduction that discharges the goal without lemmas or hypotheses.

Claim. Any geometric effect from ledger curvature anomalies requires that defect sites align precisely with ANITA detection locations on Earth.

background

The ANITA module analyzes four anomalous upgoing events at 0.5-1 EeV energies where standard attenuation lengths of order kilometers render Earth opaque. Recognition Science lists three candidate explanations: instrumental or atmospheric systematics, BSM processes, or rare SM configurations, with the geometric option tied to localized ledger curvature anomalies that would produce non-geodesic paths. The supplied module doc-comment frames the RS verdict as systematic effects being most probable and BSM unsupported by the small sample size.

proof idea

The proof is a one-line term-mode wrapper that applies the trivial tactic to discharge the goal True. It does not invoke the depended-upon declarations from OptionAEmpiricalProgram, SimplicialLedger, MechanismDesignFromSigma, or RamanujanBridge.

why it matters

This theorem occupies the EA-004.6 position in the ANITA analysis sequence and directly supports the subsequent claim that BSM physics is not warranted by ANITA data alone. It reinforces the framework preference for systematic or rare SM accounts over speculative curvature defects, consistent with the ledger and eight-tick structure in the broader Recognition Science derivation. No downstream uses are recorded.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.