Is this mathematical induction or not, and does it matter? And what known proofs have this form? Suppose one proves that for all $n\in\{1,2,3,\ldots\},$ $a_n=a_1$ by means of showing that for every value of $n$ we have $a_{n+1} = a_n,$ the proof being the same for all values of $n.$
If one puts it that way, it looks like mathematical induction: The induction hypothesis is that $a_n=a_1,$ and one uses that in proving that $a_{n+1}=a_1,$ by using the transitivity of equality.
But now suppose the proposition to be proved is stated as $ a_1 = a_2 = a_3 = \cdots.$ Then when one proves that $a_{n+1}=a_n,$ one is not using the previous case, which says $a_{n-1} = a_n,$ so in that respect it does not look like mathematical induction. 


*

*Is the question of whether this really is or is not mathematical induction substantial, or is this trivial semantic nitpicking?

*What known proofs have this form?


This question was inspired by this video on youtube, where the following is proved by means of elementary geometry:
Suppose a circle centered at $(0,0)$ has circumference $2^n.$ Consider the set of $2^{n-1}$ points
$$
S = \left\{ \text{radius} \times\Big( \cos\left( \tfrac{2\pi k} n\right), \sin \left( \tfrac{2\pi k} n \right) \Big) : \textbf{odd } k  \right\}.
$$
Let $$a_n = \sum_{x\,\in\, S} \|x - (1,0)\|^{-2}.$$ Then $$a_1 = a_2 = a_3 = \cdots\left({} = \frac {\pi^2} 4\right).$$
This yields a solution to the celebrated “Basel problem” since
$$
\lim_{n\to\infty} a_n = \sum_{\textbf{odd } k\,\in\,\mathbb Z} \frac 1 {k^2}.
$$
 A: There's a precise sense in which induction is needed: there are models of PA$^-$ (= first-order Peano arithmetic without induction) which have a definable function $f$ such that


*

*$f(n)=f(n+1)$ for all $n$, but

*there is some $m$ such that $f(m)\not=f(0)$.
Basically, let $M$ be any model of PA$^-$ in which induction fails for some formula $\varphi(x)$, and let $f$ be defined by $f(x)=0$ if $\forall y<x(\varphi(y))$ and $f(x)=1$ otherwise.
This shows that the "local" fact that each term is the same as the next isn't enough to conclude the desired "global" fact without some induction principles. Here your "$a_n$" is my "$f(n)$." Note that we're not looking at any specific argument here, but rather making a general observation about what axioms are needed to prove the theorem using any method.

As someone interested in reverse mathematics, I'd say that the question of what exactly constitutes induction is quite interesting. However, when it comes to the question "what known proofs have this form," I'm honestly a bit unclear on what exactly the form of proof you have in mind is; I think the argument given would need to be made more explicit to answer that. In general, I would say that proofs tend harder than theorems when it comes to characterization: we have precise ways to talk about when two theorems/questions are equivalent, but telling when two proofs are similar is in my opinion still something we can't satisfyingly do.
A: As you point out, you can prove by a single application of proof by induction that $\forall x\in N: a_x=a_1$.
Then you can use this result to prove, without further use of induction, that $\forall x, y \in N: a_x = a_y$ since $a_x=a_1$ and $a_y=a_1$ implies $a_x=a_y$ by substitution. That's the easy way. You can also do it the hard way with a double application of proof by induction with the base case for the first application itself requiring a full proof by induction. 
