decrypto-org / TrustIsRisk

Decentralized monetary trust network
Other
31 stars 4 forks source link

Rewrite Lemma 2 proof #121

Open dionyziz opened 7 years ago

dionyziz commented 7 years ago

The proof for Lemma 2 can be simplified quite a bit using the following sketch:

Let $\mathcal{H}$ be an execution of the Transitive Game on graph $\mathcal{G}$ and $j$ the convergence turn. We will show that a flow from $A$ to $B$ can be constructed such that $\Sum{v \in N^+(A)}{x{Av}} = Loss_A,j$. First, we construct a pseudoflow $X$ on $G$ as follows:

$\forall v, w: x{vw} = \Cup{i = 0, Player(i) = v}^j { x: Steal(x, w) \in Turn_i }$

Prove here that $X$ is a pseudoflow (i.e. flows are limited by capacities). Furthermore $X$ has no deficient nodes (please add proof). Based on the pseudoflow $X$, we can now construct a feasible flow $X'$ by eliminating all active nodes. Since this does not affect outgoing flows from $A$ we deduce:

$LossA = \Sigma{v \in N^+(A)} x{Av} = \Sigma{v \in N^+(A)} x'_{Av}$

This proves the theorem. QED

dionyziz commented 7 years ago

Pseudoflows, active and deficient nodes are defined here:

https://en.wikipedia.org/wiki/Flow_network#Flows

Perhaps we can also get a CLRS reference.

OrfeasLitos commented 7 years ago

Hmm let's leave this for after essential stuff is done.

OrfeasLitos commented 7 years ago

CLRS doesn't contain pseudoflows, I will use "Network Flows Theory, Algorithms, and Applications" instead.

dionyziz commented 7 years ago

OK

On Mon, Oct 31, 2016 at 3:45 PM, Orfeas Stefanos Thyfronitis Litos < notifications@github.com> wrote:

CLRS doesn't contain pseudoflows, I will use "Network Flows Theory, Algorithms, and Applications" instead.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/OrfeasLitos/TrustIsRisk/issues/121#issuecomment-257312963, or mute the thread https://github.com/notifications/unsubscribe-auth/AAhPPKCuE8SS3TjI4lu0ryGT7HezsUNlks5q5f8YgaJpZM4KjnlZ .

OrfeasLitos commented 7 years ago

We have a draft. However it is already a page long and has some holes, noted in parentheses. The proof is placed directly above the previous one, p. 26. Check it out.

OrfeasLitos commented 7 years ago

We have to find a reference for the fact that we can construct a valid flow that maintains the outgoing flow from the source from a pseudoflow.

OrfeasLitos commented 7 years ago

The above fact doesn't hold in all cases. Think when the outgoing capacity from the source is greater than the incoming capacity to the sink and the pseudoflow is equal to the capacities.

dionyziz commented 7 years ago

What you are describing requires a deficient node. The statement holds when no deficient nodes exist.

OrfeasLitos commented 7 years ago

So we are speaking only about pseudoflows that are not preflows.

OrfeasLitos commented 7 years ago

We have been using the terms deficit and excess to denote the opposite from the literature. I will fix it in our proof.

dionyziz commented 7 years ago

OK

On Tue, Nov 8, 2016 at 11:36 AM, Orfeas Stefanos Thyfronitis Litos < notifications@github.com> wrote:

We have been using the terms deficit and excess to denote the opposite from the literature. I will fix it in our proof.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/OrfeasLitos/TrustIsRisk/issues/121#issuecomment-259114514, or mute the thread https://github.com/notifications/unsubscribe-auth/AAhPPD4mRE7fWb9yhIP5ozLr7RjmRyZBks5q8F62gaJpZM4KjnlZ .