Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeMulRightIffOfNonnegFlagOfNotBalancedZeroChoiceFree

show as:
view Lean formalization →

Choice-free right-multiplication criterion for the signed-orbit order: under a nonnegative flag and away from the balanced-zero case, an inequality of signed orbits is equivalent to the same inequality after multiplying the right factor. Anyone building ratio or cross-multiplication order on orbits without Classical.choice would cite it. The module packages the cross-le bridge and the main iff as two sibling lemmas over the choice-free order foundation.

claimOn signed orbits, if the right factor carries a true nonnegative flag and the configuration is not the balanced-zero case, then $a \le b\cdot c$ if and only if the corresponding cross-multiplied (or right-multiplied) comparison holds in the choice-free signed-orbit order. A companion statement equates the ratio-orbit cross order $p \le_Q q$ with the signed cross product comparison of numerators and denominators.

background

Primitive recognition calculus builds integers and rationals from orbits of distinctions rather than from Mathlib's $\mathbb{Z}$. A signed orbit is an orbit equipped with a sign; nonnegative status is tracked by an explicit nonnegFlag rather than by a classical comparison of integer displays.

The parent choice-free order module records that the older route le_iff_toInt_le / nonneg_iff_toInt_nonneg funnels through SignedOrbit.toInt and Mathlib's ordered integers, which import Classical.choice. Downstream rungs such as ratio reflexivity therefore inherit choice they do not need.

Ratio orbits carry a cross-multiplication order: leQ p q means the signed orbit $p.\mathrm{num}\cdot q.\mathrm{den}$ is $\le$ the signed orbit $q.\mathrm{num}\cdot p.\mathrm{den}$, with positive denominators cast in via SignedOrbit.ofOrbit. This module sits on that cross order and on the choice-free signed order, plus ordinary orbit arithmetic.

proof idea

Two sibling declarations. cross_le_iff is the bridge that rewrites the ratio-orbit cross order as a signed-orbit inequality of cross products, using the imported ratio and signed-order infrastructure. le_mul_right_iff_of_nonnegFlag_of_not_balanced_zero_cf is the main algebraic iff: under the nonnegative-flag hypothesis on the multiplier and exclusion of the balanced-zero configuration, right multiplication preserves and reflects the choice-free signed order. The argument is equational and flag-case analysis; it does not route through toInt or classical integer order.

why it matters in Recognition Science

Recognition Science's foundation layer aims to derive discrete structure (eight-tick octave, forcing chain T0–T8) from recognition cost without smuggling classical choice into elementary order facts. This module closes a concrete gap: right-multiplication monotonicity for signed orbits in the choice-free regime, which is the arithmetic step needed to keep ratio-orbit comparisons clean.

It feeds any later development that multiplies or clears denominators in orbit rationals while staying inside the choice-free signed order (the Grow stack that begins from SignedOrbitOrderChoiceFree and RatioOrbitLeReflTotal). No downstream used-by edges are recorded yet; the module is infrastructure for those rungs rather than a leaf physics claim. It does not itself force $\varphi$, $D=3$, or the J-cost uniqueness theorems.

scope and limits

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (2)