Finite Escape Pairs

Abstract

Finite indistinguishable pairs split into persistent and theorem-unique escape.

Definition 1.1 (Selected escape pairs).

$$\mathrm{escapePairs}(C,S)=\mathrm{filter}(\mathrm{offDiagonalPairs}(X),\lambda p,\mathrm{indistinguishable}(C,S,p1,p2)).$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs (✓ std3).

Source. Repository-derived.

Commentary.

This executable finite-set definition uses the catalog’s decidable kernels.

Definition 1.2 (Unique capture pairs).

$$\mathrm{uniqueCapturePairs}(C,i)=\mathrm{filter}(\mathrm{escapePairs}(C,\mathrm{without}(C,i)),\lambda p,\neg \mathrm{agrees}(\mathrm{theoremAt}(C,i),p1,p2)).$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/EscapePairs.uniqueCapturePairs (✓ std3).

Source. Repository-derived.

Commentary.

This executable finite-set definition uses the catalog’s decidable kernels.

Theorem 1.3 (Unique capture is finite difference).

$$\mathrm{uniqueCapturePairs}(C,i)=\mathrm{escapePairs}(C,\mathrm{without}(C,i))\setminus \mathrm{escapePairs}(C,\mathrm{fullIndexSet}(C)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/EscapePairs.uniqueCapturePairs_eq_sdiff (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof reuses the canonical finite catalog kernel and Mathlib Finset laws.

Theorem 1.4 (Escape pairs are antitone).

$$S\subseteq T\Rightarrow \mathrm{escapePairs}(C,T)\subseteq \mathrm{escapePairs}(C,S).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs_anti (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof reuses the canonical finite catalog kernel and Mathlib Finset laws.

Theorem 1.5 (Insertion filters escape pairs).

$$\mathrm{escapePairs}(C,\mathrm{insert}(i,S))=\mathrm{filter}(\mathrm{escapePairs}(C,S),\lambda p,\mathrm{agrees}(\mathrm{theoremAt}(C,i),p1,p2)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs_insert (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof reuses the canonical finite catalog kernel and Mathlib Finset laws.

Theorem 1.6 (Full escape lies in leave-one-out escape).

$$\mathrm{escapePairs}(C,\mathrm{fullIndexSet}(C))\subseteq \mathrm{escapePairs}(C,\mathrm{without}(C,i)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs_full_subset_without (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof reuses the canonical finite catalog kernel and Mathlib Finset laws.

Theorem 1.7 (Leave-one-out escape decomposes).

$$\mathrm{escapePairs}(C,\mathrm{without}(C,i))=\mathrm{union}(\mathrm{escapePairs}(C,\mathrm{fullIndexSet}(C)),\mathrm{uniqueCapturePairs}(C,i)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs_without_eq_union (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof reuses the canonical finite catalog kernel and Mathlib Finset laws.

Theorem 1.8 (Persistent and unique escape are disjoint).

$$\mathrm{Disjoint}(\mathrm{escapePairs}(C,\mathrm{fullIndexSet}(C)),\mathrm{uniqueCapturePairs}(C,i)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs_full_disjoint_uniqueCapturePairs (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof reuses the canonical finite catalog kernel and Mathlib Finset laws.

References

• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs_anti
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs_full_disjoint_uniqueCapturePairs
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs_full_subset_without
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs_insert
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/EscapePairs.escapePairs_without_eq_union
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/EscapePairs.uniqueCapturePairs
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/EscapePairs.uniqueCapturePairs_eq_sdiff
• Dependency: D5/S3/ConceptDynamics/CIRPT/RoleSignature
• Dependency: D5/S3/ConceptDynamics/InformationEscape/CatalogKernel