Branch-regular principal winding is a first integral

This theorem is the conjunction of two assertions. First, for every small time type $T$, vertex type $V$, and finite small edge type $E$, every topology and preconnected-space structure on $T$, every pair of maps $\mathrm{tail},\mathrm{head}:E\to V$, and every phase function $\phi:T\to V\to\mathbb R$, assume that $t\mapsto\phi(t,v)$ is continuous for each $v\in V$ and that $\phi(t,\mathrm{head}(e))-\phi(t,\mathrm{tail}(e))\not\equiv-\pi\pmod{2\pi}$ for every $t\in T$ and $e\in E$. Then, for every integer edge chain $c:E\to\mathbb Z$ and every $t_0,t_1\in T$, the two integers $\sum_{e\in E}k_{t_0,e}c(e)$ and $\sum_{e\in E}k_{t_1,e}c(e)$ are equal, where $k_{t,e}$ is the integer correction for which $\phi(t,\mathrm{head}(e))-\phi(t,\mathrm{tail}(e))+2\pi k_{t,e}\in(-\pi,\pi]$. Thus orientation is explicitly tail-to-head, and the correction has the negative-quotient sign. Second, there exist globally continuous functions $a,b:\mathbb R\to\mathbb R$ such that the corresponding correction integers at real parameters $0$ and $1$ are unequal. The existential assertion imposes no antipodality avoidance. The first assertion has no topology or finiteness assumption on $V$, no joint-continuity requirement, and no cycle or closed-chain requirement on $c$. It is vacuous for an empty time type because there are no $t_0,t_1$, gives an automatically zero sum for an empty edge type, and is vacuous whenever either premise is unsatisfied. PreconnectedSpace is not accompanied by a nonemptiness hypothesis. The quantified types are Type, not arbitrary universe-polymorphic Type u.