In the light blue cell below, edit the values of k, verbose, and maxSteps, as desired.

k = 15;  (* We work with Stirling numbers of the form S(n,k) where k is fixed. *) 
verbose=True;  (* When verbose is set to true, the intermediate calculations are displayed. *)
maxSteps=7;  (* This is the maximum depth to be investigated.  If you don't want a maximal setting, define maxSteps to be Infinity. *)
checkClasses=False; (* For some values of k, there might not be a Proposition of the form S(n,k)≢S(n+(2^m),k)  mod(2^(m+L-(Subscript[b, k]))) for sufficiently large n.  If this is the case, then checkClasses should be set to True.  In particular, this occurs for k=13. *)
(* Below, the shift is defined as (Subscript[ν, 2])(k!) which is commonly used in conjunction with the identity k!S(n,k)==(((-1))^k)(∑_(t=1)^k)(((-1))^t)(({{k}, {t}}))(t^n).The term b below appears in the identity S(n,k)≡S(n+(2^m),k)  mod(2^(m-(Subscript[b, k]))). For any odd integer t, non-negative integer s,positive integer m≥s+1, the function binaryRep[s_,t_] produces a vector ((Subscript[c, 0]),(Subscript[c, 1]),…,(Subscript[c, s])) such that (t^(2^m))≡1+(∑_(i=0)^s)(Subscript[c, i])(2^(m+2+i))  mod(2^(m+s+3)). *)
binaryRep[s_,t_]:=Part[Reverse[PadLeft[IntegerDigits[Mod[(PowerMod[t,2^(s+1),2^(2*s+4)]-1)/(2^(s+3)),2^(s+1)],2],s+1]],1;;s+1]
(* We will commonly use the following identity k!S(n+(2^m),k)-k!S(n,k)==(((-1))^k)(∑_(t=1)^k)(((-1))^t)(({{k}, {t}}))(t^n)((t^(2^m))-1). Below we extract the terms of the difference when t is odd.  For the terms where t is even, when n is large enough, we observe that t^n is congruent to 0 modulo 2^(10+m) or whatever it might be.  Since we are only interested in whether the expression is congruent to 0, we ignore the factor (((-1))^k).*)

diffS[n_,k_,m_]:=Sum[Binomial[k,t]*t^n*(t^(2^m)-1),{t,3,k,2}];

(* The following function takes a vector of length 2^a and finds a vector of length 2^m such that when repeated forms the original vector. *)

reduce[vect_]:=Module[{a},a=Length[vect];While[((a>1)&&(vect[[1;;a/2]]==vect[[a/2+1;;a]])),a=(a/2)];vect[[1;;a]]];

shift=IntegerExponent[k!,2];
b=Ceiling[Log[2,k]]-2;
Print["Proposition 1: For m≥",b," and n≥m+",(shift-b),", we have S(n,",k,")≡S(n+(2^m),",k,") mod ",2^(m-b),"."];
Print["---------------------------------------------------"];

(* The function below determines whether nu_2 \circ S(_,k) is constant on the congruence class [n]_{2^m}. *)

constantClassQ[k_,m_,n_]:=Module[{c,b,shift,en,j},
en=n;
shift=IntegerExponent[k!,2];
b=Ceiling[Log[2,k]]-2;
While[Or[en<m-b+shift,en<k],en=en+2^m];
c=IntegerExponent[StirlingS2[en,k],2];
If[m>c+b,True,
And[Apply[And,Table[Mod[StirlingS2[en+j*2^m,k],2^c]==0,{j,0,2^(c+b-m)-1}]],Apply[And,Table[Mod[StirlingS2[en+j*2^m,k],2^(c+1)]≠0,{j,0,2^(c+1+b-m)-1}]]]
]
]

(* If the result below is True, then nu_2 \circ S(_,k) is constant on the congruence class [n]_{2^m} for all m \ge em and n \equiv d \mod 2^M. *)

constantClassesQ[k_,em_,d_,M_]:=
Length[Flatten[Position[Table[constantClassQ[k,em,j],{j,d,2^em-1,2^M}],False]]]==0

proofIncomplete=True;
step=1;

While[proofIncomplete,
minimumM=shift+step-b-2;

positions={};
equivs={};

For[base=3,base<=k,
index=(base-1)/2;
binrep=binaryRep[shift+step-b-3,base];
(* Print[binrep]; *)
tempPositions=Flatten[Position[binrep,1]];
positions=Append[positions,tempPositions];
(*Print[positions];*)
equivs=Append[equivs,1+Sum[2^(m+1+positions[[index,j]]),{j,1,Length[positions[[index]]]}]];
base=base+2
];

lower=0;
lowerFlag=True;
While[lowerFlag,
mStep=minimumM-lower;
lowerFlag=Apply[And,Table[Mod[PowerMod[base,(2^(mStep+b-2)),2^(mStep+minimumM+2)]-(equivs[[(base-1)/2]])/.m->mStep,2^(mStep+minimumM+2)]==0,{base,3,k,2}]];
If[lowerFlag,lower++,];
];
lower=lower-1;



If[verbose,Print["We need to determine when S(n,",k,")≡S(n+(2^m),",k,") mod ",2^(m+step-b),".\nSince the largest power of 2 that divides ",k,"! is ",shift,",","\nwe need to determine when ",k,"!S(n,",k,")≡",k,"!S(n+(2^m),",k,") mod ",2^(m+shift+step-b),".\nFor m≥",minimumM-lower,", we have the following congruences mod ",2^(m+shift+step-b),":"],];


For[base=3,base<=k,
index=(base-1)/2;
If[verbose,Print["    ",base^(2^(m))," ≡ ",equivs[[index]]],]; 
base=base+2
];

(* Below is the minimum value of the location of the first nonzero entries of binrep *)
minlocation=Min[#[[1]]&/@positions];
reps=Table[Sum[2^(positions[[index,j]]-minlocation),{j,1,Length[positions[[index]]]}],{index,1,(k-1)/2}];
reducedExponent=minimumM+1-minlocation;
If[verbose,Print["Therefore, whenever m≥",minimumM-lower,", we have the following congruences mod 2^",reducedExponent,":"],];
For[base=3,base<=k,
index=(base-1)/2;
If[verbose,Print["    (",base^(2^m),"-1)/",2^(m+minlocation+1)," ≡ ",reps[[index]]],];
base=base+2
];
If[verbose,Print["Next, we consider the identity \!\(\*FormBox[
RowBox[{
StyleBox[" ", "TI"], 
RowBox[{
RowBox[{
RowBox[{
RowBox[{
StyleBox["k", "TI"], "!"}], 
RowBox[{
StyleBox["S", "TI"], "(", 
RowBox[{
RowBox[{
StyleBox["n", "TI"], "+", SuperscriptBox["2", 
StyleBox["m", "TI"]]}], ",", 
StyleBox["k", "TI"]}], ")"}]}], "-", 
RowBox[{
RowBox[{
StyleBox["k", "TI"], "!"}], 
RowBox[{
StyleBox["S", "TI"], "(", 
RowBox[{
StyleBox["n", "TI"], ",", 
StyleBox["k", "TI"]}], ")"}]}]}], "==", 
RowBox[{SuperscriptBox[
RowBox[{"(", 
RowBox[{"-", "1"}], ")"}], 
StyleBox["k", "TI"]], 
RowBox[{UnderoverscriptBox["∑", 
RowBox[{
StyleBox["t", "TI"], "=", "1"}], 
StyleBox["k", "TI"],
LimitsPositioning->True], 
RowBox[{SuperscriptBox[
RowBox[{"(", 
RowBox[{"-", "1"}], ")"}], 
StyleBox["t", "TI"]], 
RowBox[{"(", GridBox[{
{
StyleBox["k", "TI"]},
{
StyleBox["t", "TI"]}
}], ")"}], 
RowBox[{SuperscriptBox[
StyleBox["t", "TI"], 
StyleBox["n", "TI"]], "(", 
RowBox[{SuperscriptBox[
StyleBox["t", "TI"], SuperscriptBox["2", 
StyleBox["m", "TI"]]], "-", "1"}], ")"}]}]}]}]}]}],
TraditionalForm]\).\nWhenever n≥m+",minimumM+2," the terms of this summation when t is even are congruent to 0 modulo ",2^(m+minimumM-lower+2),".\nThus,",k,"!S(n,",k,")-",k,"!S(n+(2^m),",k,") is congruent to the following expression mod ",2^(m+shift+step-b),":"],];
If[verbose,Print["    ",diffS[n,k,m],"."],];
If[verbose,Print["The congruence above occurs precisely when the following expression is congruent to 0 modulo 2^",reducedExponent,":"],];
testing[n_]:=Sum[Mod[Binomial[k,t]*reps[[(t-1)/2]],2^reducedExponent]*t^n,{t,3,k,2}];
If[verbose,Print["    ",testing[n],"."],];

(* reducedTable produces the locations where the desired congruence holds. *)

(* Below, {n,0,2^(reducedExponent)-1}] was replaced by {n,0,2^(reducedExponent-2)-1}]] since t^(2^(m-2)) is congruent to 1 mod 2^m *)

(* Print["Computing large table..."]; *)

reducedTable=reduce[Table[Mod[testing[n],2^reducedExponent]==0,{n,0,2^(reducedExponent-2)-1}]];
modulus=Length[reducedTable];

(* Print["Finished computing table!"]; *)

zeros=Flatten[Position[reducedTable,True]]-1;
nonzeros=Flatten[Position[reducedTable,False]]-1;

(* NZ is True if the only classes contributing to the proposition are actually constant. *)

NZ=If[And[checkClasses,Length[zeros]≠0],Apply[And,Map[constantClassesQ[k,minimumM,#,Log[2,modulus]]&,zeros]],False];

If[Length[zeros]==0,proofIncomplete=False];
If[Length[zeros]>0,Print["Proposition ",step+1,": For m≥",minimumM-lower," and n≥m+",minimumM+2-lower,", we have S(n,",k,")≢S(n+(2^m),",k,") mod ",2^(m+step-b)," iff n≡",StringReplace[ToString[nonzeros],{"{"->""," "->"","}"->""}]," mod ",modulus,"."],Print["Proposition ",step+1,": For all m≥",minimumM-lower," and n≥m+",minimumM-lower+2,", we have S(n,",k,")≢S(n+(2^m),",k,") mod ",2^(m+step-b),"."]];

If[NZ,Print["---------------------------------------------------\n\nProposition ",step+2,": For m≥",minimumM-lower," and n≥m+",minimumM-lower+2,", we have (Subscript[ν, 2])◦S(_,",k,") is constant on the class (Subscript[[n], (2^m)]) whenever n≡",StringReplace[ToString[zeros],{"{"->""," "->"","}"->""}]," mod ",modulus,"."],];

Print["---------------------------------------------------"];
step++;
If[Or[step>maxSteps,NZ],proofIncomplete=False]
]