negativeFlag_scaleByNat_of_ne_zero
plain-language theorem explainer
Scaling a signed orbit difference by a nonzero natural distinction leaves its negativity flag unchanged. Anyone building the internal integer order on signed orbits cites this for sign-homogeneity under positive scaling. The proof is a one-line unfold of the negativity flag followed by rewrite through the companion nonnegativity lemma.
Claim. For every signed orbit $z$ and every nonzero distinction natural $d$, the negativity flag of the scaled orbit $z$ scaled by $d$ equals the negativity flag of $z$.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction naturals (pos, neg) with intended meaning pos - neg. Distinction naturals are the base-neutral finite orbit of repeated distinction (zero and successor). Scaling by a distinction natural multiplies both components: (pos, neg) becomes (pos * d, neg * d), restricted to positive-only orbit positions.
Negativity is not a primitive field. It is defined as failure of the structural nonnegative flag: negativeFlag z := !z.nonnegFlag. The companion result already shows that nonzero scaling preserves the nonnegative flag. The present statement is the dual for the derived negativity flag.
The local setting is the internal order on signed orbits: a ≤ b when b - a is nonnegative. Sign flags must be homogeneous under positive scaling for that order to behave like the usual integers.
proof idea
Term-mode, two steps. Unfold the definition of the negativity flag so the goal becomes equality of negated nonnegative flags. Rewrite with nonnegFlag_scaleByNat_of_ne_zero, which already proves that nonzero scaling preserves the nonnegative flag; Boolean negation then yields the claim. No case split on the signed orbit is required.
why it matters
This lemma is a small but necessary homogeneity fact for the signed-orbit order surface. It is consumed by the left and right multiplication lemmas that show multiplying by a nonzero pure orbit preserves the negativity flag, and it feeds the aggregate integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
In the Recognition foundation stack this sits under the integer-order layer that supports later forcing and ladder constructions. It does not itself invoke J-cost, phi, or the eight-tick octave; it only guarantees that the sign bit of a difference is stable under positive scaling, which the certificate packages for downstream consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.