PRCSlimSansTwoCalibrationUniquenessTarget_refuted
plain-language theorem explainer
Without the two-point calibration at orbit 2, the slim native-cost field is not unique: the Liouville twist satisfies every remaining axiom yet disagrees with the canonical J-display at 2. Anyone citing two-point-anchor necessity for the slim ledger minimality certificate needs this refutation. The proof is a short contradiction: uniqueness applied to the twist yields canonicity at 2, which the twist explicitly fails.
Claim. The uniqueness claim for the slim native-cost class without two-point calibration is false: it is not the case that every map $F$ on ratio orbits obeying the slim-sans-two hypotheses agrees with the canonical $J$-display $q \mapsto \mathrm{onRatioOrbit}(q)$ at every orbit $q$.
background
In the Primitive Recognition Calculus, native cost is a field $F$ on ratio orbits meant to reproduce the canonical $J$-display (the RS cost $J(x)=(x+x^{-1})/2-1$ packaged on orbits). The slim ledger packages a minimal axiom set for that field. The two-point calibration (anchor) forces agreement with the canonical display at the distinguished orbit $2$.
Dropping that anchor yields the sans-two class PRCSlimSansTwoCalibrationHypotheses. Its uniqueness target asserts that every such $F$ still coincides with the canonical display everywhere. The Liouville twist is a competing field: on each orbit it displays $J(\mathrm{liouvilleSign}(t)\cdot t)$, with the unit orbit sent to the exact-zero representative. Upstream, that twist is shown to meet every slim axiom except the two-point anchor, and at orbit $2$ it returns $J(-2)=-9/4$ rather than the canonical $J(2)=1/4$.
proof idea
Term-mode contradiction. Assume the uniqueness target. Instantiate it at the Liouville-twisted native cost, using the theorem that this twist satisfies all slim-sans-two hypotheses, and evaluate at the orbit $2$. Uniqueness would force the twist to be cross-equal to the canonical display at $2$. That contradicts the explicit non-canonicity lemma, which reduces via toRat equalities and norm_num to $-9/4 \neq 1/4$. Hence the uniqueness target is false.
why it matters
This is the necessity half of the slim ledger story: uniqueness of the native cost on the slim package requires the two-point anchor; without it the Liouville twist is a concrete counter-model. Downstream, slimLedgerMinimalityCertificate_holds records the fact as two_point_anchor_necessary, and the tagged deposit slim_ledger_minimality_certificate_tagged exposes the full certificate under the deltaOnly strength tag (discrete RatioOrbit arithmetic, no continuum premises).
In the broader RS forcing chain this protects T5-style $J$-uniqueness at the ledger level: the Recognition Composition Law and the canonical $J$ are not recovered from the slim base alone; the calibration at $2$ is an indispensable pin. The companion uniqueness theorems for the fully calibrated slim field sit on the other side of the same certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.