signFlags_exhaustive
plain-language theorem explainer
Every signed orbit difference carries at least one structural sign flag: nonnegative or strictly negative. Anyone assembling the internal integer-order surface or sign laws for orbit multiplication cites this. The proof is a two-case split on the nonnegative Bool, discharging the negative branch by the complementary-flag equivalence.
Claim. For every signed orbit $z$ (intended as a difference of two distinction naturals), either the structural nonnegative flag of $z$ equals true, or the strict-negativity flag of $z$ equals true.
background
A signed orbit is a pair of distinction naturals (pos, neg), read as the formal difference pos - neg. The structural nonnegative flag is the computable comparison leq neg pos; the strict-negativity flag is defined as its Boolean negation. Together they are the only sign data the order layer exposes.
The local module builds the internal order on these orbits: a ≤ b means b - a is nonnegative under that flag. Upstream, the complementary equivalence states that the negativity flag is true if and only if the nonnegative flag is false, by unfolding the negation definition and casing on the Bool.
Exhaustiveness of the two flags is the missing half of a Boolean partition: exclusivity is the sibling lemma, and together they make the sign surface total before order axioms and certificates are assembled.
proof idea
Term-mode proof by cases on z.nonnegFlag. If it is true, the left disjunct is immediate by reflexivity. If it is false, take the right disjunct and rewrite with negativeFlag_eq_true_iff_nonnegFlag_eq_false, which converts the goal into the case hypothesis. No arithmetic on the underlying distinction naturals is required; the argument is pure Bool exhaustiveness under the flag definitions.
why it matters
This lemma closes the sign-flag partition used by the internal integer order. Downstream, integer_order_certificate packages the closed order surface (nonnegativity displays, truncated subtraction, absolute difference) and needs the flags to be total. The multiplication law negativeFlag_mul_iff also cases on sign combinations and relies on every orbit landing in one of the two flag states.
In the Primitive Recognition Calculus stack this is scaffolding for an integer order built only from distinction comparisons, not from a pre-existing ℤ. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it is part of the foundation layer those later physics identifications sit on: without a total sign surface, rung arithmetic and mass-ladder comparisons cannot be stated internally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.