Gap in Shamir's Secret Sharing Scheme security proof

I'm trying to understand the security proof of Shamir's Secret Sharing method, as I want to adapt the polynomial creation a bit, and I've found the proofs I had available to be surprisingly vague or holey.

Some nomenclature

Given a secret $S$ in the finite field $\mathbb{F}_p$ for a $(k,n)$ threshold scheme the Shamir's Secret Sharing method generates coefficients

$a_1, \dots, a_{k-1}$ randomly and uniformly in $\mathbb{F}_p$ to generate the polynomial

$q(x)=S + a_1x^1 + \dots + a_{k-1}x^{k-1}$. $n$ shares $(x_i,y_i)$ are generated by choosing pairwise distinct $x_1, \dots, x_n$, each $x_j\neq 0$ (usually $x_j:=j$) and calculating $y_j:=q(x_j)$. The polynomial $q$ can be recovered by polynomial interpolation using any $k$ shares and the secret recovered by calculating $q(0)=S$.

Now to the proofs

Starting with the original paper by Shamir, it just states (adapted to the above nomenclature): "For each candidate value $S'$ in $\mathbb{F}_p$ [an opponent] can construct one and only one polynomial $q'(x)$ of degree $k-1$ such that $q'(0)=S'$ and $q'(x_i)=y_i$ for the $k-1$ given arguments. By construction, these $p$ possible polynomials are equally likely, and thus there is absolutely nothing the opponent can deduce about the real value of $S$." Shamir does not explain why these polynomials are equally likely or why it follows that no information about the secret $S$ is revealed.

Another often stated explanation goes along a similar vein: Given $k-1$ shares $(x_1,y_1), \dots, (x_{k-1},y_{k-1})$ you can freely choose which secret the recovery process computes by choosing the last share $(x_{k},y_{k}')$ appropriately. Take a look at the recovery equation (which utilizes the Lagrange polynomial interpolation): $S=q(0)=\sum_{j=1}^{k}y_k\prod_{m=1, m\neq j}^{k}\frac{x_m}{x_m-x_j}$ . By rearranging the equation you can compute the share $y_k$ to yield any desired $S'$. (The equation is messy and does not really give more insight: $y_k':=\frac{S'-\sum_{j=1}^{k}y_k\prod_{m=1, m\neq j}^{k}\frac{x_m}{x_m-x_j}}{\prod_{m=1}^{k-1}\frac{x_m}{x_m-x_k}}$)

I find the above argument unconvincing, as it doesn't directly argue how the first $k-1$ shares necessarily can't reveal any information and doesn't even use how the polynomial is constructed in the argument. E.g., assume I don't choose the polynomial $q$ by choosing the coefficients $a_1,\dots,a_{k-1}$, but instead by choosing $y_1,\dots,y_{k-1}$ and reconstructing the polynomial $q$ out of $(0,S), (x_1,y_1), \dots, (x_{k-1},y_{k-1})$. Now the twist: I choose all aforementioned $y_i$ randomly except $y_2$, which I define maliciously as $y_2:=S-y_1$. All of the above statements about how any last share has the power to define the secret value $S'$ still holds, yet the scheme can be trivially broken with the first two shares by calculating $S=y_2-y_1$.

Another example why the way the polynomial is chosen is crucial comes from this question Coefficients in Shamir's Secret Sharing Scheme, which shows that using the constant coefficient for the secret is vital.

Einführung in die Kryptographie by Buchmann goes another route by using a counting argument: Let's say $m<k$ secret carrier come together. For every possible secret $S'\in \mathbb{F_p}$ there are $p^{k-m-1}$ polynomials $q'(x)$ of degree $k-1$ with $q'(0)=S$ and $q'(x_i)=y_i$ for $1\leq i \leq m$. Similar to Shamir it now states that no information is revealed as all constant terms of the polynomials are equally likely, without giving further proof of why that follows.

How can I conclusively proof the security of Shamir's Secret Sharing?

The central insight helpful for understanding the proofs is that all the different ways to describe the degrees of freedom of the polynomials are in a one-to-one correspondence. A polynomial of degree $k-1$ has $k$ degrees of freedom which can be described by $k$ coefficients of the polynomial, or (for $k$ given $x$-coordinates) by $k$ heights it has to pass through. The mappings from the coefficients to the polynomials of degree $k-1$ and to the $y$-coordinates are all bijective. (They are even isomorphisms on $k$-dimensional vector spaces.)

Let's formalize that: For the moment we leave out the secret as a special parameter and treat it just like any other coefficient, i.e. $a_0:=S$. We fix $k$ (pairwise distinct) $x$-coordinates. Without loss of generality they shall be denoted by $x_1,\dots,x_k$. We define the function $f$ that maps from the coefficients $a_0,\dots,a_{k-1}$ of the polynomial $q$ to the $k$ heights ($y$-values) of the polynomial at the $x$-coordinates. The coefficients are all elements of $\mathbb{F}_p$ so the domain of $f$ is $(\mathbb{F}_p)^{k}$. The same is true for all the $k$ height ($y$-components) of the fixed $x$-coordinates, so the codomain is also $(\mathbb{F}_p)^{k}$. Calculating a single $y_i$ is as simple as plugging it into the polynomial:

$y_i:=q(x_i)=a_0 + a_1 x_i^1 + \dots + a_{k-1}x_i^{k-1} \qquad \text{for } 1\leq i\leq k$

and $f$ is defined by

$f: (\mathbb{F}_p)^{k} \rightarrow (\mathbb{F}_p)^{k}$

$(a_0,\dots,a_{k-1})\mapsto(y_1,\dots,y_{k})$.

To show the bijectivity of $f$ it is sufficient to show its injectivity, as the domain and codomain have the same finite size. The high level view is that a $k-1$ degree polynomial is uniquely described by its $k$-coefficients and that it can also be uniquely described by $k$ points it passes through. So if two lists of coefficients describe two polynomials that pass through the same points, the two polynomials must be the same and thus the list of coefficients must be the same (and hence $f$ is injective). As a more elementary view on the question take two lists of coefficients $(a_0,\dots,a_{n-1})$ and $(b_0,\dots,b_{n-1})$ that map to the same heights $(y_1,\dots,y_{k})$. Subtracting the two polynomials from each other leads to the polynomial $r(x):=(a_0-b_0) + (a_1-b_1) x^1 + \dots + (a_{k-1}-b_{k-1})x^{k-1}$ which has zeros on all of the $k$ given $x$-coordinates: $r(x_i)=0 \text{ for } 1\leq i\leq k$. Thus it must be the zero polynomial and $a_j-b_j=0$ for all $0\leq j < k$, which means the two lists of coefficients are the same. It follows that $f$ is injective and thus bijective.

(Furthermore, $f$ is linear, and thus an isomorphism.)

Looking through the lens of secret sharing: You can now fix degrees of freedom on one side and reduce the respective degree of freedom on the other side. Specifically, if you fix $k-1$ degrees of freedom, you still have 1 degree left. Furthermore, the way you fixed the first $k-1$ degrees of freedom can't interact with the remaining degree of freedom. (For me this is more intuitive, if I understand the degrees of freedom as dimensions in the vector spaces. If I fix $k-1$ dimensions in the vector space of heights ($y$-coordinates to the fixed $x$-coordinates) I still have 1 dimension left and the choices of these $k-1$ heights have no bearing on my choice of the last height.) As Shamir argues, the last degree of freedom (the last dimension) is still able to completely determine the secret and vice versa. Now, if the last degree of freedom, the secret $S$, would be drawn randomly like all others, it would be easier to argue, that the uniformity of the distribution of $S$ carries over into a uniformity of the height at the last $x$-coordinate (the value of the $y$-coordinate, i.e. the last share) and vice versa. As $S$ is not (uniformly) random in practical applications, I prefer another view on the matter to show the security of the scheme:

My preferred security proof. As a first step, let's fix $S$, as that is happening in practical applications as well. We take a look at a fixed but arbitrary set of $k-1$ secret bearers, that means we fix $k-1$ $x$-coordinates. Without loss of generality we denote them with $x_1, \dots, x_{k-1}$. What I want to show is that the heights ($y$-coordinates) are independent of the value of $S$. That means that the uniform distribution of the $k-1$ randomly chosen coefficients carries over into the resulting $y$-coordinates. That has to be the case, if there is a one-to-one relationship between coefficients and heights. To show the one-to-one relationship let's adapt the above $f$ into the following function $g$, where the constant coefficient $a_0$ is fixed as $S$: Choose $y_i$ for $1\leq i\leq k-1$ as follows (note that we only have $k-1$ heights now):

$y_i:=q(x_i)=S + a_1 x_i^1 + \dots + a_{k-1}x_i^{k-1} \qquad \text{for } 1\leq i\leq k-1$

and $g$ is defined by

$g: (\mathbb{F}_p)^{k-1} \rightarrow (\mathbb{F}_p)^{k-1}$

$(a_1,\dots,a_{k-1})\mapsto(y_1,\dots,y_{k-1})$

With an analogous argument as we used for $f$ we can show that $g$ is injective, and thus bijective: Assume we have two lists of coefficients that map to the same $k-1$ heights ($y$-coordinates for the fixed $x$-coordinates). The corresponding polynomials for the two lists of coefficients thus go through the same $k-1$ points already. Additionally both go through $(0,S)$ by construction. Thus, as they are polynomials of degree $k-1$ and share $k$ points they both go through, the two polynomials must be the same. Thus $g$ is injective and thus bijective as domain and codomain have the same finite size.

As a result we know that the $k-1$ secret shares cannot reveal any information about $S$ as they are completely determined by the (uniform) random choice of the coefficients $a_1, \dots, a_{k-1}$ and can thus themselves be interpreted as being chosen uniformly and randomly in the set of possible heights.

For any finite (additive) group $G$ and any element $g\in G$ the quantity $g+a$ is uniform if $a$ takes on each value in $G$ with equal probability $1/|G|.$

Proof: The list $\{a+g\}_{a \in G}$ has no repeats and is just a permutation of the elements of $G.$ If we had $a+g=a'+g$ with $a\neq a'$ we could get a contradiction to the uniqueness of the identity element since $a-a'$ would be another identity element. Finally, since the list has no repeats the probability of each element in the list is $1/|G|.$

All the arguments in your answer can be converted directly to this context. Take $G=GF(q)$ consider the ring of polynomials over $GF(q)$ and whatever variables/coefficients you or an opponent fixes, isolate the yet unspecified variable and conclude its equidistribution, given all the fixed choices. All the complexity of the fixing of variables and coefficients can be absorbed into the selection of this fixed arbitrary $g$.