classes_disjoint
plain-language theorem explainer
classes_disjoint shows that a real parameter x satisfying both the long GRB threshold (x at least 2) and the short GRB threshold (x at most 2) must equal exactly 2. GRB modelers working in Recognition Science would cite the result to confirm the two duration classes touch only at their shared boundary. The argument is a direct one-line application of order antisymmetry to the pair of inequalities.
Claim. If a real number $x$ satisfies $2 ≤ x$ and $x ≤ 2$, then $x = 2$.
background
The module derives gamma-ray burst observables from Recognition Science, following the outline in the paper RS_Gamma_Ray_Bursts.tex. The local result uses the order relation on the reals to separate long and short burst classes at the conventional division point of 2. It rests on the upstream lemma le_antisymm from ArithmeticFromLogic, whose statement is: if a ≤ b and b ≤ a then a = b (proved there by reducing to the underlying LogicNat representation and applying congruence on the toNat embedding).
proof idea
The proof is a one-line wrapper that applies the le_antisymm lemma directly to the hypotheses hlong and hshort.
why it matters
The declaration supplies a basic disjointness check for the long/short GRB classification inside the Recognition Science treatment of gamma-ray bursts. It supports the energy and Lorentz-factor calculations appearing in sibling declarations such as grb_energy and lorentz_factor. No downstream uses are recorded, indicating the result functions as an internal consistency step rather than a high-level theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.