Theorem: Presentation independence after actual descent

Suppose labelled coefficient prescriptions descend to maps on the named actual-functional spaces and are consistent on their specified overlaps. Then their values are unchanged by any rewriting that preserves their arguments as actual off-shell polynomial functionals. This includes finite linear presentation relations, kernel permutations, tensor symmetries, polarization identities, and integration by parts with all boundary terms retained.

Proof. A descended map assigns a value to the actual arguments, not to their labels. Any equality-preserving rewriting leaves those arguments unchanged. Equivalently, the difference of two presentations lies in the relevant kernel of a presentation map and is annihilated by the descent condition. Overlap consistency ensures the same statement if the rewriting moves between two named prescriptions.