negativeFlag_mul_ofOrbit_left_of_ne_zero
plain-language theorem explainer
Left-multiplication of a signed orbit by a nonzero nonnegative δ-orbit leaves the negativity flag unchanged. Order and sign bookkeeping for the internal integer surface cite this when transporting signs through scaling. The proof chains balance of mul-with-ofOrbit against scaleByNat, then uses that nonzero natural scaling preserves the flag.
Claim. For every nonzero distinction $d$ and every signed orbit $z$, the negativity flag of $(\mathrm{ofOrbit}(d))\cdot z$ equals the negativity flag of $z$.
background
In the primitive recognition calculus, integers are represented as signed orbit differences: a SignedOrbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$. The map $\mathrm{ofOrbit}$ embeds a nonnegative distinction $n$ as $\langle n,0\rangle$. The Boolean negativeFlag is the negation of the structural nonnegative flag: strict negativity is failure of nonnegativity.
Two signed orbits are balanced when they represent the same integer (equal toInt). Balance therefore transports every flag that depends only on the integer value. Scaling a signed orbit by a distinction natural multiplies both legs; for nonzero scale the sign is unchanged. The local module builds the internal order on these signed orbits and closes it under the arithmetic operations needed for an integer certificate.
proof idea
Term-mode equality chain. First apply ofOrbit_mul_balanced_scaleByNat: left-multiplying $z$ by $\mathrm{ofOrbit}(d)$ is balanced with $z$ scaled by $d$. Then negativeFlag_eq_of_balanced moves the flag across that balance. Finally negativeFlag_scaleByNat_of_ne_zero (using $d\neq 0$) shows the scaled orbit has the same negativity flag as $z$. Compose the two equalities with Eq.trans.
why it matters
Sign stability under left multiplication by a positive δ-orbit is a basic transport law for the internal signed-orbit order. It feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (nonnegativity, flags, truncated subtraction, and absolute difference displays all line up). Without flag preservation under positive scaling and ofOrbit-multiplication, the order certificate could not treat multiplication as order-compatible on the integer surface built from distinction orbits. This sits in the Foundation layer that reconstructs integer arithmetic before the forcing chain (T0–T8) and continuum physics are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.