PRCSignedStrengthenedNativeCostUniquenessTarget_refuted
plain-language theorem explainer
The signed-strengthened native-cost uniqueness target is false. Under base reciprocity, pair axioms, and signed unit (no zero-orbit field), the zero-flat cost is an admissible countermodel: every hypothesis lives on nonzero orbits, yet the cost fails the forced identity at the zero ratio orbit. Slim-ledger and minimality-certificate results cite this refutation. Proof is a direct countermodel plug-in plus algebraic rewrite and norm_num.
Claim. Uniqueness of the native recognition cost under the signed-strengthened ledger is false. That ledger comprises reciprocity, normalization invariance, the canonical recognition composition law on nonzero ratio orbits, unit-zero, and two-calibration, without a zero-orbit field. The constantly-zero (zero-flat) cost satisfies every such hypothesis, yet at the zero ratio orbit it disagrees with the identity required by uniqueness (equivalently, the cross-equality after passage to rationals fails numerically).
background
Primitive Recognition Calculus selects a native cost on ratio orbits. The classical J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) is the unique continuous solution of the Recognition Composition Law on positive reals; here the same selection problem is posed at the discrete PRC ledger level.
The signed-strengthened package is the base native-cost hypotheses plus pair axioms and a signed unit condition, deliberately omitting any zero-orbit calibration field. All of its constraints quantify over nonzero orbits, so a cost that is identically zero can still meet them. The zero ratio orbit is the degenerate orbit whose rational representative is $0$; cross-equality of costs on orbits reduces, after toRat, to ordinary equality of real values.
Upstream cost constructions (multiplicative-recognizer derived cost, rung-coarsen weighted sums, observer forcing) supply the ambient language of native costs; the present lemma only needs the zero-flat inhabitant and the signed-strengthened hypothesis bundle attached to it.
proof idea
Assume the uniqueness target $h$. Instantiate $h$ at the zero-flat native cost, using the bundled fact that this cost satisfies the prime signed-strengthened hypotheses, and evaluate at the zero ratio orbit. Rewrite the resulting equality with the lemmas that (i) zero-flat evaluates to $0$, (ii) orbit cross-equality is equivalent to equality of toRat images, and (iii) the zero orbit and the on-orbit embedding both send to rational $0$. The rewritten goal is a false numerical identity, discharged by norm_num.
why it matters
This is the explicit refutation that forces the slim deposit to keep a two-point (or zero) calibration anchor. Downstream, nativeCostSelectionSlimPremiseLedger records the necessity note that uniqueness fails without that anchor (two-adic axis twist / zero-flat countermodel), and nativeCostSelectionSlimPremiseLedger_all_deltaOnly keeps the contracted ledger at the $\delta$-only strength floor.
The immediate corollary PRCSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget_refuted lifts the same countermodel: character-generated costs are canonical at the zero orbit, so zero-flat cannot factor through a signed-admissible character. The certificate theorem slimLedgerMinimalityCertificate_holds pairs the positive uniqueness result under zero-calibration with the matching necessity refutations, closing the minimality story for the slim native-cost selection.
In the broader forcing chain this is bookkeeping around T5 J-uniqueness: the continuous J-cost is unique, but the discrete ledger must name enough axioms (including a zero/two-point field) before that uniqueness descends.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.