IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeNeg
Module for the interaction of the cross-multiplication order leQ on ratio orbits with sign flip of both arguments. It records that negating both orbits reverses the comparison in the expected way (double negation restores the original inequality). Anyone building ordered arithmetic on RatioOrbit cites this when moving inequalities across negatives. The argument is a short reduction to the already-total reflexive order and integer order facts.
claimOn ratio orbits equipped with the cross-multiplication order $\mathrm{leQ}$, one has $\mathrm{leQ}(-p)(-q)$ if and only if $\mathrm{leQ}\, q\, p$. Equivalently, simultaneous sign flip of both arguments reverses the inequality, and applying the flip twice recovers the original comparison.
background
In the primitive recognition calculus, rational comparisons are not taken as a black-box field order. A ratio orbit packages a signed numerator orbit with a positive denominator distinction. The order $\mathrm{leQ}$ on such pairs is defined by cross-multiplication: $\mathrm{leQ}, p, q$ means the signed product $p.\mathrm{num}\cdot q.\mathrm{den}$ is at most $q.\mathrm{num}\cdot p.\mathrm{den}$ after denominators are cast into signed orbits.
The parent module RatioOrbitLeReflTotal installs that this relation is a reflexive total preorder-style comparison on orbits. IntegerOrder and IntegerRational supply the underlying signed-integer comparison and the rational packaging. The present module sits one layer above that: it treats how $\mathrm{leQ}$ behaves when both arguments are replaced by their additive inverses, which is the elementary sign rule needed before one can talk about negative rungs or oriented growth steps on the orbit lattice.
proof idea
Not a pure definition dump: the module's main content is the biconditional relating $\mathrm{leQ}(-p)(-q)$ to $\mathrm{leQ}, q, p$. The proof expands both sides via the cross-multiplication definition, pushes the two minuses through the signed products (using integer negation and order lemmas from IntegerOrder), and matches the resulting inequalities. Totality and reflexivity of $\mathrm{leQ}$ from RatioOrbitLeReflTotal are available as ambient facts but are not the main work; the work is the sign bookkeeping on numerators and the positive denominators under $\mathrm{SignedOrbit.ofOrbit}$.
why it matters in Recognition Science
Ordered growth on ratio orbits is part of the foundation layer that later supports self-similar scaling and the phi-ladder comparisons in Recognition Science. Without a clean rule for how $\mathrm{leQ}$ interacts with double negation, inequalities cannot be moved across negative orbits when one orients distinctions or compares reciprocal rungs.
No downstream consumers are wired in the current graph snapshot (used_by is empty), so this module is presently a leaf that closes a local algebraic obligation rather than a direct cite target of a named forcing-chain theorem. Its natural parents are further Grow lemmas that combine $\mathrm{leQ}$ with multiplication, inversion, or rung shifts; those will need the negation biconditional as a one-line rewrite. Relative to the forcing chain, this is pre-T5 scaffolding: pure ordered arithmetic on the recognition rationals, not yet J-cost uniqueness or dimensional forcing.
scope and limits
- Does not define leQ itself; that lives in RatioOrbitLeReflTotal.
- Does not prove trichotomy, antisymmetry, or compatibility of leQ with multiplication.
- Does not treat single-argument negation (leQ (-p) q) beyond what double negation implies.
- Does not connect ratio-orbit order to J-cost, phi, or the T5–T8 forcing chain.
- Does not claim any downstream theorem currently imports this module.