DarkMatterXENONCert
plain-language theorem explainer
The DarkMatterXENONCert structure packages the RS dark matter prediction that the mass ratio equals 1/45 together with the requirement that the cross-section ratio at J(φ) is positive and lies below 0.13. Cosmologists comparing the phi-ladder mass formula to XENONnT direct-detection limits would cite this certificate when stating the predicted band. The declaration is a plain structure definition whose three fields are later filled by reflexivity on the mass ratio and by positivity and interval lemmas defined in the same module.
Claim. A structure certifying that the dark matter to W-boson mass ratio equals $1/45$, that the dark matter cross-section ratio (evaluated at $J(φ)$) is positive, and that this ratio satisfies $0 < σ < 0.13$.
background
The module formalizes the RS dark matter prediction for XENON experiments. The mass ratio is fixed at 1/45 by the gap-45 condition on the phi-ladder, while the cross-section ratio is defined as Jcost phi and placed in the interval (0.11, 0.13). Upstream definitions supply dmMassRatio := 1/45 (appearing in both the cosmology and physics modules) and dmCrossSectionRatio := Jcost phi, with the module documentation stating: 'From the RS dark matter module: m_DM / m_W = 1/45, predicting m_DM ∈ (1.77, 1.79) GeV. The predicted cross-section band = J(φ) ∈ (0.11, 0.13).'
proof idea
The declaration is a structure definition with three fields and no proof body. No lemmas or tactics are invoked inside the structure itself. The fields receive their values downstream via the reflexivity proof for the mass-ratio equality and via the positivity and band lemmas dmCrossSection_pos and dmCrossSection_in_band.
why it matters
This structure is instantiated by the downstream definition darkMatterXENONCert, supplying a Lean witness for the XENON prediction. It connects the phi-ladder mass formula (T6 self-similar fixed point, T8 D=3) to direct-detection cosmology and realizes the J(φ) cross-section band required by the Recognition Composition Law. The module documentation notes that current XENONnT exclusion limits remain above the predicted band, leaving the RS value testable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.