PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget
plain-language theorem explainer
Names the claim that every prime-calibrated ratio character automatically has reciprocal branch transport on all nonunit directions: if one nonunit orbit is reciprocal-oriented, every nonunit orbit is. Cost-uniqueness and d'Alembert factorization work cite it as one half of the two-way nonunit transport pair. It is a pure Prop abbreviation (universal quantification over characters), not a proved theorem; a sibling later refutes it.
Claim. For every map $\chi$ from ratio orbits to ratio orbits: if $\chi$ is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and is prime-direction calibrated (its induced cost matches canonical $J$-cost on every prime orbit), then $\chi$ has nonunit reciprocal branch transport (reciprocal orientation at one nonunit direction forces reciprocal orientation at every nonunit direction).
background
In the Primitive Recognition Calculus, costs factor through ratio characters on RatioOrbit (integer numerator over nonzero orbit denominator). A ratio character $\chi$ is unit-fixing and multiplicative up to cross-equivalence, so the factorization stays quotient-native rather than definitionally equal.
Prime-direction calibration means the cost built from $\chi$ agrees with the canonical $J$-cost on every prime orbit direction. Reciprocal branch transport is the dual half of nonunit coherence: if one nonunit orbit direction is reciprocal-oriented under $\chi$, every nonunit direction is. Pass 57 isolates this dual half from two-branch agreement.
This module packages uniqueness and forcing targets for native PRC costs. The present declaration is only the named Prop for the reciprocal half of the prime-calibration transport claim.
proof idea
No proof: the body is a definitional expansion of a Prop. It universally quantifies over maps $\chi$, assumes the ratio-character structure and prime-direction calibration, and concludes nonunit reciprocal branch transport. Downstream, one theorem discharges the target from full nonunit branch agreement by applying the corresponding character-level transport lemma; another theorem refutes the target outright via a two-adic axis-twist counterexample character.
why it matters
This is one conjunct of the split pair target for the two one-way nonunit branch transports (identity and reciprocal). The pair feeds the historical open-target ledger in the universal foundation certificate, which tracks which forcing routes close and which are refuted.
Within Recognition Science, native cost uniqueness and the d'Alembert route to the unique $J$-cost (forcing chain T5) need coherent orientation of characters across nonunit directions. Naming the reciprocal half separately lets the development prove, weaken, or refute each orientation independently. The sibling refutation shows prime calibration alone does not force reciprocal transport, so stronger hypotheses (full branch agreement, or a repaired interface) are required for that surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.