no_dm_rung
plain-language theorem explainer
The declaration states that every integer rung index r with 15 ≤ r ≤ 25 equals one of the values 15 through 25. Cosmologists using the Recognition Science framework to model dark matter as topological frustration cite it when excluding discrete WIMP candidates on the φ-ladder at 10 GeV–10 TeV scales. The proof is a one-line wrapper applying the omega tactic to the integer bounds.
Claim. For every integer $r$, if $15 ≤ r ≤ 25$, then $r = 15 ∨ r = 16 ∨ ⋯ ∨ r = 25$.
background
The φ-ladder assigns masses by the formula yardstick ⋅ φ^(rung − 8 + gap(Z)). The module treats dark matter as nonzero Betti-1 homology on the parity bundle in the ℤ³ carrier, arising from accumulated Berry phase Z ≠ 0. This theorem supports the local claim that the φ-ladder contains no rung for a discrete dark-matter particle at WIMP scales.
proof idea
The proof is a one-line wrapper that applies the omega tactic to discharge the integer linear-arithmetic statement 15 ≤ r ≤ 25.
why it matters
The result supports dm_not_particle, the assertion that no φ-ladder rung exists for a discrete dark-matter particle. It fills the step that constrains the falsifier of the module hypothesis: detection of a new rung at WIMP scales. The construction aligns with T5 J-uniqueness and the phi-ladder mass formula in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.