PRCSlimSansRclHypotheses
plain-language theorem explainer
Bundles the native-cost axioms on a map F of rational orbits, omitting the nonzero Recognition Composition Law. F is slim-sans-RCL when it is reciprocal and normalization-invariant, vanishes at the unit, is calibrated at two, matches the canonical cost on prime-pair products and signed units, and has doubled trace zero at the zero orbit. Uniqueness targets and non-vacuity certificates for the sans-RCL class cite this pack. Pure Prop structure; no proof body.
Claim. A map $F$ from rational orbits to rational orbits satisfies the slim sans-RCL hypotheses when: (i) $F$ is reciprocal and invariant under normalization, with $F(1)=0$ and $F(2)$ matching the canonical display on the orbit of two; (ii) $F$ agrees with the canonical cost on products of two prime directions; (iii) $F$ is calibrated on signed units; (iv) the doubled trace $T_F(q)=2(F(q)+1)$ vanishes at the zero orbit.
background
In the Primitive Recognition Calculus, costs act on RatioOrbit: integer numerator over a nonzero distinction-nat denominator (K4.7). Two orbits are identified by cross-equality when their rational values match. A native cost $F$ is a map on these orbits meant to recover the J-cost display $J(x)=(x+x^{-1})/2-1$ after calibration.
The base pack without RCL requires reciprocity $F(q)\sim F(q^{-1})$, invariance under normalization of the ratio, $F(1)=0$, and calibration at the orbit of two. The doubled d'Alembert trace is $T_F(q)=2(F(q)+1)$; for a generated cost this equals $\chi(q)+\chi(q)^{-1}$. Zero-calibration forces $T_F(0)=0$, which the nonzero d'Alembert law cannot constrain alone.
Prime-pair product calibration closes a gap where two-adic generated costs slipped older hypothesis packs: $F$ must already be canonical on products of native prime directions. Signed-unit calibration is the remaining discrete unit check. The full Recognition Composition Law (RCL) is deliberately left out of this slim pack.
proof idea
Definitional Prop structure with four fields and no proof body. It conjoins the base sans-RCL native-cost hypotheses, prime-pair product calibration, signed-unit calibration, and zero-calibration of the doubled trace of $F$. Downstream theorems inhabit the structure by supplying each field (often via where clauses or by projecting out of the full slim pack through the bridging iff).
why it matters
This is the hypothesis class for native-cost uniqueness without assuming the nonzero RCL. The uniqueness target states that every $F$ satisfying the pack agrees with the canonical display onRatioOrbit at every orbit. Non-vacuity is witnessed by the canonical selected native cost, which inhabits the pack. The RCL-spike native cost also inhabits it, showing the class is strictly larger than the full slim pack until RCL is restored.
The bridging theorem splits full zero-calibrated signed strengthened native-cost hypotheses into this sans-RCL pack plus the explicit RCL identity on nonzero orbits. In the Recognition forcing chain this isolates how much of J-uniqueness (T5) and the composition law can be recovered from discrete orbit calibration alone, before imposing RCL globally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.