IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitOrderMulNonneg
Choice-free nonnegativity for the cross-multiplication order leQ on ratio orbits: zero is at most r exactly when the numerator's signed-orbit integer is nonnegative. Also records right-multiplication monotonicity by a nonnegative factor. Foundation users building ordered arithmetic on RatioOrbit cite both facts. Arguments route through the signed-orbit integer bridge and the zero orbit's (0,1) presentation.
claimOn ratio orbits with the cross-multiplication order $\le_Q$, one has $0 \le_Q r$ if and only if the integer attached to the numerator signed orbit is $\ge 0$. Separately, if $0 \le_Q a$ then $b \le_Q c$ implies $b\cdot a \le_Q c\cdot a$.
background
This module sits in the primitive recognition calculus grow layer, where rational-like quantities are ratio orbits rather than classical fractions. The order $\le_Q$ is the cross-multiplication order from the upstream RatioOrbitLeReflTotal module: $p \le_Q q$ means the signed orbit $p.\mathrm{num}\cdot q.\mathrm{den}$ is $\le$ the signed orbit $q.\mathrm{num}\cdot p.\mathrm{den}$, with positive distinctions (denominators) cast in via $\mathrm{SignedOrbit.ofOrbit}$.
Nonnegativity is the special case against the zero orbit. The zero orbit has numerator integer $0$ and denominator $1$, so the comparison collapses to a pure statement about the numerator's signed-orbit integer. Integer order and integer-rational scaffolding supply the underlying $\le$ on those integers and the casting maps between orbits and signed orbits.
The module is choice-free: no classical trichotomy or excluded-middle on reals is assumed; everything is stated in the constructive signed-orbit language already used for $\le_Q$.
proof idea
Two sibling lemmas carry the content. The nonnegativity characterization specializes $\le_Q$ to the zero orbit, then applies the purified bridge $\mathrm{SignedOrbit.le_iff_toInt_le}$ so that the comparison becomes an ordinary integer inequality; the zero side is immediate from numerator $0$ and denominator $1$. Right-multiplication monotonicity for a nonnegative factor is the standard cross-multiplication algebra under the nonnegativity hypothesis, again reduced to signed-orbit integer inequalities via the same bridge and the integer-order facts imported from IntegerOrder.
why it matters in Recognition Science
Ordered multiplication and a clean nonnegativity test are prerequisites for any further growth, positivity, or comparison lemmas on ratio orbits inside the primitive recognition calculus. The module does not yet show direct downstream edges in the graph, but its siblings are the natural hooks for later work on monotone maps, cones, and ladder comparisons that feed the forcing chain's early arithmetic layer (before J-uniqueness and the phi fixed point). Without a choice-free $0 \le_Q r$ criterion, subsequent positivity arguments would have to re-open the cross-multiplication definition at every use site.
scope and limits
- Does not define leQ itself; that lives in RatioOrbitLeReflTotal.
- Does not prove full ordered-field axioms or totality beyond what upstream already gives.
- Does not address left-multiplication or mixed-sign factors.
- Does not connect yet to J-cost, phi-ladder, or physical constants.
- Does not claim classical real nonnegativity; only the ratio-orbit order.