Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeCongrLeftOfBalancedChoiceFree

show as:
view Lean formalization →

Choice-free left-congruence for the signed-orbit order: multiplying both sides on the left by a balanced signed orbit preserves ≤. Order theorists building ratio-orbit comparison without Classical.choice would cite it. The module packages the left-factor case that later full congruence and product-factor lemmas import.

claimIn the choice-free signed-orbit order, if $a$ is balanced and $x \le y$, then $a\cdot x \le a\cdot y$. Equivalently, left multiplication by a balanced signed orbit is order-preserving on signed orbits, without routing through $\mathbb{Z}$ and classical choice.

background

Primitive Recognition Calculus builds rationals from orbits of positive distinctions and signed orbits that carry a sign bit. The usual order on SignedOrbit is pinned to Mathlib integers via a display map toInt, so every comparison inherits Classical.choice. The choice-free order stack (see SignedOrbitOrderChoiceFree) rebuilds nonnegativity and ≤ from native signed-orbit data so downstream rungs stay constructive.

Ratio comparison uses cross-multiplication: leQ p q holds when the signed orbit $p.\mathrm{num}\cdot q.\mathrm{den}$ is ≤ $q.\mathrm{num}\cdot p.\mathrm{den}$, dens cast in via SignedOrbit.ofOrbit. "Balanced" is the side condition that lets multiplication interact cleanly with that order (sign and magnitude aligned so left factors do not flip inequalities).

This module sits in the Grow layer: it takes the choice-free order and the ratio-orbit ≤ infrastructure and isolates the left-congruence law under that balanced hypothesis.

proof idea

Not a definition-only file: it exposes the main lemma le_congr_left_of_balanced_cf. The argument is the left-factor half of order congruence: reduce $a\cdot x \le a\cdot y$ to the choice-free comparison primitives from SignedOrbitOrderChoiceFree, using integer/orbit algebra from IntegerOrder, IntegerRational, and Orbit, and the total reflexive ratio order from RatioOrbitLeReflTotal where cross-multiplication form is needed. No classical toInt bridge; balance of $a$ discharges the sign cases that would otherwise reverse the inequality.

why it matters in Recognition Science

Left congruence is the first half of making signed-orbit ≤ a monoid-compatible order in the choice-free stack. Downstream, SignedOrbitLeCongrOfBalancedChoiceFree imports this module to assemble full congruence (both sides), and SignedOrbitLeProductRightFactorIffOfBalancedChoiceFree uses it for product right-factor characterizations of ≤. Those rungs are what keep ratio-orbit comparison and later recognition-calculus inequalities free of choice taint inherited from Mathlib $\mathbb{Z}$. In the broader foundation, this is infrastructure under the forcing chain's discrete arithmetic, not a T5–T8 landmark itself.

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)