signFlags_exclusive
plain-language theorem explainer
A signed orbit cannot carry both the nonnegative flag and the strict-negative flag at once. Anyone building the internal integer order on signed orbits cites this mutual exclusion before trichotomy or certificate assembly. The proof rewrites negativity as Boolean negation of nonnegativity and obtains an immediate contradiction.
Claim. For every signed orbit $z$ (difference of two distinction naturals, intended as $\mathrm{pos}-\mathrm{neg}$), it is impossible that both the computable nonnegative flag and the strict-negative flag of $z$ equal $\mathrm{true}$.
background
Signed orbits are the primitive integer surface in the recognition calculus: a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, read as the formal difference $\mathrm{pos}-\mathrm{neg}$. Order is not imported from $\mathbb{Z}$; it is recovered from structural comparison of the two sides.
The nonnegative flag is the Boolean DistinctionNat.leq test of $\mathrm{neg}$ against $\mathrm{pos}$. The negative flag is defined as the Boolean negation of that flag ("strict negativity as failure of the structural nonnegative flag"). An upstream lemma records the exact equivalence: the negative flag is true if and only if the nonnegative flag is false.
This module develops the internal $\le$ relation on signed orbits ($a\le b$ when $b-a$ is nonnegative) and the supporting flag lemmas needed for a closed order certificate.
proof idea
Assume both flags are true. Rewrite the negative-flag conjunct via the upstream equivalence negativeFlag = true ↔ nonnegFlag = false. The resulting pair is nonnegFlag = true together with nonnegFlag = false. Substitute and contradict.
why it matters
Mutual exclusion of the two sign flags is a local Boolean fact that the integer-order development reuses whenever a hypothesis forces one flag and a conclusion or intermediate step forces the other. Downstream it appears in the proof that a negative flag blocks balance against the absolute orbit, in the specialized balance identity under a nonnegative hypothesis, and ultimately in integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed."
Within Recognition Science this sits in the foundation layer that reconstructs discrete order before continuum or forcing-chain material (T0–T8). It does not itself force $\phi$, dimension, or the eight-tick octave; it only keeps the signed-orbit Boolean surface consistent so later certificates can treat nonnegativity and negativity as complementary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.