Finite Defect Termination

Abstract

Strict defect removal on a finite carrier stops within the initial defect count.

Theorem 1.1 (Finite strict defect repair terminates).

$$\begin{gathered} \forall W:\mathrm{Type},defects:Nat\to \mathrm{Set}(W), \\ (\mathrm{Finite}(W)\wedge \\ (\forall n:Nat,\mathrm{defects}(n)\ne \varnothing \Rightarrow \mathrm{defects}(n+1)\ne \mathrm{defects}(n))\wedge \\ (\forall n:Nat,\mathrm{defects}(n+1)\subseteq \mathrm{defects}(n)))\Rightarrow \\ \exists n:Nat,n\le \mathrm{ncard}(\mathrm{defects}(0))\wedge \mathrm{defects}(n)=\varnothing . \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Termination/FiniteDefectTermination.finite_defect_repairs_terminate (✓ std3). ∎

Source. Repository-derived.

Commentary.

The defect sequence is an independent source primitive on the finite carrier. Its initial set determines the public stopping bound.

Strict change while defects remain and no-new-defects inclusion are separate public premises; together they give proper set descent.

Strict inclusion lowers finite set cardinality at every nonterminal step. After at most the initial cardinality, zero cardinality forces the defect set to be empty.

References

• Truth anchor: D5/S3/ConceptDynamics/Termination/FiniteDefectTermination.finite_defect_repairs_terminate