Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitNonnegFlagMulOfOrbitRightOfNeZeroChoiceFree

show as:
view Lean formalization →

Choice-free lemma module for the nonnegativity flag of a signed orbit multiplied on the right by a nonzero positive orbit embedding. It isolates the algebraic fact that right-multiplication by `ofOrbit` of a nonzero orbit preserves the Boolean nonneg flag without routing through Mathlib integers. Downstream ratio-order and cross-multiplication arguments cite it to stay choice-free. The argument is a short case analysis on the signed-orbit constructors plus the choice-free order API.

claimFor a signed orbit $s$ and a nonzero positive orbit $o$, the Boolean nonnegativity flag of the product $s \cdot \iota(o)$ (right multiplication by the canonical embedding $\iota$ of positive orbits into signed orbits) is decided by a choice-free criterion, equivalent to the constructive nonnegativity predicate on signed orbits.

background

Primitive Recognition Calculus builds rationals from orbits of positive distinctions and signed orbits that carry an integer-like sign. Positive orbits embed into signed orbits via a canonical map (often written ofOrbit / $\iota$). Order and nonnegativity on signed orbits were originally characterized by display into Mathlib $\mathbb{Z}$ (toInt), which imports Classical.choice.

The parent package SignedOrbitOrderChoiceFree rebuilds the order foundation so that nonnegFlag, reflexivity, and related comparisons do not need that display. RatioOrbitLeReflTotal then defines cross-multiplication order on ratio orbits: $p \le q$ iff the signed product of numerator and opposite denominator is nonneg in that choice-free sense.

This module sits between those layers. It records the multiplicative interaction of the nonneg flag with right-multiplication by a nonzero embedded positive orbit, which is the elementary step needed when clearing denominators or comparing cross-multiples without choice.

proof idea

Definition-plus-lemma module, not a large development. It exposes one main choice-free statement (sibling nonnegFlag_mul_ofOrbit_right_of_ne_zero_cf) built from the signed-orbit order API in SignedOrbitOrderChoiceFree and the orbit/integer scaffolding in Orbit, IntegerRational, and IntegerOrder.

The proof pattern is constructor case-split on the signed orbit, use that the embedded positive orbit is nonzero, and reduce the flag of the product to the flag of the original signed factor via the choice-free nonneg characterizations (avoiding toInt and Mathlib $\mathbb{Z}$ order). Imports from RatioOrbitLeReflTotal supply the ambient ratio-orbit order context in which the lemma is meant to be applied.

why it matters in Recognition Science

Recognition Science's foundation layer aims to force the cost $J$, the golden ratio fixed point, and the discrete octave structure without classical choice smuggled in through integer displays. Every order rung on ratio orbits that still went through le_iff_toInt_le or nonneg_iff_toInt_nonneg reintroduced that taint.

This module closes one multiplicative gap in the choice-free path: nonnegativity of right products by embedded nonzero orbits. That step is required for clean cross-multiplication comparisons (RatioOrbit order) and for later growth and forcing arguments that treat signed orbit arithmetic as constructive data. No downstream edges are recorded yet on this page (used_by empty), so its immediate consumers are sibling Grow lemmas and any ratio-order proofs that must multiply by a denominator orbit while staying choice-free.

scope and limits

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (1)