PRCJCostDistanceThreeLegModulusTarget
plain-language theorem explainer
For every positive PRC-rational ε there is a positive δ such that three successive J-cost steps each shorter than δ force the composite a-to-d step below ε. Completeness and diagonal-selection arguments cite this as the modulus that matches the three-hop path (selected diagonal → raw point → representatives → selected diagonal). The declaration is pure Prop packaging; the content is discharged by iterating the ordinary two-leg triangle modulus.
Claim. For every positive PRC-rational $\varepsilon$ there exists a positive PRC-rational $\delta$ such that for all PRC-rationals $a,b,c,d$, if the $J$-cost distances $d_J(a,b)$, $d_J(b,c)$, and $d_J(c,d)$ are each strictly less than $\delta$, then $d_J(a,d)<\varepsilon$.
background
In the Primitive Recognition Calculus, rationals (PRCRat) are quotient classes of ratio orbits under cross-multiplication. Strict order is the native positivity of the difference: $a<b$ means $b-a$ has a positive ratio-orbit representative. The $J$-cost distance on those rationals is the metric-like quantity built from the Recognition cost $J$, the unique solution of the Recognition Composition Law forced at T5.
Real completeness in this module is assembled from Cauchy data, raw-ledger realizations, and diagonal selection. Diagonal arguments hop three times: from a selected diagonal point down to an intermediate raw point, across representatives, then back up another selected diagonal point. A plain two-leg triangle modulus is therefore one hop short of what the diagonal needs.
This definition packages exactly that three-leg uniform modulus as a bare proposition, parallel to the sibling triangle-modulus target already proved upstream in the same completeness development.
proof idea
No proof body: the declaration is a def equal to a Prop. The mathematical content is the quantified statement itself. Discharge lives in the companion theorem, which applies the ordinary two-leg $J$-cost triangle modulus twice: first to produce an intermediate $\eta$ controlling a two-step composite under $\varepsilon$, then again on $\eta$ to obtain $\delta$ so that three $\delta$-small legs compose below $\varepsilon$.
why it matters
The three-leg modulus is the continuity control that matches the geometry of diagonal selection in PRC real completeness. Its proved form is recorded on the Step 10e sharpened certificate (PRCRealCompletenessSharpenedCertificate), which bundles raw-Cauchy realization, quotient-point existence, diagonal selection from the raw diagonal ledger, and representative completeness for the null-closed reals.
Inside the Recognition forcing chain this sits in the foundation layer that builds ordered complete scalars before mass ladders and physical constants appear. It does not itself force $\phi$, the eight-tick octave, or $D=3$; it supplies the metric modulus those later constructions assume when they work over PRC reals rather than bare rationals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.