PRCTwoAdicAxisTwistGeneratedCostNativeHypothesesTarget_constructed
plain-language theorem explainer
An explicit native cost on ratio orbits exists that meets the full native-cost hypothesis interface and is cross-equivalent to the cost induced by the two-adic axis-twist character. Anyone closing the native-cost uniqueness / admissibility-upgrade branch cites this witness. The proof is a three-field existential package: the patched generated cost, its hypothesis record, and the pointwise cross-equivalence lemma.
Claim. There exists a map $F$ from ratio orbits to ratio orbits such that $F$ satisfies the native-cost hypotheses (including exact unit-zero) and, for every ratio orbit $q$, $F(q)$ is cross-equivalent to the cost obtained from the two-adic axis-twist character at $q$.
background
In the Primitive Recognition Calculus, costs on ratio orbits are the discrete stand-in for the continuous $J$-cost of the forcing chain. A native cost must obey a fixed interface PRCNativeCostHypotheses, whose most rigid clause is definitional unit-zero at the identity orbit, not merely cross-equivalence to zero.
Characters on the ratio group induce candidate costs via costFromCharacter. The two-adic axis-twist character yields a cost with the desired quotient behavior, but the raw character cost need not meet unit-zero definitionally. The patched map twoAdicGeneratedNativeCost forces the identity orbit to zero and otherwise copies the character cost.
The construction target records exactly what remains: an $F$ that both satisfies the native hypotheses and stays pointwise cross-equivalent to the two-adic generated character cost. That target is the last constructive step before refuting an admissibility-upgrade route to uniqueness.
proof idea
Term-mode existential introduction. The witness map is twoAdicGeneratedNativeCost (identity orbit sent to zero; otherwise the two-adic character cost). The second component is the already-proved record twoAdicGeneratedNativeCost_hypotheses, which discharges reciprocal and the remaining native-cost fields by transporting along the cross-equivalence. The third component is the pointwise lemma twoAdicGeneratedNativeCost_crossEq_generated, which checks cross-equivalence by case split on whether the orbit is the identity. No further tactics are needed beyond packaging these three facts.
why it matters
This construction is the positive witness that kills the admissibility-upgrade path to native-cost uniqueness. Downstream, PRCNativeCostFactorizationAdmissibilityUpgradeTarget_refuted applies the not-of-two-adic lemma to this theorem and obtains a hard negation of the upgrade target.
In the broader Recognition framework the native cost is meant to be unique and to recover the forced $J(x)=(x+x^{-1})/2-1$ of T5. Showing that a two-adic axis-twist generated cost still satisfies the native interface (up to cross-equivalence) blocks any proof strategy that would upgrade mere admissibility or factorization into uniqueness without tighter constraints. The result therefore narrows the uniqueness program to routes that rule out such character-generated competitors directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.