PRCCharacterNonunitBranchTransportPair
plain-language theorem explainer
Packages nonunit two-branch agreement as the conjunction of identity-branch transport and reciprocal-branch transport for a ratio-orbit character χ. Cited wherever branch agreement is rewritten as a pair of one-way transport laws. The body is a pure definitional ∧ of the two transport props.
Claim. For a map $\chi$ from ratio orbits to ratio orbits, the nonunit branch-transport pair holds when both of the following are true: (i) if any nonunit orbit direction is identity-oriented under $\chi$, then every nonunit orbit direction is identity-oriented; (ii) if any nonunit orbit direction is reciprocal-oriented under $\chi$, then every nonunit orbit direction is reciprocal-oriented.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator: the discrete display of a positive rational scale. A character $\chi$ acts on ratio orbits and may orient each nonunit direction either toward the identity event (the J-cost minimum at state $1$) or toward its reciprocal.
Identity-branch transport says that a single nonunit identity orientation forces every other nonunit direction to be identity-oriented. Reciprocal-branch transport is the dual statement for reciprocal orientation. The module isolates these as the two halves of nonunit coherence (Pass 57 for the reciprocal half).
The local setting is native-cost uniqueness: characters that match the doubled-trace cost must not mix identity and reciprocal branches on nonunit orbits. Packaging the two transports as one Prop makes that no-mixing law interchangeable with a split transport form.
proof idea
Definitional abbreviation only: the predicate is the conjunction of the identity-branch transport Prop and the reciprocal-branch transport Prop on the same character $\chi$. No tactics, no lemmas applied at the definition site.
why it matters
Gives the split-transport face of two-branch agreement used throughout the native-cost uniqueness development. Downstream, branch agreement is proved equivalent to this pair, each direction is recovered from the pair, and coherence of nonunit orbit orientation implies the pair. The pair also appears among the exact Lean targets named by the Pass-25 native-cost uniqueness blocker certificate, which records that uniqueness is not closed but the missing mathematics is split into named obligations.
In the broader forcing chain this sits under J-uniqueness (T5): characters feeding the native cost must obey the Recognition Composition Law branch structure, so identity and reciprocal orientations cannot mix on nonunit orbits. The packaging lets later proofs discharge agreement by transporting one known orientation rather than quantifying over all pairs at once.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.