Pith. sign in
module module high

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal

show as:
view Lean formalization →

Defines the cross-multiplication order on ratio orbits: p is at most q when the signed orbit of p.num times q.den is at most that of q.num times p.den. Supplies reflexivity and totality for that relation. Downstream order modules (transitivity, trichotomy, monotonicity) import it as the base comparison. Arguments stay choice-free by routing through the purified signed-orbit order bridge.

claimOn ratio orbits, define $p \le_Q q$ if and only if the signed orbit of $p_{\mathrm{num}}\cdot q_{\mathrm{den}}$ is $\le$ the signed orbit of $q_{\mathrm{num}}\cdot p_{\mathrm{den}}$, with positive denominators embedded via the signed-orbit-of-orbit map. Then $\le_Q$ is reflexive and total.

background

Ratio orbits are the primitive rational-like objects in the recognition calculus: pairs of an integer-like numerator orbit and a positive denominator orbit. Ordering them by cross-multiplication is the standard schoolbook rule for fractions, lifted to the orbit setting so that no classical choice is smuggled in through Mathlib integers.

Signed orbits carry a choice-free order foundation. The upstream module notes that the older characterization routed through toInt and Mathlib's $\mathbb{Z}$ order, which carries classical choice; every downstream rung would inherit that taint. Positive denominators are cast into signed orbits so the two cross products live in the same ordered type.

This module sits in the Grow layer of PrimitiveRecognitionCalculus: it only introduces the comparison and the two structural facts (reflexivity, totality) needed before denseness, negation, and algebraic monotonicity can be stated.

proof idea

The module is definition-plus-two-lemmas, not a long development. The relation is the cross-product comparison of signed orbits after embedding denominators. Reflexivity is immediate: both cross products coincide, so the signed-orbit order's reflexivity applies. Totality follows from totality of the underlying signed-orbit order on the two cross products. No cancellation or mediant arithmetic appears here; those live in sibling Grow modules.

why it matters in Recognition Science

This is the base order rung for ratio orbits. Downstream imports include density via mediants, order under negation, transitivity and antisymmetry, strict-order trichotomy, positivity of products, and add/mul monotonicity. The transitivity module explicitly calls the relation the delta-native cross-multiplication order and stresses the choice-free bridge. Without reflexivity and totality here, the later total-order and ordered-semiring facts on ratio orbits cannot start. In the broader Recognition stack this keeps rational comparison inside the constructive foundation rather than leaning on classical $\mathbb{Q}$.

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)