Domain Immunization Audit

Abstract

Target-dependent domain restriction can erase admitted defects while deleting empirical states.

Theorem 1.1 (Domain immunization requires deletion and dependence audits).

$$\begin{array}{c}(\forall X,B,Y:\mathrm{Type},[\mathrm{Finite}\left(X\right)],\\ C:X\to B,T:X\to Y,\\ \mathrm{Nonempty}\left(\mathrm{Defect}\left(C,T\right)\right)\Rightarrow \exists z:X\times X,\exists A:\mathrm{Set}\left(X\right),\\ z\in \mathrm{Defect}\left(C,T\right)\wedge A=\mathrm{singleton}\left(\mathrm{fst}\left(z\right)\right)\wedge \\ \mathrm{Defect}\left(\mathrm{restrict}\left(C,A\right),\mathrm{restrict}\left(T,A\right)\right)=\varnothing \wedge \mathrm{ncard}\left(A\right)=1\wedge \\ \mathrm{ncard}\left(\mathrm{compl}\left(A\right)\right)=\mathrm{NatCard}\left(X\right)-1)\wedge \\ (Czero=\mathrm{constant}\left(unit\right),Tzero=id,Azero=\{x\mid Tzero(x)=false\}:\\ \mathrm{Nonempty}\left(\mathrm{Defect}\left(Czero,Tzero\right)\right)\wedge \mathrm{Defect}\left(\mathrm{restrict}\left(Czero,Azero\right),\mathrm{restrict}\left(Tzero,Azero\right)\right)=\varnothing \wedge \\ \mathrm{ncard}\left(Azero\right)=1\wedge \mathrm{ncard}\left(\mathrm{compl}\left(Azero\right)\right)=1\wedge \\ \forall x:Bool,x\in Azero⟺Tzero(x)=false)\wedge \\ (\forall S:\mathrm{Type},E:\mathbb{N}\to \mathrm{Set}\left(S\right),\\ \mathrm{Monotone}\left(E\right)\Rightarrow \exists M:\mathbb{N}\to \mathrm{Set}\left(S\right),\\ (\forall n,M(n)=\mathrm{compl}\left(E(n)\right))\wedge \mathrm{Antitone}\left(M\right)\wedge \\ (\forall n,\mathrm{inter}\left(M(n),E(n)\right)=\varnothing )\wedge \\ (\forall n,E(n)\subset E(n+1)\Rightarrow M(n+1)\subset M(n))).\end{array}$$

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

Source. Repository-derived.

Commentary.

For every defective readout on a finite state carrier, a witnessed target collision selects a singleton admitted domain. The restricted readout has empty target defect, and the displayed complement count records exactly how many states were deleted.

The Boolean clause is the required contrast model: the constant readout has a full-domain target defect, while the target-defined one-state domain has none. Both retained and deleted counts are explicit.

For a cumulative family of counterexamples, the admitted domains are their complements. They remain disjoint from all current counterexamples, are antitone, and shrink strictly whenever the counterexample set grows strictly.

References

• Truth anchor: D5/S3/ConceptDynamics/Audits/DomainImmunizationAudit.domain_immunization_audit
• Dependency: D5/S3/ConceptDynamics/TargetRisk/RefinementRiskCostTradeoff