negate_respects_cross
plain-language theorem explainer
Negation of ratio-orbit displays preserves cross-multiplication equivalence. Anyone building the PRC rational field cites this to descend negation through the quotient by crossEq. The proof rewrites to integer cross-products, applies signed-orbit negate-to-int, and closes by linear combination of the hypothesis.
Claim. Let $a,b$ be ratio orbits (signed-orbit numerator over nonzero distinction-nat denominator). If $a$ and $b$ are cross-equivalent, i.e. the signed-orbit products $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ and $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$ balance, then the same cross-equivalence holds after pointwise negation of both numerators.
background
In the Primitive Recognition Calculus integer/rational layer, a signed orbit is a pair of distinction-nats read as $\mathrm{pos}-\mathrm{neg}$. A ratio orbit (K4.7) packages a signed-orbit numerator with a nonzero distinction-nat denominator: the internal display of a rational before quotienting.
Cross-equivalence (K4.10) is the PRC-native rational relation: $a\sim b$ when $a_{\mathrm{num}}$ scaled by $b_{\mathrm{den}}$ balances $b_{\mathrm{num}}$ scaled by $a_{\mathrm{den}}$ as signed orbits. The choice-free hub crossEq_iff_toIntCross rewrites this to ordinary integer equality of cross products $a_{\mathrm{num}}.\mathrm{toInt}\cdot b_{\mathrm{den}}.\mathrm{toNat}=b_{\mathrm{num}}.\mathrm{toInt}\cdot a_{\mathrm{den}}.\mathrm{toNat}$, depending only on propext and Quot.sound rather than Classical.choice.
Signed-orbit negation swaps pos and neg; its integer display satisfies $(\mathrm{negate},a).\mathrm{toInt}=-a.\mathrm{toInt}$. Ratio-orbit negation applies that swap to the numerator only.
proof idea
Tactic proof, four steps. First rewrite the hypothesis and goal through the integer characterization of cross-equivalence, so both sides become equalities of integer cross products. Unfold ratio-orbit negation (numerator swap). Simplify with the signed-orbit lemma that negation sends toInt to additive inverse. The resulting integer identity is the original cross-product equality with both sides multiplied by $-1$; close by linear_combination -h.
why it matters
This is the respect-of-equivalence lemma that makes PRC rational negation well-defined. Immediately downstream, K4.11 defines negation on the quotient type of ratio orbits by crossEq via Quot.lift, feeding negate_respects_cross into Quot.sound. Without it, the PRC rational field would lack a choice-free additive inverse at the orbit level.
In the broader Recognition foundation, integer and rational arithmetic on $\delta$-orbits is the discrete substrate under the forcing chain and the Recognition Composition Law; well-defined negation is a prerequisite for additive group structure on those displays before any continuum or J-cost analysis. The lemma is private scaffolding for the public K4.11 constructor rather than a cited end theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.