PRCJCostDistanceThreeLegModulusTarget_proved
plain-language theorem explainer
J-cost distance on recognition rationals has a three-leg modulus: any positive eps admits a positive delta so that three consecutive steps each shorter than delta force the endpoints within eps. Diagonal and completeness arguments cite it when a path runs selected-diagonal to raw point to representative to selected-diagonal. The proof stacks the two-leg triangle modulus twice and takes a common unit-fraction threshold.
Claim. For every positive recognition-rational $\varepsilon$ there exists a positive recognition-rational $\delta$ such that for all recognition-rationals $a,b,c,d$, if $d_J(a,b)<\delta$, $d_J(b,c)<\delta$, and $d_J(c,d)<\delta$, then $d_J(a,d)<\varepsilon$, where $d_J$ denotes J-cost distance on the recognition rationals.
background
This module builds real completeness inside Primitive Recognition Calculus: Cauchy data on recognition rationals (PRCRat) are realized, quotiented, and selected along diagonals so that the real line emerges with a usable metric structure. The metric ingredient here is J-cost distance, the distance induced by the unique cost $J$ forced in the foundation chain (T5: $J(x)=(x+x^{-1})/2-1$).
The two-leg triangle modulus already says that for each positive eps one can find a positive eta controlling pairs of consecutive short steps. The three-leg target strengthens that control to three consecutive steps, matching the geometry of diagonal proofs that travel selected point to intermediate raw point, across representatives, then back down another selected point.
Unit fractions supply a cofinal positive schedule on PRCRat: for any positive tolerance, some unit fraction (and all later ones) lie strictly below it. That schedule is how a single concrete delta is chosen below both intermediate thresholds produced by the triangle modulus.
proof idea
Tactic proof by successive unpacking of the two-leg triangle modulus. Fix positive eps. Apply the proved triangle-modulus target to eps to obtain positive eta and a two-leg bound at scale eta. Apply the same target again to eta to obtain positive theta and a two-leg bound at scale theta.
Invoke the unit-fraction eventual-strict-below lemmas at eta and at theta, obtaining indices Neta and Ntheta. Set delta to the unit fraction at max(Neta, Ntheta). Positivity is immediate; delta is strictly below both eta and theta by the eventual-below witnesses and max inequalities.
Given a,b,c,d with each consecutive J-distance below delta, transitively lift to a-b below eta and both b-c and c-d below theta. The theta-scale triangle bound yields b-d below eta; the eta-scale triangle bound then yields a-d below eps.
why it matters
Three-leg modulus is the metric glue for diagonal completeness arguments in PRC. Downstream, the real tail-selection target uses it when thinning Cauchy ledgers along selected indices, and the sharpened real-completeness certificate packages the whole stack (raw Cauchy realization, quotient points, diagonal selection) as a single structure.
In framework terms this sits under foundation completeness for the recognition calculus that underwrites later forcing landmarks (phi fixed point, eight-tick octave, D=3). Without a three-leg form, the natural diagonal path (selected to raw to representative to selected) would not close under a single eps-delta budget. The declaration is fully proved, not scaffolding: it discharges the named Prop target rather than leaving a hypothesis interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.