PRCSlimSansTwoCalibrationUniquenessTarget
plain-language theorem explainer
Packages the uniqueness claim for cost maps that obey the slim-ledger axioms with the two-point calibration dropped: every such map must match the canonical rational J-cost on every ratio orbit (via cross-equivalence). The minimality certificate cites this Prop only to refute it, proving the two-point anchor is necessary. Pure definition of a quantified Prop; no proof content.
Claim. Every map $F$ from ratio orbits to ratio orbits that satisfies the slim-ledger hypotheses without the two-point calibration obeys, for every ratio orbit $q$, the cross-multiplication equivalence $F(q)\sim J(q)$, where $J(q)=((q+q^{-1})/2)-1$ is the canonical rational J-cost on ratio orbits.
background
In the Primitive Recognition Calculus (PRC), rationals are carried as RatioOrbit objects: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of two such displays is internal cross-multiplication balance (crossEq): the scaled numerators match as signed orbits. The canonical cost on this type is the ratio-orbit J-object $J(q)=((q+q^{-1})/2)-1$, built from orbit arithmetic (add, recip, half, sub), not from real analysis.
The slim ledger is the native-cost uniqueness package for PRC. Its calibration fields can be stripped one at a time. The sans-two class keeps the other slim hypotheses but drops the two-point anchor (the requirement that pins the cost at the orbit 2). The present definition is exactly the uniqueness target for that stripped class: every $F$ meeting those weaker hypotheses should still equal $J$ everywhere under crossEq.
Upstream, the J-cost on ratio orbits and the cross-equivalence relation are already defined; the monotone d'Alembert and functional-equation layers supply the broader uniqueness context that the slim ledger specializes.
proof idea
Definition only: the body is the quantified proposition $\forall F,;(\text{sans-two slim hypotheses on }F)\Rightarrow\forall q,; F(q)\mathrel{\mathrm{crossEq}} J(q)$. No tactics, no lemmas applied. Downstream theorems treat this Prop as a claim to refute or as a named field in a certificate structure.
why it matters
This target is the formal statement that gets killed to prove two-point-anchor necessity. Downstream, PRCSlimSansTwoCalibrationUniquenessTarget_refuted shows $\neg$ of this Prop by feeding the Liouville-twist impostor (which satisfies the sans-two hypotheses) and checking it fails to match $J$ at the orbit 2. That negation is then recorded as the field two_point_anchor_necessary inside SlimLedgerMinimalityCertificate, whose doc states that each of the slim ledger's four removable calibration fields is necessary because dropping any one admits a kernel-checked impostor.
In the broader RS chain this sits under T5 J-uniqueness: the ledger forces the same $J(x)=(x+x^{-1})/2-1$ that the forcing chain isolates, and the certificate shows you cannot drop the two-point pin without losing uniqueness. The bridging comment on the module notes that the slim ledger is exactly the sans-two class plus the two-point anchor, so the refutation is a necessity statement about the slim ledger's own field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.