Solution 1:

This is not an entirely complete proof but I think the ideas can transformed to a rigorous proof.

So the inclusion of $\mathbb{Z}$ to your order $\mathcal{O}$ gives a finite surjective map $\textrm{Spec}(\mathcal{O})\to\textrm{Spec}(\mathbb{Z})$. I want to think about it as a branched covering map $X\to Y$ of curves. In the geometric situation, a singularity of $X$ is always among the ramification points (and I expect this to be true in our situation as well). So in order to check whether $X$ is nonsingular, we can restrict to the finitely many ramification points. This is one thing that your proposition does since the ramification points are precisely the points where the trace bilinear form is degenerate. What it does after that is not quite looking at tangent spaces but rather looking at their push-forwards to $\textrm{Spec}(\mathbb{Z})$.

Lets look at the map $\textrm{Spec}(\mathcal{O}_K)\to\textrm{Spec}(\mathcal{O})$ which is the normalization. Being a nonsingular point of $\textrm{Spec}(\mathcal{O})$ is equivalent to this map being locally an isomorphism. Checking this requires checking whether the two $\mathbb{Z}_p$-modules, that you get from localizing your orders, are the same. Now applying Nakayama's Lemma restricts this to the criterion from your proposition.

In particular, this answers one of your initial questions. Namely, we see that if these $\beta_i$ are linearly dependent over $\mathbb{F}_p$, then there is a singular point above $p$ in $\mathcal{O}$ and vice versa.