Finite Anchor Coverage

Abstract

Finite bounded test families have bounded coverage and admit exact off-union evasion.

Theorem 1.1 (Finite anchor coverage bound and evasion).

$$\forall A,X[\mathrm{Fintype}(A)][\mathrm{DecidableEq}(X)],S:A\to \mathrm{Finset}(X),t:X\to \mathrm{Bool},h,m\in \mathbb{N},\mathrm{card}(A)\le 2^h\wedge (\forall a,\mathrm{card}(S(a))\le m)\Rightarrow \mathrm{card}(\mathrm{coveredInputs}(S))\le 2^h\cdot m\wedge \exists p:X\to \mathrm{Bool},(\forall a,x,x\in S(a)\Rightarrow p(x)=t(x))\wedge \{x\mid p(x)\ne t(x)\}=X\setminus \mathrm{coveredInputs}(S).$$

Proof. Machine-checked in Lean as D5/S3/ResourceOrder/FiniteAnchorCoverage.finite_anchor_coverage_bound_and_evasion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite anchor type represents all possible revealed seeds. The first hypothesis bounds its size by two to the anchor budget, and the second bounds every exposed suite by m inputs. Finset.card_biUnion_le then gives the displayed two-to-h times m coverage bound.

The witness implementation agrees with the truth on the union of all possible suites and flips the Boolean truth everywhere else. It therefore passes every suite while its error set is exactly the uncovered complement.

This is a partial closure of the leading finite-coverage clause only. The covering-number and logarithmic consequences, the nonatomic-domain clause, and the random-family sufficiency clause remain unresolved.

Pinned Mathlib supplies Finset.card_biUnion_le. Repository searches found no complete theorem combining that bound with the off-union implementation and exact error-set identity.

References

• Truth anchor: D5/S3/ResourceOrder/FiniteAnchorCoverage.finite_anchor_coverage_bound_and_evasion