mul_div_cancel
plain-language theorem explainer
Nonzero PRC rationals cancel under multiplication and division: a·b/b equals a whenever the verifier display of b is nonzero. Anyone assembling the field laws on the primitive recognition calculus quotient would cite this. The proof pushes the identity through the injective display map into ℚ and finishes by ordinary field simplification.
Claim. Let $a,b$ be primitive recognition calculus rationals (ratio-orbit quotient classes). If the rational display of $b$ is nonzero, then $a \cdot b / b = a$.
background
The ambient type is the PRC rational quotient: nonzero-denominator ratio-orbit classes identified by cross-multiplication (K4.8). Each class carries a verifier display toRat into ordinary rationals, specified as a transport wrapper whose internal characterization is cross-multiplication; that display is injective.
Division and multiplication on the quotient are defined so that they intertwine with the display: the display of a product (resp. quotient) is the product (resp. quotient) of the displays. The local module builds the arithmetic skeleton needed before the J-cost can be lifted from ratio-orbit representatives to the rational quotient (the PRCJCost namespace that follows in the same file).
Upstream, injectivity of the display and the multiplicative intertwining lemmas are already available from the IntegerRational development; the present lemma is the corresponding cancellation identity.
proof idea
One short tactic proof. Apply injectivity of the rational display so it suffices to check equality after toRat. Rewrite the display of the quotient and of the product via the intertwining lemmas, then run field_simp on the resulting identity in ℚ, using the hypothesis that the display of the denominator is nonzero.
why it matters
Field cancellation is a routine but mandatory step in turning the PRC rational quotient into a usable arithmetic carrier for recognition cost. Immediately below this lemma the file opens the PRCJCost namespace, whose purpose is to lift the J-cost from ratio-orbit representatives onto the rational quotient; without cancellation, that lift cannot treat multiplicative inverses cleanly.
In the broader Recognition Science chain this sits in the foundation layer that prepares the cost functional before the forcing steps (T5 J-uniqueness, RCL). No downstream consumers are wired yet (used_by is empty), so the lemma is presently infrastructure rather than a cited parent of a named forcing theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.