PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted
plain-language theorem explainer
Zero-orbit calibration is irreducible for native cost uniqueness. Without it, the prime-signed strengthened ledger admits a zero-flat countermodel that meets every prime-signed condition yet disagrees with the canonical cost at the zero orbit (value 0 versus canonical $-1$). Anyone citing the continuum price residue wall or the native cost-selection ledger needs this refutation. The proof is a short counterexample: instantiate the uniqueness claim on the zero-flat cost at the zero orbit and reduce by rewriting plus `norm_num`.
Claim. The uniqueness target for native costs under the prime-signed strengthened ledger is false. Concretely: it is not the case that every native cost $C$ satisfying the base native hypotheses plus prime-pair products, signed unit, and all prime axes is cross-equation equal to the canonical ratio-orbit cost at every point of the ratio orbit (in particular, uniqueness already fails at the zero orbit).
background
In the Primitive Recognition Calculus, a native cost is a real-valued assignment on the countable carrier RatioOrbit obeying reciprocity, normalization invariance, the Recognition Composition Law (RCL) on nonzero orbits, unit-zero, and two-point calibration. The canonical selection is the restriction of the unique $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) to that orbit.
The parent uniqueness program asks how much of a countable calibration ledger is needed before every native cost is forced to agree with that canonical restriction under cross-equation equality. Strengthened ledgers add prime-pair products, a signed unit condition, and all prime axes. The zero orbit is special: the canonical cost evaluates to $-1$ there, so any ledger that omits an explicit zero-orbit pin leaves room for a flat-zero impostor.
This module is the $\delta$-native counterpart of the public cost-selection package: it isolates which algebraic conditions on the countable carrier actually buy uniqueness, without continuum completion or continuity.
proof idea
Assume the uniqueness target $h$. Instantiate $h$ on the zero-flat native cost, using the sibling fact that this cost satisfies the full prime-signed strengthened hypothesis package, and evaluate at the zero point of the ratio orbit.
Rewrite the resulting equality with the zero-flat evaluation lemma (value $0$), the characterization of cross-equation equality via rationalization, the rationalization of the zero orbit point, and the canonical-on-orbit evaluation at zero. The goal collapses to a pure numerical falsehood ($0=-1$), discharged by norm_num.
No induction or RCL propagation is required: the countermodel already lives inside the strengthened class and fails only at the omitted zero pin.
why it matters
This is one of the three insufficiency legs of the continuum price residue wall: that wall records that base uniqueness, strengthened uniqueness, and prime-signed strengthened uniqueness are all refuted, so every prime-axis orientation remains free until further calibration is deposited. Downstream, the native cost-selection premise ledger cites the pattern of these refutations to justify why the full ledger must include a zero-orbit clause (and why each clause is tagged $\delta$-only).
In framework terms the result sharpens T5 $J$-uniqueness: RCL alone, even with extensive prime-signed generator data, does not propagate to the zero orbit. The honest name for the eventual deposit is rigidity from an explicit countable calibration ledger, not an economical selector. The zero-orbit pin is therefore irreducible data, not a cosmetic normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.