PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget
plain-language theorem explainer
Packages the uniqueness claim for the slim native-cost ledger: any F on ratio orbits obeying base axioms plus prime-pair products, signed unit, and zero-orbit calibration must match the canonical J-cost under cross-multiplication at every orbit. Cited by the slim cost-selection package and the field-by-field minimality certificate. The body is a Prop quantifier, not a proof; discharge lives in the companion proved theorem.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the slim native-cost hypotheses (signed strengthened base plus zero-orbit calibration of the doubled trace), then for every ratio orbit $q$ one has cross-multiplication equivalence $F(q) \sim J(q)$, where $J(q) = \frac{q+q^{-1}}{2}-1$ is the canonical cost on ratio orbits.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator (the internal rational display). Two ratio orbits are cross-equivalent when scaled numerators balance as signed orbits; that is the PRC stand-in for rational equality.
The canonical cost on a ratio orbit is the orbit-level J-object $J(q)=((q+q^{-1})/2)-1$. The slim hypothesis class drops the all-prime axis field from the round-1 ledger: it keeps reciprocity, normalization invariance, nonzero RCL, unit-zero, and two-calibration, then adds prime-pair products, a signed unit, and zero-orbit calibration of the doubled trace.
This module packages native-cost selection and minimality for that slim ledger. The uniqueness target is the Prop that every F in the slim class is pointwise cross-equivalent to canonical J.
proof idea
Definition of a Prop, not a proved theorem. The body is a universal quantifier: for all F, slim hypotheses on F imply that for all ratio orbits q, F(q) is crossEq to onRatioOrbit q (canonical J). No tactics or lemmas fire here; discharge is deferred to the companion theorem, which factors through character factorization, transfers pair and sign fields, recovers per-prime calibration from the pair field plus base two-calibration, and closes by signed-admissible rigidity.
why it matters
This is the uniqueness half of the slim native cost-selection package (prereg j-free minimality): every native cost on the slim ledger is forced to canonical J. The companion proved theorem discharges it under the slogan that the slim ledger already forces J. Downstream, CostSelectionPackageNativeSlim records j_unique_native_slim as this target plus a non-vacuous witness, and SlimLedgerMinimalityCertificate uses it as slim_uniqueness while proving each removable calibration field is necessary via impostors.
In the broader framework this is the PRC-native route to T5 J-uniqueness (J(x)=(x+x^{-1})/2-1) without the all-prime axis field, tightening the ledger that selects the Recognition Composition Law cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.