Manuscript VIII-A@3 · VIII-A-v3.tex · proposition · 2398a747
Proposition: Affected-output reevaluation
The finite admissibility contract › Four rule types · lines 885–900 · proof included or linked
VIII-A@3#A:prop:complete-output
If an update changes an argument of an obligation in (E1)–(E5), that obligation and all other affected checks must be reevaluated on the output. An incompatible input certificate does not certify the new data.
Proof. Acceptance verifies evaluated output equalities and output realization requirements. An input equality with changed arguments is not the required output equality. If incompatible old values are retained, the corresponding output equality fails. Unaffected witnesses may be reused only when they still verify the same obligation.