PRCCharacterMixedNonunitWitnessesReflectPrimeWitnessesSplit
plain-language theorem explainer
A ratio-orbit character satisfies mixed nonunit reflection in split form exactly when both the identity-branch half and the reciprocal-branch half hold. Anyone proving two-branch agreement or native cost uniqueness cites this packaging. It is a pure definitional conjunction of the two already-isolated half-laws.
Claim. For a map $\chi$ sending ratio orbits to ratio orbits, the split mixed-nonunit reflection property holds when both of the following are true: under a mixed nonunit witness antecedent, every identity-oriented nonunit witness reflects to an identity-oriented prime-axis witness; and under the same antecedent, every reciprocal-oriented nonunit witness reflects to a reciprocal-oriented prime-axis witness.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Characters here are maps $\chi$ on ratio orbits used to build native cost from doubled-trace data and to match the J-cost calculus.
Mixed nonunit witnesses are nonunit orbit directions that appear together with both identity and reciprocal orientations in the same context. The identity half-law says that, given such a mixed antecedent, an identity-oriented nonunit witness must pull back to an identity-oriented prime-axis witness. The reciprocal half-law is the dual statement for reciprocal orientation (the reciprocal automorphism swaps source and target and inverts the ratio).
This module isolates native cost uniqueness blockers. The split form packages the two half-laws as a single Prop so later certificates and iff lemmas can name one object rather than two separate antecedents.
proof idea
Definitional abbreviation only: the Prop is the conjunction of the identity-half reflection law and the reciprocal-half reflection law applied to the same character $\chi$. No tactics, no lemmas beyond naming those two sibling Props.
why it matters
Native cost uniqueness is the PRC route toward J-uniqueness (forcing-chain T5: $J(x)=(x+x^{-1})/2-1$). Two-branch agreement on nonunit orbits is a coherence gate on that route: identity and reciprocal orientations must both reflect cleanly onto the prime axis under mixed antecedents.
Downstream, the unsplit reflection law is equivalent to this split form via a pair of one-direction theorems (split-of-reflects and reflects-of-split) and their iff packaging. The pass-25 blocker certificate also names this split object among the exact Lean targets that remain open, so closing native cost uniqueness tracks progress against this Prop rather than an opaque bundle.
Pass 57 isolates the reciprocal branch as the dual half of two-branch agreement; this definition is the bookkeeping hinge that keeps both halves visible in certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.