Multi-Target Defect Graph Coloring

Abstract

Joint-target defect graphs are component unions, with chromatic minimum repair.

Theorem 1.1 (Joint defect graph union and minimum repair labels).

$$\begin{array}{c}\forall X,Index,Current:\mathrm{Type},\\ Target:Index\to \mathrm{Type},\\ [\mathrm{Fintype}(X)],\\ current:\mathrm{Concept}\left(X,Current\right),\\ targets:(\forall index:Index,\mathrm{Concept}\left(X,Target(index)\right)),\\ (\mathrm{defectGraph}\left(current,\mathrm{jointTarget}\left(targets\right)\right)=\mathrm{iSup}\left(index:Index,\mathrm{defectGraph}\left(current,targets(index)\right)\right))\wedge \\ (\mathrm{minimumRepairLabels}\left(current,\mathrm{jointTarget}\left(targets\right)\right)=\mathrm{chromaticNumber}\left(\mathrm{iSup}\left(index:Index,\mathrm{defectGraph}\left(current,targets(index)\right)\right)\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GraphColoring/MultiTargetDefectGraphColoring.joint_target_defect_graph_and_minimum_labels (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite state carrier, the canonical defect graph of a dependent joint target is the indexed supremum of the component defect graphs.

The same graph equality identifies the least number of finite repair labels with the chromatic number of that indexed supremum.

References

• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/MultiTargetDefectGraphColoring.joint_target_defect_graph_and_minimum_labels
• Dependency: D5/S3/ConceptDynamics/GraphColoring/DefectRelationMinimumColoring
• Dependency: D5/S3/ConceptDynamics/ObservationTopology/MultiTargetObservationTopology