Winding flow/reset claim boundary

The theorem has no parameters and asserts all four of the following propositions simultaneously. First, for every continuous field $F\colon I\times I\to S^1$ on the closed unit interval $I=[0,1]$ whose spatial endpoints agree, $F(t,1)=F(t,0)$ for every $t$, define the normalized based loop $\gamma_t(x)=F(t,x)F(t,0)^{-1}$; lift each $\gamma_t$ through the circle exponential covering to the specified real-valued path $\widetilde\gamma_t$ starting at $0$, set $E(\gamma_t)=\widetilde\gamma_t(1)$, and set $W(\gamma_t)=\left\lfloor E(\gamma_t)/(2\pi)\right\rfloor$. Then $\gamma_0$ and $\gamma_1$ are homotopic as based paths, their lifted endpoints are exactly equal, and their integer values $W$ are equal. Second, define $p(a,b)=-q$, where $q$ is the integer quotient selected by division modulo $2\pi$ that reduces $b-a$ to the half-open interval $(-\pi,\pi]$, call $(a,b)$ antipodal when $b-a\equiv-\pi\pmod{2\pi}$, and, for maps $\operatorname{tail},\operatorname{head}\colon E\to V$, a phase $\phi\colon T\to V\to\mathbb R$, an integer edge weighting $c\colon E\to\mathbb Z$, and $t\in T$, define $K_c(t)=\sum_{e\in E}p(\phi(t,\operatorname{tail}(e)),\phi(t,\operatorname{head}(e)))c(e)$. For every topological preconnected type $T$, every type $V$, every finite type $E$, and every such tail, head, and phase, if $t\mapsto\phi(t,v)$ is continuous for every vertex $v$ and no ordered pair of endpoint phases is antipodal at any time and edge, then $K_c(t_0)=K_c(t_1)$ for every integer edge weighting $c$ and every $t_0,t_1\in T$; moreover, independently of that universal assertion, there exist continuous functions $a,b\colon\mathbb R\to\mathbb R$ for which $p(a(0),b(0))\ne p(a(1),b(1))$, with no non-antipodality requirement imposed on this existential example. Third, for every type $E$, every ledger consisting of a natural number $N$ and an arbitrary sequence $u_i\colon E\to\mathbb Z$ indexed by all $i\in\mathbb N$, and every $e\in E$, one has $\sum_{i=0}^{N-1}(u_{i+1}(e)-u_i(e))=u_N(e)-u_0(e)$; and, for every type $V$, finite type $E$, arbitrary incidence coefficients $B(e,v)\in\mathbb Z$, such a ledger, and every integer edge chain $c\colon E\to\mathbb Z$ certified to satisfy $\sum_{e\in E}c(e)B(e,v)=0$ for every $v\in V$, writing $\langle a,c\rangle=\sum_{e\in E}a(e)c(e)$, one has $\langle u_N,c\rangle-\langle u_0,c\rangle=\sum_{i=0}^{N-1}\langle u_{i+1}-u_i,c\rangle$. Fourth, for every topological type $S$ and every segment consisting of a subset $A\subseteq S$, a continuous trajectory $\tau\colon I\times I\to S$ lying in $A$ with $\tau(t,1)=\tau(t,0)$ for every $t$, and a continuous readout $r\colon A\to S^1$, form $G(t,x)=r(\tau(t,x))$, normalize it to the based loops $\delta_t(x)=G(t,x)G(t,0)^{-1}$, and compute $W$ by the same specified lift-and-floor construction above; then $W(\delta_0)=W(\delta_1)$. Also, for every simply connected topological type $X$, every continuous $r\colon X\to S^1$, every $x\in X$, and every loop $\ell$ in $X$ based at $x$, the image loop $r\circ\ell$ is homotopic as a based path to the constant loop at $r(x)$. All universal type quantifiers include degenerate cases: the finite edge type may be empty, making all edge sums zero and assertions quantified over an edge vacuous; $N$ may be $0$, making the ledger sums empty and both differences zero; $T$, $V$, $S$, or $X$ is not explicitly assumed nonempty, so conclusions requiring chosen elements or structures may be vacuous when those data do not exist; an empty vertex type makes the chain-closure certificate vacuous; and the branch-regular conservation implication imposes no conclusion when either its continuity hypothesis or its non-antipodality hypothesis fails. Conversely, a carrier segment over an empty state or with an empty carrier cannot be supplied because its trajectory has the nonempty domain $I\times I$ and must lie in the carrier. No closed-chain condition is imposed in the branch-regular conjunct, while the closedness certificate in the ledger conjunct is quantified but the displayed ledger identity itself is purely the stated finite-sum equality.