Who Paid for the Schema? Honest Amortized Interpolation Complexity of Reusable Reasoning Languages

Representation design can appear to simplify reasoning by hiding computation in an encoder or in newly introduced schema symbols. We define honest amortized interpolation complexity (HAIC) for families of propositional entailment tasks. Every shared intermediate gate must factor through the canonical semantic interface common to all tasks using it. We prove an exact library--adapter normal form and a capacity theorem: semantic HAIC lower-bounds a fractional cover of the task-interface hypergraph, equal by LP duality to a task-price packing. This yields exact direct sums for disjoint interfaces and a sharp $1/d$ law under maximum overlap $d$. For proof-certified schemas, recursive interpolation signatures give the unique minimum-weight coherent refinement of a fixed proof bundle; executing each normalized state once produces an honest multi-output separator with overhead $\kappa$. Hence proof HAIC is at least $\kappa^{-1}$ times semantic HAIC and its packing bound. McMillan interpolation combined with clique--colouring monotone-circuit lower bounds gives unconditional overlap-sensitive lower bounds for batched Resolution reasoning. The theory is invariant under typed renaming and extends to charged translations, approximation, and public randomization.