Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitMulPos

show as:
view Lean formalization →

Choice-free lemmas on how positive multiplication interacts with the cross-multiplication order on ratio orbits. Establishes that multiplying by a strictly positive ratio preserves strict inequality, and that positivity of a ratio is equivalent to positivity of its numerator orbit. Cited by anyone building ordered-field structure on the primitive recognition calculus without Classical.choice.

claimOn ratio orbits equipped with the cross-multiplication order $\le_Q$ and strict order $<_Q$: (i) a ratio $q$ satisfies $0 <_Q q$ if and only if its numerator signed orbit is strictly positive; (ii) if $r$ is strictly positive, then $p <_Q q$ implies $p\cdot r <_Q q\cdot r$ (and the corresponding non-strict form).

background

In the primitive recognition calculus, integers and rationals are rebuilt from orbits of distinctions rather than from Mathlib's $\mathbb{Z}$ and $\mathbb{Q}$. A ratio orbit is a pair of a signed numerator orbit and a positive denominator orbit. Order on ratios is defined by cross-multiplication: $p \le_Q q$ means the signed orbit $p_{\mathrm{num}}\cdot q_{\mathrm{den}}$ is at most $q_{\mathrm{num}}\cdot p_{\mathrm{den}}$, with denominators cast via SignedOrbit.ofOrbit.

The upstream choice-free signed-orbit order module removes dependence on Mathlib's $\mathbb{Z}$ order (and thus on Classical.choice). Reflexivity/totality of $\le_Q$ and trichotomy for $<_Q$ are already available from sibling Grow modules. This module sits on top of that ordered skeleton and treats the multiplicative action of positive ratios.

proof idea

Three tightly related results. Positivity of a ratio is reduced to positivity of its numerator by unfolding $\le_Q$ against the zero ratio and using the signed-orbit order characterizations. Strict-positivity of a multiplier is then fed into the cross-multiplication comparison: multiplying both sides of an orbit inequality by a positive denominator/numerator pair preserves the signed-orbit order, which translates back into $<_Q$ (or $\le_Q$) on the products. The choice-free path is kept by routing only through the signed-orbit order API, not through toInt.

why it matters in Recognition Science

Ordered multiplication by positives is the missing rung between a pure order on ratio orbits and a genuine ordered semifield/field structure in the recognition foundation. Without it one cannot scale inequalities, clear denominators, or compare costs along the phi-ladder in a choice-free way. Downstream work that builds monotonicity of recognition cost, defect distances, or rung comparisons on rational parameters depends on these facts even though this module currently has no recorded used-by edges in the graph. It continues the program begun in the choice-free signed-orbit order foundation: every order fact about ratios should be free of classical choice taint inherited from Mathlib integers.

scope and limits

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (3)