dispCross
plain-language theorem explainer
Equality of verifier rational displays of two ratio orbits implies their internal cross-multiplication equivalence. Cited throughout the PRC native-cost structural ledger and in gauge-orbit classification when costs or characters are compared via the internal relation. One-line term proof: reverse direction of the cross-equivalence iff display-equality biconditional.
Claim. Let $a$ and $b$ be ratio orbits (signed-orbit numerator over a nonzero distinction-nat denominator). If their verifier displays as ordinary rationals agree, then $a$ and $b$ are cross-equivalent: the scaled signed orbits $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ and $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$ are balanced.
background
In the Primitive Recognition Calculus, rationals live as ratio orbits: a signed orbit as numerator over a nonzero distinction-nat denominator (K4.7). Internal equality is not quotiented at definition; it is the cross-multiplication relation (K4.10): two orbits are cross-equivalent when the scaled products of numerator and opposite denominator balance as signed orbits, entirely on $\delta$-orbit positions.
The map sending a ratio orbit to an ordinary rational is only a verifier display. Its doc tags it as a transport wrapper whose internal characterization is cross-multiplication. Upstream, the biconditional records that this display equality agrees exactly with the internal relation (via signed-orbit balance iff integer equality after scaling).
The ambient module is the structural ledger for PRC native-cost uniqueness: costs on ratio orbits, ratio characters, calibration on positive integers, and gauge rigidity that force the canonical cost.
proof idea
One-line term proof. Apply the reverse implication of the upstream biconditional that cross-equivalence of ratio orbits is equivalent to equality of their verifier rational displays, feeding the given display equality.
why it matters
Bridge lemma that lets every downstream comparison written in display language land on the internal cross-equivalence relation used by the ledger.
In-module parents: character display pushes display equality through a PRC ratio character by first converting to cross-equivalence; structural character calibration on positive integers and structural gauge rigidity compare factored costs via the same relation; the Round 5 terminal uniqueness target assembles those pieces to force the canonical native cost.
On the cost side, gauge-orbit classification uses it in the degenerate branch (trace at two equals two forces the sign gauge) and the nondegenerate branch (signed power costs). That free-side stratification (form forced, unit free) is the ledger path toward J-uniqueness (forcing-chain T5) without smuggling ordinary rational equality into the internal PRC language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.