PRCSlimSansSignHypotheses
plain-language theorem explainer
Packages the slim native-cost ledger without the signed-unit field: strengthened hypotheses (base RCL/normalization plus prime-pair product calibration) together with doubled-trace zero calibration. Anyone proving uniqueness or non-vacuity for the absolute-value cost class cites this interface. It is a pure Prop structure, not a proved theorem.
Claim. For a map $F$ on rational orbits, the slim sans-sign hypothesis class holds when (i) $F$ satisfies the strengthened native-cost interface (ordinary native-cost axioms plus prime-pair product calibration at cost level), and (ii) the doubled d'Alembert trace $T_F(q)=2(F(q)+1)$ is zero-calibrated: $T_F(0)$ equals the zero orbit under cross-equality.
background
In the Primitive Recognition Calculus, costs are maps $F$ on RatioOrbit (integer numerator over a nonzero distinction-nat denominator). The native-cost interface encodes Recognition Composition Law style constraints, normalization, and calibration on that discrete ledger.
The strengthened interface keeps those fields and adds prime-pair product calibration after the two-adic no-go. Separately, the doubled trace $T_F(q)=2(F(q)+1)$ is the d'Alembert form carried by a native cost; for generated costs it equals $\chi(q)+\chi(q)^{-1}$. Zero calibration demands $T_F(0)=0$ under orbit cross-equality, which the nonzero d'Alembert law alone cannot force.
This structure is the slim ledger with the signed-unit field stripped: strengthened base-plus-pairs plus zero. The full slim package is recovered by adjoining signed-unit calibration.
proof idea
No proof body: this is a Prop-valued structure definition. It simply records two fields, strengthened : PRCStrengthenedNativeCostHypotheses F and zero_calibrated : PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F). Inhabitants are built by supplying those two certificates (as in the absolute-value and canonical-selected non-vacuity theorems downstream).
why it matters
This is the hypothesis class for sans-sign uniqueness. Downstream, PRCSlimSansSignUniquenessTarget asks that every $F$ in this class agree with the on-orbit absolute-value cost under cross-equality. The bridging theorem slim_iff_sansSign_and_signed_unit splits the full zero-calibrated signed strengthened package into this sans-sign class plus signed-unit calibration, isolating where the Liouville/sign data is needed.
Non-vacuity is witnessed by canonicalSelectedNativeCost_sans_sign_hypotheses and absValueGeneratedNativeCost_sans_sign_hypotheses. In the Recognition forcing picture this sits under native-cost uniqueness toward the J-cost fixed by T5 and the RCL, before signed-unit necessity closes the full slim ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.