same_strict_sign_of_pos_mul
plain-language theorem explainer
If a product of two reals is strictly positive, the factors share a strict sign: both positive or both negative. Orientation and thrackle arguments in the distance-shell module cite this scalar fact when converting a positive product of orientations into a same-side alternative. The proof is a three-way trichotomy on the first factor, with the zero case ruled out by the product hypothesis and the opposite-sign cases killed by nonpositive-product lemmas plus linarith.
Claim. For real numbers $x,y$, if $0 < xy$, then either $0 < x$ and $0 < y$, or $x < 0$ and $y < 0$.
background
The module Distance Shell Multiplicity records the Recognition Science physicalization of Erdős problem #132: classical pairwise distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count.
In the plane geometry layer, side-of-line tests are encoded by the scalar orientation orient2. Same-side and proper-separation statements are phrased as strict inequalities on products of orientations. The elementary real-arithmetic fact needed is that a strictly positive product forces matching strict signs.
No Recognition-specific cost or ladder structure enters here; the lemma is pure ordered-field arithmetic over $\mathbb{R}$, used as a bridge into geometric disjointness of segments.
proof idea
Case-split on the trichotomy of $x$ relative to $0$.
If $x < 0$, take the right disjunct and show $y < 0$ by contradiction: a nonnegative $y$ would make $xy \le 0$ via the nonpositive-times-nonnegative product lemma, contradicting $0 < xy$ by linarith.
If $x = 0$, substitute and simplify the hypothesis to false.
If $0 < x$, take the left disjunct and symmetrically force $0 < y$: a nonpositive $y$ would again make $xy \le 0$, contradicting the hypothesis.
why it matters
This is the scalar sign engine behind the module's separation lemmas. Downstream, same_side_segments_disjoint applies it (via a positive product of orientations) to prove that a segment joining two same-side points cannot meet the supporting segment: the core separation fact for thrackle and matching arguments. proper_segment_separation_signs unpacks proper separation into same-side alternatives on both supporting lines, again relying on matching strict signs.
In the broader RS reading of Erdős #132, these geometric disjointness facts control shell occupancy and sparse-shell divergence. The lemma itself is classical real arithmetic; its place in the framework is as infrastructure for the ordered-distance spectrum and diameter-shell uniqueness developed in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.