SolidResolvingTournamentProfiles

Abstract

SolidResolvingTournamentProfiles

Theorem 1.1 (card le of chain cover).

$$\forall U\in Type,\forall P\in Type,[\mathrm{Fintype}\left(U\right)][\mathrm{Preorder}\left(P\right)]\forall f\in \left(U\right)\to \left(P\right),\forall m\in \mathrm{Nat},\forall chains\in \left(\mathrm{Fin}\left(m\right)\right)\to \left(\mathrm{Set}\left(P\right)\right),\left(\forall u\in U,\exists i\in \mathrm{Fin}\left(m\right),\left(f\right)\left(u\right)\in \left(chains\right)\left(i\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(m\right),\forall a\in P,\forall b\in P,a\in \left(chains\right)\left(i\right)\Rightarrow \left(b\in \left(chains\right)\left(i\right)\Rightarrow \left(a\le b\vee b\le a\right)\right)\right)\Rightarrow \left(\left(\forall a\in U,\forall b\in U,a\ne b\Rightarrow \left(\neg \left(\left(f\right)\left(a\right)\le \left(f\right)\left(b\right)\right)\wedge \neg \left(\left(f\right)\left(b\right)\le \left(f\right)\left(a\right)\right)\right)\right)\Rightarrow \mathrm{Fintype}.\mathrm{card}\left(U\right)\le m\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.card_le_of_chain_cover (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assigning an incomparable element to a chain containing its image is injective. Therefore the number of elements is at most the number of covering chains.

Theorem 1.2 (profile finite bound).

$$\forall k\in \mathrm{Nat},\forall R\in \mathrm{Nat},\forall D\in \left(\mathrm{Fin}\left(k\right)\right)\to \left(\left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Nat}\right)\right),\left(\forall i\in \mathrm{Fin}\left(k\right),\forall j\in \mathrm{Fin}\left(k\right),\left(D\right)\left(i,j\right)\le R\right)\Rightarrow \left(\mathrm{Fin}\left(k\right)\right)\to \left(\forall x\in \left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{ENat}\right),\left(\forall j\in \mathrm{Fin}\left(k\right),\exists i\in \mathrm{Fin}\left(k\right),\left(x\right)\left(i\right)<\left(fun\left(i:\mathrm{Fin}\left(k\right)\right)\mapsto fun\left(j:\mathrm{Fin}\left(k\right)\right)\mapsto \left(\left(D\right)\left(i,j\right):\mathrm{ENat}\right)\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(k\right),\forall j\in \mathrm{Fin}\left(k\right),\left(x\right)\left(i\right)\le \left(fun\left(i:\mathrm{Fin}\left(k\right)\right)\mapsto fun\left(j:\mathrm{Fin}\left(k\right)\right)\mapsto \left(\left(D\right)\left(i,j\right):\mathrm{ENat}\right)\right)\left(i,j\right)+\left(x\right)\left(j\right)\right)\Rightarrow \left(\exists y\in \left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Nat}\right),\left(\forall i\in \mathrm{Fin}\left(k\right),\left(\left(y\right)\left(i\right):\mathrm{ENat}\right)=\left(x\right)\left(i\right)\right)\wedge \left(\forall i\in \mathrm{Fin}\left(k\right),\left(y\right)\left(i\right)\le 2\cdot R-1\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.profile_finite_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

One strict column inequality makes one coordinate finite; the triangle inequalities then make every coordinate finite and at most twice R minus one.

Definition 1.3 (D32).

$$\left(D32:\left(\mathrm{Fin}\left(3\right)\right)\to \left(\left(\mathrm{Fin}\left(3\right)\right)\to \left(\mathrm{Nat}\right)\right)\right)=![![0,2,1],![1,0,2],![2,1,0]]$$

Formalization. D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D32 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed concrete matrix gives directed distance upper-bound codes for the representative landmark tournament. Code eight denotes infinity when upperOfCode is applied.

Theorem 1.4 (nat profile bound 3 2).

$$\forall x\in \left(\mathrm{Fin}\left(3\right)\right)\to \left(\mathrm{Nat}\right),\left(\forall i\in \mathrm{Fin}\left(3\right),1\le \left(x\right)\left(i\right)\right)\Rightarrow \left(\left(\forall j\in \mathrm{Fin}\left(3\right),\exists i\in \mathrm{Fin}\left(3\right),\left(x\right)\left(i\right)<\left(D32\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(3\right),\forall j\in \mathrm{Fin}\left(3\right),\left(x\right)\left(i\right)\le \left(D32\right)\left(i,j\right)+\left(x\right)\left(j\right)\right)\Rightarrow \left(\forall i\in \mathrm{Fin}\left(3\right),\left(x\right)\left(i\right)\le 2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_3_2 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The necessary inequalities for an outside distance profile force every coordinate to be at most two.

Definition 1.5 (D44).

$$\left(D44:\left(\mathrm{Fin}\left(4\right)\right)\to \left(\left(\mathrm{Fin}\left(4\right)\right)\to \left(\mathrm{Nat}\right)\right)\right)=![![0,2,2,1],![1,0,3,2],![1,1,0,2],![2,1,1,0]]$$

Formalization. D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D44 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed concrete matrix gives directed distance upper-bound codes for the representative landmark tournament. Code eight denotes infinity when upperOfCode is applied.

Theorem 1.6 (nat profile bound 4 4).

$$\forall x\in \left(\mathrm{Fin}\left(4\right)\right)\to \left(\mathrm{Nat}\right),\left(\forall i\in \mathrm{Fin}\left(4\right),1\le \left(x\right)\left(i\right)\right)\Rightarrow \left(\left(\forall j\in \mathrm{Fin}\left(4\right),\exists i\in \mathrm{Fin}\left(4\right),\left(x\right)\left(i\right)<\left(D44\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(4\right),\forall j\in \mathrm{Fin}\left(4\right),\left(x\right)\left(i\right)\le \left(D44\right)\left(i,j\right)+\left(x\right)\left(j\right)\right)\Rightarrow \left(\forall i\in \mathrm{Fin}\left(4\right),\left(x\right)\left(i\right)\le 2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_4_4 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The necessary inequalities for an outside distance profile force every coordinate to be at most two.

Definition 1.7 (D58).

$$\left(D58:\left(\mathrm{Fin}\left(5\right)\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right)\right)=![![0,2,2,2,1],![1,0,3,3,2],![1,1,0,3,2],![1,1,1,0,2],![2,1,1,1,0]]$$

Formalization. D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D58 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed concrete matrix gives directed distance upper-bound codes for the representative landmark tournament. Code eight denotes infinity when upperOfCode is applied.

Theorem 1.8 (nat profile bound 5 8).

$$\forall x\in \left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right),\left(\forall i\in \mathrm{Fin}\left(5\right),1\le \left(x\right)\left(i\right)\right)\Rightarrow \left(\left(\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)<\left(D58\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le \left(D58\right)\left(i,j\right)+\left(x\right)\left(j\right)\right)\Rightarrow \left(\forall i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le 2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_8 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The necessary inequalities for an outside distance profile force every coordinate to be at most two.

Definition 1.9 (D510).

$$\left(D510:\left(\mathrm{Fin}\left(5\right)\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right)\right)=![![0,2,1,2,1],![1,0,2,3,2],![2,1,0,4,3],![1,1,1,0,2],![2,1,1,1,0]]$$

Formalization. D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D510 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed concrete matrix gives directed distance upper-bound codes for the representative landmark tournament. Code eight denotes infinity when upperOfCode is applied.

Theorem 1.10 (nat profile bound 5 10).

$$\forall x\in \left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right),\left(\forall i\in \mathrm{Fin}\left(5\right),1\le \left(x\right)\left(i\right)\right)\Rightarrow \left(\left(\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)<\left(D510\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le \left(D510\right)\left(i,j\right)+\left(x\right)\left(j\right)\right)\Rightarrow \left(\forall i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le 2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_10 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The necessary inequalities for an outside distance profile force every coordinate to be at most two.

Definition 1.11 (D512).

$$\left(D512:\left(\mathrm{Fin}\left(5\right)\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right)\right)=![![0,2,2,1,1],![1,0,3,2,2],![1,1,0,2,2],![2,1,1,0,3],![2,1,1,1,0]]$$

Formalization. D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D512 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed concrete matrix gives directed distance upper-bound codes for the representative landmark tournament. Code eight denotes infinity when upperOfCode is applied.

Theorem 1.12 (nat profile bound 5 12).

$$\forall x\in \left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right),\left(\forall i\in \mathrm{Fin}\left(5\right),1\le \left(x\right)\left(i\right)\right)\Rightarrow \left(\left(\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)<\left(D512\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le \left(D512\right)\left(i,j\right)+\left(x\right)\left(j\right)\right)\Rightarrow \left(\forall i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le 2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_12 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The necessary inequalities for an outside distance profile force every coordinate to be at most two.

Definition 1.13 (D540).

$$\left(D540:\left(\mathrm{Fin}\left(5\right)\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right)\right)=![![0,2,2,2,1],![1,0,2,1,2],![1,1,0,2,2],![1,2,1,0,2],![2,1,1,1,0]]$$

Formalization. D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D540 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed concrete matrix gives directed distance upper-bound codes for the representative landmark tournament. Code eight denotes infinity when upperOfCode is applied.

Theorem 1.14 (nat profile bound 5 40).

$$\forall x\in \left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right),\left(\forall i\in \mathrm{Fin}\left(5\right),1\le \left(x\right)\left(i\right)\right)\Rightarrow \left(\left(\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)<\left(D540\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le \left(D540\right)\left(i,j\right)+\left(x\right)\left(j\right)\right)\Rightarrow \left(\forall i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le 2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_40 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The necessary inequalities for an outside distance profile force every coordinate to be at most two.

Definition 1.15 (D541).

$$\left(D541:\left(\mathrm{Fin}\left(5\right)\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right)\right)=![![0,1,2,2,1],![2,0,2,1,3],![1,1,0,2,2],![1,2,1,0,2],![2,1,1,1,0]]$$

Formalization. D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D541 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed concrete matrix gives directed distance upper-bound codes for the representative landmark tournament. Code eight denotes infinity when upperOfCode is applied.

Theorem 1.16 (nat profile bound 5 41).

$$\forall x\in \left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right),\left(\forall i\in \mathrm{Fin}\left(5\right),1\le \left(x\right)\left(i\right)\right)\Rightarrow \left(\left(\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)<\left(D541\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le \left(D541\right)\left(i,j\right)+\left(x\right)\left(j\right)\right)\Rightarrow \left(\forall i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le 2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_41 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The necessary inequalities for an outside distance profile force every coordinate to be at most two.

Definition 1.17 (D576).

$$\left(D576:\left(\mathrm{Fin}\left(5\right)\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right)\right)=![![0,2,2,1,1],![1,0,2,2,1],![1,1,0,2,2],![2,1,1,0,2],![2,2,1,1,0]]$$

Formalization. D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D576 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed concrete matrix gives directed distance upper-bound codes for the representative landmark tournament. Code eight denotes infinity when upperOfCode is applied.

Theorem 1.18 (nat profile bound 5 76).

$$\forall x\in \left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right),\left(\forall i\in \mathrm{Fin}\left(5\right),1\le \left(x\right)\left(i\right)\right)\Rightarrow \left(\left(\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)<\left(D576\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le \left(D576\right)\left(i,j\right)+\left(x\right)\left(j\right)\right)\Rightarrow \left(\forall i\in \mathrm{Fin}\left(5\right),\left(x\right)\left(i\right)\le 2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_76 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The necessary inequalities for an outside distance profile force every coordinate to be at most two.

Definition 1.19 (acBool).

$$\forall k\in \mathrm{Nat},\forall b\in \mathrm{Nat},\forall D\in \left(\mathrm{Fin}\left(k\right)\right)\to \left(\left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Nat}\right)\right),\forall x\in \left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Fin}\left(b\right)\right),\mathrm{acBool}\left(D,x\right)=\mathrm{Bool}.\mathrm{and}\left(\mathrm{Bool}.\mathrm{and}\left(\mathrm{List}.\mathrm{all}\left(\mathrm{List}.\mathrm{finRange}\left(k\right),fun\left(i:\mathrm{Fin}\left(k\right)\right)\mapsto \mathrm{decide}\left(1\le \mathrm{val}\left(\left(x\right)\left(i\right)\right)\right)\right),\mathrm{List}.\mathrm{all}\left(\mathrm{List}.\mathrm{finRange}\left(k\right),fun\left(j:\mathrm{Fin}\left(k\right)\right)\mapsto \mathrm{List}.\mathrm{any}\left(\mathrm{List}.\mathrm{finRange}\left(k\right),fun\left(i:\mathrm{Fin}\left(k\right)\right)\mapsto \mathrm{decide}\left(\mathrm{val}\left(\left(x\right)\left(i\right)\right)<\left(D\right)\left(i,j\right)\right)\right)\right)\right),\mathrm{List}.\mathrm{all}\left(\mathrm{List}.\mathrm{finRange}\left(k\right),fun\left(i:\mathrm{Fin}\left(k\right)\right)\mapsto \mathrm{List}.\mathrm{all}\left(\mathrm{List}.\mathrm{finRange}\left(k\right),fun\left(j:\mathrm{Fin}\left(k\right)\right)\mapsto \mathrm{decide}\left(\mathrm{val}\left(\left(x\right)\left(i\right)\right)\le \left(D\right)\left(i,j\right)+\mathrm{val}\left(\left(x\right)\left(j\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.acBool (✓ std3).

Source. Repository-derived.

Commentary.

The Boolean test is the conjunction of positivity, a strict comparison in every landmark column, and every triangle upper bound.

Theorem 1.20 (profile mem of certificate).

$$\forall k\in \mathrm{Nat},\forall D\in \left(\mathrm{Fin}\left(k\right)\right)\to \left(\left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Nat}\right)\right),\forall ps\in \mathrm{List}\left(\left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Fin}\left(3\right)\right)\right),\mathrm{List}.\mathrm{all}\left(\mathrm{enumTuple}\left(\mathrm{List}.\mathrm{finRange}\left(3\right),k\right),fun\left(x:\left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Fin}\left(3\right)\right)\right)\mapsto \mathrm{Bool}.\mathrm{or}\left(\mathrm{Bool}.\mathrm{not}\left(\mathrm{acBool}\left(D,x\right)\right),\mathrm{decide}\left(x\in ps\right)\right)\right)=true\Rightarrow \left(\forall y\in \left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Nat}\right),\left(\forall i\in \mathrm{Fin}\left(k\right),\left(y\right)\left(i\right)<3\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(k\right),1\le \left(y\right)\left(i\right)\right)\Rightarrow \left(\left(\forall j\in \mathrm{Fin}\left(k\right),\exists i\in \mathrm{Fin}\left(k\right),\left(y\right)\left(i\right)<\left(D\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(k\right),\forall j\in \mathrm{Fin}\left(k\right),\left(y\right)\left(i\right)\le \left(D\right)\left(i,j\right)+\left(y\right)\left(j\right)\right)\Rightarrow \left(\exists x\in \left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Fin}\left(3\right)\right),\left(\forall i\in \mathrm{Fin}\left(k\right),\mathrm{val}\left(\left(x\right)\left(i\right)\right)=\left(y\right)\left(i\right)\right)\wedge x\in ps\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.profile_mem_of_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

A certificate listing all bounded positive profiles supplies a listed Fin-valued representative of every natural profile satisfying the same inequalities.

Theorem 1.21 (cardinal le profile chains).

$$\forall U\in Type,[\mathrm{Fintype}\left(U\right)]\forall k\in \mathrm{Nat},\forall f\in \left(U\right)\to \left(\left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Nat}\right)\right),\forall chains\in \mathrm{List}\left(\mathrm{List}\left(\left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Fin}\left(3\right)\right)\right)\right),\left(\forall u\in U,\exists z\in \left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Fin}\left(3\right)\right),\left(\forall j\in \mathrm{Fin}\left(k\right),\mathrm{val}\left(\left(z\right)\left(j\right)\right)=\left(f\right)\left(u,j\right)\right)\wedge z\in \mathrm{List}.\mathrm{flatten}\left(chains\right)\right)\Rightarrow \left(\left(\forall ch\in \mathrm{List}\left(\left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Fin}\left(3\right)\right)\right),ch\in chains\Rightarrow \left(\forall a\in \left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Fin}\left(3\right)\right),a\in ch\Rightarrow \left(\forall b\in \left(\mathrm{Fin}\left(k\right)\right)\to \left(\mathrm{Fin}\left(3\right)\right),b\in ch\Rightarrow \left(\left(\forall j\in \mathrm{Fin}\left(k\right),\mathrm{val}\left(\left(a\right)\left(j\right)\right)\le \mathrm{val}\left(\left(b\right)\left(j\right)\right)\right)\vee \left(\forall j\in \mathrm{Fin}\left(k\right),\mathrm{val}\left(\left(b\right)\left(j\right)\right)\le \mathrm{val}\left(\left(a\right)\left(j\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\left(\forall a\in U,\forall b\in U,a\ne b\Rightarrow \left(\neg \left(\left(f\right)\left(a\right)\le \left(f\right)\left(b\right)\right)\wedge \neg \left(\left(f\right)\left(b\right)\le \left(f\right)\left(a\right)\right)\right)\right)\Rightarrow \mathrm{Fintype}.\mathrm{card}\left(U\right)\le \mathrm{List}.\mathrm{length}\left(chains\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.cardinal_le_profile_chains (✓ std3). ∎

Source. Repository-derived.

Commentary.

A finite list of chains covering the natural profiles bounds the cardinality of any mutually incomparable family of those profiles.

Theorem 1.22 (strong profile antichain bound 3 2).

$$\forall U\in Type,[\mathrm{Fintype}\left(U\right)]\forall f\in \left(U\right)\to \left(\left(\mathrm{Fin}\left(3\right)\right)\to \left(\mathrm{Nat}\right)\right),\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(3\right),1\le \left(\left(f\right)\left(u\right)\right)\left(i\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall j\in \mathrm{Fin}\left(3\right),\exists i\in \mathrm{Fin}\left(3\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)<\left(D32\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(3\right),\forall j\in \mathrm{Fin}\left(3\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)\le \left(D32\right)\left(i,j\right)+\left(\left(f\right)\left(u\right)\right)\left(j\right)\right)\Rightarrow \left(\left(\forall a\in U,\forall b\in U,a\ne b\Rightarrow \left(\neg \left(\left(f\right)\left(a\right)\le \left(f\right)\left(b\right)\right)\wedge \neg \left(\left(f\right)\left(b\right)\le \left(f\right)\left(a\right)\right)\right)\right)\Rightarrow \mathrm{Fintype}.\mathrm{card}\left(U\right)\le 1\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_3_2 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite family of positive profiles satisfying the displayed inequalities and mutual incomparability has the stated cardinality bound. The finite chain cover is used after bounding every coordinate by two.

Theorem 1.23 (strong profile antichain bound 4 4).

$$\forall U\in Type,[\mathrm{Fintype}\left(U\right)]\forall f\in \left(U\right)\to \left(\left(\mathrm{Fin}\left(4\right)\right)\to \left(\mathrm{Nat}\right)\right),\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(4\right),1\le \left(\left(f\right)\left(u\right)\right)\left(i\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall j\in \mathrm{Fin}\left(4\right),\exists i\in \mathrm{Fin}\left(4\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)<\left(D44\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(4\right),\forall j\in \mathrm{Fin}\left(4\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)\le \left(D44\right)\left(i,j\right)+\left(\left(f\right)\left(u\right)\right)\left(j\right)\right)\Rightarrow \left(\left(\forall a\in U,\forall b\in U,a\ne b\Rightarrow \left(\neg \left(\left(f\right)\left(a\right)\le \left(f\right)\left(b\right)\right)\wedge \neg \left(\left(f\right)\left(b\right)\le \left(f\right)\left(a\right)\right)\right)\right)\Rightarrow \mathrm{Fintype}.\mathrm{card}\left(U\right)\le 2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_4_4 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite family of positive profiles satisfying the displayed inequalities and mutual incomparability has the stated cardinality bound. The finite chain cover is used after bounding every coordinate by two.

Theorem 1.24 (strong profile antichain bound 5 8).

$$\forall U\in Type,[\mathrm{Fintype}\left(U\right)]\forall f\in \left(U\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right),\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),1\le \left(\left(f\right)\left(u\right)\right)\left(i\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)<\left(D58\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)\le \left(D58\right)\left(i,j\right)+\left(\left(f\right)\left(u\right)\right)\left(j\right)\right)\Rightarrow \left(\left(\forall a\in U,\forall b\in U,a\ne b\Rightarrow \left(\neg \left(\left(f\right)\left(a\right)\le \left(f\right)\left(b\right)\right)\wedge \neg \left(\left(f\right)\left(b\right)\le \left(f\right)\left(a\right)\right)\right)\right)\Rightarrow \mathrm{Fintype}.\mathrm{card}\left(U\right)\le 5\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_8 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite family of positive profiles satisfying the displayed inequalities and mutual incomparability has the stated cardinality bound. The finite chain cover is used after bounding every coordinate by two.

Theorem 1.25 (strong profile antichain bound 5 10).

$$\forall U\in Type,[\mathrm{Fintype}\left(U\right)]\forall f\in \left(U\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right),\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),1\le \left(\left(f\right)\left(u\right)\right)\left(i\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)<\left(D510\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)\le \left(D510\right)\left(i,j\right)+\left(\left(f\right)\left(u\right)\right)\left(j\right)\right)\Rightarrow \left(\left(\forall a\in U,\forall b\in U,a\ne b\Rightarrow \left(\neg \left(\left(f\right)\left(a\right)\le \left(f\right)\left(b\right)\right)\wedge \neg \left(\left(f\right)\left(b\right)\le \left(f\right)\left(a\right)\right)\right)\right)\Rightarrow \mathrm{Fintype}.\mathrm{card}\left(U\right)\le 5\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_10 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite family of positive profiles satisfying the displayed inequalities and mutual incomparability has the stated cardinality bound. The finite chain cover is used after bounding every coordinate by two.

Theorem 1.26 (strong profile antichain bound 5 12).

$$\forall U\in Type,[\mathrm{Fintype}\left(U\right)]\forall f\in \left(U\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right),\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),1\le \left(\left(f\right)\left(u\right)\right)\left(i\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)<\left(D512\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)\le \left(D512\right)\left(i,j\right)+\left(\left(f\right)\left(u\right)\right)\left(j\right)\right)\Rightarrow \left(\left(\forall a\in U,\forall b\in U,a\ne b\Rightarrow \left(\neg \left(\left(f\right)\left(a\right)\le \left(f\right)\left(b\right)\right)\wedge \neg \left(\left(f\right)\left(b\right)\le \left(f\right)\left(a\right)\right)\right)\right)\Rightarrow \mathrm{Fintype}.\mathrm{card}\left(U\right)\le 5\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_12 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite family of positive profiles satisfying the displayed inequalities and mutual incomparability has the stated cardinality bound. The finite chain cover is used after bounding every coordinate by two.

Theorem 1.27 (strong profile antichain bound 5 40).

$$\forall U\in Type,[\mathrm{Fintype}\left(U\right)]\forall f\in \left(U\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right),\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),1\le \left(\left(f\right)\left(u\right)\right)\left(i\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)<\left(D540\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)\le \left(D540\right)\left(i,j\right)+\left(\left(f\right)\left(u\right)\right)\left(j\right)\right)\Rightarrow \left(\left(\forall a\in U,\forall b\in U,a\ne b\Rightarrow \left(\neg \left(\left(f\right)\left(a\right)\le \left(f\right)\left(b\right)\right)\wedge \neg \left(\left(f\right)\left(b\right)\le \left(f\right)\left(a\right)\right)\right)\right)\Rightarrow \mathrm{Fintype}.\mathrm{card}\left(U\right)\le 5\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_40 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite family of positive profiles satisfying the displayed inequalities and mutual incomparability has the stated cardinality bound. The finite chain cover is used after bounding every coordinate by two.

Theorem 1.28 (strong profile antichain bound 5 41).

$$\forall U\in Type,[\mathrm{Fintype}\left(U\right)]\forall f\in \left(U\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right),\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),1\le \left(\left(f\right)\left(u\right)\right)\left(i\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)<\left(D541\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)\le \left(D541\right)\left(i,j\right)+\left(\left(f\right)\left(u\right)\right)\left(j\right)\right)\Rightarrow \left(\left(\forall a\in U,\forall b\in U,a\ne b\Rightarrow \left(\neg \left(\left(f\right)\left(a\right)\le \left(f\right)\left(b\right)\right)\wedge \neg \left(\left(f\right)\left(b\right)\le \left(f\right)\left(a\right)\right)\right)\right)\Rightarrow \mathrm{Fintype}.\mathrm{card}\left(U\right)\le 5\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_41 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite family of positive profiles satisfying the displayed inequalities and mutual incomparability has the stated cardinality bound. The finite chain cover is used after bounding every coordinate by two.

Theorem 1.29 (strong profile antichain bound 5 76).

$$\forall U\in Type,[\mathrm{Fintype}\left(U\right)]\forall f\in \left(U\right)\to \left(\left(\mathrm{Fin}\left(5\right)\right)\to \left(\mathrm{Nat}\right)\right),\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),1\le \left(\left(f\right)\left(u\right)\right)\left(i\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall j\in \mathrm{Fin}\left(5\right),\exists i\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)<\left(D576\right)\left(i,j\right)\right)\Rightarrow \left(\left(\forall u\in U,\forall i\in \mathrm{Fin}\left(5\right),\forall j\in \mathrm{Fin}\left(5\right),\left(\left(f\right)\left(u\right)\right)\left(i\right)\le \left(D576\right)\left(i,j\right)+\left(\left(f\right)\left(u\right)\right)\left(j\right)\right)\Rightarrow \left(\left(\forall a\in U,\forall b\in U,a\ne b\Rightarrow \left(\neg \left(\left(f\right)\left(a\right)\le \left(f\right)\left(b\right)\right)\wedge \neg \left(\left(f\right)\left(b\right)\le \left(f\right)\left(a\right)\right)\right)\right)\Rightarrow \mathrm{Fintype}.\mathrm{card}\left(U\right)\le 5\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_76 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite family of positive profiles satisfying the displayed inequalities and mutual incomparability has the stated cardinality bound. The finite chain cover is used after bounding every coordinate by two.

References

• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D32
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D44
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D510
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D512
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D540
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D541
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D576
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.D58
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.acBool
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.card_le_of_chain_cover
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.cardinal_le_profile_chains
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_3_2
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_4_4
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_10
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_12
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_40
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_41
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_76
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.nat_profile_bound_5_8
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.profile_finite_bound
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.profile_mem_of_certificate
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_3_2
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_4_4
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_10
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_12
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_40
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_41
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_76
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/SolidResolvingTournamentProfiles.strong_profile_antichain_bound_5_8
• Dependency: D5/S3/ObserverMemory/Algorithms/UniformDescriptorSupport