PRCStrengthenedNativeCostHypotheses
plain-language theorem explainer
Bundles ordinary native-cost hypotheses on a map F of ratio orbits with an extra cost-level calibration on products of two prime directions. Used wherever uniqueness or ledger targets must block the two-adic absolute-value loophole that slipped past the older native package. Pure interface structure: no proof content.
Claim. A map $F$ on ratio orbits satisfies the strengthened native-cost hypotheses when (i) it satisfies the ordinary native-cost package (RCL, normalization, and prior calibrations), and (ii) for every pair of prime distinction orbits $p,r$, the value of $F$ on the product of the corresponding prime directions is cross-equal to the canonical on-orbit cost of that same product.
background
In the Primitive Recognition Calculus, a native cost is a map $F$ on ratio orbits meant to realize the Recognition Composition Law (RCL) cost $J$ at the discrete orbit level. The older native-cost hypothesis bundle already encodes RCL-style identities, normalization, and single-prime calibrations, but it does not force canonicity on products of two distinct prime directions.
The two-adic (absolute-value) generated cost satisfies those older fields while erasing signed-unit information. The repair is the prime-pair product calibration: for primes $p,r$, $F$ on the product of prime directions must match the canonical on-ratio-orbit cost. That is exactly the surface where the two-adic counterexample escaped.
Local setting is native-cost uniqueness after that no-go: keep the old fields and add the pair product field before asking for character factorization or uniqueness.
proof idea
Definitional Prop-structure, not a proved theorem. It is the conjunction of two fields: the existing native-cost hypothesis bundle on $F$, and the prime-pair product calibration predicate (universal quantification over prime orbits $p,r$ with a cross-equality between $F$ on the product of prime directions and the canonical on-orbit cost). No tactics or lemmas discharge anything here.
why it matters
This is the post two-adic-no-go native interface used throughout the uniqueness stack. Downstream it is the base field of the signed strengthened package (adds signed-unit calibration), the slim-sans-sign ledger (adds zero calibration), and the sign-reversing ledger (pairs plus intrinsic antisymmetry). Uniqueness and factorization targets are restated as: every $F$ meeting this strengthened package factors through an admissible character, or coincides with the absolute-value generated cost in the no-go target.
Framework role: it hardens the discrete side of J-uniqueness (forcing chain T5 / RCL) so that native costs cannot deviate from the canonical $J$-shaped cost on composite prime probes. It does not yet force the signed unit; that is a later repair layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.