twoAdicGeneratedNativeCost
plain-language theorem explainer
The two-adic axis-twist native cost maps each rational orbit to zero on the unit orbit and otherwise to the cost generated by the two-adic branch-twist character. Uniqueness and minimality certificates cite it as the explicit counterexample cost that satisfies base native hypotheses yet fails prime-pair product calibration. The body is a classical case split wrapping cost-from-character.
Claim. For each rational orbit $q$, define the two-adic generated native cost by $C_{2}(q)=0$ if $q$ is the unit orbit, and otherwise $C_{2}(q)$ equal to the cost generated from the two-adic axis-twist character evaluated at $q$.
background
In the primitive recognition calculus, a rational orbit is an integer numerator over a nonzero distinction-nat denominator (the K4.7 display of ratios of orbits). Native costs are maps on these orbits; the generator costFromCharacter builds a cost by applying a ratio-orbit character $\chi$ and then the on-ratio-orbit cost map. The identity character recovers the canonical PRC cost.
The two-adic axis-twist character is the ratio-orbit realization of the verifier two-adic branch twist: it sends $q$ to the orbit of the two-adic twist of the underlying rational. The present definition packages that character into a full native-cost candidate, with an explicit unit-orbit calibration to zero so the map sits in the native-cost hypothesis class used by uniqueness arguments.
The ambient module studies uniqueness of native costs under d'Alembert-type and cross-equation constraints; this object is the concrete two-adic twist inhabiting those classes.
proof idea
Definition by classical case split on the input orbit. If $q$ equals the unit rational orbit, return the zero orbit. Otherwise return costFromCharacter applied to the two-adic axis-twist character at $q$. No further lemmas are invoked in the body; the noncomputable marker comes from the character and the rational-orbit conversion underneath.
why it matters
This is the explicit counterexample cost that drives pair-field necessity and uniqueness refutations in the PRC native-cost stack. Downstream, the minimality certificate proves it satisfies the slim sans-pair hypotheses (signed-unit and zero calibration) yet fails prime-pair product calibration at the mixed $(2,3)$ orbit, so PRCSlimSansPairUniquenessTarget is refuted: base + sign + zero alone admit the two-adic twist, and the pair field cannot be dropped.
In the parent uniqueness module it witnesses PRCTwoAdicAxisTwistGeneratedCostNativeHypothesesTarget (native hypotheses plus generated cross-equation) and feeds PRCNativeCostUniquenessTarget_refuted by disagreeing with the canonical cost on a two-three prime composite direction. Within the Recognition forcing picture this is a foundation-level uniqueness obstruction for the native cost before J-uniqueness (T5) and the RCL are locked; it shows which calibration axioms are load-bearing rather than optional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.