negativeFlag_negate_ofOrbit_of_ne_zero
plain-language theorem explainer
Negating the positive signed orbit of a nonzero distinction natural yields a strictly negative signed integer (negative flag true). Sign-flag and order lemmas on the internal integer surface cite this one-direction fact. The proof rewrites through the toInt embedding and finishes by omega once nonzeroness of the underlying Nat is established from injectivity of toNat.
Claim. Let $n$ be a distinction natural with $n \neq 0$. Embedding $n$ as a nonnegative signed orbit and then negating produces a signed orbit whose negative flag equals true (equivalently, whose integer value is strictly negative).
background
In the Primitive Recognition Calculus, integers are coded as signed orbits: pairs of distinction naturals (pos, neg) with integer value pos.toNat - neg.toNat. The embedding ofOrbit places a distinction natural on the nonnegative ray. Negation swaps the two components; the upstream identity negate_toInt records (negate a).toInt = -a.toInt.
The Boolean negativeFlag is the surface predicate for strict negativity. Upstream, negativeFlag_eq_true_iff_toInt_neg equates the flag with toInt < 0. Distinction naturals carry toNat (the iteration-count map from ArithmeticFromLogic), with toNat_zero and injectivity available to move nonzero hypotheses between the logic-natural and Nat layers.
This module develops the order theory on that signed-orbit surface: reflexivity, totality, trichotomy, and the dictionary linking order relations to the nonneg and negative flags.
proof idea
Rewrite the goal with negativeFlag_eq_true_iff_toInt_neg, then apply negate_toInt and ofOrbit_toInt. The claim reduces to showing the embedded integer of ofOrbit n is positive, so its negation is negative.
Prove n.toNat ≠ 0 by contraposition: if toNat n = 0, then toNat_inj with toNat_zero forces n = zero, contradicting the hypothesis. The residual integer inequality is closed by omega.
why it matters
Direct parent of the biconditional negativeFlag_negate_ofOrbit_eq_true_iff_ne_zero and of recipNonzero_num_negativeFlag_eq, which preserves the numerator negative flag when forming the reciprocal of a nonzero ratio orbit. Both feed integer_order_certificate, whose doc-comment states the goal: "The internal signed-orbit order surface is closed."
In the Recognition foundation stack this is arithmetic infrastructure beneath ratios and later ladder constructions, not a forcing-chain landmark (T5 J-uniqueness through T8). It guarantees that sign flags behave under negation of positive orbits, so signed numerators remain consistent before any mass or coupling identities are stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.