IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitMulBalancedZeroOfBalancedZeroRightChoiceFree
Module for a choice-free right-factor lemma: if a signed orbit factor is balanced zero, the product signed orbit is balanced zero. It sits in the primitive recognition calculus grow layer, above integer rationals, integer order, orbits, and the cross-multiplication order on ratio orbits. Researchers building constructive arithmetic of signed distinctions would cite it. The argument is a direct algebraic reduction from the balanced-zero and multiplication interfaces, without classical choice.
claimIn the signed-orbit calculus, if the right factor $b$ is balanced zero, then the product signed orbit $a \cdot b$ is balanced zero. The proof is choice-free (no appeal to classical choice on the right factor).
background
Primitive recognition calculus treats positive distinctions as orbits and extends them to signed orbits so that integer-like arithmetic and order can be stated before full rationals. Balanced zero is the neutral signed distinction that behaves as additive identity in this calculus.
Multiplication of signed orbits must preserve that neutrality on either side. This module isolates the right-factor case and insists on a choice-free construction, matching the constructive stance of the surrounding grow layer.
It imports integer rationals and integer order for the underlying arithmetic, the orbit API, and RatioOrbitLeReflTotal, whose cross-multiplication order says leQ p q iff the signed orbit $p.\mathrm{num}\cdot q.\mathrm{den}$ is $\le$ $q.\mathrm{num}\cdot p.\mathrm{den}$ after casting positive dens via SignedOrbit.ofOrbit.
proof idea
The module exposes a single main lemma (sibling mul_balanced_zero_of_balanced_zero_right_cf). Structure is a direct reduction: unfold signed-orbit multiplication and the balanced-zero predicate on the right factor, then rewrite the product to the zero representative using the integer/orbit multiplication laws already available from the imported integer-rational and orbit modules. No case splits that would require choice on the right factor; the right-neutrality hypothesis discharges the product identity constructively.
why it matters in Recognition Science
Choice-free right absorption of balanced zero is a small but necessary brick in the grow layer of primitive recognition calculus: signed-orbit arithmetic must stay constructive while supporting ratio-orbit comparison and later forcing-chain infrastructure. Downstream use is not yet wired in this graph snapshot (used_by empty), but the lemma is the natural right-hand companion to any left-factor balanced-zero absorption and feeds any development that multiplies signed distinctions under a zero hypothesis without classical choice. It keeps the foundation aligned with the Recognition program's preference for explicit, choice-free algebraic steps before continuum or measure structure appears.
scope and limits
- Does not prove the left-factor balanced-zero absorption lemma.
- Does not define balanced zero, signed-orbit multiplication, or orbits themselves.
- Does not establish order properties of ratio orbits beyond what imports already give.
- Does not claim classical uniqueness results that would require choice.
- Does not yet show downstream consumers in the supplied used-by graph.
depends on (4)
-
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit