PRCUnitFraction_positive
plain-language theorem explainer
Every PRC unit fraction 1/(n+1) is positive in the PRC-rational sense. Completeness and tail-selection arguments cite this to feed a cofinal tolerance schedule into Cauchy diagonal constructions. The proof rewrites positivity across the classical toRat bridge and finishes by the positivity tactic on 1/(n+1).
Claim. For every natural number $n$, the PRC rational unit fraction $1/(n+1)$ is positive: its signed numerator is nonnegative and unbalanced against zero.
background
In the Primitive Recognition Calculus, rationals (PRCRat) are quotient classes of ratio orbits with nonzero denominator, identified by cross-multiplication. Positivity on a ratio orbit means the signed numerator is nonnegative and not balanced against zero; equivalently, via positive_iff_toRat_pos, the classical rational image is strictly positive.
PRCUnitFraction n is verifier display machinery, not a new PRC primitive: it builds the ratio with numerator the unit signed orbit and denominator the distinction-nat for $n+1$. Its classical image is exactly $1/(n+1)$ by PRCUnitFraction_toRat. The ambient module develops real completeness from ordered PRC rationals and Cauchy data, importing the real-order congruence layer.
proof idea
Rewrite the goal with PRCRat.positive_iff_toRat_pos, then substitute PRCUnitFraction_toRat so the claim becomes $0 < (1:\mathbb{Q})/(n+1)$. Discharge that inequality by Mathlib's positivity tactic. No case split on $n$ is needed: the denominator construction already guarantees $n+1 \ge 1$.
why it matters
This lemma is the positivity half of the exact cofinal tolerance schedule used by the real-completeness diagonal. Downstream, PRCRealCofinalToleranceScheduleTarget_proved packages the family as ⟨PRCUnitFraction, PRCUnitFraction_positive, …⟩ together with eventual smallness. Finite row and representative tail-selection targets invoke it at each rank $r$ to choose outer indices under positive tolerances. The three-leg J-cost modulus target sits in the same completeness cluster. In the broader RS foundation this is scaffolding for realizing reals from recognition orbits before the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$) is applied at the physics layer; it does not itself force those landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.