16 Coherence need not mean removable phase
On this page · Permalink · Source line 1
The preceding descent theory starts with transition data that already satisfy their composition laws. It is useful to see, in a completely finite calculation, how those laws can hold while a further simplification remains impossible. The following model separates coherent composition from a choice of coordinates that removes every phase.
The coefficient group and the degree of the data matter. The cocycles in Section 13 label individual arrows in a view category. Here a phase is attached to a pair of group elements. These are different constructions. The finite example is not obtained by renaming the earlier section obstruction as a general second cohomology group.
16.1 A two-bit phase law
On this page · Permalink · Source line 6
Write \(\mathbf F_2={\mathbb Z}/2{\mathbb Z}\) additively, and let
All entries and operations in this subsection lie in \(\mathbf F_2\). In particular minus and plus agree, although retaining a minus sign in the coboundary formula helps explain its origin.
Proposition 16.1: A normalized associative phase
The phase vanishes when either argument is zero and satisfies
There is no function \(a:G\to\mathbf F_2\) such that
Proof
Normalization follows from multiplication by zero. Expanding the two sides of (16.1) gives, respectively,
which are equal by distributivity.
Every expression \(a(x)+a(y)-a(x+y)\) is symmetric in \(x,y\), because \(G\) is abelian. With \(e_1=(1,0)\) and \(e_2=(0,1)\), however,
This contradicts the symmetry required by (16.2).
The proof rules out all sixteen possible scalar functions \(a\), not just linear functions or selected trial gauges. The source ProjectiveExample.lean proves the normalization, cocycle, asymmetry, and no-scalar-flattening statements. The matrix interpretation and group construction below are worked derivations of the finite model, not separate formal declarations.
16.2 The phase is visible in actual matrices
On this page · Permalink · Source line 43
Over \({\mathbb R}\), define
Direct multiplication gives \(X^2=Z^2=I\) and \(ZX=-XZ\). Moving \(Z^{x_2}\) past \(X^{y_1}\) therefore yields
For example \(U_{e_1}U_{e_2}=XZ\), while \(U_{e_2}U_{e_1}=-XZ\). The two-bit labels add commutatively, but their chosen matrix lifts do not commute.
Associativity of three lifted matrices requires the same total sign on both parenthesizations. Equation (16.1) is exactly that requirement:
Thus a nonzero phase is not automatically a failed associativity law. It can be the data that make the composition law explicit.
Changing lifts to \(U'_x=(-1)^{a(x)}U_x\) changes the phase to
No such change makes \(c'\) vanish identically. The antisymmetric part is unchanged by every scalar change of lift. In this model it is
This is a directly observable obstruction certificate for the model. Its nonzero value at \((e_1,e_2)\) is enough, without a search over gauges.
The same symmetry argument rules out removing this sign multiplier by arbitrary nonzero complex scalar lifts as well. A multiplicative scalar coboundary \(b(x)b(y)/b(x+y)\) on an abelian group is symmetric, whereas the multiplier in (16.3) is not. This last sentence is an algebraic consequence written here. The retained Lean example uses the stated \(\mathbf F_2\)-valued formulation.
16.3 Retaining the phase restores an ordinary multiplication law
On this page · Permalink · Source line 80
Instead of trying to discard the phase, include it in the state. On the eight-element set \(\widetilde G=\mathbf F_2\times G\), put
The first coordinate of the left-associated product of three elements is \(a+b+d+c(x,y)+c(x+y,z)\). The right-associated coordinate is \(a+b+d+c(y,z)+c(x,y+z)\). Equation (16.1) proves equality. Normalization gives identity \((0,0)\), and
Both inverse products are the identity because \(x+x=0\) and arithmetic is modulo two. Hence (16.4) defines a group.
Projection \((a,x)\mapsto x\) is a homomorphism onto \(G\). Its kernel is \(\{(0,0),(1,0)\}\), which commutes with every element. The map
is a homomorphism by (16.3). Its eight matrices are distinct: they are \(\pm I,\pm X,\pm Z,\pm XZ\). It is therefore faithful. The phase extension is not an assertion that \(G\) itself has acquired an ordinary representation with these same lifts. The represented group has changed.
How to read the result
A precise form of retaining the obstruction. The original four labels do not support a phase-free multiplication of the chosen matrices. Keeping one additional bit gives an eight-element multiplication that does. This repairs the description by retaining information, not by proving that the original phase was a coboundary.
16.4 How this example fits the realization calculus
On this page · Permalink · Source line 103
There are three different questions in this small model. First, the phase satisfies the associativity relation. Second, scalar changes cannot trivialize it. Third, an enlarged state that retains the phase admits an ordinary multiplication law. Each question has a complete answer, but their answers are not interchangeable.
The example illustrates why an obstruction should be attached to the allowed changes and to a specified presentation problem. Enlarging the presentation can be mathematically productive, but it changes what is being realized and what information is carried. No general theorem that every obstruction can be removed by a finite enlargement is claimed. The finite checker enumerates all group triples, all scalar gauges, and all multiplication triples in \(\widetilde G\), independently of the symmetry proof above.