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 under balanced multiplication: if two signed orbits compare and a third factor is balanced, left-multiplying preserves the inequality. Ratio-orbit and product-factor lemmas in the Grow stack cite this. The argument routes through the choice-free order foundation rather than the classical integer display.

claimFor signed orbits $x,y,z$ under the choice-free order, if $z$ is balanced and $x \le y$, then $z \cdot x \le z \cdot y$. The comparison is the native signed-orbit order, not the classical $\mathbb{Z}$ display.

background

Primitive Recognition Calculus builds integers and rationals from orbits of distinctions, then equips them with an order. SignedOrbit is the signed version of a positive orbit; the classical path compares via toInt : SignedOrbit → ℤ and Mathlib's integer order, which pulls in Classical.choice.

The sibling module SignedOrbitOrderChoiceFree rebuilds nonnegativity and $\le$ without that display, so downstream rungs need not inherit choice taint. RatioOrbitLeReflTotal defines cross-multiplication order on ratio orbits: $p \le_Q q$ iff the signed product $p.num \cdot q.den$ is $\le$ $q.num \cdot p.den$ after casting dens via SignedOrbit.ofOrbit.

This module sits in that choice-free Grow layer: left-multiplication congruence of signed-orbit $\le$ when the left factor is balanced.

proof idea

The module exposes a single main lemma (left-congruence under a balanced factor) on top of the choice-free signed-orbit order and the integer/orbit infrastructure. It applies the choice-free order primitives rather than le_iff_toInt_le, so the congruence stays choice-free. Structure is a thin algebraic step: reduce the multiplied comparison to the underlying order axioms and the balanced-factor hypothesis, then discharge with the imported order lemmas.

why it matters in Recognition Science

Left-congruence is the missing half of two-sided order compatibility for signed orbits. Downstream, SignedOrbitLeCongrOfBalancedChoiceFree imports this module to assemble full congruence, and SignedOrbitLeProductRightFactorIffOfBalancedChoiceFree uses it for product right-factor characterizations of $\le$.

In the Recognition stack this keeps ratio-orbit inequalities and later forcing-chain arithmetic off the classical $\mathbb{Z}$ display. Without a choice-free left-congruence step, every product and ratio comparison would reintroduce choice through toInt.

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)