forced_cost_exists_on_completion
plain-language theorem explainer
The canonical cost exists on ratio orbits of the continuum completion: the map sending each rational orbit q to (q + q^{-1})/2 − 1, and it is reciprocal-symmetric under cross-equality. Continuum-forcing and uniqueness arguments in the foundation layer cite this existence package. The proof is a direct term witness: the native orbit formula, with reciprocity from the established symmetry lemma and definitional equality.
Claim. There exists a map $J$ from ratio orbits to ratio orbits such that for every ratio orbit $q$, $J(q)$ is cross-equal to $J(q^{-1})$ and $J(q)$ equals the native formula $(q + q^{-1})/2 - 1$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator: the internal stand-in for a rational. Reciprocal sends the zero orbit to zero and otherwise inverts. Cross-equality is balanced cross-multiplication on signed orbits, and it agrees with rational equality of the verifier displays.
The native cost on a ratio orbit is $J(q)=((q+q^{-1})/2)-1$, the same algebraic shape forced at T5 in the unified forcing chain. The module lives in the continuum layer of PRC: after character rigidity, one packages this cost on the completion $R_\delta$ via the rational embedding, with closure under the countable field $T$.
Upstream, reciprocal symmetry of the native cost is already proved, and the canonical identity event sits at the J-cost minimum $x=1$.
proof idea
One-line term-mode existence proof. The witness is the native cost map on ratio orbits. For each orbit $q$ the proof packages the pair: reciprocal symmetry of that map (from the established symmetry lemma), and definitional equality of the witness with itself (rfl). No further algebraic reduction.
why it matters
This is the existence half of the forced cost on the continuum completion, the PRC-native counterpart of T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$). Sibling results in the same module include the forced-J identity on the completion, calibration propagation along cyclic subgroups, and the one-point calibration target.
The module flags an open all-primes target immediately below: one-point calibration at two forcing global identity on every nonzero ratio orbit remains open in native cost uniqueness. Capstone rigidity is per-direction; propagating a single calibration across independent prime directions is the remaining content. Present downstream use count is zero, so the declaration is a local existence package for the continuum layer rather than a heavily cited leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.