PRCSlimSansPairUniquenessTarget_refuted
plain-language theorem explainer
Uniqueness fails for native costs that keep base, signed-unit, and zero calibration but drop the pair field. Anyone citing pair-field necessity in the slim-ledger minimality certificate needs this refutation. The proof feeds the two-adic twist (which inhabits the sans-pair class) into the uniqueness hypothesis and recovers a contradiction with its known failure on mixed prime-pair products.
Claim. The uniqueness target for the sans-pair class is false: it is not the case that every map $F$ on ratio orbits that satisfies the slim hypotheses without the pair field agrees with the canonical on-orbit cost under cross-equality for every ratio orbit $q$.
background
In the primitive recognition calculus, costs act on RatioOrbit displays: an integer numerator over a nonzero orbit denominator. The canonical cost is the on-orbit J-display. A uniqueness target asserts that every map $F$ obeying a listed hypothesis package agrees with that canonical display under cross-equality.
The sans-pair package keeps the base native-cost axioms, signed-unit calibration, and zero calibration, but omits the pair field (calibration on products of distinct prime directions). The two-adic generated native cost is already known to satisfy exactly those remaining hypotheses.
The parent uniqueness module shows that same two-adic twist fails prime-pair product calibration at mixed orbits such as $(2,3)$. That failure is the lever for the refutation.
proof idea
Assume the sans-pair uniqueness target. Apply the known lemma that the two-adic generated native cost is not calibrated on prime-pair products. For arbitrary native primes $p,r$, instantiate the uniqueness hypothesis at the two-adic cost, using the theorem that it satisfies the sans-pair hypotheses, on the product of the two prime directions. The resulting cross-equality would force pair-product calibration, contradicting the parent non-calibration lemma. Hence the uniqueness target is false.
why it matters
This is the pair-field necessity half of the slim-ledger story: base + sign + zero alone are too weak, because the two-adic twist still fits and breaks uniqueness. Downstream, slimLedgerMinimalityCertificate_holds and the tagged deltaOnly deposit assemble the full certificate from uniqueness of the strengthened package plus the various necessity refutations (pair field among them).
In Recognition terms this is ledger hygiene on the discrete ratio-orbit carrier: the cost that will later match J-uniqueness (T5) and feed the forcing chain cannot shed the pair axiom without admitting a non-canonical two-adic competitor. No continuum, completed carrier, or continuity premise enters; the witnesses stay arithmetic on RatioOrbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.