module module moderate

`IndisputableMonolith.Experimental.ANITAUpgoing`

This module assembles ANITA experimental data on anomalous upgoing events, recording a count of approximately four events. Physicists comparing Recognition Science predictions on defects or attenuation to neutrino telescope observations cite these values. The module is purely definitional, importing Constants and containing no theorems or proofs.

claimThe number of anomalous upgoing events detected by ANITA satisfies $N_{\text{ANITA}} \approx 4$ over multiple flights.

background

Recognition Science starts from a single functional equation whose time quantum is the tick $\tau_0 = 1$, supplied by the imported Constants module. This experimental module supplies ANITA flight data for direct numerical comparison against RS-derived quantities such as attenuation length and curvature defect strength. Sibling definitions inside the module encode event counts, energies, and probability bounds that later feed into statistical tests.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies empirical inputs for testing Recognition Science against real detector data. It stands ready to connect to downstream comparisons involving the eight-tick octave and phi-ladder mass formulas, although the current dependency graph records no explicit parent theorems.

scope and limits

Does not derive the observed events from the J-functional equation.
Does not perform statistical hypothesis testing on the count.
Does not claim the events violate standard-model expectations.
Does not supply raw ANITA flight logs or error budgets.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (17)

def anita_upgoing_count L53
def anita_event_energy L57
def attenuation_length L61
theorem upgoing_statistically_limited L65
theorem attenuation_prevents_upgoing L71
def p_systematic L79
def p_rare_sm L83
def p_bsm L87
theorem systematic_dominant L91
theorem bsm_probability_small L97
def curvature_defect_strength L105
theorem defect_must_be_small L109
theorem geometric_requires_alignment L115
theorem bsm_not_warranted L121
theorem defect_site_prediction L125
theorem anita_inconclusive L129
def ea004_certificate L150