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

Abstract

Fix Cook--Nguyen's two-sorted language \(L_{FP}\), its universal theory \(VPV\), and named \(L_{FP}\)-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 \(\Pi^B_1(L_{FP})\) and \(\Pi^B_2(L_{FP})\). 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 \(\mathbf{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.