One-Way Permutations and the Conditional Unprovability of Exact Semantic Carrier Separation in PV

The Exact Semantic Carrier condition EC1b requires a distinguishing admitted query whenever two carrier codes differ. We study this requirement in a fixed conservative definitional extension of Cook's universal theory \(PV\). A width \(n\) is represented by a supplied marker \(M=2^n\), so admitted state and query codes are bounded by the \(LPV\)-term \(M\); no exponentiation from a binary-coded security parameter occurs. For a uniformly polynomial-time, length-preserving permutation family, a named evaluation function induces the preimage-membership response map, and the identity carrier is full-response exact in the standard model. We give a normalized separation sentence whose matrix is open after expansion of its bounded existential. Relative Herbrand witnessing for the fixed universal presentation \(PV_f\) yields finitely many terms; a fixed first-success selector combines them into a deterministic \(FP\) separator whose output is provably within the admitted width. Calling that separator on both orders of an independent challenge--comparison pair gives a probabilistic inverter with success probability at least \(1/2+2⁻ⁿ⁻¹\). Hence a one-way permutation family makes the true normalized separation sentence unprovable in the fixed universal presentation \(PV_f\). The conclusion is conditional and construction-specific; no transfer to another response model is claimed without an explicit reduction.