PRCSignReversingNativeCostUniquenessTarget
plain-language theorem explainer
Packages the uniqueness claim that any map on ratio orbits obeying the sign-reversing native-cost hypotheses agrees with the canonical on-orbit cost under cross-equality. Round-4 ledger work cites this Prop as the statement discharged by the terminal uniqueness theorem. Definitional packaging only: the body is the quantified implication, with no proof content.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the sign-reversing native-cost hypotheses, then for every ratio orbit $q$, $F(q)$ is cross-equal to the canonical on-orbit image of $q$.
background
In the Primitive Recognition Calculus structural ledger, native cost is the recognition cost carried by ratio data, ultimately the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) from the forcing chain. Observer and multiplicative-recognizer layers already identify event cost with that J-cost or a derived comparator cost on positive ratios.
Ratio orbits are the equivalence classes on which the ledger compares costs. Cross-equality is the ledger's identification relation between orbits; the canonical on-orbit map is the reference native cost on those classes. Sign-reversing native-cost hypotheses encode the structural constraints (including sign-reversal and calibration-style conditions) that a candidate cost map $F$ must obey.
This module sits after the minimality-certificate import and collects Prop targets for uniqueness of that native cost under successively stronger ledger assumptions.
proof idea
Definitional Prop only: the right-hand side is the universal statement that every $F$ satisfying the sign-reversing native-cost hypotheses is pointwise cross-equal to the canonical on-orbit map. No tactics, no lemmas applied at this declaration. The companion theorem discharges the Prop by reducing to the zero-calibrated signed-strengthened uniqueness target and supplying the strengthened hypothesis bundle from the sign-reversing package.
why it matters
This is the statement object for Round 4 of the PRC native-cost structural ledger: the sign-reversing ledger is claimed to force the canonical cost. The sole immediate consumer is the terminal theorem that proves the target, by refining through the zero-calibrated signed-strengthened uniqueness result and packing the sign-reversing hypotheses into the strengthened bundle.
In framework terms it is a ledger-level uniqueness interface toward J-uniqueness (T5): once sign-reversal and native-cost structure pin the orbit map to the canonical on-orbit cost, competing cost functionals are excluded at the PRC layer before constants and mass-ladder work. It does not itself invoke RCL or the eight-tick/D=3 steps; it only freezes the cost representative those later steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.