Conservative Channel Addition

Abstract

Every deadlocked repair class can be added as an exact conservative channel.

Theorem 1.1 (A conservative channel exists for every deadlocked repair class).

$$\begin{array}{r}\forall Repair:\mathrm{Type},\\ \forall repairClass,allo{w}_1,allo{w}_2:Set(Repair),\\ \\ Deadlocked(repairClass,allo{w}_1,allo{w}_2)\Rightarrow \\ \exists channel:Set(Repair),\\ \\ ConservativeChannel(repairClass,allo{w}_1,allo{w}_2,channel).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GovernanceFixedPoint/ConservativeChannelAddition.conservative_channel_exists (✓ std3). ∎

Source. Repository-derived.

Commentary.

The explicit channel is the repair class itself. Deadlock makes that class disjoint from the old joint allowance, so adjoining the channel preserves every old allowance and adds exactly the repair class.

References

• Truth anchor: D5/S3/ConceptDynamics/GovernanceFixedPoint/ConservativeChannelAddition.conservative_channel_exists
• Dependency: D5/S3/ConceptDynamics/GovernanceFixedPoint/DualRuleDeadlockCriterion