PRCNativeCostUniquenessTarget_refuted
plain-language theorem explainer
The base native-cost hypotheses do not force a unique recognition cost. A two-adic axis twist yields a second native cost that matches the canonical orbit cost on primes yet disagrees on a 2–3 composite direction. Anyone citing the continuum price residue wall or the native-cost selection ledgers needs this refutation. The proof chains ratio-orbit cross-equations from the twist character into the known J-cost mismatch on mixed versus composite images.
Claim. The native-cost uniqueness target is false: it is not the case that every cost satisfying the base native hypotheses (reciprocity, normalization invariance, canonical recognition composition on nonzero orbits, unit-zero, and two-calibration) agrees with the canonical ratio-orbit cost on every direction.
background
In the Primitive Recognition Calculus, a native cost is a real-valued function on positive ratio orbits obeying a short list of structural axioms: reciprocity, normalization invariance, the Recognition Composition Law (RCL) on nonzero orbits, vanishing at the unit, and a two-point calibration. The canonical choice is the orbit restriction of the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), the unique continuous solution forced later in the T5 step of the unified forcing chain.
The uniqueness target asserts that those base axioms already pin the cost down to the canonical orbit cost. The two-adic generated native cost is a competing construction: it is built from a ratio character that twists the 2-adic axis, so on a composite direction assembled from the primes 2 and 3 it lands on a mixed image rather than the pure composite image. Cost-from-character turns that character into a genuine native cost still satisfying the older hypothesis pack.
Cross-equation on ratio orbits is the pointwise agreement relation used throughout the module; the mismatch lemma records that the canonical J-cost separates the mixed 2–3 image from the pure composite image.
proof idea
Assume the uniqueness target. Instantiate it on the two-adic generated native cost (with its verified native hypotheses) at the 2–3 prime composite direction; uniqueness forces that cost to be cross-equal to the canonical orbit cost there.
Separately, the generated-cost cross-equation lemma identifies the two-adic generated cost with the cost induced by the two-adic axis-twist character. The twist character sends the composite direction to the mixed 2–3 direction, so cost-from-character of the twist is cross-equal (via orbit congruence) to the canonical cost on the mixed direction.
Transitivity and symmetry of cross-equation then force the canonical costs on the mixed and composite directions to agree. The prime-orbit mismatch lemma for the 3-orbit contradicts that agreement, discharging the assumption.
why it matters
This is the necessity half of the native-cost selection story: the base hypothesis pack is strictly too weak. Downstream, continuumPriceResidueWall_holds records it as base_insufficient, and both the full and slim native-cost selection premise ledgers cite it under the base strength claim (“Necessity: two-adic axis twist”). The companion blocker certificate in the same module packages related factorization refutations.
In framework terms it sits upstream of T5 J-uniqueness. RCL plus continuity and positivity force $J$, but the discrete native axioms alone admit a two-adic monodromy. The repair path (flagged in the module) is to demand canonicity already on products of native prime directions, exactly the surface where the twist slips through. Until that strengthening is imposed, continuum price residue and native-cost minimality cannot claim uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.