zero_crossEq_mul_iff
plain-language theorem explainer
Zero is cross-equivalent to a product of ratio orbits exactly when at least one factor is cross-equivalent to zero. Order and rational-display developers cite it as the left-zero form of the zero-product law on RatioOrbit. The proof is a two-direction constructor that flips sides with cross-equivalence symmetry and applies the existing product-on-the-left zero law.
Claim. For ratio orbits $a$ and $b$, the zero orbit is cross-equivalent to the product $a\cdot b$ if and only if $a$ is cross-equivalent to zero or $b$ is cross-equivalent to zero.
background
In the Primitive Recognition Calculus integer layer, a ratio orbit is an integer numerator over a nonzero orbit denominator (K4.7). Cross-equivalence is the internal rational relation: two ratio orbits match when the scaled numerators balance under cross-multiplication of signed orbits (K4.10). It is the PRC stand-in for ordinary rational equality, defined entirely on $\delta$-orbit positions rather than classical $\mathbb{Q}$.
Multiplication of ratio orbits inherits a zero-product law. The sibling theorem mul_crossEq_zero_iff states that the product is cross-equivalent to zero exactly when a factor is. Because cross-equivalence is symmetric, the same law holds with zero written on the left of the relation. That left-zero packaging is what this declaration records, inside the IntegerOrder module that builds the signed-orbit order surface.
proof idea
Term-mode proof by constructor on the biconditional.
Forward: assume zero is cross-equivalent to the product. Symmetry of cross-equivalence moves zero to the right; the existing product-zero law then yields that a factor is cross-equivalent to zero.
Backward: assume a factor is cross-equivalent to zero. The product-zero law produces product cross-equivalent to zero; symmetry flips the sides to put zero on the left.
No new arithmetic is done; the work is packaging and side-flipping.
why it matters
Closes the left-zero form of the zero-product law on ratio orbits, which the order layer needs when testing whether a product vanishes. Downstream, zero_not_crossEq_mul_iff rewrites through this biconditional to obtain the negated form (product nonzero iff both factors nonzero). That pair feeds the broader IntegerOrder certificate, whose doc-comment states that "the internal signed-orbit order surface is closed."
In the Recognition foundation this is bookkeeping on the rational display used before cost uniqueness and the forcing chain, not a physics law itself. It keeps the PRC rational layer coherent so later uniqueness and ladder arguments can treat zero factors without classical $\mathbb{Q}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.