Fixed-Function Exact Semantic Carrier Conditions over VPV: Internal Invariants and External Representation Theorems

Fix Cook--Nguyen's two-sorted language \(LFP\), its universal theory \(VPV\), and named \(LFP\)-functions for admittedness, response, preparation, carrier coding, decoding, and dynamics. With the instance string as a free parameter, we give bounded formulas for response soundness and response separation, display their fully expanded length-guard forms, and verify that the bounded formulas are respectively \(Π^B_1(LFP)\) and \(Π^B_2(LFP)\). Over \(VPV\) augmented by the universal closures of these fixed-carrier assumptions, carrier equality is a complete invariant of equality of Full Admitted Response. In the standard two-sorted structure, the admitted-state carrier image presents the external response quotient. Fibre-constant semantics factor uniquely through the history-realized carrier image, whereas response-compatible dynamics descend uniquely to the admitted-state carrier image. For fixed named functions, explicit sections or direct translations yield \(VPV\)-definable decoders, descended dynamics, and carrier translations. We also state an external polynomial-time pipeline normal form: a language has such a fixed, polynomially bounded carrier pipeline exactly when it belongs to \(P\). This is a representation sanity check obtained by unpacking the pipeline definition, not a new complexity characterization. Uniform quantification over machine or pipeline codes is not formalized here and requires a separate arithmetized development.