Geometric picture of Grover's algorithm

This theorem, named amplitude_rotation inside a Grover namespace, has three binders and no additional hypotheses: an implicit natural number $N$, an explicit index $w_0$ ranging over the $N$-element finite type $\{0,\dots,N-1\}$ (so implicitly $N\ge 1$ is required for $w_0$ to exist at all — if $N=0$ this finite type is empty, and the universally-quantified claim is vacuously true for that instantiation of $N$), and an explicit natural number $k$ (which may be $0$). The body asserts a single equation of complex numbers. The left-hand side is the standard Hermitian inner product $\langle x,y\rangle=\sum_i \overline{x_i}\,y_i$ (conjugate-linear in the first slot, linear in the second) on $\mathbb{C}^N$, evaluated between the standard basis vector $e_{w_0}$ (the vector whose $w_0$-th coordinate is $1$ and all other $N-1$ coordinates are $0$) and the vector obtained by applying, $k$ times in succession, a named linear operator $G_{w_0}$ (called groverIterate w0, an operator on $\mathbb{C}^N$ whose defining formula is not part of this statement) to the fixed vector $u_N\in\mathbb{C}^N$ all of whose $N$ coordinates equal $1/\sqrt{N}$ (the "uniform superposition"); here "applying $k$ times" is literal functional iteration, so $k=0$ means the identity map is used and $G_{w_0}$ is not applied at all. Because the first argument $e_{w_0}$ has a single nonzero (real) entry, this inner product is, by the stated definition, exactly the $w_0$-th coordinate of $G_{w_0}^{\,k}(u_N)$. The right-hand side is the real number $\sin\big((2k+1)\arcsin(1/\sqrt{N})\big)$, formed with the standard real sine and the standard real arcsine (valued in $[-\pi/2,\pi/2]$, genuinely inverse to sine only on inputs in $[-1,1]$), and then this real number is embedded into $\mathbb{C}$ as a complex number with zero imaginary part. For every $N\ge1$ the quantity $1/\sqrt{N}$ lies in $(0,1]\subseteq[-1,1]$, so the arcsine here is always evaluated within its genuine invertibility range and no clamping/junk-value behavior is triggered (the potential edge case $N=0$, where Lean's conventions would give $\sqrt{0}=0$ and $1/0=0$, does not need to be considered separately since, as noted, no $w_0$ exists when $N=0$). The equality is claimed for all such $N$, $w_0$, and $k$ simultaneously, with the entire proof body consisting of sorry, meaning the statement is currently asserted without proof.