PRCPrimeSignedStrengthenedNativeCostHypotheses
plain-language theorem explainer
Packages the repaired native-cost hypothesis bundle used after the absolute-value and two-calibration no-gos: signed strengthened ledger axioms plus direct cost-level calibration on every native prime direction. Anyone proving uniqueness or character factorization of native costs on ratio orbits cites this interface. It is a pure Prop structure, not a proved statement.
Claim. For a map $F$ on ratio orbits, the prime-signed strengthened native-cost hypotheses hold when (i) $F$ satisfies the signed strengthened native-cost hypotheses (strengthened ledger axioms plus signed-unit calibration), and (ii) for every native prime $p$, $F$ agrees with the canonical on-orbit cost on the prime direction of $p$ (cross-equality of ratio orbits).
background
In the Primitive Recognition Calculus, a native cost is a map $F$ on ratio orbits meant to reproduce the doubled $J$-cost ledger (the recognition cost $J(x)=(x+x^{-1})/2-1$ lifted to orbits). Earlier uniqueness attempts failed two no-gos: absolute-value collapse and the fact that two-point calibration does not force all-prime calibration at the cost level.
PRCSignedStrengthenedNativeCostHypotheses already repairs the sign side: strengthened native-cost axioms plus direct calibration at the signed unit. The second field, prime-direction calibration, asserts that on every prime orbit direction $F$ matches the canonical on-orbit cost via cross-equality. Pass 283 records that this prime calibration cannot be derived from two-calibration alone, so it is imposed directly.
The local module builds uniqueness and character-factorization targets on top of successively stronger hypothesis bundles; this structure is the prime-signed layer before zero-orbit calibration is added.
proof idea
No proof body: the declaration is a structure ... : Prop that conjoins two existing propositions. Inhabiting it means supplying a term of the signed strengthened interface and a proof of universal prime-direction cross-equality. Downstream theorems (for example the zero-flat countermodel) build instances field-by-field with nested structure literals.
why it matters
This is the repaired hypothesis interface after both no-go repairs (sign and all-prime axes). It is the hypothesis of the replacement uniqueness target: every $F$ satisfying these hypotheses should agree with the canonical on-orbit cost on every ratio orbit. It is also the hypothesis of the signed-admissible character-factorization target: once prime and signed-unit calibration sit on the cost itself, ordinary character factorization is asked to produce a signed-admissible factor.
The next strengthening, zero-calibrated prime-signed hypotheses, adds zero-trace at the zero orbit on top of this bundle for the final character-factorization route. The zero-flat native cost is shown to satisfy this prime-signed interface while failing zero calibration, so the structure cleanly separates those layers. In the broader RS forcing chain this sits in the foundation cost-uniqueness work that pins the $J$-cost (T5) as the unique native ledger before phi and the eight-tick structure are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.