Minimum Audit Set Cover

Abstract

Minimum target-complete audit suites are minimum defect set covers.

Theorem 1.1 (Minimum complete audit suites are minimum defect covers).

$$\forall X\in Type,C\in Type,T\in Type,I\in Type,O\in I\to Type,c\in X\to C,t\in X\to T,q\in \forall i:I,X\to O\left(i\right),J\in \mathrm{Finset}\left(I\right),\mathrm{let}Complete(K:\mathrm{Finset}\left(I\right)):=\forall x\in X,y\in X,(c\left(x\right),\mathrm{jointReadout}\left(\mathrm{restrict}\left(q,K\right),x\right))=(c\left(y\right),\mathrm{jointReadout}\left(\mathrm{restrict}\left(q,K\right),y\right))\Rightarrow t\left(x\right)=t\left(y\right);\mathrm{let}Covers(K:\mathrm{Finset}\left(I\right)):=\mathrm{Union}\left(i\in K,\left\{q\left(i\right)\left(\mathrm{fst}\left(p\right)\right)\ne q\left(i\right)\left(\mathrm{snd}\left(p\right)\right)\mid p\in \mathrm{defectRelation}\left(c,t\right)\right\}\right)=\mathrm{defectRelation}\left(c,t\right);\left(\mathrm{Complete}\left(J\right)\wedge \left(\forall L\in \mathrm{Finset}\left(I\right),\mathrm{Complete}\left(L\right)\Rightarrow \mathrm{card}\left(J\right)\le \mathrm{card}\left(L\right)\right)\right)\iff \left(\mathrm{Covers}\left(J\right)\wedge \left(\forall L\in \mathrm{Finset}\left(I\right),\mathrm{Covers}\left(L\right)\Rightarrow \mathrm{card}\left(J\right)\le \mathrm{card}\left(L\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The current and target concepts construct the canonical defect relation. Each test covers exactly the defects on which its response differs.

Completeness is stated on the canonical joint readout of a selected finite suite. The theorem transports both feasibility and cardinality comparison against every candidate suite, so no optimizer is assumed to exist.

References

• Truth anchor: D5/S3/ConceptDynamics/Audits/MinimumAuditSetCover.minimum_audit_set_is_set_cover
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion
• Dependency: D5/S3/ConceptDynamics/TargetRisk/RefinementRiskCostTradeoff