Pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.UltraHighEnergyCosmicRay

show as:
view Lean formalization →

Module packaging the Recognition Science account of ultra-high-energy cosmic rays: a domain cost on the relevant kinematic scale, its nonnegativity, a positive canonical energy threshold, and an inhabited certificate type. Astrophysicists citing RS predictions for the UHECR cutoff or composition ladder would import it. Content is definitional plus short positivity lemmas over the Cost and Constants layers.

claimThe module introduces a UHECR domain cost $C$ (nonnegative), a canonical threshold $E_* > 0$, and a certificate type $\mathrm{UHECRCert}$ inhabited by a witness $\mathrm{cert}$ that packages these structural facts for downstream astrophysical use.

background

Recognition Science measures kinematic and compositional mismatch with the J-cost $J(x) = (x + x^{-1})/2 - 1$ from the Cost layer, forced uniquely by the Recognition Composition Law and the T5 step of the unified forcing chain. Constants supplies the RS-native tick $\tau_0$ and the golden ratio $\varphi$ that set the phi-ladder and the mass/energy yardsticks.

Ultra-high-energy cosmic rays sit at the extreme end of that ladder. The module localizes the general cost machinery to a UHECR domain cost and a single positive canonical threshold intended as the RS-native scale against which observed events (and cutoffs such as GZK-like suppression) are compared. Sibling lemmas record equality at the evaluation point and nonnegativity of the cost, plus positivity of the threshold.

The certificate type $\mathrm{UHECRCert}$ is the standard RS pattern: a Prop-carrying bundle that downstream astrophysics modules can assume or inhabit without re-proving the local arithmetic.

proof idea

Definition module with thin lemma layer. domainCost and canonicalThreshold are defs over Cost/Constants; domainCost_at_eq is an evaluation identity; domainCost_nonneg and canonicalThreshold_pos are short nonnegativity/positivity arguments. UHECRCert packages the structural hypotheses; cert and cert_inhabited supply a concrete inhabitant. No deep tactic proof; the work is naming the domain objects and discharging the obvious sign facts.

why it matters in Recognition Science

Places UHECR inside the same cost-and-threshold pattern used elsewhere in RS astrophysics, so energy scales inherit the phi-ladder and J-cost rather than being inserted by hand. Downstream used_by is currently empty: this is a leaf packaging module ready for spectrum, composition, or cutoff theorems. It touches the broader program of deriving astrophysical thresholds from T5–T8 landmarks (J-uniqueness, $\varphi$, eight-tick structure, $D=3$) without adding new free parameters. Open work is connecting the canonical threshold to concrete observables (GZK-scale suppression, composition steps) in later modules.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)