long_not_short
plain-language theorem explainer
No real duration x can satisfy both x > 2 and x < 2, which enforces mutual exclusivity between long and short gamma-ray burst classes. Researchers classifying GRB populations or deriving statistical distributions in Recognition Science models would cite the result to justify treating the categories as disjoint. The proof is a one-line term that applies linear arithmetic to derive an immediate contradiction from the incompatible strict inequalities.
Claim. There exists no real number $x$ such that $2 < x$ and $x < 2$.
background
Gamma-ray bursts are partitioned by observed duration in seconds, with the conventional boundary at 2 s separating long bursts (typically >2 s) from short bursts (<2 s) in the Recognition Science treatment given in RS_Gamma_Ray_Bursts.tex. The module imports Mathlib for real arithmetic and JcostCore for cost functions, yet this declaration uses only the ordered field structure of the reals. No upstream lemmas are invoked; the result stands on the irreflexivity and transitivity of the strict order on ℝ.
proof idea
The declaration is a one-line term proof that invokes the linarith tactic. The tactic receives the two contradictory hypotheses 2 < x and x < 2 and automatically produces a contradiction by linear combination of the inequalities.
why it matters
The theorem supplies the disjointness property required for GRB class separation inside the Recognition Science gamma-ray burst module. It supports sibling results such as classes_disjoint, grb_energy, and typical_grb_in_range by guaranteeing that no single burst can be assigned to both populations. The placement in the RS_Gamma_Ray_Bursts.tex paper aligns with the broader framework use of the phi-ladder and eight-tick octave for scaling burst observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.