Source-Cutset Inclusion-Minimal Hitting Duality

Abstract

Source cuts are exactly the hitting sets of the canonical family of inclusion-minimal proof supports, with equal minimum cardinalities.

Theorem 1.1 (Source cuts and canonical minimal-support hitting sets coincide).

$$\begin{array}{c}\forall Source:\mathrm{Type},P:\mathrm{Finset}\left(Source\right)\to Prop,\\ \mathrm{Fintype}\left(Source\right)\wedge \mathrm{DecidableEq}\left(Source\right)\wedge \mathrm{Monotone}\left(P\right)\Rightarrow \\ \mathrm{let}hitsEveryInclusionMinimalSupport:=\lambda H:\mathrm{Finset}\left(Source\right),\forall S:\mathrm{Finset}\left(Source\right),\mathrm{InclusionMinimalSupport}\left(P,S\right)\Rightarrow \mathrm{Nonempty}\left(\mathrm{inter}\left(H,S\right)\right)\\ \mathrm{in}(\forall H:\mathrm{Finset}\left(Source\right),\mathrm{IsSourceCut}\left(P,H\right)⟺\mathrm{hitsEveryInclusionMinimalSupport}\left(H\right))\wedge \\ \mathrm{proofResilience}\left(P\right)=\mathrm{sInf}\left(\{n:\mathbb{N}\mid \exists H:\mathrm{Finset}\left(Source\right),\mathrm{hitsEveryInclusionMinimalSupport}\left(H\right)\wedge \mathrm{card}\left(H\right)=n\}\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Provenance/SourceCutsetInclusionMinimalHittingDuality.source_cutset_inclusion_minimal_hitting_duality (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite source carrier, decidable equality, and monotone provability predicate are explicit premises. InclusionMinimalSupport is imported from the canonical dependency-support family.

The displayed local predicate expands hitting every canonical minimal support. It is not identified with the cut predicate: the equivalence is inherited from the frozen source-cutset theorem through the exact alpha-equivalence of the old and canonical support predicates.

Proof resilience retains its independent frozen definition as the least source-cut cardinality. The second conjunct identifies it with the natural infimum of cardinalities satisfying the displayed hitting predicate.

References

• Truth anchor: D5/S3/ConceptDynamics/Provenance/SourceCutsetInclusionMinimalHittingDuality.source_cutset_inclusion_minimal_hitting_duality
• Dependency: D5/S3/ConceptDynamics/DagCompletion/MinimalDependencySupport
• Dependency: D5/S3/ConceptDynamics/Provenance/SourceCutsetHittingDuality