PRCUnitFraction
plain-language theorem explainer
Defines the PRC rational unit fraction $1/(n+1)$ used as a discrete tolerance rung in real-completeness arguments. Completeness and diagonal-selection proofs cite it as the canonical cofinal positive schedule. Construction is a short package: orbit denominator $n+1$, nonzero proof, numerator one.
Claim. For each natural number $n$, write $\mathrm{PRCUnitFraction}(n)$ for the PRC rational equal to the unit fraction $1/(n+1)$ (numerator the unit signed orbit, denominator the distinction-orbit of $n+1$).
background
The module builds completeness for PRC reals from Cauchy data over PRC rationals. PRC rationals are quotient classes of ratio orbits with nonzero distinction-orbit denominators (cross-multiplication identification). Distinction orbits are the base-neutral finite iteration type of repeated distinction; ofNat embeds ordinary naturals into that type.
A signed orbit is an intended difference of two distinction orbits. The unit signed orbit supplies the numerator $1$. The local setting is verifier display machinery for completeness, not a new recognition primitive: tolerances are ordinary unit fractions $1/(n+1)$ packaged so Cauchy and diagonal schedulers can quantify over a cofinal positive sequence in PRC rationals.
Upstream arithmetic maps (toNat, toNat_zero) convert orbit equalities back to ordinary naturals so the denominator nonzero obligation is discharged by omega.
proof idea
Set the denominator orbit to ofNat(n+1). Prove it is not the zero orbit by transporting equality through toNat, rewriting with toNat_ofNat and toNat_zero, then omega on $n+1 \neq 0$. Package PRCRat.mk with numerator the unit signed orbit, that denominator, and the nonzero witness.
why it matters
Supplies the standard positive cofinal tolerance schedule for PRC real completeness. Downstream, the cofinal-tolerance target is proved by packaging this family with positivity and the eventual-strict-inequality lemma. Finite row-tail, representative-tail, and diagonal schedule targets quantify closeness at rung $r$ via this unit fraction; their proved forms choose Cauchy thresholds at PRCUnitFraction r. The three-leg J-cost modulus target sits in the same completeness stack. In the Recognition foundation this is display scaffolding for Cauchy completeness of the real layer built on the primitive recognition calculus, not a forcing-chain step (T5–T8) or a new cost identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.