PRCSlimSansRclUniquenessTarget
plain-language theorem explainer
Defines the uniqueness target for native cost maps under the slim ledger with RCL dropped: any F on ratio orbits obeying those hypotheses must match the J-cost via cross-multiplication equality at every orbit. Used to state the claim that the refutation theorem then kills. Pure Prop packaging; no proof content.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the slim native-cost hypotheses without the Recognition Composition Law (base sans-RCL ledger, prime-pair product calibration, signed-unit calibration, and zero calibration), then for every ratio orbit $q$ one has cross-multiplication equality $F(q)\sim J(q)$, where $J(q)=((q+q^{-1})/2)-1$ is the PRC rational J-cost on that orbit.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). Cross-equivalence of two ratio orbits is the internal rational relation: numerators and denominators balance under cross-multiplication of signed orbits (K4.10). The PRC J-cost on a ratio orbit is the orbit-level object $J(q)=((q+q^{-1})/2)-1$, not yet the real-analytic uniqueness theorem.
The slim sans-RCL hypothesis bundle packages the native-cost ledger with the nonzero Recognition Composition Law removed, retaining base sans-RCL structure plus prime-pair product, signed-unit, and zero calibrations. The local module certifies minimality and uniqueness targets for native cost; this definition is the uniqueness Prop for that stripped class.
proof idea
Definitional Prop only. It quantifies over maps $F:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$, assumes the slim sans-RCL hypothesis structure on $F$, and asserts pointwise cross-equivalence of $F(q)$ with the J-cost onRatioOrbit q. No tactics, no lemmas applied.
why it matters
This target is the claim that the downstream theorem PRCSlimSansRclUniquenessTarget_refuted negates: slim-minus-nonzero-RCL admits the 5-spike, so uniqueness fails and the RCL field cannot be dropped. That is the bonus RCL-core necessity result in the native-cost minimality certificate.
In the broader forcing chain, T5 forces $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) as the unique cost; the Recognition Composition Law is the algebraic identity that pins $J$. Packaging uniqueness without RCL lets the certificate exhibit an explicit counterexample map, separating which ledger axioms are load-bearing for J-uniqueness on ratio orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.