all_prime_axis_field_redundant
plain-language theorem explainer
Any native cost on ratio orbits that meets the slim ledger (base axioms, prime-pair products, signed unit, zero-orbit calibration) is automatically calibrated on every native prime axis. Cost-selection and uniqueness arguments cite this to drop the all-prime field from the hypothesis package. The proof is a one-line specialization of slim-ledger uniqueness to prime directions.
Claim. Let $F$ map ratio orbits to ratio orbits. If $F$ satisfies the slim native-cost hypotheses (signed strengthened ledger plus zero-orbit calibration of the doubled trace), then $F$ is prime-direction calibrated: for every native prime orbit $p$, $F$ agrees with the canonical $J$-cost on the associated prime direction.
background
Native costs act on ratio orbits: each orbit is an integer numerator over a nonzero distinction-nat denominator. The canonical cost is the $J$-cost from the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$, forced unique in the T5 step of the forcing chain.
The slim hypothesis class packages reciprocity, normalization invariance, nonzero RCL, unit-zero, two-calibration, prime-pair products, signed unit, and zero-orbit calibration of the doubled trace. It deliberately omits the all-prime axis field that would demand calibration on every native prime direction by hand.
Prime-direction calibration asserts that $F$ agrees with canonical $J$ on each primeDirection orbit. Upstream uniqueness already shows the slim ledger forces $J$ everywhere; the present result records the prime-axis special case needed to equate slim and full ledgers.
proof idea
One-line term wrapper. The goal is prime-direction calibration of $F$, i.e. agreement with canonical $J$ at every primeDirection p hp. Apply the already-proved slim uniqueness target (PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved) to $F$, the slim hypotheses, and that prime direction. Uniqueness supplies the required cross-equality, so the all-prime field is recovered rather than assumed.
why it matters
This is the redundancy lemma that lets the framework drop the all-prime axis field from the native-cost ledger. Downstream, slim_class_iff_full_class uses it to prove the slim ledger and the round-1 minted ledger carve out the same class of native costs; the contracted selection ledger then stays at the $\delta$-only floor (nativeCostSelectionSlimPremiseLedger_all_deltaOnly).
In the broader RS picture this is a bookkeeping win for T5 $J$-uniqueness: once base axioms, pair products, sign, and zero calibration are in place, per-prime calibration is free. No new physics is claimed; the gain is a strictly smaller hypothesis surface for every later uniqueness or selection argument that quotes the slim class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.