Partial Tests Leave a Defect

Abstract

Partial tests can pass while a disjoint nonempty defect set remains.

Theorem 1.1 (Passing partial tests can leave a defect).

$$\begin{gathered} \exists covered,defects:\mathrm{Set}\left(Bool\right), \\ \mathrm{Nonempty}\left(covered\right)\wedge \mathrm{Nonempty}\left(defects\right)\wedge \\ \mathrm{Disjoint}\left(covered,defects\right)\wedge \forall candidate\in Bool,candidate\in covered\Rightarrow \neg candidate\in defects. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Audits/PartialTestsLeaveDefect.passing_partial_tests_can_leave_a_defect (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Boolean countermodel uses one covered set and one defect set throughout. Both are nonempty, they are disjoint, and every covered candidate is absent from the defect set.

Consequently the same construction witnesses both successful tests and a surviving defect; no completeness certificate is assumed.

Pinned Mathlib singleton and disjointness lemmas discharge the four public clauses directly. The Lean module introduces no definition.

References

• Truth anchor: D5/S3/ConceptDynamics/Audits/PartialTestsLeaveDefect.passing_partial_tests_can_leave_a_defect