Verification Collision Contract Incompleteness

Abstract

A verification interface cannot implement an ideal obligation that varies inside one verification fiber.

Theorem 1.1 (Unverifiable states make exact contracts incomplete).

$$\begin{array}{c}\forall State,Verification,Obligation:\mathrm{Type},\\ V:State\to Verification,O:State\to Obligation,x,y:State,\\ V(x)=V(y)\wedge O(x)\ne O(y)\Rightarrow \\ \neg \exists c:Verification\to Obligation,O=c\circ V.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Contracts/VerificationCollisionContractIncompleteness.verification_collision_contract_incomplete (✓ std3). ∎

Source. Repository-derived.

Commentary.

The public primitives are a state verification map V and an ideal obligation map O. A verifiable contract is a function on the verification output.

If x and y have the same verification output, every contract assigns them the same implemented obligation. That equality contradicts the supplied inequality between their ideal obligations.

The result formalizes an interface limitation rather than a missing contract clause: no function of the available verification output can equal O on every state.

The proof directly applies the arbitrary-carrier factorization half of the existing informed-disclosure theorem.

References

• Truth anchor: D5/S3/ConceptDynamics/Contracts/VerificationCollisionContractIncompleteness.verification_collision_contract_incomplete
• Dependency: D5/S0/Rewriting/Quotients/InformedDisclosureDefect