Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeCongrOfBalancedChoiceFree

show as:
view Lean formalization →

Packages two-sided order congruence for signed orbits under a balanced, choice-free hypothesis: if two signed orbits are related by a balanced scaling, the cross-multiplication order is preserved on both sides. Anyone building the rational order on ratio orbits from primitive recognition data cites this. The argument glues the already-proved left and right congruence lemmas.

claimIf signed orbits $a,b,c$ satisfy a balanced choice-free relation (equal absolute scale on the free factor), then $a \le b$ if and only if $c\cdot a \le c\cdot b$ and $a\cdot c \le b\cdot c$ in the signed-orbit order. Equivalently, the cross-multiplication order $\mathrm{leQ}$ on ratio orbits is invariant under balanced left/right multiplications.

background

Primitive Recognition Calculus builds integers, rationals, and their order from orbits of distinctions rather than from classical $\mathbb{Z}$ and $\mathbb{Q}$. An orbit is a positive distinction class; a signed orbit adjoins a sign so that numerators can cancel. The module sits in the Grow layer that lifts these objects toward a total order on ratios.

The ambient order on ratio orbits is the cross-multiplication relation $\mathrm{leQ}$: $p \le q$ means the signed product $p.\mathrm{num}\cdot q.\mathrm{den}$ is at most $q.\mathrm{num}\cdot p.\mathrm{den}$, with positive denominators injected via $\mathrm{SignedOrbit.ofOrbit}$. Integer order and integer-rational scaffolding supply the underlying $\le$ on signed products.

"Balanced choice-free" means the free multiplicative factor used in a congruence has matching absolute scale on both sides, so no classical choice of representatives is required. Separate upstream modules already prove left-only and right-only congruence; this file unifies them.

proof idea

Definition-and-glue module rather than a long tactic development. It imports the left congruence lemma and the right congruence lemma for signed-orbit $\le$ under the balanced choice-free hypothesis, together with the ratio-orbit order and the integer/orbit primitives those lemmas need. The exported statement le_congr_of_balanced_cf is the two-sided package: apply left congruence, apply right congruence, and combine. No new arithmetic is invented here beyond that pairing.

why it matters in Recognition Science

In the Recognition foundation, rational comparison must be forced from orbit data without smuggling classical choice or unbalanced scalings. Two-sided congruence is the algebraic step that lets $\mathrm{leQ}$ descend to a well-defined order on ratio classes and support later forcing-chain material (dimension, octave ticks, and cost calculus sit downstream of a clean rational order). Upstream left/right modules are incomplete for that purpose alone; this module is the join point. No downstream edges are recorded yet in the mirror graph, so its consumers are still local to the Grow/ratio-order development rather than named parent theorems in the forcing chain.

scope and limits

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (1)