Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitMulBalancedZeroOfBalancedZeroRightChoiceFree

show as:
view Lean formalization →

Module for a choice-free identity: if a right-hand signed orbit is balanced at zero, its product with any left signed orbit is again balanced at zero. It sits in the primitive recognition calculus grow layer, next to ratio-orbit order. Anyone building multiplicative structure on signed orbits without classical choice would cite it. The argument is a short algebraic reduction from orbit and integer-order primitives.

claimIn the signed-orbit monoid of the primitive recognition calculus, if the right factor $s$ is balanced at zero, then for every left factor $r$ the product $r \cdot s$ is balanced at zero. The proof is choice-free (no appeal to excluded middle or choice on orbit representatives).

background

Primitive recognition calculus builds rationals and order from orbits of distinctions rather than from classical $\mathbb{Z}$ and $\mathbb{Q}$. An orbit packages a positive distinction count; a signed orbit adds a sign so that additive and multiplicative structure can be stated before integers are fully constructed.

Balanced zero is the recognition-native notion of the zero class: opposing signed contributions cancel, so the signed orbit is indistinguishable from the zero orbit. The grow layer develops how these objects multiply and how order interacts with that multiplication.

Upstream, RatioOrbitLeReflTotal supplies cross-multiplication order on ratio orbits: $p \le q$ iff the signed orbit $p.\mathrm{num}\cdot q.\mathrm{den}$ is $\le$ $q.\mathrm{num}\cdot p.\mathrm{den}$, with positive denominators cast via SignedOrbit.ofOrbit. Integer-order and integer-rational modules supply the comparison and cancellation lemmas used when products hit zero.

proof idea

The module is organized around one main lemma (the choice-free right-balanced-zero product rule). It reduces the claim to the definitions of signed-orbit multiplication and balanced zero, then applies integer-order facts about multiplying by zero on the right and the orbit casting maps. No case splits that would require choice on representatives; the reduction stays inside the constructive fragment already available from Orbit, IntegerOrder, and IntegerRational.

why it matters in Recognition Science

Multiplicative cancellation and order on ratio orbits need a clean zero law for signed products. Without a choice-free right-zero rule, later grow lemmas about ratio comparison and ladder arithmetic would either admit classical gaps or repeat the same cancellation argument. This module isolates that lemma so the rest of the foundation can treat "right factor balanced zero implies product balanced zero" as a named fact. No downstream edges are recorded yet; the natural consumers are further Grow lemmas on ratio-orbit order and any forcing-chain scaffolding that multiplies signed defects before T5–T8 specialize $J$, $\varphi$, and dimension.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (1)