How to postulate a formula for the following Mathematica function

Question

I am using Mathematica to explore the properties of the Fibonacci Sequence. Below is the functions I have defined

H[n_] := \[Phi]^n/Sqrt[5]

F[n_] := Round[H[n]]

S[m_] := Sum[F[n], {n, 1, m}]

Through experimentation I have realised that S[m]=SF[m-1]+F[m]. How do I obtain a conjectured formula for this and prove it by induction?

Please let me know if you need me to clarify anything further.

Answer 1

H[n_] = GoldenRatio^n/Sqrt[5];

S[m_] := Total@Round[H /@ Range[m] // FunctionExpand // Simplify]

Generate a sequence of S[m]

seq = S /@ Range[10]

(* {1, 2, 4, 7, 12, 20, 33, 54, 88, 143} *)

Use FindSequenceFunction to find a function that generates the sequence

S2[m_] = FindSequenceFunction[seq, m]

(* 1/2 (-2 + 3 Fibonacci[m] + LucasL[m]) *)

Verifying that S and S2 are equivalent beyond the range of the original sequence

And @@ (Table[S[m] == S2[m], {m, 100}] // Simplify)

(* True *)

While S[m] is discrete, S2[m] is continuous.

Show[
  Plot[S2[m], {m, 0, 5.25}],
  DiscretePlot[S[m], {m, 0, 5}, PlotStyle -> Red]]

Verifying your conjecture

S2[m] == S2[m - 1] + Fibonacci[m] // FunctionExpand // Simplify

(* True *)