PRCCharacterOrbitProductLocalOrientationPropagates
plain-language theorem explainer
Product-factor propagation of local orientation for a ratio-orbit character: if two nonunit nonzero factors are each identity- or reciprocal-oriented, their product is oriented the same way. Anyone lifting prime-axis orientation to composite orbits cites this Prop. It is a pure definition packaging the multiplicative closure step, not a proved theorem.
Claim. A map $\chi$ from ratio orbits to ratio orbits has product-local orientation propagation when, for all nonzero nonunit $a,b,p$ in the distinction naturals with $a\cdot b=p$, if each of $a$ and $b$ is locally oriented (either $\chi$ fixes the orbit direction of the factor, or sends it to its reciprocal), then $p$ is likewise locally oriented.
background
The ambient setting is native cost uniqueness in the Primitive Recognition Calculus: characters on ratio orbits must be forced into the unique cost shape compatible with the doubled-trace d'Alembert law. A ratio orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). Distinction naturals are the base-neutral finite orbits of repeated distinction (K2.12); the only multiplicative unit among them is the one-step orbit.
Local orientation at a nonzero orbit direction $p$ means the character either fixes that direction (identity orientation: cross-equality of $\chi$ on the direction with the direction itself) or sends it to its reciprocal. Those two predicates extend orientation beyond prime axes so that trace transport can pass through composite positions.
The present definition packages the exact multiplicative step that carries orientation from factors to products. Downstream targets ask whether prime calibration forces this propagation, and whether it plus prime-local orientation yields full nonunit local orientation.
proof idea
Definition only: the body is a single universal Prop. It quantifies over nonzero nonunit distinction-nats $a,b,p$ with $a\cdot b=p$, assumes each factor satisfies identity-or-reciprocal local orientation under $\chi$, and concludes the same disjunction for the product. No tactics or lemmas are invoked; the named orientation predicates are the identity and reciprocal direction props already defined in-module.
why it matters
This is the multiplicative bridge from prime-axis orientation to composite orbit directions inside the native-cost uniqueness program. Downstream, nonunit local orientation is recovered from prime-local orientation plus this propagation hypothesis. A companion theorem derives the propagation itself from display-compatibility and a no-mixed-orientation hypothesis on the character.
It appears as the conclusion of the sharper target "prime calibration forces nonunit orbit product-local orientation," and is invoked when reducing the coherent-orientation target under a product no-mixed hypothesis. The Pass-25 blocker certificate lists the remaining open factorization and calibration targets that still separate the development from a closed uniqueness theorem; this Prop is one of the exact Lean interfaces those targets must discharge.
In the broader Recognition chain it supports uniqueness of the native cost (the J-cost shape forced at T5), by ensuring character orientation is coherent on the full multiplicative monoid of orbits rather than only on primes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.