Target-Conditioned Admission Audit

Abstract

Target-conditioned admission can erase defects only by deleting states.

Theorem 1.1 (Restricted closure records deletion and target dependence).

$$\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,\\ z\in \mathrm{Defect}\left(C,T\right)\wedge \mathrm{Defect}\left(\mathrm{restrict}\left(C,\mathrm{singleton}\left(\mathrm{fst}\left(z\right)\right)\right),\mathrm{restrict}\left(T,\mathrm{singleton}\left(\mathrm{fst}\left(z\right)\right)\right)\right)=\varnothing \wedge 0<\mathrm{ncard}\left(\mathrm{compl}\left(\mathrm{singleton}\left(\mathrm{fst}\left(z\right)\right)\right)\right))\wedge \\ (C_0:Bool\to Unit=\mathrm{constant}\left(unit\right),\\ A:(Bool\to Bool)\to \mathrm{Set}\left(Bool\right),A(U)=\{x\mid U(x)=false\}:\\ \mathrm{Nonempty}\left(\mathrm{Defect}\left(C_0,id\right)\right)\wedge \mathrm{Defect}\left(\mathrm{restrict}\left(C_0,A(id)\right),\mathrm{restrict}\left(id,A(id)\right)\right)=\varnothing \wedge \\ A(id)\ne A(not)\wedge \mathrm{ncard}\left(\mathrm{compl}\left(A(id)\right)\right)=1)\wedge \\ (\forall S:\mathrm{Type},M:\mathbb{N}\to \mathrm{Set}\left(S\right),e:\mathbb{N}\to S,\\ (\forall n,e(n)\in M(n))\Rightarrow \\ (\forall n,M(n+1)=\mathrm{diff}\left(M(n),\mathrm{singleton}\left(e(n)\right)\right))\Rightarrow \\ \forall n,\neg (e(n)\in M(n+1))\wedge M(n+1)\subset M(n)).\end{array}$$

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

Source. Repository-derived.

Commentary.

A target collision supplies two distinct states. Restricting both channels to the singleton containing the first state removes all target defects, but the complement has positive cardinality.

In the Boolean contrast, the readout stays constant. Its whole-domain defect is nonempty, its target-conditioned singleton domain has no defect, and changing the target from identity to negation changes the admitted set.

The final clause takes admission domains as independent inputs. When an admitted counterexample is removed at each update, that state is absent at the next stage and the domain shrinks strictly.

References

• Truth anchor: D5/S3/ConceptDynamics/Audits/TargetConditionedAdmissionAudit.target_conditioned_admission_audit
• Dependency: D5/S3/ConceptDynamics/TargetRisk/RefinementRiskCostTradeoff