Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitOrderAddMono

show as:
view Lean formalization →

Choice-free bridge from the cross-multiplication order on ratio orbits to the integer display, plus right-addition monotonicity of that order. Anyone building ordered arithmetic on RatioOrbit without Classical.choice cites this. The module unfolds toInt as a pos/neg Nat-cast difference and transfers inequalities through that display.

claimOn ratio orbits, the cross-multiplication order $p \le_Q q$ is equivalent (choice-free) to the integer comparison of their displays, and is monotone under right addition: $p \le_Q q$ implies $p+r \le_Q q+r$. The integer display of a signed orbit unfolds as the difference of its positive and negative Nat-casts.

background

Primitive Recognition Calculus builds rationals from orbits of distinctions rather than from Mathlib's $\mathbb{Q}$. A RatioOrbit is a signed numerator orbit over a positive denominator orbit. The order leQ is defined by cross-multiplication: $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 dens cast in via SignedOrbit.ofOrbit.

The ambient signed-orbit order was originally routed through SignedOrbit.toInt : SignedOrbit \to \mathbb{Z}$ and Mathlib's $\mathbb{Z}$ order, which carries Classical.choice. The upstream module SignedOrbitOrderChoiceFreeremoves that taint so downstream rungs (reflexivity, totality, and now add-monotonicity) need not inherit it.IntegerRationalandIntegerOrder` supply the underlying signed-orbit and integer-order primitives.

proof idea

Three coordinated pieces. First, toInt_eq unfolds the integer display of a signed orbit as the difference of its positive and negative Nat-casts, without invoking choice. Second, le_iff_toInt_le_cf rephrases the signed-orbit (and hence ratio-orbit) order as comparison of those displays, choice-free. Third, leQ_add_right lifts right-addition monotonicity through the cross-multiplication characterization, using the choice-free comparison and the integer-order facts from the imports. The module is a thin Grow-layer assembly over RatioOrbitLeReflTotal and SignedOrbitOrderChoiceFree.

why it matters in Recognition Science

Ordered addition on ratio orbits is a prerequisite for any Recognition-native arithmetic that treats cost comparisons, rung gaps, or mass-ladder inequalities as order statements rather than ad-hoc $\mathbb{Z}$ facts. By keeping the bridge choice-free, the module protects the forcing chain's constructive character at the rational layer: later rungs that need $p \le_Q q \Rightarrow p+r \le_Q q+r$ can cite this without reintroducing classical choice into the Foundation stack. No downstream edges are recorded yet; the natural consumers are further Grow lemmas on ordered fields of ratio orbits and any cost or defect comparisons stated in leQ.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (3)