(* Example of proof technique for GoldenRatio *)

(ϕ^n)==(ϕ^n)

(* For n>1, *)

-(((-(1/ϕ)))^n)+((ϕ^n)+(((-(1/ϕ)))^n))+Round[-(((-(1/ϕ)))^n)]==(ϕ^n)

(* ϕ and (-(1/ϕ)) are the roots of (x^2)-x-1. Since this is monic and has integer coefficients, and since ϕ-(1/ϕ) is an integer, *)

-(((-(1/ϕ)))^n)+Round[(ϕ^n)+(((-(1/ϕ)))^n)-(((-(1/ϕ)))^n)]==(ϕ^n)

-(((-(1/ϕ)))^n)+Round[(ϕ^n)]==(ϕ^n)

Round[(ϕ^n)]-(ϕ^n)==(((-(1/ϕ)))^n)

(* and summing over n∈[1,∞] while respecting that the above conclusions are only valid for n>1, *)

(∑_(n=1)^∞)(Round[(ϕ^n)]-(ϕ^n))==2-ϕ+(∑_(n=2)^∞)(((-(1/ϕ)))^n)

(∑_(n=1)^∞)(Round[(ϕ^n)]-(ϕ^n))==(1/ϕ)

(* The full version: let α be a Pisot-Vijayaraghavan number, and (Subscript[r, i]), 1≤i≤d be the Galois conjugates. (d is the degree of the minimum polynomial, minus 1.) Furthermore, let k be an integer such that (Subscript[∀, n≥k])Abs[(∑_(i=1)^d)(Subscript[r, i]^n)]<(1/2) - e.g. such that (∑_(i=1)^d)Abs[(Subscript[r, i]^k)]<(1/2). Then, for n≥k,
*)

-(∑_(i=1)^d)(Subscript[r, i]^n)+(α^n)+(∑_(i=1)^d)(Subscript[r, i]^n)+Round[-(∑_(i=1)^d)(Subscript[r, i]^n)]==(α^n)

(* Since α must be a root of an irreducible monic polynomial of degree d with integer coefficients, and the sum of α along with its Galois conjugates is an integer by Vieta's formulas, 
*)

-(∑_(i=1)^d)(Subscript[r, i]^n)+Round[(α^n)+(∑_(i=1)^d)(Subscript[r, i]^n)-(∑_(i=1)^d)(Subscript[r, i]^n)]==(α^n)

Round[(α^n)]-(α^n)==(∑_(i=1)^d)(Subscript[r, i]^n)

(* Now, summing over n∈[k,∞] *)

(∑_(n=k)^∞)(Round[(α^n)]-(α^n))==(∑_(n=k)^∞)(∑_(i=1)^d)(Subscript[r, i]^n)

(∑_(n=k)^∞)(Round[(α^n)]-(α^n))==(∑_(i=1)^d)(∑_(n=k)^∞)(Subscript[r, i]^n)

(∑_(n=0)^∞)(Round[(α^n)]-(α^n))==(∑_(n=0)^(k-1))(Round[(α^n)]-(α^n))+(∑_(i=1)^d)(((Subscript[r, i])^k)/(1-(Subscript[r, i])))

(* We can also raise both sides of (1) to the (Subscript[p, 1])th power, getting *)

(((Round[(α^n)]-(α^n)))^(Subscript[p, 1]))==((((∑_(i=1)^d)(Subscript[r, i]^n)))^(Subscript[p, 1]))

(* And finally, because Bill wanted me to spell it out, here it is with an extra (q^k) on the denominator: *)

(∑_(n=k)^∞)(((∏_(j=1)^(j=na))(Round[(α^n)]-(α^n)))/(q^n))==(∑_(n=k)^∞)(((∏_(j=1)^(j=na))(∑_(i=1)^(Subscript[d, j]))(Subscript[r, i]^n))/(q^n))

(∑_(n=0)^∞)(((∏_(j=1)^(j=na))(Round[(Subscript[α, j]^n)]-(Subscript[α, j]^n)))/(q^n))==(∑_(n=0)^(k-1))(((∏_(j=1)^(j=na))(Round[(Subscript[α, j]^n)]-(Subscript[α, j]^n)))/(q^n))+(∑_(n=k)^∞)(((∏_(j=1)^(j=na))(∑_(i=1)^(Subscript[d, j]))(Subscript[r, j,i]^n))/(q^n))

(* Simplifying the RHS (first-time readers should skip this part. No, really. I mean it.) *)

(∑_(n=k)^∞)(((∏_(j=1)^(j=na))(∑_(i=1)^(Subscript[d, j]))(Subscript[r, j,i]^n))/(q^n))

(∑_(n=k)^∞)(((∑_(1≤(Subscript[i, 1])≤(Subscript[d, 1]), ..., 1≤(Subscript[i, na])≤(Subscript[d, na])))(∏_(j=1)^na)(Subscript[r, j,(Subscript[i, j])]^n))/(q^n))

(* above this line is okay *)

(* lines below this are not *)

(∑_(n=k)^∞)(∑_(1≤(Subscript[i, 1])≤(Subscript[d, 1]), ..., 1≤(Subscript[i, na])≤(Subscript[d, na])))(((∏_(j=1)^na)(Subscript[r, j,(Subscript[i, j])]^n))/(q^n))

(∑_(1≤(Subscript[i, 1])≤(Subscript[d, 1]), ..., 1≤(Subscript[i, na])≤(Subscript[d, na])))(∑_(n=k)^∞)(((∏_(j=1)^na)(Subscript[r, j,(Subscript[i, j])]^n))/(q^n))

(∑_(1≤(Subscript[i, 1])≤(Subscript[d, 1]), ..., 1≤(Subscript[i, na])≤(Subscript[d, na])))(∑_(n=k)^∞)(((((∏_(j=1)^na)(Subscript[r, j,(Subscript[i, j])])))^n)/(q^n))

(∑_(1≤(Subscript[i, 1])≤(Subscript[d, 1]), ..., 1≤(Subscript[i, na])≤(Subscript[d, na])))(∑_(n=k)^∞)(((((((∏_(j=1)^na)(Subscript[r, j,(Subscript[i, j])])))/q)))^n)

(∑_(1≤(Subscript[i, 1])≤(Subscript[d, 1]), ..., 1≤(Subscript[i, na])≤(Subscript[d, na])))(((((((∏_(j=1)^na)(Subscript[r, j,(Subscript[i, j])]))/q)))^k)/((1-(((∏_(j=1)^na)(Subscript[r, j,(Subscript[i, j])]))/q))))

(∑_(1≤(Subscript[i, 1])≤(Subscript[d, 1]), ..., 1≤(Subscript[i, na])≤(Subscript[d, na])))(((∏_(j=1)^na)(Subscript[r, j,(Subscript[i, j])]^k))/((q^k)(1-(((∏_(j=1)^na)(Subscript[r, j,(Subscript[i, j])]))/q))))

(∑_(1≤(Subscript[i, 1])≤(Subscript[d, 1]), ..., 1≤(Subscript[i, na])≤(Subscript[d, na])))(((∏_(j=1)^na)((Subscript[r, j,(Subscript[i, j])]^k)))/((q^k)-(q^(k-1))(∏_(j=1)^na)(Subscript[r, j,(Subscript[i, j])])))

(* Which seems to be about as simple as it gets. *)

(* Finally, we have *)

(∑_(n=0)^∞)(((∏_(j=1)^(j=na))(Round[(Subscript[α, j]^n)]-(Subscript[α, j]^n)))/(q^n))==(∑_(n=0)^(k-1))(((∏_(j=1)^(j=na))(Round[(Subscript[α, j]^n)]-(Subscript[α, j]^n)))/(q^n))+(∑_(1≤(Subscript[i, 1])≤(Subscript[d, 1]), ..., 1≤(Subscript[i, na])≤(Subscript[d, na])))(((∏_(j=1)^na)((Subscript[r, j,(Subscript[i, j])]^k)))/((q^k)-(q^(k-1))(∏_(j=1)^na)(Subscript[r, j,(Subscript[i, j])])))

(* FUNCTIONS TO DO THE SUMMATION: *)

pisotNumberQ[a_]:=AlgebraicIntegerQ[a]&&Element[a,Reals]&&(a>1)&&(Count[List@@(Last/@Roots[MinimalPolynomial[a,x]==0,x]),_?(Abs[#]>1&)]==1)

roundoffsum[a_]:=
If[(!pisotNumberQ[a])||(InexactNumberQ[a]),Print["roundoffsum::nonpisot - This isn't a Pisot number!"],
Block[{minpoly=MinimalPolynomial[a],conjugates,k},
(conjugates=Select[#[[1,2]]&/@Solve[minpoly[x]==0,x],Abs[#]<1&];
(*Compute k satisfying (∑_(i=0)^(d-1))Abs[(Subscript[r, i]^k)]<(1/2) *)
k=getRoundoffCutoff[conjugates];
Print["minpoly degree "~~ToString[Length[conjugates]+1]~~", k="~~ToString[k]];
(∑_(n=0)^(k-1))(Round[(a^n)]-(a^n))+(∑_(i=1)^(Length[conjugates]))(((conjugates[[i]])^k)/(1-conjugates[[i]])))]]

getConjugates[a_]:=Select[#[[1,2]]&/@Solve[MinimalPolynomial[a,x]==0,x],Abs[#]<1&]

getRoundoffCutoff[conjugates_]:=Block[{k=0},
(While[(∑_(i=1)^(Length[conjugates]))((Abs[conjugates[[i]]])^k)≥1/2,k++];k)]

roundoffsum[a_List,q_]:=Block[{ks,k,conjugates,ft,rd,st,prod,iter},
(conjugates=getConjugates/@a;
ks=getRoundoffCutoff/@conjugates;
k=Max[ks];
Print["ks are "~~ToString[ks]];
rd=Times@@(Round[((#)^n)]-((#)^n)&/@a);
ft=(∑_(n=1)^(k-1))(rd/(q^n));
iter=Sequence@@Table[{(Subscript[i, j]),1,Length[conjugates[[j]]]},{j,1,Length[a]}];Print[iter];
st=(1/(q^(k-1)))Total[Flatten[
Table[(prod=Product[conjugates[[j,(Subscript[i, j]) ]],{j,1,Length[a]}];
((prod^k)/(q-prod))),Evaluate[iter]]
]
];
Return[ft+st];
)]