PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_of_prime_pair_product_cost_consistency
plain-language theorem explainer
From prime-pair product cost consistency under prime calibration, the orbit-2 reciprocal exclusion follows: no identity-oriented native prime witness may coexist with a reciprocal-oriented 2-axis. Character-rigidity arguments in the primitive recognition calculus cite this bridge. The proof is a pure two-step composition through the mixed 2*p composite consistency intermediate.
Claim. Assume that every ratio character that is prime-direction calibrated has cost consistency on the product of any two native prime directions. Then every such character also satisfies the exclusion: if the orbit-$2$ prime axis is reciprocal-oriented, no identity-oriented native prime witness exists.
background
In the primitive recognition calculus, a ratio character $\chi$ assigns an orbit map on ratio orbits. Prime-direction calibration fixes the cost of each native prime direction. The product-calibration target asks that this calibration propagate to products of any two such directions: the cost of $\mathrm{mul}(\mathrm{primeDirection},p,\mathrm{primeDirection},r)$ must match the character-derived cross-equation surface.
The mixed composite surface specializing one factor to the orbit-$2$ prime is the current branch-rigidity blocker. The exclusion target is the two-specific statement that a reciprocal orientation on the orbit-$2$ axis forbids any identity-oriented native prime witness. The module builds a chain of Prop-targets that turn product consistency into that exclusion.
Upstream, the pair-product target specializes immediately to the $2*p$ mixed composite target, and a direct lemma already converts mixed composite consistency into the reciprocal-exclusion target.
proof idea
Term-mode composition of two prior results. First apply the specialization lemma that turns the full prime-pair product consistency hypothesis into mixed composite consistency on the orbit-$2$ factor times an arbitrary native prime. Feed that intermediate into the direct lemma that converts mixed composite cost consistency into the reciprocal-excludes-identity-witness target. No new case analysis is performed here.
why it matters
Closes one link in the native-cost uniqueness chain: product-level prime calibration implies the orbit-$2$ mixed-witness exclusion that blocks non-rigid character branches. Downstream it is consumed by the conditional universal-foundation certificate in UniversalFoundation, which packages kernel, real-complete ordered field, and trace-logic certificates into a single PRC foundation bundle. Within the Recognition forcing picture this is local algebraic rigidity on prime directions, not yet the global T5 J-uniqueness or T6 $\varphi$ fixed-point step, but it is part of the cost-character uniqueness route those landmarks presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.