module module high

`IndisputableMonolith.Experimental.ANITAUpgoing`

The ANITAUpgoing module tabulates the observed count of anomalous upgoing events from the ANITA experiment at approximately four events across flights. Physicists testing Recognition Science defect predictions against cosmic-ray data cite these counts when evaluating attenuation or BSM probabilities. The module consists solely of definitions that import the RS time quantum and organize sibling quantities for downstream comparison.

claimThe module supplies the ANITA upgoing event count $N_{ANITA}≈4$, event energies, attenuation lengths, and derived probabilities $p_{BSM}$ and $p_{rare,SM}$ in RS-native units.

background

Recognition Science derives all physics from the J-cost functional equation and the phi-ladder with eight-tick octave and D=3. This experimental module supplies ANITA data to confront those predictions. It imports the fundamental RS time quantum from Constants, whose doc-comment states: 'The fundamental RS time quantum (RS-native). τ₀ = 1 tick.' The module lists sibling definitions covering counts, energies, attenuation, and probabilities such as systematic_dominant and defect_must_be_small.

proof idea

This is a definition module, no proofs. It organizes experimental inputs as Lean definitions that reference the imported Constants module and expose the listed sibling declarations for use in probability calculations.

why it matters in Recognition Science

The module anchors empirical input for downstream theorems on upgoing suppression and BSM probabilities within the Recognition framework. It supplies the observed ~4 events that feed claims about attenuation_prevents_upgoing and bsm_probability_small, connecting experimental data to the T0-T8 forcing chain and the phi-ladder mass formula.

scope and limits

Does not derive the ~4 event count from any RS equation.
Does not simulate detector response or acceptance.
Does not compute statistical significance or p-values.
Does not address energy spectrum reconstruction beyond listing values.

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