PRCSlimSansSignUniquenessTarget_refuted
plain-language theorem explainer
Uniqueness of the native cost fails if the signed-unit field is dropped from the slim hypothesis package. The absolute-value cost satisfies base, pairs, and zero calibration, yet disagrees with the canonical cost at the orbit of $-1$. Anyone assembling the slim ledger minimality certificate cites this necessity step. The proof is a direct contradiction: feed that witness into the uniqueness target and invoke the known failure at $-1$.
Claim. It is false that every map $F$ on ratio orbits obeying the slim hypotheses without the signed-unit field is cross-equal to the canonical native cost on every orbit. Equivalently: base, pairs, and zero calibration alone do not force $F(q)\simeq$ the canonical cost for all $q$.
background
In the Primitive Recognition Calculus, costs are maps on ratio orbits. The canonical native cost is the orbit-level display of the RS $J$-cost. Cross-equality is the discrete identity relation used to compare two such displays.
The slim package is a minimal axiom set for uniqueness. The sans-sign fragment keeps the strengthened base and pair axioms plus zero calibration, and drops the signed-unit field. Its uniqueness target asserts that every $F$ in that fragment agrees with the canonical cost everywhere.
The parent uniqueness module already builds the absolute-value generated cost (fold the absolute character through the cost-from-character construction) and proves it fails cross-equality at the orbit of $-1$. A sibling lemma records that this same absolute-value cost inhabits the sans-sign class.
proof idea
Term-mode contradiction. Assume the sans-sign uniqueness target. Instantiate it at the absolute-value generated cost, using the sibling theorem that this cost satisfies the sans-sign hypotheses, and evaluate at the orbit of $-1$. The resulting cross-equality contradicts the parent lemma that the absolute-value cost is not canonical at $-1$. Discharge.
why it matters
This is the signed-unit necessity half of the slim ledger story: base, pairs, and zero are not enough; the sign field cannot be omitted if uniqueness is required. Downstream it feeds slimLedgerMinimalityCertificate_holds and the tagged public-spine deposit slim_ledger_minimality_certificate_tagged (deltaOnly strength: discrete ratio-orbit arithmetic, no continuum premises).
In the broader Recognition framework this protects the identification of the native cost with the unique $J$-display forced by the Recognition Composition Law and T5 $J$-uniqueness. Without a signed unit, an absolute-value impostor survives the remaining axioms and breaks canonicity at $-1$, so the ledger certificate must retain the sign field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.