nonnegFlag_scaleByNat_of_ne_zero
plain-language theorem explainer
Scaling a signed orbit by a nonzero distinction-natural leaves its nonnegativity flag unchanged. Order and sign lemmas for the internal integer surface cite this when multiplying by positive naturals. The proof cases on the flag, rewrites through the integer embedding of scale-by-nat, and closes both sides by linear arithmetic from positivity of the scaler.
Claim. For every signed orbit $z$ and every distinction-natural $d \neq 0$, the nonnegativity flag of $z$ scaled by $d$ equals the nonnegativity flag of $z$: $\mathrm{nonneg}(z \cdot d) = \mathrm{nonneg}(z)$.
background
In the primitive recognition calculus, integers are recovered as signed orbits: equivalence classes that embed into ordinary $\mathbb{Z}$ via a recovery map toInt. A Boolean nonnegativity flag on a signed orbit is defined to match $0 \le \mathrm{toInt}(z)$, with a matching characterization when the flag is false ($\mathrm{toInt}(z) < 0$).
Distinction-naturals are the constructive naturals built from iterated distinction (with toNat reading off the iteration count). Scaling a signed orbit by such a $d$ multiplies the embedded integer by $d.\mathrm{toNat}$. The local module develops the order surface on these signed orbits: reflexivity, totality, trichotomy, and the exclusive/exhaustive interplay of nonneg and negative flags.
Upstream arithmetic supplies toNat_zero and injectivity of toNat, so $d \neq 0$ lifts to $d.\mathrm{toNat} \neq 0$ and hence to a strictly positive integer scaler.
proof idea
First lift $d \neq 0$ to $d.\mathrm{toNat} \neq 0$ by injectivity of toNat against toNat_zero. Case on the Boolean value of $z$'s nonnegativity flag.
If the flag is false, rewrite the goal via the false-flag characterization and the identity $\mathrm{toInt}(z.\mathrm{scaleByNat}, d) = \mathrm{toInt}(z) \cdot d.\mathrm{toNat}$. The hypothesis gives $\mathrm{toInt}(z) < 0$; positivity of $d.\mathrm{toNat}$ as an integer yields the product still negative, closed by nlinarith.
If the flag is true, the same rewrite with the true-flag characterization and nonnegativity of both factors again closes by nlinarith.
why it matters
This is a sign-stability lemma for positive integer scaling on the internal signed-orbit order. It feeds the matching statement for the negative flag (which simply unfolds and rewrites through this result) and the two multiplication lemmas that say multiplying on either side by a nonzero orbit-of-distinction preserves the nonnegativity flag.
Those facts sit inside the closed integer-order certificate: the package that records display equalities for truncated subtraction, $\le$, absolute difference, and the nonnegativity characterizations. Closing sign under scale-by-nat is part of showing the internal order surface is coherent before it is used higher in the foundation stack.
Relative to the Recognition forcing chain this is pure arithmetic scaffolding (not a T5–T8 landmark), but it is required infrastructure for treating signed orbits as an ordered ring-like object inside the calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.