PRCSquareGap_toRat
plain-language theorem explainer
The square-gap comparison on PRC rationals displays on ordinary rationals as one plus the squared difference of the two displays. Anyone building the first PRC Cauchy surface or the J-cost distance cites this identity. The proof unfolds the gap definition and pushes the embedding through addition and multiplication.
Claim. For PRC rationals $a,b$, the ordinary-rational display of the positive square gap $1+(a-b)(a-b)$ equals $1+(a^{\mathrm{rat}}-b^{\mathrm{rat}})^2$, where $(\cdot)^{\mathrm{rat}}$ is the canonical embedding of PRC rationals into $\mathbb{Q}$.
background
Primitive Recognition Calculus builds rationals (PRCRat) as nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication. The map toRat is the canonical display of a PRC rational as an ordinary rational. Subtraction on the PRC side is the internal difference operation, related to the integer-level sub by a simp identity.
The square gap is the first Cauchy-pass comparison for additive separation: it is defined as $1+(a-b)(a-b)$. Squaring removes any need for a rational absolute value at this stage, and the leading $1$ keeps the result strictly positive. Downstream, this gap is fed into the PRC rational J-cost to produce the J-cost distance used by the first PRC Cauchy surface.
The local module constructs that Cauchy surface over PRC rationals before completing to reals. The identity here is the bridge that lets metric properties (self-distance zero, symmetry, triangle) be checked after display into ordinary rationals.
proof idea
Term-mode proof by direct computation. Unfold the square-gap definition to $1+(a-b)(a-b)$. Rewrite the display of the sum and of the product via the PRC-rational embedding lemmas for addition and multiplication. Finish by simplifying the internal subtraction to the ordinary difference of displays. No case splits or induction.
why it matters
This is the display lemma that makes the PRC J-cost distance computable on ordinary rationals. The parent display theorem PRCJCostDistance_toRat rewrites through it after applying the on-PRCRat J-cost display. The same rewrite discharges self-distance zero and symmetry of the J-cost distance: both proofs inject via toRat, unfold the distance, and invoke this identity so that $1+(a-a)^2=1$ and the squared difference is symmetric.
In the Recognition framework the J-cost is the unique cost forced by the Recognition Composition Law (T5: $J(x)=(x+x^{-1})/2-1$). The square-gap route is the additive first pass that feeds that cost without introducing absolute values on the rational layer. Closing these elementary metric identities is scaffolding for the PRC Cauchy sequences and the later real completion used throughout the foundation stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.