PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses
plain-language theorem explainer
Packages the slim native-cost hypothesis class on ratio orbits: signed strengthened axioms plus zero-orbit calibration of the doubled d'Alembert trace. Anyone proving uniqueness or decoy exclusion without the all-prime axis field cites this ledger. It is a Prop structure, not a proved statement.
Claim. For a map $F$ from ratio orbits to ratio orbits, the slim native-cost hypotheses hold when (i) $F$ satisfies the signed strengthened native-cost interface (base reciprocity, normalization invariance, nonzero RCL, unit-zero, two-calibration, prime-pair products, and signed-unit calibration), and (ii) the doubled trace $T_F(q)=2(F(q)+1)$ is zero-calibrated: $T_F(0)=0$ in the cross-equality sense.
background
In the Primitive Recognition Calculus, costs act on RatioOrbit values: rational displays with a signed-orbit numerator and a nonzero distinction-orbit denominator. A native cost $F$ carries a doubled d'Alembert trace $T_F(q)=2(F(q)+1)$; for generated costs this is exactly $\chi(q)+\chi(q)^{-1}$.
The signed strengthened interface already bundles the repaired base axioms after the absolute-value no-go, plus direct calibration at the signed unit. Separately, the nonzero d'Alembert law does not constrain $T(0)$; character traces with the intended zero image need an extra zero-orbit condition $T(0)=0$.
This module isolates the slim ledger: that signed strengthened package together with zero-orbit calibration, deliberately omitting the all-prime axis field from the round-1 minted hypotheses.
proof idea
No proof body: this is a Prop-valued structure definition. It conjoins two fields already defined upstream: the signed strengthened native-cost hypotheses on $F$, and zero-calibration of nativeCostDoubledTrace F via cross-equality of the doubled trace at the zero orbit with zero. Inhabitants are built by supplying both components (or transported via the slim/full class equivalence proved later in the module).
why it matters
This is the hypothesis class for the slim native cost-selection package: uniqueness is asked only for maps satisfying base + prime-pair products + signed unit + zero orbit, without an all-prime axis field. Downstream, all_prime_axis_field_redundant shows every slim inhabitant is automatically prime-direction calibrated, so the deleted field is redundant. The uniqueness target, non-vacuity of the canonical selected cost, and decoy exclusions (constant-zero, linear, zero-flat) are all stated against this class. It tightens the J-uniqueness path (T5 / RCL) by shrinking the ledger while keeping the same canonical cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.