At the end of Section 1.2 or beginning of Section 1.3, you need to explain what is going on. The point here is that the "recurrence" that you have extracted looks nothing like a recurrence that would come out of a typical complexity analysis. The point is that a more typical recurrence is the result of interpreting our extracted recurrence in some sort of semantics. That is, we need an interpretation of the complexity language. Such an interpretation requires an interpretation of datatype values in the complexity language, and that interpretation is how we define "size" of the corresponding values in the source language.
At the end of Section 1.2 or beginning of Section 1.3, you need to explain what is going on. The point here is that the "recurrence" that you have extracted looks nothing like a recurrence that would come out of a typical complexity analysis. The point is that a more typical recurrence is the result of interpreting our extracted recurrence in some sort of semantics. That is, we need an interpretation of the complexity language. Such an interpretation requires an interpretation of datatype values in the complexity language, and that interpretation is how we define "size" of the corresponding values in the source language.