zero_crossEq_iff_num_balanced_zero
plain-language theorem explainer
Cross-equality of the zero ratio orbit against an arbitrary ratio orbit a holds exactly when a's numerator balances the zero signed orbit. Order and reciprocal-identity lemmas in the primitive recognition calculus cite this left-zero orientation. The proof is a two-sided constructor that flips the already-proved right-zero form via cross-equality symmetry.
Claim. For every ratio orbit $a$, $\mathrm{crossEq}(0,a)$ if and only if the numerator of $a$ is balanced against the zero signed orbit.
background
In the Primitive Recognition Calculus, integers and rationals are rebuilt from $\delta$-orbit positions rather than classical $\mathbb{Z}$ and $\mathbb{Q}$. A signed orbit carries positive and negative distinction counts. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$ (K4.9); this is the internal PRC integer relation.
A ratio orbit is a signed numerator over a nonzero distinction-natural denominator (K4.7). Cross-equality is the internal rational relation: two ratio orbits satisfy $\mathrm{crossEq}$ when the cross-scaled numerators balance as signed orbits (K4.10). The sibling lemma already characterizes $\mathrm{crossEq}(a,0)$ by balance of $a$'s numerator against zero. The present statement is the symmetric orientation $\mathrm{crossEq}(0,a)$, so order and reciprocal identities can place zero on either side uniformly.
proof idea
Term-mode constructor on the biconditional. Forward: from $\mathrm{crossEq}(0,a)$, apply cross-equality symmetry to obtain $\mathrm{crossEq}(a,0)$, then the mp direction of the sibling $\mathrm{crossEq_zero_iff_num_balanced_zero}$. Reverse: from numerator-balance against zero, apply that sibling's mpr to get $\mathrm{crossEq}(a,0)$, then flip back by symmetry. No new arithmetic is introduced.
why it matters
Closes the zero-on-the-left orientation of the rational zero test inside IntegerOrder. Downstream, the reciprocal variants (reciprocal cross-equals zero iff zero cross-equals $a$; zero cross-equals reciprocal iff numerator balances zero; zero cross-equals reciprocal iff zero cross-equals $a$) chain through this flip so reciprocal ratio orbits inherit the same zero characterization. Those pieces feed the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed. Within the Recognition foundation this is pure PRC bookkeeping for the discrete order used before the forcing chain (T5 J-uniqueness through T8 dimension) lifts costs; it is not itself a physical law claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.