not_balanced_ofOrbit_abs_of_negativeFlag
plain-language theorem explainer
A strictly negative signed orbit is never balanced against the nonnegative representative built from its absolute value. Order and integer-structure proofs in the Primitive Recognition Calculus cite this to separate the negative cone from the absolute-value embedding. The argument is a short contradiction: balance forces the nonnegative flag, which is exclusive of the negative flag.
Claim. Let $z$ be a signed orbit with negative flag true. Then $z$ is not balanced with the signed orbit obtained by embedding the absolute value of $z$: $\neg\,\mathrm{balanced}(z,\,\mathrm{ofOrbit}(|z|))$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of $\delta$-orbit positions with a structural nonnegative flag. Two signed orbits $a,b$ are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that is the internal integer equality relation, defined entirely on orbit positions. The absolute value $|z|$ is the distinction-nat $\mathrm{absDiff}$ of the positive and negative legs, and $\mathrm{ofOrbit}$ re-embeds that magnitude as a (nonnegative) signed orbit.
The negative flag is the Boolean negation of the nonnegative flag, so the two flags are exclusive by construction. An upstream equivalence states that $z$ is balanced with $\mathrm{ofOrbit}(|z|)$ if and only if the nonnegative flag of $z$ is true. The present lemma is the negative-cone half of that dictionary: negativity blocks balance against the absolute-value representative.
The local module builds the internal order on these signed orbits (reflexivity, transitivity, antisymmetry up to balance, totality, trichotomy) without leaving the orbit language.
proof idea
Term-mode proof by contradiction. Assume balance of $z$ with $\mathrm{ofOrbit}(|z|)$. Apply the forward direction of $\mathrm{balanced_ofOrbit_abs_iff_nonnegFlag}$ to obtain that the nonnegative flag of $z$ is true. Feed that flag together with the given negative flag into $\mathrm{signFlags_exclusive}$, which asserts that the two flags cannot both hold. The resulting falsehood discharges the assumption.
why it matters
This lemma seals one direction of the sign-versus-absolute-value interface used by the internal integer order. Downstream it is consumed by $\mathrm{integer_order_certificate}$, whose doc-comment states that "the internal signed-orbit order surface is closed": the certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity so that the order can be treated as a finished foundation object.
In the Recognition Science stack this sits under the ledger and forcing layer that eventually feeds the T0--T8 chain. Clean separation of the negative cone from the absolute-value embedding is required before one can treat signed integers as well-ordered recognition data rather than an external $\mathbb{Z}$ import. No open scaffold remains here; the claim is fully proved and only serves the certificate assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.