Friendship Theorem (#83 of "100 theorem list")

[Alexander van der Vekens]

(I changed my mind and created this new topic to discuss the friendship theorem instead of discussing about it in the general topic "Graph Theory" (https://groups.google.com/d/topic/metamath/KdVXdL3IH3k/discussion).

Currently, there are two approaches to prove the friendship theorem from the "100 theorem list" (#83).

First approach

The first approach is described in topic "Best way to define things"  (r00nk 16.01.2017 04:21, https://groups.google.com/d/topic/metamath/05rpwBurSmc/discussion).

This approach bases on the definitions and theorems for "Undirected Multigraphs" (~ df-umgra to ~ konigsberg in Mario's Mathbox, see also topic "set.mm update" (Mario Carneiro 16.04.2015 11:10, https://groups.google.com/d/topic/metamath/VAGNmzFkHCs/discussion). It uses the following definitions:

  $( Undirected Simple Graph. This definition is loosely based on the UMGrph definition $)
  ${
    $d e v x $.
    df-usgra $a |- USGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } } $.
  $}

  ${
    $d x y z v e $.
    df-cfrng $a |- FRNDGrph = { <. v , e >. | ( <. v , e >. e. USGrph ) /\ ( A. x e. v A. y e. v E! z ( ( ( z , x ) e. e ) /\ ( ( z , y ) e. e ) ) ) }  $.
  $}

The friendship theorem is formalized as follows:

  ${
    $d x y z $.
    frndshp $p |- ( <. v , e >. e. FRNDGrph ) -> ( E x ( ( x e. v ) /\ ( VDeg ` x = card ` ( v / x ) )  $= ? $.
  $}

Second approach
I follow a different approach. My goal is to formailze the proof published in the paper "The friendship problem on graphs" of G.B. Mertizios and W. Unger (ROGICS'08, 12-17 May 2008, Mahida, Tunisia, pp 152-158), which is based on a purely combinatorial approach.
Although I use exactly the same definition (and name!) for undirected simple graphs (without loops) as r00nk, I need a definition for the neighbors of a vertex in an undirected simple graphs without loops ("called "graph" in short in the following):
  ${
    $d e v x k n g f p $.
    $( Define the class of all Neighbors of a vertex in a graph.
       The neighbors of a vertex are all vertices which are connected with
       this vertex by an edge.
       (Contributed by Alexander van der Vekens, 11-Aug-2017.) $)
    df-nbgra $a |- Neighbors = ( k e. _V , g e. ( _V X. _V )
      |-> { n e. ( 1st ` g ) | [. ( 1st ` g ) / v ]. [. ( 2nd ` g ) / e ].
            ( v USGrph e /\ E. x e. dom e ( e ` x ) = { k , n } ) } ) $.
  $}

Using this definition, I define the friendship graphs as follows:
${
    $d e v k l f $.
    $( Define the class of all Friendship Graphs. 
       A graph is called a friendship graph if every pair of its vertices has
       exactly one common neighbor.
       (Contributed by Alexander van der Vekens, 10-Aug-2017.) $)
    df-frgra $a |- FriendGrph = { <. v , e >. | ( v USGrph e
         /\ A. k e. v A. l e. v E. f e. v ( k =/= l
            -> ( ( k Neighbors <. v , e >. ) i^i ( l Neighbors <. v , e >. ) ) = { f } ) ) } $.
$}
As in the paper of Mertizios and Unger, I want to show that "every friengship graph is a windmill graph", in Metamath syntax:
  $( Any friendship graph is a windmill graph.
  friswmgra $p |- ( V FriendGrph E -> V WindmillGrph E ) $=
    ? $.

with the following definition of a windmill graph:
  ${
    $d e v k l f $.
    $( Define the class of all Windmill Graphs. 
       A graph is called a windmill graph if there is one vertex which is a
       neighbor of all other vertices, and the other vertices have exactly one
       additional neighbor.
       (Contributed by Alexander van der Vekens, 10-Aug-2017.) $)
    df-wmgra $a |- WindmillGrph = { <. v , e >. | ( v USGrph e
       /\ E. f e. v A. k e. v ( k =/= f -> E. l e. v
          ( l =/= f /\ ( k Neighbors <. v , e >. ) = { l , f } ) ) ) } $.
  $}
Before I continue with my work, I have the following questions:

• Are there any remarks on/objections against these definitions?
• Are there any remarks on the two approaches?
  

Your feedback is welcome.
I will provide first results in replies to this topic (and put these results into my mathbox) later.
Regards,
Alexander

[Mario Carneiro]

On Mon, Oct 2, 2017 at 5:39 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

(I changed my mind and created this new topic to discuss the friendship theorem instead of discussing about it in the general topic "Graph Theory" (https://groups.google.com/d/topic/metamath/KdVXdL3IH3k/discussion).

Currently, there are two approaches to prove the friendship theorem from the "100 theorem list" (#83).

First approach

The first approach is described in topic "Best way to define things"  (r00nk 16.01.2017 04:21, https://groups.google.com/d/topic/metamath/05rpwBurSmc/discussion).

This approach bases on the definitions and theorems for "Undirected Multigraphs" (~ df-umgra to ~ konigsberg in Mario's Mathbox, see also topic "set.mm update" (Mario Carneiro 16.04.2015 11:10, https://groups.google.com/d/topic/metamath/VAGNmzFkHCs/discussion). It uses the following definitions:

  $( Undirected Simple Graph. This definition is loosely based on the UMGrph definition $)
  ${
    $d e v x $.
    df-usgra $a |- USGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } } $.
  $}

  ${
    $d x y z v e $.
    df-cfrng $a |- FRNDGrph = { <. v , e >. | ( <. v , e >. e. USGrph ) /\ ( A. x e. v A. y e. v E! z ( ( ( z , x ) e. e ) /\ ( ( z , y ) e. e ) ) ) }  $.
  $}

Let me play compiler:

    df-cfrng $a |- FRNDGrph = { <. v , e >. | ( <. v , e >. e. USGrph /\ A. x e. v A. y e. ( v \ { x } ) E! z ( { z , x } e. ran e /\ { z , y } e. ran e ) ) }  $.  

or:

    df-cfrng $a |- FRNDGrph = { <. v , e >. | ( <. v , e >. e. USGrph /\ A. x e. v A. y e. ( v \ { x } ) E! z { { z , x } , { z , y } } C_ ran e ) }  $.  

Note that "ran e" is used here because e as you've defined it is still a function (presumably for compatibility with UMGrph), although it is injective so its range is all that matters structurally speaking.

I also added a disjointness on x and y here to mirror the second version below - without this, it would require that every vertex have degree 1.

The friendship theorem is formalized as follows:

  ${
    $d x y z $.
    frndshp $p |- ( <. v , e >. e. FRNDGrph ) -> ( E x ( ( x e. v ) /\ ( VDeg ` x = card ` ( v / x ) )  $= ? $.
  $}

After fixing the grammar:

    frndshp $p |- ( V FRNDGrph E -> E. x e. V ( VDeg ` x ) = ( card ` ( V / x ) ) )  $= ? $.

 

this still doesn't make sense because card returns an ordinal and VDeg gives a natural number. Also, is this theorem supposed to be true in the infinite case? This will probably affect the approach. Probably you want this:

    frndshp $p |- ( V FRNDGrph E -> E. x e. V ( VDeg ` x ) = ( ( # ` V ) - 1 ) )  $= ? $.

 

but I would be more specific about the windmill part:

    frndshp $p |- ( V FRNDGrph E -> E. x e. V A. y e. ( V \ { x } ) { x , y } e. ran E )  $= ? $.

 

Second approach
I follow a different approach. My goal is to formailze the proof published in the paper "The friendship problem on graphs" of G.B. Mertizios and W. Unger (ROGICS'08, 12-17 May 2008, Mahida, Tunisia, pp 152-158), which is based on a purely combinatorial approach.
Although I use exactly the same definition (and name!) for undirected simple graphs (without loops) as r00nk, I need a definition for the neighbors of a vertex in an undirected simple graphs without loops ("called "graph" in short in the following):
  ${
    $d e v x k n g f p $.
    $( Define the class of all Neighbors of a vertex in a graph.
       The neighbors of a vertex are all vertices which are connected with
       this vertex by an edge.
       (Contributed by Alexander van der Vekens, 11-Aug-2017.) $)
    df-nbgra $a |- Neighbors = ( k e. _V , g e. ( _V X. _V )
      |-> { n e. ( 1st ` g ) | [. ( 1st ` g ) / v ]. [. ( 2nd ` g ) / e ].
            ( v USGrph e /\ E. x e. dom e ( e ` x ) = { k , n } ) } ) $.

This definition generalizes to UMGrph:

    df-nbgra $a |- Neighbors = ( g e. UMGrph , k e. ( 1st ` g ) |-> { n e. ( 1st ` g ) | { k , n } e. ran ( 2nd ` g ) ) } ) $.

(I've reordered the arguments because of the dependency order.) Because of its generality, you probably shouldn't use this statement for reverse closure, meaning that the mention of UMGrph here can also just be replaced with _V.

  $}

Using this definition, I define the friendship graphs as follows:
${
    $d e v k l f $.
    $( Define the class of all Friendship Graphs. 
       A graph is called a friendship graph if every pair of its vertices has
       exactly one common neighbor.
       (Contributed by Alexander van der Vekens, 10-Aug-2017.) $)
    df-frgra $a |- FriendGrph = { <. v , e >. | ( v USGrph e
         /\ A. k e. v A. l e. v E. f e. v ( k =/= l
            -> ( ( k Neighbors <. v , e >. ) i^i ( l Neighbors <. v , e >. ) ) = { f } ) ) } $.

The quantifier order is a bit funky here. Shouldn't the E. f come after the k =/= l?

    df-frgra $a |- FriendGrph = { <. v , e >. | ( v USGrph e /\ A. k e. v A. l e. ( v \ { k } ) ( ( <. v , e >. Neighbors k ) i^i ( <. v , e >. Neighbors l ) ) ~~ 1o ) ) } $.

I don't like that this is more work to say than the first attempt without the definition:

    df-frgra $a |- FriendGrph = { <. v , e >. | ( v USGrph e /\ A. k e. v A. l e. ( v \ { k } ) E! x { { x , k } , { x , l } } C_ ran e ) } $.

Hopefully "Neighbors" pays for itself elsewhere.

 

$}
As in the paper of Mertizios and Unger, I want to show that "every friengship graph is a windmill graph", in Metamath syntax:
  $( Any friendship graph is a windmill graph.
  friswmgra $p |- ( V FriendGrph E -> V WindmillGrph E ) $=

    ? $.

with the following definition of a windmill graph:
  ${
    $d e v k l f $.
    $( Define the class of all Windmill Graphs. 
       A graph is called a windmill graph if there is one vertex which is a
       neighbor of all other vertices, and the other vertices have exactly one
       additional neighbor.
       (Contributed by Alexander van der Vekens, 10-Aug-2017.) $)
    df-wmgra $a |- WindmillGrph = { <. v , e >. | ( v USGrph e
       /\ E. f e. v A. k e. v ( k =/= f -> E. l e. v
          ( l =/= f /\ ( k Neighbors <. v , e >. ) = { l , f } ) ) ) } $.

Not a fan of the WindmillGrph definition, because it will probably only be used here. I also don't like it when 100 theorems are too obfuscated by definitions - they should try to be clear about the content of the theorem where feasible. I will suggest this version again:

  friswmgra $p |- ( V FriendGrph E -> E. x e. V A. y e. ( V \ { x } ) { x , y } e. ran E ) $=

One might argue that this doesn't fully specify the edge structure (specifically that every spoke vertex is connected only to the hub), but this follows trivially enough from the definition of FriendGrph that I think this is sufficient for the claim of "proving the friendship theorem".

I want to emphasize that this statement of friswmgra (are we calling it that? I'd much prefer something snappier like "friendship") allows for infinite graphs, in which both the concept of a friendship graph and a windmill graph make sense, but I don't know if the theorem or the proof holds in this regime (I haven't researched the theorem). If you are interested in the infinite case, then you should not use VDeg, because that only makes sense in the finite case.

Mario

[r00nk]

 Unfortunately, finishing my version of the metamath proof has been tumbling

around the bottom of my to do list for a rather long time now. I think it's safe

to say mine is not going to be finished, so your version wont be a repeat.

However, I'd like to share the paper version of my proof. I'm not sure if its

been done like this before, I've (re)discovered this version myself. Here's a

rough outline of it:

1. In any graph where there exists a n-path between any 2 vertices, if there

exits a k-cycle, where k > n, then there must exist a (k-1)-cycle also in that

graph.

2. There is no 4-cycle in a friendship graph.

3. Due to steps 1 and 2, there is no cycle in a friendship graph higher then 3.

4. Every element of a friendship graph must have degree >= 2.

5. Due to step 3 and 4, friendship graphs are entirely composed of 3-cycles.

6. The only way to merge any number of 3-cycles without creating a 4-cycle is

to connect them at one vertice.

7. Thus, a friendship graph is composed of cycles connected by one vertice.

I can go into more detail about (and prove) the steps if anybody requests. This

is just a short version to be compared with other proofs. Unless your set on the

Mertzios and Ugner proof, my version might be easier to implement.

[savask]

I would also like to draw attention to the paper "The Friendship Theorem" by Craig Huneke. The author proves the theorem in two ways and both don't require any eigenvalues or developed linear algebra whatsoever. Both proofs start by proving some regularity conditions for the graph (which roughly corresponds to Lemma 4 in Mertizios) and then diverge: the first proof counts walks in the graph, while the second uses some trivial matrix properties to derive a contradiction. The proofs are very short and I think may yield a pretty and easy approach to the theorem.

The only notions which need to be defined (to try formalizing Huneke's proof) are those concerning matrix multiplication and traces. Sefan O'Rear's mathbox already contains all needed ingredients for the matrix part, and I guess defining the trace should be pretty straightforward.

[Alexander van der Vekens]

Hi Mario,
thank you very much for your comments and hints - they show that you have really much more experience with Metamath than I have, and it is a good advice to ask you for your opinion. On the other hand, it is always good to get a second opinion in general, because the other one sees problems/improvements to which oneself is "blind". I will consider your suggestions for  my further work.

However, I have some remarks on your comments, see below.

Best regards,
Alexander

These are not my definitions/theorems, I just copied these from the post of r00nk (https://groups.google.com/d/topic/metamath/05rpwBurSmc/discussion) without verifying them. However, I think it was a good idea to show both approaches, because this results in improvements of my approach (see below).

 

Second approach
I follow a different approach. My goal is to formailze the proof published in the paper "The friendship problem on graphs" of G.B. Mertizios and W. Unger (ROGICS'08, 12-17 May 2008, Mahida, Tunisia, pp 152-158), which is based on a purely combinatorial approach.
Although I use exactly the same definition (and name!) for undirected simple graphs (without loops) as r00nk, I need a definition for the neighbors of a vertex in an undirected simple graphs without loops ("called "graph" in short in the following):
  ${
    $d e v x k n g f p $.
    $( Define the class of all Neighbors of a vertex in a graph.
       The neighbors of a vertex are all vertices which are connected with
       this vertex by an edge.
       (Contributed by Alexander van der Vekens, 11-Aug-2017.) $)
    df-nbgra $a |- Neighbors = ( k e. _V , g e. ( _V X. _V )
      |-> { n e. ( 1st ` g ) | [. ( 1st ` g ) / v ]. [. ( 2nd ` g ) / e ].
            ( v USGrph e /\ E. x e. dom e ( e ` x ) = { k , n } ) } ) $.

This definition generalizes to UMGrph:

    df-nbgra $a |- Neighbors = ( g e. UMGrph , k e. ( 1st ` g ) |-> { n e. ( 1st ` g ) | { k , n } e. ran ( 2nd ` g ) ) } ) $.

(I've reordered the arguments because of the dependency order.) Because of its generality, you probably shouldn't use this statement for reverse closure, meaning that the mention of UMGrph here can also just be replaced with _V.

  $}

 

I like your definition - it is very concise, much shorter and maybe easier to use. However, it may be useful to assume that ( G Neighbors k ) = (/) if G e/ UMGrph in some proofs, and I do not see any meaning of the term "neighbor" outside the context of a graph.

Using this definition, I define the friendship graphs as follows:
${
    $d e v k l f $.
    $( Define the class of all Friendship Graphs. 
       A graph is called a friendship graph if every pair of its vertices has
       exactly one common neighbor.
       (Contributed by Alexander van der Vekens, 10-Aug-2017.) $)
    df-frgra $a |- FriendGrph = { <. v , e >. | ( v USGrph e
         /\ A. k e. v A. l e. v E. f e. v ( k =/= l
            -> ( ( k Neighbors <. v , e >. ) i^i ( l Neighbors <. v , e >. ) ) = { f } ) ) } $.

The quantifier order is a bit funky here. Shouldn't the E. f come after the k =/= l?

    df-frgra $a |- FriendGrph = { <. v , e >. | ( v USGrph e /\ A. k e. v A. l e. ( v \ { k } ) ( ( <. v , e >. Neighbors k ) i^i ( <. v , e >. Neighbors l ) ) ~~ 1o ) ) } $.

 

Because of ~ r19.37zv, both definitions should be equivalent, since if v = (/), A. k e. v ... is always true (see ~ ral0 ), aren't they?

I don't like that this is more work to say than the first attempt without the definition:

    df-frgra $a |- FriendGrph = { <. v , e >. | ( v USGrph e /\ A. k e. v A. l e. ( v \ { k } ) E! x { { x , k } , { x , l } } C_ ran e ) } $.

OK, this could be an alternative definition. I'll check if this will save effort during the proofs. However, I do not see yet if ` A. l e. ( v \ { k } ) ph ` is easier to use than ` A. l e. v ( l =/= k -> ph ) `

Hopefully "Neighbors" pays for itself elsewhere.

 

$}
As in the paper of Mertizios and Unger, I want to show that "every friengship graph is a windmill graph", in Metamath syntax:
  $( Any friendship graph is a windmill graph.
  friswmgra $p |- ( V FriendGrph E -> V WindmillGrph E ) $=

    ? $.

with the following definition of a windmill graph:
  ${
    $d e v k l f $.
    $( Define the class of all Windmill Graphs. 
       A graph is called a windmill graph if there is one vertex which is a
       neighbor of all other vertices, and the other vertices have exactly one
       additional neighbor.
       (Contributed by Alexander van der Vekens, 10-Aug-2017.) $)
    df-wmgra $a |- WindmillGrph = { <. v , e >. | ( v USGrph e
       /\ E. f e. v A. k e. v ( k =/= f -> E. l e. v
          ( l =/= f /\ ( k Neighbors <. v , e >. ) = { l , f } ) ) ) } $.

Not a fan of the WindmillGrph definition, because it will probably only be used here. I also don't like it when 100 theorems are too obfuscated by definitions - they should try to be clear about the content of the theorem where feasible.

I think the concept of a windmill graph is very helpful for visualizing the graphs (in one's mind and on paper).Therfore, it could help to understand certain problems. Additionally, the proof in the paper of Mertzios and Unger relies on windmill graphs. Therefore I do not know how difficult it will be to prove the theorem without that concept.

I will suggest this version again:

  friswmgra $p |- ( V FriendGrph E -> E. x e. V A. y e. ( V \ { x } ) { x , y } e. ran E ) $=

One might argue that this doesn't fully specify the edge structure (specifically that every spoke vertex is connected only to the hub), but this follows trivially enough from the definition of FriendGrph that I think this is sufficient for the claim of "proving the friendship theorem".

Although it should be sufficient to prove this theorem to count for the 100 theorem list, it can be proven that ( V =/= (/) -> ( V FriendGrph E <-> V WindmillGrph E ) ) (sorry, my previously mentioned theorem friswmgra, which represent only one direction of the equivalence, is also valid only for V =/= (/), because (/) FriendGrph E can be true, while (/) WindmillGrph E is always false).

I want to emphasize that this statement of friswmgra (are we calling it that? I'd much prefer something snappier like "friendship")

... I called the theorem  ( V =/= (/) -> ( V FriendGrph E <-> V WindmillGrph E ) ) "friendship" ...

allows for infinite graphs, in which both the concept of a friendship graph and a windmill graph make sense, but I don't know if the theorem or the proof holds in this regime (I haven't researched the theorem). If you are interested in the infinite case, then you should not use VDeg, because that only makes sense in the finite case.

Unfortunately, I didn't read anything about the special case of infinite graphs yet. In the original paper of Erdös at al., it is explictly assumed that only finite graphs are considered. I'll continue not to distinguish between finite and infinite graphs as long as this causes no problems within any proof...  

Mario

[Mario Carneiro]

On Mon, Oct 2, 2017 at 1:53 PM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

Hi Mario,
thank you very much for your comments and hints - they show that you have really much more experience with Metamath than I have, and it is a good advice to ask you for your opinion. On the other hand, it is always good to get a second opinion in general, because the other one sees problems/improvements to which oneself is "blind". I will consider your suggestions for  my further work.

However, I have some remarks on your comments, see below.

Good, rebuttals lead to discussion which results in a better thought out result in the end.

 

Best regards,
Alexander

On Monday, October 2, 2017 at 12:51:51 PM UTC+2, Mario Carneiro wrote:

On Mon, Oct 2, 2017 at 5:39 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

    df-nbgra $a |- Neighbors = ( k e. _V , g e. ( _V X. _V )
      |-> { n e. ( 1st ` g ) | [. ( 1st ` g ) / v ]. [. ( 2nd ` g ) / e ].
            ( v USGrph e /\ E. x e. dom e ( e ` x ) = { k , n } ) } ) $.

This definition generalizes to UMGrph:

    df-nbgra $a |- Neighbors = ( g e. UMGrph , k e. ( 1st ` g ) |-> { n e. ( 1st ` g ) | { k , n } e. ran ( 2nd ` g ) ) } ) $.

(I've reordered the arguments because of the dependency order.) Because of its generality, you probably shouldn't use this statement for reverse closure, meaning that the mention of UMGrph here can also just be replaced with _V.

 

I like your definition - it is very concise, much shorter and maybe easier to use. However, it may be useful to assume that ( G Neighbors k ) = (/) if G e/ UMGrph in some proofs, and I do not see any meaning of the term "neighbor" outside the context of a graph.

In most functions on structures, I recommend an approach in which the original definition does not reference the "intended domain" but the domain precondition instead appears naturally in the proofs of basic properties. For example df-sbg (group subtraction) follows this pattern. This usually makes the definitional theorem have few to no assumptions, while the basic property theorems have the assumptions they need for the context. Another way to phrase this as a maxim is "make your definition as general as possible without making it more complicated". The domain of your definition will be the largest class on which all the subterms make sense.

There is an exception to this rule however, for functions that return sets (yes I know this is set theory, but I mean sets within our soft typing, as opposed to things that return an element of the base set of the structure, for example), because in these cases we can meaningfully prove "reverse closure" laws that cut down on assumptions in several cases. For example, df-subg, which returns the set of subgroups of a group, restricts its domain to Grp so that subgrcl is provable, meaning that we don't need both G e. Grp and S e. ( SubGrp ` G ) as assumptions in theorems with this precondition. However, it's a mildly hackish technique, which depends on ndmfv, and the type theorist in me finds it a bit distasteful, so I am torn on recommendations. I guess I would say you should only use it if you really intend to make use of reverse closure and eliminating these side hypotheses.

 

    df-frgra $a |- FriendGrph = { <. v , e >. | ( v USGrph e
         /\ A. k e. v A. l e. v E. f e. v ( k =/= l
            -> ( ( k Neighbors <. v , e >. ) i^i ( l Neighbors <. v , e >. ) ) = { f } ) ) } $.

The quantifier order is a bit funky here. Shouldn't the E. f come after the k =/= l?

    df-frgra $a |- FriendGrph = { <. v , e >. | ( v USGrph e /\ A. k e. v A. l e. ( v \ { k } ) ( ( <. v , e >. Neighbors k ) i^i ( <. v , e >. Neighbors l ) ) ~~ 1o ) ) } $.

 

Because of ~ r19.37zv, both definitions should be equivalent, since if v = (/), A. k e. v ... is always true (see ~ ral0 ), aren't they?

This is true, but it still seems a bit weird to require the existence of f before we have all the preconditions. I generally don't like to see E. x ( ph -> ps ) anyway, it's an easy thing to misread. Plus I doubt you will want to use it in this form.

 

I don't like that this is more work to say than the first attempt without the definition:

    df-frgra $a |- FriendGrph = { <. v , e >. | ( v USGrph e /\ A. k e. v A. l e. ( v \ { k } ) E! x { { x , k } , { x , l } } C_ ran e ) } $.

OK, this could be an alternative definition. I'll check if this will save effort during the proofs. However, I do not see yet if ` A. l e. ( v \ { k } ) ph ` is easier to use than ` A. l e. v ( l =/= k -> ph ) `

It's just symbol-pinching, but we have enough infrastructure around statements of the form A e. ( B \ { X } ) that it should be pretty efficient to use as well. I also like less parentheses and preconditions before the main statement if I can make it work.

 

    df-wmgra $a |- WindmillGrph = { <. v , e >. | ( v USGrph e
       /\ E. f e. v A. k e. v ( k =/= f -> E. l e. v
          ( l =/= f /\ ( k Neighbors <. v , e >. ) = { l , f } ) ) ) } $.

Not a fan of the WindmillGrph definition, because it will probably only be used here. I also don't like it when 100 theorems are too obfuscated by definitions - they should try to be clear about the content of the theorem where feasible.

I think the concept of a windmill graph is very helpful for visualizing the graphs (in one's mind and on paper).Therfore, it could help to understand certain problems. Additionally, the proof in the paper of Mertzios and Unger relies on windmill graphs. Therefore I do not know how difficult it will be to prove the theorem without that concept.

I'm not saying you should prove the theorem without the concept at all, only that it should be local to the proof itself. Depending on how the proof goes, you may not need to talk about anything other than "G is a windmill graph" where G is the particular graph in the statement of the theorem, in which case the windmill statement may even just pop out at the end. But if you need to deal with many windmill graphs and establish properties of them, then you can do this with temporary definitions instead, which are hypotheses that you carry through many lemmas (such as the definition R in pntrval through pntleml, almost 50 theorems).

That the concept is useful for conceptualization and drawing is mostly an argument for using the windmill terminology in the theorem comments (and proof exposition, if you want to write one). It doesn't really affect the formalization decisions unless ease of conceptualization translates to an efficient encapsulation pattern for the proof.

 

I will suggest this version again:

  friswmgra $p |- ( V FriendGrph E -> E. x e. V A. y e. ( V \ { x } ) { x , y } e. ran E ) $=

One might argue that this doesn't fully specify the edge structure (specifically that every spoke vertex is connected only to the hub), but this follows trivially enough from the definition of FriendGrph that I think this is sufficient for the claim of "proving the friendship theorem".

Although it should be sufficient to prove this theorem to count for the 100 theorem list, it can be proven that ( V =/= (/) -> ( V FriendGrph E <-> V WindmillGrph E ) ) (sorry, my previously mentioned theorem friswmgra, which represent only one direction of the equivalence, is also valid only for V =/= (/), because (/) FriendGrph E can be true, while (/) WindmillGrph E is always false).

I would still call this a corollary of the friendship theorem, since the converse is much easier to prove.

 

I want to emphasize that this statement of friswmgra (are we calling it that? I'd much prefer something snappier like "friendship")

... I called the theorem  ( V =/= (/) -> ( V FriendGrph E <-> V WindmillGrph E ) ) "friendship" ...

allows for infinite graphs, in which both the concept of a friendship graph and a windmill graph make sense, but I don't know if the theorem or the proof holds in this regime (I haven't researched the theorem). If you are interested in the infinite case, then you should not use VDeg, because that only makes sense in the finite case.

Unfortunately, I didn't read anything about the special case of infinite graphs yet. In the original paper of Erdös at al., it is explictly assumed that only finite graphs are considered. I'll continue not to distinguish between finite and infinite graphs as long as this causes no problems within any proof...

Based on r00nk's proof sketch, I think that the infinite case also holds. It should also be possible to use a compactness type result to generalize from the finite friendship theorem, although hopefully as you say finiteness just won't come up in the proof so that it is already general.

Mario

[Alexander van der Vekens]

Hi r00nk,

this is a very interesting approach, which I did not see anywhere before. And, you are right, it seems that the formalization of this proof is much simpler than the proof of Mertzios and Unger. If we succeed in proving the friendship theorem in this way, we shoul publish it in a paper ;-).

Although you offered to provide more details, I want to add details by myself (as far as I can, see below) to verify if I understand your approach correctly, and you can check if I am right. The only problem I have is with step 1, which, however, is essential for the whole proof.

For your proof (and also for the proof of Mertzios and Unger), the definition of a cycle is required, which is not available yet. My proposal would be:

    $( Define the set of all n-cycles in a graph.
       A (simple) cycle is a closed walk without repeated vertices or edges.
       A walk is an alternating sequence of vertices and edges, starting and
       ending at a vertex, in which each edge is adjacent in the sequence to
       its two endpoints.
       An n-cycle is a cycle of length n (having n vertices and n edges).
       Therefore, an n-cycle can be represented by two mappings f and p from
       { 0 , ... , n }, where f enumerates the (indices of the) edges, and p
       enumerates the vertices. So the cycle is represented by the following
       sequence: ... p(n-1) e(f(n)) p(n) e(f(0)) p(0) e(f(1)) p(1) e(f(2)) ...
       In an undirected graph, only cycles of length greater than 2 are
       meaningful.

       (Contributed by Alexander van der Vekens, 11-Aug-2017.) $)

    df-cycl $a |- Cycles = ( n e. NN , g e. ( _V X. _V ) |-> { <. f , p >. |

      [. ( 1st ` g ) / v ]. [. ( 2nd ` g ) / e ]. ( v USGrph e

      /\ ( f : ( 0 ... ( n - 1 ) ) -1-1-> dom e
        /\ p : ( 0 ... ( n - 1 ) ) --> v )
      /\ ( A. k e. ( 1 ... ( n - 1 ) ) ( e ` ( f ` k ) )
           = { ( p ` ( k - 1 ) ) , ( p ` k ) }
           /\ ( e ` ( f ` 0 ) ) = { ( p ` ( n - 1 ) ) , ( p ` 0 ) } ) ) } ) $.

I think this definition can be simplified as Mario did for my definition of Neighbors, but the intention should be the same (no "degenerated" cases).

Since the definitial issues are almost clarified (see my discussion with Mario), I think we can start proving the theorem then (after clarifying my problem with step 1).

On Monday, October 2, 2017 at 6:28:03 PM UTC+2, r00nk wrote:

 Unfortunately, finishing my version of the metamath proof has been tumbling

around the bottom of my to do list for a rather long time now. I think it's safe

to say mine is not going to be finished, so your version wont be a repeat.

However, I'd like to share the paper version of my proof. I'm not sure if its

been done like this before, I've (re)discovered this version myself. Here's a

rough outline of it:

 

At first, the "small cases" (graphs with 0, 1 , 2 vertices) should be considered separately. I already proved that a graph with 0 vertices (and therefore 0 edges) is a friendship graph, but does not fulfil the theorem as stated by Mario. Therefore, this case must be excluded, and the theorem should be as follows:

friendship $p |- ( ( V FriendGrph E /\ V =/= (/) )
                     -> E. v e. V A. w e. ( V \ { v } ) { v ,w } e. ran E ) $=

I also proved that a graph with 1 vertex (and therefore also 0 edges) is a friendship graph as well as a windmill graph, so the theorem is valid for this case. Finally, I proved that a graph with 2 vertices (and therefore with 0 or 1 edge) is not a friendship graph in both cases (and also no windmill graph). Therefore, the theorem holds for this case, too.

So these cases are already covered and we can concentrate on graphs with 3 or more vertices.

1. In any graph where there exists a n-path between any 2 vertices, if there

exits a k-cycle, where k > n, then there must exist a (k-1)-cycle also in that

graph.

I think this is valid only for n>1 and k>3 (maybe depending on how a cycle is defined - do you think two nodes connected by an edge should be regared as 2-cycle? Using my definition, this is not possible).

Furthermore, to prove the friendship theorem, it should be sufficient to consider the case n=2 (see step 3.).

To prove this statement for n=2, we take a k-cycle and construct a (k-1)-cycle from it by cutting short two vertices:

k-cycle: ... - v_(k-1) - v_k - v_1 - v_2 - v_3 - ...

(k-1)-cycle: ... - v_(k-1) - v_k - v_x - v_3 - ...

The edge { v_k , v_x } exists because there is a path of length 2 between v_k and v_3,

and therefore there must be a vertex v_x with the edges { v_k , v_x }.

However, this argument is only valid for k >=6! For k=5, v_x could be v_4, so the constructed "(5-1)-cycle" would be the path v_5 - v_4 - v_3 which is not a 4-cycle (unless you regard a 2-path x-y-z as a 4-cycle  ... x - y - z - y - x ... , which is not possible with my definition). Since the case k=5 is essential for step 3, this must be clarified first.

2. There is no 4-cycle in a friendship graph.

 This is proven in proposition 1 by Mertzios and Unger

3. Due to steps 1 and 2, there is no cycle in a friendship graph higher then 3.

For this, it must be shown that in a friendship graph there is a 2-path between any
2 vertices. Using the definition proposed by Mario (FriendGrph = { <. v , e >. | ( v USGrph e /\ A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ ran e ) }),
for any 2 (different) vertices k and l there is such a 2-path: k-x-l!

The rest is proven by induction (this should be possible to be formalized with metamath, but I have not done this before) and contradiction:

- induction basis ( k=4): There is no k-cycle in a friendship graph, see step 2

- induction step (k>4): Assume that there is no (k-1)-cycle in a friendship graph. However, if there was a k-cycle in a friendship graph, there would also be a (k-1)-cycle according to step 1. Therefore, there cannot be a k-cycle.

4. Every element of a friendship graph must have degree >= 2.

That means each vertex has at least 2 neighbors. Again using FriendGrph = { <. v , e >. | ( v USGrph e /\ A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ ran e ) }),
for any vertex k there is a vertex  l (we assume that the graph has more than 2 vertices!) and a vertex x with the edges k-x and l-x (x must be different from k and l, because otherwise either the edge k-x or the edge l-x would not exist). But there are also a vertex x1 (x playing the role of l in the definition) and the edges k-x1 and x-x1.

Since x1 must be again different from k and x, we have two different edges k-x and k-x1 with vertex k as endpoint, therefore k has degree >=2.

5. Due to step 3 and 4, friendship graphs are entirely composed of 3-cycles.

To continue with the facts and notations of step 4, each vertex k is contained in a 3-cycle ...x-k-x1-x-...

6. The only way to merge any number of 3-cycles without creating a 4-cycle is

to connect them at one vertice.

The 3-cycles of step 5. cannot have one edge in common, otherwise there would be a 4-cycle. But to show that they are connected at one vertex, the graph must be coherent. This is the case because between arbitrary vertices there is a (2-)path between them (see remarks to step 3.). However, this could be difficult to formalize...

7. Thus, a friendship graph is composed of cycles connected by one vertice.

... i.e. a friendship graph is a windmill graph, and this vertex is the (unique) common neighbor of all pairs of the other vertices. 

[r00nk]

On Tuesday, October 3, 2017 at 2:40:32 AM UTC-7, Alexander van der Vekens wrote:

If we succeed in proving the friendship theorem in this way, we shoul publish it in a paper ;-).

That would be awesome. 

1. In any graph where there exists a n-path between any 2 vertices, if there

exits a k-cycle, where k > n, then there must exist a (k-1)-cycle also in that

graph.

I think this is valid only for n>1 and k>3 (maybe depending on how a cycle is defined - do you think two nodes connected by an edge should be regared as 2-cycle? Using my definition, this is not possible).

Furthermore, to prove the friendship theorem, it should be sufficient to consider the case n=2 (see step 3.).

 

A cycle should have at least 3 vertices I think. 

To prove this statement for n=2, we take a k-cycle and construct a (k-1)-cycle from it by cutting short two vertices:

k-cycle: ... - v_(k-1) - v_k - v_1 - v_2 - v_3 - ...

(k-1)-cycle: ... - v_(k-1) - v_k - v_x - v_3 - ...

The edge { v_k , v_x } exists because there is a path of length 2 between v_k and v_3,

and therefore there must be a vertex v_x with the edges { v_k , v_x }.

 

I proved this part in a similar fashion 

However, this argument is only valid for k >=6! For k=5, v_x could be v_4, so the constructed "(5-1)-cycle" would be the path v_5 - v_4 - v_3 which is not a 4-cycle (unless you regard a 2-path x-y-z as a 4-cycle  ... x - y - z - y - x ... , which is not possible with my definition). Since the case k=5 is essential for step 3, this must be clarified first.

 

This, on the other hand, I had not considered. It is indeed a problem. I'm currently trying to figure out whether or the theorem still works, I haven't been able to prove or disprove it yet. 

A possible solution is to try to prove that there are no 5-cycles in the friendship graph, and then follow the proof almost the same as before. We can modify step 1 to instead state that for ( k > n+1 )

However, I think the theorem might still have a chance as it is. Rather then cutting the cycle short, the fact that two vertices with one edge between them must also have a two path between them might yield a 4-cycle yet. Every graph I draw satisfying the 2-path condition with a 5-cycle also has a 4-cycle some where in it. I'll need some time to figure it out.

[Alexander van der Vekens]

Hi Mario,
I started to prove some theorems for Neighbors defined as you proposed:

df-nbgra $a |- Neighbors = ( g e. _V , k e. ( 1st ` g ) |-> { n e. ( 1st ` g ) | { k , n } e. ran ( 2nd ` g ) } ) $)

But I got stuck because of the usage of the first argument in the base set of the second argument ( k e. ( 1st ` g ) ).

I tried to prove something analogous to ~ elmpt2cl, like

    elmpt2clop.f $e |- F = ( x e. A , y e. ( 1st ` x ) |-> C ) $.
    elmpt2clop $p |- ( X e. ( <. R , S >. F T ) -> ( <. R , S >. e. A /\ T e. R ) ) $=

but I ended up in disjoint variable violations in all of my attempts. I found your theorems ~ cbvmpt2x and ~ dmmpt2ssx which go in the same direction, but I found no way to apply them.
It would be very great if you can give me a hint how to solve this problem.

My goal of all of this is to prove

nbusgra $p |- ( V USGrph E -> ( <. V , E >. Neighbors N )  = { n e. V | { N , n } e. ran E } ) $=

for an arbitrary N ( for N e. V this is easy; for N e/  V, there should be no neighbors: ( <. V , E >. Neighbors N )  = (/) ). With my previous definition of Neighbors, I could prove a theorem of that kind.

Regards, and thanks in advance,
Alexander

[Mario Carneiro]

"

On Sun, Oct 8, 2017 at 6:04 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

Hi Mario,
I started to prove some theorems for Neighbors defined as you proposed:

df-nbgra $a |- Neighbors = ( g e. _V , k e. ( 1st ` g ) |-> { n e. ( 1st ` g ) | { k , n } e. ran ( 2nd ` g ) } ) $)

But I got stuck because of the usage of the first argument in the base set of the second argument ( k e. ( 1st ` g ) ).

I tried to prove something analogous to ~ elmpt2cl, like

    elmpt2clop.f $e |- F = ( x e. A , y e. ( 1st ` x ) |-> C ) $.
    elmpt2clop $p |- ( X e. ( <. R , S >. F T ) -> ( <. R , S >. e. A /\ T e. R ) ) $=

but I ended up in disjoint variable violations in all of my attempts. I found your theorems ~ cbvmpt2x and ~ dmmpt2ssx which go in the same direction, but I found no way to apply them.
It would be very great if you can give me a hint how to solve this problem.

Given a definition like Neighbors, you will generally want to prove something like the following definitional theorem:

( ( V e. W /\ E e. X ) -> ( N e. ( <. V , E >. Neighbors K ) <-> ( K e. V /\ N e. V /\ { K , N } e. ran E ) ) )

If you like, you can substitute "V USGrph E" for "V e. W /\ E e. X", but I would suggest that this be a separate theorem (with an easy proof given this one). There is a bit of reverse closure going on here - the fact that "N e. ( <. V , E >. Neighbors K )" implies "K e. V" is not going to follow from the usual function value theorems. Unfortunately, as you have pointed out elmpt2cl is not geared for dependent binary functions like this, so we will have to either work around it or write a generalization. Here is a proof of this theorem in mmj2:

50::df-nbgra             |- Neighbors = ( g e. _V , k e. ( 1st ` g ) |-> { n e. ( 1st ` g ) | { k , n } e. ran ( 2nd ` g ) } )
51:50:a1i                |- ( ( ( V e. W /\ E e. X ) /\ K e. V ) -> Neighbors = ( g e. _V , k e. ( 1st ` g ) |-> { n e. ( 1st ` g ) | { k , n } e. ran ( 2nd ` g ) } ) )
52::fveq2                 |- ( g = <. V , E >. -> ( 1st ` g ) = ( 1st ` <. V , E >. ) )
53::op1stg             |- ( ( V e. W /\ E e. X ) -> ( 1st ` <. V , E >. ) = V )
54:53:adantr              |- ( ( ( V e. W /\ E e. X ) /\ K e. V ) -> ( 1st ` <. V , E >. ) = V )
55:52,54:sylan9eqr       |- ( ( ( ( V e. W /\ E e. X ) /\ K e. V ) /\ g = <. V , E >. ) -> ( 1st ` g ) = V )
56::opex                  |- <. V , E >. e. _V
57:56:a1i                |- ( ( ( V e. W /\ E e. X ) /\ K e. V ) -> <. V , E >. e. _V )
58::simpr                |- ( ( ( V e. W /\ E e. X ) /\ K e. V ) -> K e. V )
59:55:adantrr             |- ( ( ( ( V e. W /\ E e. X ) /\ K e. V ) /\ ( g = <. V , E >. /\ k = K ) ) -> ( 1st ` g ) = V )
60::fveq2                     |- ( g = <. V , E >. -> ( 2nd ` g ) = ( 2nd ` <. V , E >. ) )
61::op2ndg                     |- ( ( V e. W /\ E e. X ) -> ( 2nd ` <. V , E >. ) = E )
62:61:adantr                  |- ( ( ( V e. W /\ E e. X ) /\ K e. V ) -> ( 2nd ` <. V , E >. ) = E )
63:60,62:sylan9eqr           |- ( ( ( ( V e. W /\ E e. X ) /\ K e. V ) /\ g = <. V , E >. ) -> ( 2nd ` g ) = E )
64:63:rneqd                 |- ( ( ( ( V e. W /\ E e. X ) /\ K e. V ) /\ g = <. V , E >. ) -> ran ( 2nd ` g ) = ran E )
65:64:adantrr              |- ( ( ( ( V e. W /\ E e. X ) /\ K e. V ) /\ ( g = <. V , E >. /\ k = K ) ) -> ran ( 2nd ` g ) = ran E )
66::simprr                  |- ( ( ( ( V e. W /\ E e. X ) /\ K e. V ) /\ ( g = <. V , E >. /\ k = K ) ) -> k = K )
67:66:preq1d               |- ( ( ( ( V e. W /\ E e. X ) /\ K e. V ) /\ ( g = <. V , E >. /\ k = K ) ) -> { k , n } = { K , n } )
68:67,65:eleq12d          |- ( ( ( ( V e. W /\ E e. X ) /\ K e. V ) /\ ( g = <. V , E >. /\ k = K ) ) -> ( { k , n } e. ran ( 2nd ` g ) <-> { K , n } e. ran E ) )
69:59,68:rabeqbidv       |- ( ( ( ( V e. W /\ E e. X ) /\ K e. V ) /\ ( g = <. V , E >. /\ k = K ) ) ->
                              { n e. ( 1st ` g ) | { k , n } e. ran ( 2nd ` g ) } = { n e. V | { K , n } e. ran E } )
70::rabexg                |- ( V e. W -> { n e. V | { K , n } e. ran E } e. _V )
71:70:ad2antrr           |- ( ( ( V e. W /\ E e. X ) /\ K e. V ) -> { n e. V | { K , n } e. ran E } e. _V )
72:51,69,55,57,58,71:ovmpt2dx
                        |- ( ( ( V e. W /\ E e. X ) /\ K e. V ) -> ( <. V , E >. Neighbors K ) = { n e. V | { K , n } e. ran E } )
73:72:eleq2d           |- ( ( ( V e. W /\ E e. X ) /\ K e. V ) -> ( N e. ( <. V , E >. Neighbors K ) <-> N e. { n e. V | { K , n } e. ran E } ) )
74::preq2                |- ( n = N -> { K , n } = { K , N } )
75:74:eleq1d            |- ( n = N -> ( { K , n } e. ran E <-> { K , N } e. ran E ) )
76:75:elrab            |- ( N e. { n e. V | { K , n } e. ran E } <-> ( N e. V /\ { K , N } e. ran E ) )
77:73,76:syl6bb       |- ( ( ( V e. W /\ E e. X ) /\ K e. V ) -> ( N e. ( <. V , E >. Neighbors K ) <-> ( N e. V /\ { K , N } e. ran E ) ) )
78:77:pm5.32da       |- ( ( V e. W /\ E e. X ) -> ( ( K e. V /\ N e. ( <. V , E >. Neighbors K ) ) <-> ( K e. V /\ ( N e. V /\ { K , N } e. ran E ) ) ) )
79::3anass           |- ( ( K e. V /\ N e. V /\ { K , N } e. ran E ) <-> ( K e. V /\ ( N e. V /\ { K , N } e. ran E ) ) )
80:78,79:syl6bbr    |- ( ( V e. W /\ E e. X ) -> ( ( K e. V /\ N e. ( <. V , E >. Neighbors K ) ) <-> ( K e. V /\ N e. V /\ { K , N } e. ran E ) ) )
81::elfvdm               |- ( N e. ( Neighbors ` <. <. V , E >. , K >. ) -> <. <. V , E >. , K >. e. dom Neighbors )
82::df-ov                |- ( <. V , E >. Neighbors K ) = ( Neighbors ` <. <. V , E >. , K >. )
83:81,82:eleq2s         |- ( N e. ( <. V , E >. Neighbors K ) -> <. <. V , E >. , K >. e. dom Neighbors )
84:50:dmmpt2ssx         |- dom Neighbors C_ U_ g e. _V ( { g } X. ( 1st ` g ) )
85:84,83:sseldi        |- ( N e. ( <. V , E >. Neighbors K ) -> <. <. V , E >. , K >. e. U_ g e. _V ( { g } X. ( 1st ` g ) ) )
86::fveq2                |- ( g = <. V , E >. -> ( 1st ` g ) = ( 1st ` <. V , E >. ) )
87:86:opeliunxp2        |- ( <. <. V , E >. , K >. e. U_ g e. _V ( { g } X. ( 1st ` g ) ) <-> ( <. V , E >. e. _V /\ K e. ( 1st ` <. V , E >. ) ) )
88:87:simprbi          |- ( <. <. V , E >. , K >. e. U_ g e. _V ( { g } X. ( 1st ` g ) ) -> K e. ( 1st ` <. V , E >. ) )
89:85,88:syl          |- ( N e. ( <. V , E >. Neighbors K ) -> K e. ( 1st ` <. V , E >. ) )
90:53:eleq2d          |- ( ( V e. W /\ E e. X ) -> ( K e. ( 1st ` <. V , E >. ) <-> K e. V ) )
91:89,90:syl5ib      |- ( ( V e. W /\ E e. X ) -> ( N e. ( <. V , E >. Neighbors K ) -> K e. V ) )
92:91:pm4.71rd      |- ( ( V e. W /\ E e. X ) -> ( N e. ( <. V , E >. Neighbors K ) <-> ( K e. V /\ N e. ( <. V , E >. Neighbors K ) ) ) )
qed:92,80:bitrd    |- ( ( V e. W /\ E e. X ) -> ( N e. ( <. V , E >. Neighbors K ) <-> ( K e. V /\ N e. V /\ { K , N } e. ran E ) ) )

The key lemmas for working with dependent maps are ovmpt2dx (which evaluates a dependent mapping at a point), and dmmpt2ssx (which tells us the domain information which is necessary for reverse closure). Also opeliunxp2 is useful to evaluate the result of dmmpt2ssx (the dependent pair type).

 

My goal of all of this is to prove

nbusgra $p |- ( V USGrph E -> ( <. V , E >. Neighbors N )  = { n e. V | { N , n } e. ran E } ) $=

for an arbitrary N ( for N e. V this is easy; for N e/  V, there should be no neighbors: ( <. V , E >. Neighbors N )  = (/) ). With my previous definition of Neighbors, I could prove a theorem of that kind.

The theorem above is essentially equivalent to this one, except it has "more capital letters" which is useful in applications. You can derive nbusgra from the above by using df-rab and abbi2dv. (This combo should really exist as its own theorem - the closest equivalent is rabbi2dva, but this introduces an undesirable intersection on the left which needs to be postprocessed away.

Actually, there is a slight complication on the right when N e/ V: The condition { N , n } e. ran E implies that N e. V, but only for very roundabout reasons: If N e/ _V, then { N , n } = { n }, and since this is a simple graph, not a multigraph, no singleton is in E. Thus N e. _V, but then { N , n } e. ran E implies { N , n } C_ V and hence N e. V. In other words, the above theorem could also be stated

|- ( V USGrph E -> ( N e. ( <. V , E >. Neighbors K ) <-> { K , N } e. ran E ) )

 

but there are a lot of encoding tricks that are needed to make this theorem hold, so it strikes me as a bit brittle.

Mario

[Alexander van der Vekens]

Hi Mario,
thank you for your hints. I'll look how far I can get with them. If I'm successful, I'll commit these theorems to my Mathbox.

Regards,
Alexander

[Alexander van der Vekens]

I made some progress in proving the friendship theorem. At least I could prove Proposition 1 of Mertzios and Unger, see de, see 2pthfrgrarn2 and n4cyclfrgra. Furthermore, I tried different approaches to prove the assumption of r00nk that in a friendship graph there are no 5-cycles. However, I did not succeed in any case. Starting with a 5-cycle and adding new common neighbors to reach a contradiction (ie. to get an 4-cycle) results in more and more new vertices. But maybe this could be a promising approach: To show that if a friendship graph contains a 5-cycle, it must be non-finite, by constructing an endless chain of vertices to be added to this cycle to fulfill the friendship condition.

Does anybody has an idea how to prove that in a friendship graph there are no 5-cycles (without using the friendship theorem, of course)?

[Alexander van der Vekens]

By the way, there are many hints available in the literature (e.g. in "Proofs from the books" from M. Aigner and G.M. Ziegler) that the friendship theorem does not hold for infinite graphs, and this is shown by starting with a 5-cycle to construct a contradiction. But I found no formal proof for that: neither a precise rule how to construct such an infinite graph nor a formal proof that such a graph is really no windmill graph.

The "proof" in "Proofs from the book" says: ".. one may start ... with a 5-cycle, and repeatedly add common neighbors for all pairs of vertices in the graph that don't have one, yet. This leads to a (countably) infinite friendship graph without politician". The main gaps in this "proof", from my point of view, are to show that there are always pairs of vertices in the graph that still don't have common neighbors in each of the repetitions, and to prove why there is no polititian in the resulting graph. In another paper I found the phrase "since it is clearly not a windmill graph". This is, again, such a "left to the reader" case which motivated Norman to invent Metamath (see "A Personal Note" in the Preface of the "Metamath" book), and which is annoying me in the same way.

Does anybody know of a more formal/elaborated proof of this fact?

[savask]

You should think of that "extension" process inductively. Say, G_0 is your original 5-cycle, then G_1 is the graph where you've added one common neighbor to some "bad" pair, G_2 is the same operation applied to G_1 and so on. Then the resulting graph will be the union (i.e. limit) of G_k for k >= 0. Now, every pair of vertices lies in some G_k for k big enough, thus G_(k+1) contains the common neighbor (which obviously will be unique even in the union). Windmill graphs don't contain 5-cycles (you can consider the cases when the politician lies in or outside of the 5-cycle, and see that it always leads to the contradiction), so our graph is a needed counterexample.

For a more formal explanation, I guess you can try this article: http://www-labs.iro.umontreal.ca/~hahn/IFT3545/ChKR.pdf, where authors show that there are 2^a nonisomorphic friendship graphs of an infinite cardinal a.

[Alexander van der Vekens]

Thank you very much for your hints, and the link to the paper. Both helped me a lot to understand the case of infinite friendship graphs. To show that a windmill graph cannot contain a 5-cycle should not be difficult then: maybe by showing that every 5-circuit (walk of length 5 beginning and ending at the same vertex) must contain the "politician" at least twice, so none of these circuits can be a cycle.

However, I still do not see immediatly how this could help us to prove the friendship theorem for finite graphs:

• Starting with the 5-cycle, it has to be shown that there is always a "bad" pair for which a new vertex (as common neighbor) can be added. If the friendship theorem is already regarded as valid, then such a "bad" pair must always exist, because otherwise we have a finite graph fulfilling the friendship condition, but having a 5-cycle => being not a windmill graph => contradiction to friendship theorem.
• It is still not clear to me how we can assure that we can always find a new vertex without breaking the friendship condition (maybe by creating a 4-cycle). Maybe the article "On countable friendship graphs" mentioned in the article you provided can answer this question...

[savask]

No, I don' t think it helps to establish the finite case :-) Well, knowing that the theorem doesn't work in the infinite case is still a nice fact, maybe it can become a corollary from the friendship theorem once it gets formalized.

And as for the proof plan... I don't want to be repetitive, but I don't think that purely graph-theoretic proofs of the theorem are worth it. The proof by Mertzios is pretty complicated and I'm not sure if the approach by r00nk will yield a significant simplification. Once again, I can suggest the following paper by Huneke https://www.researchgate.net/publication/268313555_The_Friendship_Theorem, with the proof which uses only simple graph theory and elementary arithmetic. Moreover, as far as I'm concerned, proofs of Mertzios and Huneke have some common steps, so you can do "safe" work, if you still haven't decided on the way to go.

[r00nk]

On Saturday, December 2, 2017 at 4:17:01 AM UTC-6, Alexander van der Vekens wrote:

I made some progress in proving the friendship theorem. At least I could prove Proposition 1 of Mertzios and Unger, see de, see 2pthfrgrarn2 and n4cyclfrgra. Furthermore, I tried different approaches to prove the assumption of r00nk that in a friendship graph there are no 5-cycles. However, I did not succeed in any case. Starting with a 5-cycle and adding new common neighbors to reach a contradiction (ie. to get an 4-cycle) results in more and more new vertices. But maybe this could be a promising approach: To show that if a friendship graph contains a 5-cycle, it must be non-finite, by constructing an endless chain of vertices to be added to this cycle to fulfill the friendship condition.

Does anybody has an idea how to prove that in a friendship graph there are no 5-cycles (without using the friendship theorem, of course)?

The work I've done ultimately comes back to this same problem, adding new common neighbors resulting in more and more vertices. The progress I have made is mostly around trying to prove that if there exists a 5-cycle in a graph where every two vertices have a common neighbor, there exists a 4-cycle.  The things I've learned are;

* Any internal connection in a 5-cycle creates a 4-cycle

* If any external vertice has 3 or more connections to the 5-cycle, there exists a 4-cycle.

* There must be at least 5 connections from the external graph to the 5-cycle.

From what I can see, the 'endless chain' approach seems the most promising. 

I'd still like to figure out whether or not step one of my original proof still works. Seeing as its not as trivial to prove as I thought makes me think it could be interesting/useful someplace else. 

[Alexander van der Vekens]

Eureka, mission accomplished - the Friendship Theorem is proven.

I just finished the formalization of Huneke's proof of the Friendship Theorem (#83 of "100 theorem list") with Metamath, see ~ friendship , committing the proof and all required lemmata and auxiliary theorems to the GitHub repository metamath/set.mm.

It was a hard work: it took me over 14 month, creating hundreds of new theorems in set.mm (mainly in my Mathbox). I proved many new theorems especially for unordered and ordered pairs, functions, integers (nonnegative, upper partitions, finite intervals, half-open ranges), modulo operation, floor function, hash function, words (first/last symbol, length, concatenation, subwords, singleton words, cyclic shifts), finite sums and prime numbers. And of course a lot of theorems for graph theory itself, especially for walks and regular graphs.

Crucial was the definition of walks represented as words in simple graphs (see ~ df-wwlk and others): by this, theorems about words could be used to prove the required characteristics of (closed) walks. This would have been very tedious using the general definition ~ df-wlk of walks for arbitrary graphs, consisting of two functions.

Since my primary goal was to get the Friendship Theorem proven (relatively) quickly (to make progress in proving more theorems of the 100 theorem list), there are many imperfections in the auxiliary theorems, definitions, proofs and comments. However, the proof is valid, of course. Since the main goal is reached, I should have time to tidy up my Mathbox now. 

Many thanks to savask(?) who encouraged me to use the proof of Huneke, to Gerard who gave many hints to improve my contributions, to Mario who ensured that I used adequate definitions, and of course to Norman for supporting me with all kinds of help during the last months.

@David, will you care for reporting the proof of the Friendship Theorem as usual? Thanks in advance, and also for pushing people (like me) to prove additional theorems of the 100 theorem list.

Best regards,

Alexander

[Thierry Arnoux]

Congratulations Alexander!
_
Thierry

[David A. Wheeler]

>@David, will you care for reporting the proof of the Friendship Theorem
>as
>usual?

Absolutely, and congratulations for a big achievement!

--- David A.Wheeler

[David A. Wheeler]

On Thu, 11 Oct 2018 00:03:06 -0700 (PDT), "'Alexander van der Vekens' via Metamath" <meta...@googlegroups.com> wrote:
> Eureka, mission accomplished - the Friendship Theorem is proven.
>
> I just finished the formalization of Huneke's proof of the Friendship
> Theorem (#83 of "100 theorem list") with Metamath, see ~ friendship ,
> committing the proof and all required lemmata and auxiliary theorems to the
> GitHub repository metamath/set.mm.

This is spectacular work, and a big congrats.

Not only does this proof the friendship theorem, but as noted by Alexander van der Vekens,
this includes lots of other theorems, many of which seem very general purpose.

> @David, will you care for reporting the proof of the Friendship Theorem as
> usual? Thanks in advance, and also for pushing people (like me) to prove
> additional theorems of the 100 theorem list.

Done! This is already in the metamath 100 file in set.mm and in the
Google docs file that tracks things. I've also sent an email to Freek.
Some things won't appear on the main site until the theorems are
regenerated, but it's now all set for that.

--- David A. Wheeler