Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeCongrRightOfBalancedChoiceFree

show as:
view Lean formalization →

Choice-free right-congruence for the signed-orbit order: under a balanced multiplier, a ≤ b implies a·m ≤ b·m. Ratio-orbit and product-factor arguments cite it to move inequalities across right multiplication without Mathlib ℤ choice. The argument reduces to the choice-free nonnegativity and order API already built for signed orbits.

claimFor signed orbits $a,b$ and a balanced multiplier $m$, if $a \le b$ in the choice-free signed-orbit order, then $a \cdot m \le b \cdot m$. The order is the constructive one on signed orbits (not the classical $\mathbb{Z}$ display).

background

Primitive Recognition Calculus builds rationals and order from orbits of distinctions rather than from Mathlib integers. A signed orbit packages a sign with a positive orbit; the classical path orders them by toInt : SignedOrbit → ℤ, which imports Classical.choice. The sibling module SignedOrbitOrderChoiceFree replaces that path with a choice-free order and nonnegativity API so later rungs stay constructive.

Ratio orbits compare by cross-multiplication: leQ p q means the signed orbit $p.num \cdot q.den$ is ≤ $q.num \cdot p.den$ after casting dens via SignedOrbit.ofOrbit. Right-congruence (multiply both sides by the same balanced factor and preserve ≤) is the algebraic step that lets product and ratio lemmas rearrange inequalities without leaving the choice-free fragment.

This module sits in the Grow layer: integer/rational scaffolding, orbit algebra, the choice-free signed order, and the total reflexive ratio order are imported; the local goal is the right-hand congruence law under a balanced multiplier.

proof idea

Definition-plus-lemma module centered on le_congr_right_of_balanced_cf. It applies the choice-free signed-orbit order API (nonnegativity and ≤ characterizations that avoid toInt) together with orbit multiplication and the balanced-multiplier hypothesis, reducing right-congruence to already-proved order facts on signed orbits and the ratio-orbit cross-multiply setup. No classical ℤ comparison is invoked.

why it matters in Recognition Science

Feeds the two immediate parents SignedOrbitLeCongrOfBalancedChoiceFree (two-sided congruence package) and SignedOrbitLeOfProductRightFactorIffOfBalancedChoiceFree (product right-factor iff form). Those close the constructive order rung needed for ratio-orbit inequalities without choice taint inherited from Mathlib ℤ. In the broader foundation, this keeps the Primitive Recognition Calculus path to ordered rationals aligned with the choice-free forcing style used upstream of the T0–T8 chain, rather than smuggling classical order into early arithmetic.

scope and limits

used by (2)

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

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (1)