PRCTwoAdicAxisTwistGeneratedCostNativeHypothesesTarget
plain-language theorem explainer
Existence of a native cost on ratio orbits that meets the PRC native-cost hypotheses and is cross-equivalent to the cost generated by the two-adic axis-twist character. Anyone closing the two-adic counterexample against the admissibility-upgrade route for native-cost uniqueness cites this target. It is a pure Prop packaging that existence claim; a sibling construction theorem discharges it by exhibiting an explicit generator.
Claim. There exists a map $F$ from ratio orbits to ratio orbits such that $F$ satisfies the PRC native-cost hypotheses (reciprocal symmetry, normalization invariance, canonical recognition composition, and exact unit-zero calibration) and, for every ratio orbit $q$, $F(q)$ is cross-equivalent under balanced cross-multiplication to the cost generated from the two-adic axis-twist character evaluated at $q$.
background
In the primitive recognition calculus (PRC), rationals are displayed as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Two such displays are identified by cross-equivalence when the scaled numerators balance as signed orbits (internal cross-multiplication, not external real equality).
A native cost is a map $F$ on ratio orbits obeying the native-cost hypotheses: reciprocal symmetry, invariance under normalization, the canonical recognition composition law on the discrete rational surface, and an exact unit-zero field. The unit-zero clause is definitional equality at the unit orbit, not mere cross-equivalence; that rigidity is the delicate point flagged in the module comment.
Costs may also be generated from rational characters via the on-orbit cost constructor. The two-adic axis-twist character is the ratio-orbit realization of the verifier's two-adic branch twist; its generated cost already has the correct quotient behavior and is the candidate counterexample against upgrading factorization admissibility to full native uniqueness.
proof idea
Definitional packaging only: the declaration is a Prop equal to an existential quantifier over maps $F$ on ratio orbits, conjoining the native-cost hypothesis structure with pointwise cross-equivalence of $F(q)$ to the character-generated cost at the two-adic axis twist. No tactics or lemmas fire here. Discharge is deferred to the sibling construction theorem, which supplies an explicit two-adic generated native cost, verifies the hypothesis bundle, and checks the cross-equivalence identity.
why it matters
This target is the exact remaining construction needed to refute the admissibility-upgrade route for PRC native-cost uniqueness. Downstream, the negation theorem assumes the target and derives failure of the factorization-admissibility upgrade: if a native cost cross-equivalent to the two-adic generated cost exists, the upgrade cannot hold. A matching construction theorem already proves the target by exhibiting that cost, so the two-adic path is closed rather than left open.
In the broader Recognition framework this sits inside the discrete native-cost classification that precedes continuous J-uniqueness (T5) and the Recognition Composition Law. The two-adic twist probes whether character-generated costs can satisfy the rigid unit-zero native interface; settling that question keeps the uniqueness chain from admitting non-canonical discrete costs before the real completion is available.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.