negativeFlag_mul_ofOrbit_right_of_ne_zero
plain-language theorem explainer
Right-multiplication of a signed orbit by a nonzero nonnegative orbit leaves the negativity flag unchanged. Order and sign bookkeeping in the primitive recognition calculus cite this when products by pure positive distinctions must not flip sign. The proof is a two-step equality chain: balance the product against natural scaling, then invoke scale-invariance of the flag away from zero.
Claim. For any signed orbit $z$ and any nonzero distinction $d$, the negativity flag of $z$ multiplied on the right by the nonnegative orbit built from $d$ equals the negativity flag of $z$ itself: $\mathrm{neg}(z \cdot \iota(d)) = \mathrm{neg}(z)$, where $\iota(d)$ is the signed orbit with positive part $d$ and zero negative part.
background
In the primitive recognition calculus, integers are represented as signed orbits: pairs $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$. The structural nonnegative flag detects whether the difference is nonnegative; the negativity flag is its Boolean negation (strict negativity as failure of nonnegativity).
The embedding $\iota(d)=\mathrm{ofOrbit}(d)$ builds a nonnegative signed orbit from a pure distinction position $d$, with zero negative part. Right-multiplication by such an orbit is the natural product against a nonnegative integer factor. A companion relation, balancedness, identifies signed orbits that represent the same integer (equal $\mathrm{toInt}$).
Upstream, multiplication by $\iota(d)$ is balanced with scaling $z$ by the natural $d$, and scaling by nonzero $d$ preserves the negativity flag. Equality of flags under balancedness then transfers the invariance from the scaled form back to the product.
proof idea
Term-mode equality chain via $\mathrm{Eq.trans}$. First apply $\mathrm{negativeFlag_eq_of_balanced}$ to the balancedness witness $\mathrm{mul_ofOrbit_balanced_scaleByNat},z,d$, which equates the product $z\cdot\iota(d)$ with the scaled orbit $z.\mathrm{scaleByNat},d$ at the level of negativity flags. Then compose with $\mathrm{negativeFlag_scaleByNat_of_ne_zero},z,d,hd$, which states that scaling by nonzero $d$ leaves the flag of $z$ unchanged. The composite yields $\mathrm{neg}(z\cdot\iota(d))=\mathrm{neg}(z)$.
why it matters
This lemma is a sign-stability fact for the internal integer order on signed orbits. It feeds $\mathrm{integer_order_certificate}$, whose doc-comment states that "the internal signed-orbit order surface is closed," packaging display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity.
Within Recognition Science foundation work, signed orbits are the discrete carrier for integer comparisons before continuum limits and the forcing chain (T0–T8). Preserving negativity under right-multiplication by nonzero pure distinctions keeps the order and trichotomy apparatus coherent when products appear in comparisons. Without it, the certificate could not treat multiplicative scaling as sign-neutral on the negative side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.