nonnegFlag_mul_ofOrbit_left_of_ne_zero
plain-language theorem explainer
Left multiplication of a signed orbit by a nonzero nonnegative orbit (the pure positive difference built from a distinction count) leaves the structural nonnegative flag unchanged. Anyone closing the signed-orbit order surface cites this when positive scaling must not flip sign. The proof is a two-step term chain: the product is balanced with natural scaling, and nonzero scaling preserves the flag.
Claim. Let $d$ be a nonzero distinction count and let $z$ be a signed orbit (intended meaning $z = \mathrm{pos}-\mathrm{neg}$). Form the nonnegative orbit $\langle d,0\rangle$. Then the structural nonnegative flag of the product $\langle d,0\rangle\cdot z$ equals the nonnegative flag of $z$.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction counts $(\mathrm{pos},\mathrm{neg})$ read as the formal difference $\mathrm{pos}-\mathrm{neg}$. The structural nonnegative flag is the Boolean $\mathrm{neg}\le\mathrm{pos}$ under the distinction order; it is the computable stand-in for "$z\ge 0$" before the integer embedding is fully certified.
The map that sends a distinction count $d$ to the pure nonnegative orbit $\langle d,0\rangle$ embeds nonnegative positions into signed orbits. Multiplication of signed orbits interacts with natural scaling: the product of $\langle d,0\rangle$ with $z$ is balanced (same integer image) with the natural scale of $z$ by $d$. Balanced orbits share the same nonnegative flag, and scaling by a nonzero distinction count leaves that flag fixed.
This lemma lives in the IntegerOrder layer that assembles reflexivity, totality, trichotomy, and sign-flag exclusivity for the internal order surface.
proof idea
Term-mode proof by trans of two equalities on the Boolean flag.
First apply the balance lemma: $\langle d,0\rangle\cdot z$ is balanced with the natural scale of $z$ by $d$, so the two sides have equal nonnegative flags (via the general fact that balanced signed orbits share the flag).
Second apply scale-invariance: for $d\neq 0$, scaling $z$ by $d$ does not change the nonnegative flag.
Composing the two equalities yields the claim. No case split on the flag itself is needed at this site.
why it matters
The parent consumer is the integer-order certificate, which packages display lemmas for truncated subtraction, distinction $\le$, absolute difference, and the signed nonnegative flag, declaring that "the internal signed-orbit order surface is closed." This lemma supplies the multiplicative left-action stability needed so that positive orbit factors do not disturb the flag used in those displays.
Within Recognition Science foundation work, signed orbits are the discrete carrier before continuum limits and the forcing chain (T5–T8) are attached. Keeping the structural sign flag invariant under nonzero positive left multiplication is a small but necessary algebraic hygiene step: without it, the order certificate could not treat multiplication by pure positive orbits as order-sign preserving.
No open scaffold remains here; the claim is fully proved and feeds the closed certificate rather than a hypothesis interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.