WIMP
plain-language theorem explainer
The WIMP structure records the conventional parameters for weakly interacting massive particles inside the Recognition Science ledger-shadow model. Cosmologists and direct-detection experimentalists cite it when framing null results from DAMA, XENON, and COSINE-100. The definition is a direct three-field record with no lemmas or computational steps.
Claim. A WIMP is specified by a real mass value (in GeV), a real cross-section value (in cm²), and a boolean flag for thermal-relic freeze-out production.
background
The Cosmology.DarkMatter module treats dark matter as ledger shadows: gravitationally active but electromagnetically invisible configurations arising from odd-phase orbits in the 8-tick parity cycle. Mass is imported as an alias for the reals; Status is an inductive type with constructors spec, derived, hypothesis, and scaffold. The module doc states that the phantom sector at temporal resolution supplies one of five projections of the same object, with the rs_explains_null_detection theorem providing a phase-mismatch suppression mechanism.
proof idea
Direct structure definition introducing three fields; no lemmas or tactics are applied.
why it matters
This definition supplies the standard WIMP template used by downstream results such as frustration_gravity_only (which notes the phi-ladder has no matching rung for 10 GeV–10 TeV scales) and the DAMA/XENON modulation theorems that quantify experimental tension. It fills the COS-010 ledger-shadow proposition by contrasting the particle candidate against the 8-tick phase structure (T7) that produces electromagnetic decoupling. The module links the 1.79 GeV W-image to a separate spectrum-level projection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.