A Witness Logic for Semantic Composition

Abstract

Classical program logics make local correctness compositional under a stable semantic frame. Open autonomous systems break that assumption: components satisfying their local contracts can produce globally incoherent behavior because the semantic frame itself fails to glue across interfaces. Working over the category of semantic interface complexes — finite diagrams of local semantic carriers with observable projections and latent seam dimensions — we state six natural axioms for an obstruction invariant and prove that, in the exact regime, the unique invariant satisfying them is the witness rank, equal to the dimension of the first cohomology of the seam complex. Consequences: a repair duality identifying minimum disclosure cardinality with the obstruction invariant; a disclosure normal form exhibiting every coherence certificate as a typed disclosure derivation; and a communication lower bound showing that protocols whose transcript carries fewer independent declarations than the witness rank cannot soundly certify coherence.