An Unproven Conjecture

The functions ominvar and omplot

In[]:=

ominvar@n_:=Module[{q,r,s},q=Partition[Flatten@Table[{m,k},{m,n},{k,n}],2];r=Flatten@Table[Range@n,{n}];s=Partition[Flatten@Transpose@{q,r},3];s/.{m_Integer,u_,v_}:>τ[m,u,v]]

In[]:=

omplot@n_:=Grid[Partition[ominvar@n,n],Frame->All]

In[]:=

omplot/@Range@4

Make this a “shell game” with the “switch operator” sw

In[]:=

sw[u_,v_]@c_List:=sw[u,v]/@c

In[]:=

sw[a_,b_]@τ[u_,v_,w_]:=τ[sw[a,b]@u,sw[a,b]@v,sw[a,b]@w]

In[]:=

sw[a_Integer,b_Integer]@c_Integer:=c/.{a->b,b->a}

conjecture

Let n, u, and v be any positive integers with u and v each less than or equal to n . Then we assert

In[]:=

conjecture[n_,{u_,v_}]:=(ominvar@n)==(Sort@sw[u,v]@ominvar@n)

A test of conjecture

In[]:=

n=20;

In[]:=

Select[Partition[Flatten@Outer[List,Range@n,Range@n],2],(#[[1]]<#[[2]])&]

In[]:=

conjecture[n,#]&/@%//Tally

Out[]=

Question

I have found conjecture to be true for all cases considered, but how do you find a deductive proof that it is true for all cases?

In[]:=

(*Defineominvarandswfunctions*)ominvar[n_]:=Module[{q,r,s},q=Partition[Flatten@Table[{m,k},{m,n},{k,n}],2];r=Flatten@Table[Range@n,{n}];s=Partition[Flatten@Transpose@{q,r},3];s/.{m_Integer,u_,v_}:>τ[m,u,v]]sw[u_,v_]@c_List:=sw[u,v]/@csw[a_,b_]@τ[u_,v_,w_]:=τ[sw[a,b]@u,sw[a,b]@v,sw[a,b]@w]sw[a_Integer,b_Integer]@c_Integer:=c/.{a->b,b->a}conjecture[n_,{u_,v_}]:=(ominvar@n)==(Sort@sw[u,v]@ominvar@n)(*Basecase*)baseCase=conjecture[1,{1,1}];(*Inductivestep*)inductiveStep=ForAll[{k,u,v},k>=1&&u<=k&&v<=k,conjecture[k,{u,v}]conjecture[k+1,{u,v}]];(*Verifythebasecaseandinductivestep*){baseCase,Resolve[inductiveStep]}

ForAll

:Evaluation of {k≥1&&u≤k&&v≤k,conjecture[k,{u,v}]conjecture[k+1,{u,v}]} generated message(s) {General::stop,Table::iterb}.

Out[]=

{True,True}