crossEq_refl
plain-language theorem explainer
Reflexivity of cross-multiplication equality on ratio orbits: every rational orbit display is cross-equivalent to itself. Anyone assembling the PRC rational quotient, order, or arithmetic cites it. The proof unfolds the cross relation and applies signed-orbit balance reflexivity.
Claim. For every ratio orbit $a$ (signed-orbit numerator over a nonzero distinction-nat denominator), the cross-multiplication relation holds of $a$ with itself: $a.\mathrm{num}$ scaled by $a.\mathrm{den}$ balances $a.\mathrm{num}$ scaled by $a.\mathrm{den}$ as signed orbits.
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 is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator (K4.7).
Cross-equivalence (K4.10) is the internal PRC stand-in for rational equality: two ratio orbits $a,b$ satisfy $\mathrm{crossEq},a,b$ when the signed orbits $a.\mathrm{num}\cdot b.\mathrm{den}$ and $b.\mathrm{num}\cdot a.\mathrm{den}$ are balanced. Balance itself is the signed-orbit equality relation used throughout this module.
Upstream, $\mathrm{balanced_refl}$ already gives $a\sim a$ for every signed orbit by commutativity of distinction-nat addition. This theorem lifts that fact to ratio orbits under cross-multiplication.
proof idea
Term-mode, two steps. Unfold $\mathrm{crossEq}$ so the goal becomes balance of $a.\mathrm{num}$ scaled by $a.\mathrm{den}$ against itself. Discharge with $\mathrm{SignedOrbit.balanced_refl}$ on that scaled numerator. No arithmetic beyond the upstream reflexivity lemma.
why it matters
This is the reflexivity leg of $\mathrm{crossEq_equivalence}$, which packages cross-multiplication as an $\mathrm{Equivalence}$ and underwrites the PRC rational quotient. Downstream it is the default witness in left/right multiplication congruence ($\mathrm{mul_crossEq_congr_left/right}$), in irreflexivity of the rational strict order ($\mathrm{ltQ_irrefl}$: a self-less-than would force $\mathrm{crossEq},p,p$ and then contradiction), and in native-cost uniqueness arguments that respect cross-equivalence.
In the foundation stack it is bookkeeping for K4 rationals built only from $\delta$-orbit positions, before J-cost uniqueness (T5) and the forcing chain attach physical meaning. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.