rat_eq_of
plain-language theorem explainer
Two rationals are equal once their numerators and denominators agree. The argument is pure structure-eta: unpack the canonical ℚ representation and discard the proof fields by irrelevance. Downstream injectivity of the explicit ℚ→ℕ certificate (pairing forced num and den) cites this lemma.
Claim. For $a,b\in\mathbb{Q}$, if $\mathrm{num}(a)=\mathrm{num}(b)$ and $\mathrm{den}(a)=\mathrm{den}(b)$, then $a=b$. Equality is structure-eta on the reduced fraction representation; the nonzero-denominator and reducedness witnesses are proof-irrelevant and choice-free.
background
In Lean's mathlib, a rational is a four-field structure: integer numerator, natural denominator, a proof that the denominator is nonzero, and a proof that the fraction is in lowest terms. Two such records are equal precisely when the data fields match; the two Prop fields are definitionally irrelevant.
This module (DeltaForced) builds choice-free certificates that map physically forced discrete data into naturals. Sibling constructions include an integer-to-natural injection and a pairing map on $\mathbb{N}\times\mathbb{N}$. The present lemma is the rational counterpart of the integer case: agreement of num and den forces equality of the rationals themselves.
The local setting is the primitive recognition calculus, where discrete forced quantities (deltas) must inject into $\mathbb{N}$ without classical choice, so that later mass-ladder and forcing-chain arguments stay constructive.
proof idea
Tactic proof by structure unpacking. Destructure $a$ and $b$ into their four components (num, den, den-nonzero proof, reducedness proof). Simplify the hypotheses so they become equalities of the raw data fields. Substitute those equalities and close by reflexivity: the remaining Prop fields match by proof irrelevance. No external lemmas are required.
why it matters
Feeds directly into ratToNat_inj, the injectivity of the explicit certificate $\mathbb{Q}\to\mathbb{N}$ that pairs the (forced) numerator with the denominator. That injection is part of the DeltaForced stack: physically real discrete data must land injectively in $\mathbb{N}$ so that recognition-forced quantities can be enumerated without choice.
In the broader Recognition Science foundation, choice-free discrete certificates underwrite the forcing chain (T0–T8) and the passage from continuous cost geometry to countable rung data on the $\varphi$-ladder. Without rational equality from matching num/den, the rational certificate would not be known injective, and downstream uniqueness of forced deltas would stall.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.