zero_lt_iff_nonnegFlag_and_not_balanced_zero
plain-language theorem explainer
Strict positivity of a signed orbit against zero is equivalent to the nonnegativity flag being true and the orbit not balancing with zero. Order and arithmetic developers in the Primitive Recognition Calculus cite this when rewriting 0 < z into flag-and-inequivalence form. The proof unfolds the internal strict order, rewrites nonnegativity via the zero-le flag lemma, and symmetrizes balance in both directions.
Claim. For every signed orbit $z$, one has $0 < z$ if and only if the nonnegativity flag of $z$ is true and $z$ is not balanced with zero (i.e., $z.\mathrm{pos}+0.\mathrm{neg}\neq 0.\mathrm{pos}+z.\mathrm{neg}$).
background
In the Primitive Recognition Calculus, integers are realized as signed orbits: pairs of nonnegative orbit lengths (positive and negative legs). Two signed orbits are balanced when their cross-sums agree, $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the internal integer equality relation, defined entirely on $\delta$-orbit positions.
The internal order is built from that relation. Non-strict order $a\le b$ is a nonnegative difference; strict order is $a\le b$ together with failure of balance. A Boolean nonnegativity flag on a signed orbit records whether the orbit sits on the nonnegative side of zero; the sibling lemma zero_le_iff_nonnegFlag already equates $0\le z$ with that flag being true.
This module closes the order surface on signed orbits (reflexivity, transitivity, antisymmetry up to balance, totality, trichotomy, and the sign-flag dictionary). The present statement is the strict-positive half of that dictionary.
proof idea
Unfold the definition of strict order: $0<z$ means $0\le z$ and not balanced$(0,z)$. Rewrite $0\le z$ by the sibling equivalence with the nonnegativity flag. Both directions of the resulting biconditional are identical: keep the flag conjunct and transport the negated balance conjunct across balanced_symm, which swaps the two arguments of balance. No arithmetic on orbit lengths is needed.
why it matters
The lemma is a small but load-bearing rewrite rule in the signed-orbit order package. Downstream, recipNonzero_num_zero_lt_iff applies it twice to move strict positivity of a reciprocal numerator back to positivity of the original numerator. It also sits under integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed," packaging flag displays and order facts for the larger foundation stack.
Within Recognition Science this is pre-physics scaffolding: integers and their order must be forced from recognition structure before the forcing chain (T0–T8), the Recognition Composition Law, or the $\varphi$-ladder mass formula can be stated on a discrete substrate. Closing the $0<z$ dictionary removes a gap between Boolean sign flags and the Prop-valued strict order used in ratio and reciprocal constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.