Twisted boundaries square to zero and ignore lift bases

Expand ${\mathrm{\partial }}^2(m\sigma )$. As in the ordinary simplicial cancellation, every codimension-two face occurs twice with opposite signs. If neither deletion removes the current first vertex, both coefficients remain $m$. If only the first vertex is removed, both occurrences use the same edge transport. In the remaining exceptional pair, one occurrence transports along $v_0{v}_1$ and then $v_1{v}_2$, while the other transports along $v_0{v}_2$; these paths are endpoint-fixed homotopic inside $\sigma ({\mathrm{\Delta }}^n)$, so functoriality of the local system makes the transports equal. Hence all paired terms cancel and ${\mathrm{\partial }}^2=0$. Reversing these transports gives the identical paired-face calculation for ${\delta }^2=0$.

Fix a basepoint and write a supplied old lifted oriented $n$-cell basis as $e_j$ with $\mathrm{\partial }{e}_j={\sum }_i{e}_i\cdot r_{ij}$. Any supplied new basis has $e_j^{\mathrm{\prime }}={ϵ}_j{e}_j\cdot a_j$, with ${ϵ}_j\in \{1,-1\}$ and $a_j\in \pi$. Then $\mathrm{\partial }{e}_j^{\mathrm{\prime }}={\sum }_i{e}_i^{\mathrm{\prime }}\cdot ({ϵ}_i{a}_i^{-1}{r}_{ij}{a}_j{ϵ}_j)$. Thus the new incidence matrix is obtained from the old one by the appropriate diagonal changes. In the tensor complex $e_j^{\mathrm{\prime }}\otimes m={ϵ}_j{e}_j\otimes a_{j}m$, so diagonal coefficient change is a chain isomorphism; precomposition by its inverse is the corresponding equivariant-cochain isomorphism.

In the universal-cover models, the singular and cellular boundaries already square to zero and are right $R[\pi ]$-linear. Therefore $(\mathrm{\partial }\otimes 1{)}^2=0$, while precomposition gives ${\delta }^2\phi =\phi {\mathrm{\partial }}^2=0$. The intrinsic/model identifications in [F1] intertwine the formulas, so this also verifies every component and relative quotient or kernel.

If the basepoint changes from $x$ to $x^{\mathrm{\prime }}$, a supplied path $q:x\to x^{\mathrm{\prime }}$ identifies the loop groups by $a\mapsto [\bar{q}\ast a\ast q]$ and the fibers by $T_q$. The local-system identity $T_q{T}_{\bar{a}}=T_{\overline{\stackrel{ˉ}{q}\ast a\ast q}}{T}_q$ intertwines the two left module actions. Lifting $q$ identifies the two pointed universal-cover models and their deck actions, so it yields chain isomorphisms on tensor and equivariant-Hom complexes. A different $q$ changes this comparison by the already accounted-for group action, hence by an isomorphic diagonal basis change rather than by a new homology theory.

Steps 1.1–2.2 prove square-zero and all asserted independence statements. They are conditional on supplied lift/orientation/path choices and do not select a set-indexed family, so no AC is used. Empty spaces, zero modules, zero ring, degree zero, absent cells, and degenerate singular simplices are included in the same zero or paired-face calculations.