PRCSquareGap
plain-language theorem explainer
Defines the positive square gap on PRC rationals: one plus the square of the additive difference. It supplies a strictly positive comparison quantity without introducing a rational absolute value. Downstream Cauchy and J-cost distance constructions cite it as the first separation kernel on the PRC real line.
Claim. For PRC rationals $a,b$, the square gap is the PRC rational $1+(a-b)(a-b)$. It is always at least $1$ in the underlying rational embedding and vanishes from the difference term precisely when $a=b$.
background
The Primitive Recognition Calculus builds reals from a quotient of ratio orbits rather than from classical $\mathbb{Q}$ first. PRCRat is that type: nonzero-denominator ratio-orbit classes identified by cross-multiplication (K4.8).
This module starts the first Cauchy surface on those rationals. A metric needs a nonnegative separation; absolute value is not yet available in the PRC rational API. Squaring the difference and shifting by one yields a strictly positive rational that still detects additive separation.
The same gap is the input to the PRC rational $J$-cost in the companion distance PRCJCostDistance, tying the Cauchy filter to the Recognition cost functional $J$.
proof idea
Pure definitional abbreviation: the body is the term $1+(a-b)(a-b)$ in the PRC rational ring. No lemmas are applied at the definition site. The companion theorem PRCSquareGap_toRat unfolds the definition and rewrites through toRat of addition, multiplication, and subtraction to match the ordinary rational formula.
why it matters
This is the separation kernel for the first PRC Cauchy surface. PRCJCostDistance composes it with the PRC rational $J$-cost: distance sends additive separation through the positive ratio $1+(a-b)^2$, then applies $J$. That distance underwrites Cauchy sequences, null equivalence, and the completeness path toward PRC reals.
In the broader Recognition stack, $J$ is the unique cost forced by the Recognition Composition Law (forcing chain T5). Routing Cauchy separation through $J$ keeps the real completion inside the same cost geometry that later forces $\varphi$, the eight-tick octave, and $D=3$. The square-gap choice is deliberately absolute-value-free so the early foundation stays inside the rational orbit calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.