nonnegFlag_mul_ofOrbit_right_of_ne_zero
plain-language theorem explainer
Right-multiplying a signed orbit by a nonzero pure nonnegative δ-orbit leaves the structural nonnegative flag unchanged. Anyone building the integer order surface on signed orbits cites this when products against orbit units must not flip sign. The proof is a two-step equality: the product is balanced with a nonzero natural scale, and that scale preserves the flag.
Claim. For any signed orbit $z$ (difference of two distinction naturals) and any nonzero distinction natural $d$, the structural nonnegative flag of the product $z \cdot \mathrm{ofOrbit}(d)$ equals the nonnegative flag of $z$.
background
In the primitive recognition calculus, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, read as the integer difference $\mathrm{pos}-\mathrm{neg}$. The structural nonnegative flag is the Boolean $\mathrm{leq}(\mathrm{neg},\mathrm{pos})$: true precisely when the negative side does not exceed the positive side. The pure embedding $\mathrm{ofOrbit}(d)$ builds the nonnegative signed orbit $\langle d,0\rangle$.
Two signed orbits are balanced when they represent the same integer (equal toInt). Balancing transfers the nonnegative flag. Scaling a signed orbit by a distinction natural multiplies both sides; for nonzero scale the flag is unchanged. The local module develops the order laws and sign flags needed for an internal integer order on this representation.
proof idea
Term-mode equality chain. First apply the balancing lemma: the right product of $z$ by $\mathrm{ofOrbit}(d)$ is balanced with the natural scale of $z$ by $d$. Balanced pairs share the same nonnegative flag, so the product's flag equals the scaled orbit's flag. Then apply the nonzero-scale lemma: scaling by $d\neq 0$ leaves the flag of $z$ unchanged. Transitivity of Boolean equality closes the claim.
why it matters
This is a sign-stability fact for right multiplication by pure nonnegative orbit units. It feeds integer_order_certificate, which packages the closed internal signed-orbit order surface (truncated subtraction, leq display, abs-diff, and both signed-nonneg characterizations). Without flag preservation under nonzero orbit products, the certificate's signed-nonneg flag display would not be stable under the multiplicative structure used to present integers. In the Recognition foundation stack this sits below the forcing chain: it is pure integer-order scaffolding for the primitive calculus, not yet a T5–T8 physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.