PRCSlimSansPairHypotheses
plain-language theorem explainer
Packages the slim native-cost hypothesis class without prime-pair product calibration: base PRC native axioms, signed-unit repair at −1, and zero-orbit calibration of the doubled d'Alembert trace. Cited by uniqueness targets and non-vacuity certificates for the sans-pair ledger class. Pure structure definition bundling three existing Prop fields.
Claim. For a map $F$ from rational orbits to rational orbits, the slim sans-pair hypothesis package asserts three properties: (i) $F$ satisfies the PRC-native cost axioms (reciprocity, normalization invariance, and the discrete Recognition Composition Law); (ii) $F$ is calibrated on the signed unit, $F(-1)\sim J(-1)$; (iii) 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 displays: integer numerator over a nonzero distinction-orbit denominator (K4.7). A native cost $F$ is constrained by PRCNativeCostHypotheses: reciprocity under orbit inversion, invariance under distinction-normalization, and the discrete Recognition Composition Law on the rational surface. The field two_calibrated in that package rules out the zero cost until a real completion exists.
The doubled d'Alembert trace is $T_F(q)=2(F(q)+1)$; for generated costs this equals $\chi(q)+\chi(q)^{-1}$. Zero-orbit compatibility is not forced by the nonzero d'Alembert law, so PRCDoubledTraceZeroCalibrated requires $T_F(0)\sim 0$. Separately, after an absolute-value no-go, signed-unit calibration demands that $F$ see $-1$, not only positive prime probes.
This module certifies minimality and uniqueness for PRC-native costs. The slim package here is the full base ledger with sign and zero repairs, deliberately omitting prime-pair product calibration.
proof idea
No proof body: this is a Prop-valued structure definition. It simply records three fields already defined upstream: the base native-cost hypothesis bundle, signed-unit calibration of $F$ at the negative unit orbit, and zero-calibration of the doubled trace of $F$. Inhabitants are constructed elsewhere by supplying those three witnesses.
why it matters
This is the working hypothesis class for the sans-pair uniqueness program. Downstream, PRCSlimSansPairUniquenessTarget asks that every $F$ satisfying the package agree with the canonical on-orbit cost. The bridging theorem slim_iff_sansPair_and_pair_calibrated splits the stronger zero-calibrated signed strengthened package into this sans-pair core plus prime-pair product calibration, isolating which field is still open.
Non-vacuity is settled: both canonicalSelectedNativeCost and twoAdicGeneratedNativeCost inhabit the class. In the broader RS forcing chain this sits under native $J$-cost uniqueness (T5 / RCL): the discrete rational surface must force $F$ to the unique cost $J(x)=(x+x^{-1})/2-1$ once enough calibration probes are present. Dropping pair products keeps the ledger slim while still carrying sign and zero repairs needed after the absolute-value obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.