Pith. sign in
module module high

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal

show as:
view Lean formalization →

Defines the cross-multiplication preorder leQ on ratio orbits: p ≤ q when the signed product p.num·q.den is at most q.num·p.den after casting positive denominators into signed orbits. Proves reflexivity and totality of that relation. Downstream Grow modules cite it as the base order before transitivity, trichotomy, and monotonicity. The argument routes through the choice-free signed-orbit order bridge rather than classical ℤ.

claimOn ratio orbits, write $p \le_Q q$ iff the signed orbit $p_{\mathrm{num}}\cdot q_{\mathrm{den}}$ is $\le$ the signed orbit $q_{\mathrm{num}}\cdot p_{\mathrm{den}}$, with positive denominators embedded by the signed-orbit-of-orbit map. The relation $\le_Q$ is reflexive and total.

background

In the Primitive Recognition Calculus, orbits are the positive integer-like distinctions, and ratio orbits package a signed numerator with a positive denominator orbit, playing the role of rationals before a classical field is assumed. Ordering those ratios by cross-multiplication is the standard schoolbook move: compare $a/b$ and $c/d$ by comparing $ad$ and $bc$, here lifted to signed orbits.

The upstream module SignedOrbitOrderChoiceFree exists because the earlier signed-orbit order was characterized only through a verifier display into Mathlib integers, which imports classical choice. That taint would infect every ratio-order lemma. The purified bridge gives a choice-free $\le$ on signed orbits, so the ratio layer can stay constructive.

This module sits in the Grow stack: it only introduces the relation and the two structural facts (reflexivity, totality) needed before denseness, negation, and algebraic monotonicity.

proof idea

Definition module plus two short structural theorems. The relation leQ is defined by comparing the two cross products in the signed-orbit order after casting denominators with ofOrbit. Reflexivity is immediate: both sides become the same signed product, so signed-orbit reflexivity applies. Totality follows from totality of the underlying signed-orbit order on the two cross products. No deep arithmetic cancellation is needed here; that appears in the transitivity and trichotomy modules that import this one.

why it matters in Recognition Science

This is the base rung of the choice-free ratio-orbit order. Downstream modules import it for denseness via mediants, negation compatibility, transitivity and antisymmetry (which multiply through by positive outer denominators and cancel the shared middle denominator), strict-order trichotomy, positivity of products, and add/mul monotonicity. Without a clean leQ, the later constructive comparison theory of recognition ratios cannot start. In the broader Recognition foundation it supplies the ordered-rational skeleton on which ladder comparisons and forcing-chain arithmetic eventually rest, while keeping Classical.choice out of the order core.

scope and limits

used by (17)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (3)