PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses
plain-language theorem explainer
Final native-cost hypothesis class on the character-factorization route: a map F on ratio orbits is prime-signed strengthened and its doubled trace vanishes at the zero orbit. Selection, uniqueness, and decoy-exclusion theorems cite this ledger as the frozen full class. Pure Prop structure with two fields; no proof body.
Claim. For $F:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$, the zero-calibrated prime-signed strengthened native-cost hypotheses hold when (i) $F$ satisfies the prime-signed strengthened package (signed unit, all prime-axis and prime-pair cost calibrations, and the strengthened base), and (ii) the doubled trace $T_F(q)=2(F(q)+1)$ is zero-calibrated: $T_F(0)\simeq 0$ under cross-equality of ratio orbits.
background
In the Primitive Recognition Calculus, costs live on RatioOrbit (signed numerator over a nonzero distinction denominator). A native cost $F$ induces a doubled d'Alembert trace $T_F(q)=2(F(q)+1)$; for costs generated by a ratio character $\chi$ this is exactly $\chi(q)+\chi(q)^{-1}$. The nonzero d'Alembert law does not fix $T(0)$, so zero-orbit compatibility is stated separately: cross-equality of $T$ at the zero orbit with zero.
The prime-signed strengthened package already folds in signed-unit recognition, all-prime direction calibration at the cost level, and the earlier strengthened native hypotheses. This structure simply conjoins that package with zero calibration of $T_F$.
The module sits in the native-cost uniqueness / selection stack that aims to force the canonical J-cost (Recognition Composition Law / T5 uniqueness) without external analytic assumptions beyond the ledger.
proof idea
Definitional packaging only: a Prop-valued structure with two fields. The first field is the prime-signed strengthened native-cost interface; the second asserts zero calibration of nativeCostDoubledTrace F via PRCDoubledTraceZeroCalibrated (cross-equality of the doubled trace at the zero orbit with zero). No tactics, no lemmas applied.
why it matters
This is the frozen full ledger for native cost selection. Downstream, CostSelectionPackageNative takes uniqueness over exactly this class and non-vacuity via an explicit witness; canonicalSelectedNativeCost_full_hypotheses shows the selected cost inhabits it; constant-zero and linear decoys are excluded against it. Uniqueness and signed-admissible character-factorization targets are quantified over the same hypotheses.
slim_class_iff_full_class equates a slimmer signed ledger with this full prime-signed zero-calibrated class, so minting and bookkeeping can switch presentations without changing the forced cost. In framework terms it is the native stand-in for the J-uniqueness step (T5 / RCL): every F meeting the itemized calibrations is forced to the canonical on-orbit cost once the uniqueness target discharges.
It closes the no-go repairs (sign and every prime axis calibrated at native-cost level, plus zero orbit) named in the module comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.