From the logical fault hypothesis \(\mathrm{hlog}\), we extract \(\mathrm{hnotpres} := \mathrm{hlog}.2\), which states that the full outcome is not preserved. Unfolding the definition of \(\operatorname {FullOutcomePreserving}\) and pushing the negation inward, we obtain that either the sign is not preserved or the Pauli error is not in the stabilizer group. By the dichotomy \(\operatorname {flipsOrPreserves}(\mathrm{proc}, F)\), the fault either flips or preserves the gauging sign. In the first case, we conclude \(\operatorname {FlipsGaugingSign}(\mathrm{proc}, F)\) directly. In the second case, since the sign is preserved, the negated conjunction forces \(F.\operatorname {pauliErrorAt}(t_i) \notin \mathcal{S}\).

Expanding the definition of \(\operatorname {gaussSignFlip}\) and of \(\operatorname {compose}\) (which takes the symmetric difference of time-faults), we rewrite the sum using \(\sum \)-distributivity over addition. For each vertex \(v\), we apply the \(\mathbb {Z}_2\) indicator additivity lemma for symmetric differences, which states that \(\sum _{b \in S \mathbin {\triangle } T} \mathbf{1}[g(b)] = \sum _{b \in S} \mathbf{1}[g(b)] + \sum _{b \in T} \mathbf{1}[g(b)]\) in \(\mathbb {Z}/2\mathbb {Z}\). This gives the result by congruence.

By extensionality, we verify both the \(x\)-vector and \(z\)-vector components separately. For the \(x\)-vector component: expanding the definitions of \(\operatorname {pauliErrorAt}\), \(\operatorname {spaceFaultsAt}\), and \(\operatorname {compose}\), and using the fact that filtering distributes over symmetric difference (\(\operatorname {filter}_p(S \mathbin {\triangle } T) = \operatorname {filter}_p(S) \mathbin {\triangle } \operatorname {filter}_p(T)\)), we apply the \(\mathbb {Z}_2\) sum additivity over symmetric differences with the function \(f \mapsto \text{if } f.\mathrm{qubit} = q \text{ then } f.\mathrm{xComponent} \text{ else } 0\). The \(z\)-vector component follows identically with \(\mathrm{zComponent}\) replacing \(\mathrm{xComponent}\).

Let \(\mathrm{idx}\) be an arbitrary detector index. We need to show that the detector is not violated by \((F \cdot S).\mathrm{timeFaults} = F.\mathrm{timeFaults} \mathbin {\triangle } S.\mathrm{timeFaults}\). By the characterization of violation via \(\operatorname {flipParity}\), we rewrite the goal using the \(\mathbb {Z}_2\)-additivity of \(\operatorname {flipParity}\) over symmetric differences. Since \(F\) is syndrome-free, \(\operatorname {flipParity}(D, F.\mathrm{timeFaults}) \neq 1\), and since every element of \(\mathbb {Z}/2\mathbb {Z}\) that is not \(1\) equals \(0\), we get \(\operatorname {flipParity}(D, F.\mathrm{timeFaults}) = 0\). Similarly \(\operatorname {flipParity}(D, S.\mathrm{timeFaults}) = 0\). Therefore \(\operatorname {flipParity}(D, F.\mathrm{timeFaults} \mathbin {\triangle } S.\mathrm{timeFaults}) = 0 + 0 = 0 \neq 1\).

This follows directly from the fact that composing two syndrome-free faults preserves syndrome-freeness, since a full gauging stabilizer is in particular syndrome-free.

We verify each condition:

1. Syndrome-free: This follows from \(\operatorname {compose\_ preserves\_ syndromeFree}\), since \(F_1\) is syndrome-free and \(F_2\) is a full gauging stabilizer.

2. Preserves sign: By \(\mathbb {Z}_2\)-additivity, \(\operatorname {gaussSignFlip}(\mathrm{proc}, F_1 \cdot F_2) = \operatorname {gaussSignFlip}(\mathrm{proc}, F_1) + \operatorname {gaussSignFlip}(\mathrm{proc}, F_2) = 0 + 0 = 0\).

3. Pauli in stabilizer group: By multiplicativity of \(\operatorname {pauliErrorAt}\), the Pauli error of the composition is the product of two stabilizer group elements, which is in the stabilizer group by closure under multiplication.

We verify each condition:

1. Syndrome-free: With no time-faults, no detector can be violated, so this follows from the fact that a detector with an empty fault set is not violated.

2. Preserves sign: With no time-faults, the \(\operatorname {gaussSignFlip}\) reduces to a sum over the empty set, which is \(0\).

3. Pauli error is \(\mathbf{1}\): The Pauli error at any time of the empty fault is the identity \(1\), which is in the stabilizer group.

We take \(S_2 = \operatorname {empty}\), the empty spacetime fault. By the previous theorem, \(\operatorname {empty}\) is a full gauging stabilizer. For the concentration property, let \(t \neq t_i\). Then \((F' \cdot \operatorname {empty}).\operatorname {spaceFaultsAt}(t) = F'.\operatorname {spaceFaultsAt}(t) = \emptyset \) by the hypothesis, using the fact that composing with the empty fault on the right is the identity.

From the \(\operatorname {space\_ fault\_ cleaning}\) axiom (Lem 5), applied to \(F\) and the syndrome-freeness hypothesis, we obtain \(S_1\) together with witnesses that \(S_1\) is syndrome-free, preserves the gauging sign, has its Pauli error in the stabilizer group, and cleans the space-faults. Packaging the first three properties gives \(\operatorname {IsFullGaugingStabilizer}(\mathrm{proc}, S_1)\), and the fourth gives the concentration property.

This follows directly from the \(\operatorname {syndromeFree\_ pureSpace\_ inCentralizer}\) result from Lem 5, which encodes the quantum-mechanical fact that the deformed code checks are the active checks at \(t_i\) and the cleaning process preserves commutation.

By \(\operatorname {pureTime\_ syndromeFree\_ logical\_ or\_ stabilizer\_ generators}\) from Lem 6, applied to \(F_T\), \(\mathrm{hpure}\), and \(\mathrm{hfree}\), we obtain a disjunction. In the first case, \(F_T\) flips the gauging sign directly. In the second case, we extract that \(F_T\) preserves the sign and combine with syndrome-freeness to form the gauging stabilizer witness.

Expanding the definition of \(\operatorname {gaussSignFlip}\) as a double sum over vertices \(v\) and rounds \(r\), the result follows by congruence: for each \(v\) and \(r\), the summand depends only on \(F.\mathrm{timeFaults}\), which is equal for \(F_1\) and \(F_2\) by hypothesis.

Unfolding \(\operatorname {PreservesGaugingSign}\) and \(\operatorname {gaussSignFlip}\), and using \(F.\mathrm{isPureSpace}\) to replace \(F.\mathrm{timeFaults}\) with \(\emptyset \), every indicator \(\mathbf{1}[f \in \emptyset ]\) evaluates to \(0\). The entire double sum therefore equals \(0\).

By extensionality, we verify both the \(x\)-vector and \(z\)-vector components. Each component of \(\operatorname {pauliErrorAt}\) is defined as a sum over \(\operatorname {spaceFaultsAt}(t)\), which is a filter of \(\mathrm{spaceFaults}\). Since \(F_1.\mathrm{spaceFaults} = F_2.\mathrm{spaceFaults}\), simplification gives the result in both components.

Unfolding \(F.\mathrm{isPureTime}\) gives \(F.\mathrm{spaceFaults} = \emptyset \). For both the \(x\)-vector and \(z\)-vector components, \(\operatorname {spaceFaultsAt}(t)\) is a filter of the empty set, hence empty, and the sum over the empty set is \(0\), which matches the identity Pauli operator’s components.

We prove both parts. For part (1), we apply \(\operatorname {gaussSignFlip\_ depends\_ only\_ on\_ timeFaults}\), noting that \(F.\mathrm{timeComponent}.\mathrm{timeFaults} = F.\mathrm{timeFaults}\) by definition of the time component. For part (2), for each \(t\), we apply \(\operatorname {pauliErrorAt\_ depends\_ only\_ on\_ spaceFaults}\), noting that \(F.\mathrm{spaceComponent}.\mathrm{spaceFaults} = F.\mathrm{spaceFaults}\) by definition of the space component.

We apply \(\operatorname {gaussSignFlip\_ depends\_ only\_ on\_ timeFaults}\). Since \(F_S\) is pure-space, \(F_S.\mathrm{timeFaults} = \emptyset \), so \((F_S \cdot F_T).\mathrm{timeFaults} = \emptyset \mathbin {\triangle } F_T.\mathrm{timeFaults} = F_T.\mathrm{timeFaults}\).

Step 1: Clean space-faults to \(t_i\) using time-propagating stabilizers (Lem 5). By \(\operatorname {space\_ fault\_ cleaning\_ fullStabilizer}\), applied to \(F\) and its syndrome-freeness, we obtain a stabilizer \(S_1\) with \(\operatorname {IsFullGaugingStabilizer}(\mathrm{proc}, S_1)\) and the property that for all \(t \neq t_i\), \((F \cdot S_1).\operatorname {spaceFaultsAt}(t) = \emptyset \). Set \(F' := F \cdot S_1\). Then \(F'\) is syndrome-free by \(\operatorname {compose\_ preserves\_ syndromeFree}\).

Step 2: Absorb boundary faults. By \(\operatorname {boundary\_ faults\_ trivially\_ absorbed}\),applied to \(F'\), we obtain \(S_2\) with \(\operatorname {IsFullGaugingStabilizer}(\mathrm{proc}, S_2)\) such that \(F'' := F' \cdot S_2\) has space-faults concentrated at \(t_i\). Again \(F''\) is syndrome-free.

Step 3: Decompose \(F''\) into space and time components. Let \(F_S := F''.\mathrm{spaceComponent}\), \(F_T := F''.\mathrm{timeComponent}\), and \(S := S_1 \cdot S_2\). Then \(S\) is a full gauging stabilizer by \(\operatorname {compose\_ fullGaugingStabilizer}\).

We now verify each claimed property:

• \(F = (F_S \cdot F_T) \cdot S\): By the space-time decomposition \(F'' = F_S \cdot F_T\), and \(F'' = F \cdot S_1 \cdot S_2 = F \cdot S\). So \(F = F'' \cdot S\) (since composition is involutive: \(F \cdot S \cdot S = F\)), hence \(F = (F_S \cdot F_T) \cdot S\) by associativity and self-cancellation.

• \(F_S\) is pure-space: By \(F''.\operatorname {spaceComponent\_ isPureSpace}\).

• \(F_S\) concentrated at \(t_i\): The space-faults of \(F_S\) equal those of \(F''\) (by definition of spaceComponent), which are concentrated at \(t_i\).

• \(F_T\) is pure-time: By \(F''.\operatorname {timeComponent\_ isPureTime}\).

• \(F_T\) is syndrome-free: Since \(F_T.\mathrm{timeFaults} = F''.\mathrm{timeFaults}\), detector violations are the same, so syndrome-freeness of \(F''\) transfers.

• \(S\) is a full gauging stabilizer: Already established.

• Nontriviality: Since \(F\) is a logical fault, \(\neg \operatorname {FullOutcomePreserving}(\mathrm{proc}, F)\). By \(\operatorname {flipsOrPreserves}\), either \(F\) flips the sign or preserves it.

  If \(F\) flips the sign, then \(\operatorname {gaussSignFlip}(\mathrm{proc}, F_T) = \operatorname {gaussSignFlip}(\mathrm{proc}, F'') = \operatorname {gaussSignFlip}(\mathrm{proc}, F') + \operatorname {gaussSignFlip}(\mathrm{proc}, S_2) = \operatorname {gaussSignFlip}(\mathrm{proc}, F) + 0 + 0 = 1\) by \(\mathbb {Z}_2\)-additivity and the fact that \(S_1, S_2\) preserve the sign.

  If \(F\) preserves the sign, then since the outcome is not preserved, the Pauli error \(F.\operatorname {pauliErrorAt}(t_i) \notin \mathcal{S}\). We show \(F_S.\operatorname {pauliErrorAt}(t_i) = F''.\operatorname {pauliErrorAt}(t_i)\) (same space-faults). By multiplicativity, \(F''.\operatorname {pauliErrorAt}(t_i) = F.\operatorname {pauliErrorAt}(t_i) \cdot (S_1.\operatorname {pauliErrorAt}(t_i) \cdot S_2.\operatorname {pauliErrorAt}(t_i))\), with \(S_1, S_2\) having Pauli errors in \(\mathcal{S}\). Since \(F_S\) is syndrome-free, concentrated at \(t_i\), and pure-space, it lies in the centralizer by \(\operatorname {centralizer\_ of\_ syndromeFree\_ pureSpace}\). Moreover, \(F_S.\operatorname {pauliErrorAt}(t_i) \notin \mathcal{S}\) (otherwise \(F.\operatorname {pauliErrorAt}(t_i) \in \mathcal{S}\) by group closure and the inverse, contradicting the hypothesis). Finally \(F_S.\operatorname {pauliErrorAt}(t_i) \neq 1\) (otherwise it would be in \(\mathcal{S}\)). Combining centralizer membership, non-membership in \(\mathcal{S}\), and non-identity gives \(\operatorname {isLogicalOp}\).

The three conditions are established directly:

1. Pure-time: by \(\operatorname {gaussStringFault\_ isPureTime}\).

2. Syndrome-free: by \(\operatorname {gaussStringFault\_ syndromeFree}\).

3. Flips the gauging sign when \(d\) is odd: by \(\operatorname {gaussStringFault\_ flipsSign\_ of\_ odd}\).

This follows directly from \(\operatorname {pureTime\_ logicalFault\_ weight\_ ge\_ d}\) from Lem 6, applied to \(F_T\) with the pure-time, syndrome-free, and sign-flipping hypotheses extracted from \(\operatorname {IsTimeLogicalFault}\).

This follows directly from \(\operatorname {gaussStringFault\_ flipsSign\_ of\_ odd}\).

This follows directly from \(\operatorname {pureSpace\_ preservesSign}\).

This is the symmetric form of \(\operatorname {SpacetimeFault.decompose\_ space\_ time}\).

This follows directly from \(F.\operatorname {weight\_ eq\_ space\_ plus\_ time}\).

Unfolding \(\mathrm{isPureSpace}\) and \(\mathrm{isPureTime}\) gives \(F_S.\mathrm{timeFaults} = \emptyset \) and \(F_T.\mathrm{spaceFaults} = \emptyset \). By extensionality, for the space-faults: \((F_S \cdot F_T).\mathrm{spaceComponent}.\mathrm{spaceFaults} = (F_S.\mathrm{spaceFaults} \mathbin {\triangle } \emptyset ) = F_S.\mathrm{spaceFaults}\). For the time-faults: the space component has time-faults from the symmetric difference of the original time-fault sets, but since \(F_S.\mathrm{timeFaults} = \emptyset \), the time-faults of the space component are empty.

Unfolding \(\mathrm{isPureSpace}\) and \(\mathrm{isPureTime}\) gives \(F_S.\mathrm{timeFaults} = \emptyset \) and \(F_T.\mathrm{spaceFaults} = \emptyset \). By extensionality, for the space-faults: the time component has space-faults from the composition, but since \(F_T.\mathrm{spaceFaults} = \emptyset \), the result is \(\emptyset \). For the time-faults: \((F_S \cdot F_T).\mathrm{timeComponent}.\mathrm{timeFaults} = (\emptyset \mathbin {\triangle } F_T.\mathrm{timeFaults}) = F_T.\mathrm{timeFaults}\).

Expanding the definition of weight as \(|\mathrm{spaceFaults}| + |\mathrm{timeFaults}|\) and using \(F_S.\mathrm{timeFaults} = \emptyset \) and \(F_T.\mathrm{spaceFaults} = \emptyset \), the symmetric differences simplify: \(|F_S.\mathrm{spaceFaults} \mathbin {\triangle } \emptyset | + |\emptyset \mathbin {\triangle } F_T.\mathrm{timeFaults}| = |F_S.\mathrm{spaceFaults}| + |F_T.\mathrm{timeFaults}|\), using \(S \mathbin {\triangle } \bot = S\) and \(\bot \mathbin {\triangle } S = S\).

By \(\operatorname {sign\_ flip\_ implies\_ odd\_ full\_ strings}\), the number of vertices \(v\) with \(\operatorname {gaussFaultCount}(\mathrm{proc}, v, F) = d\) is odd. In particular, the filter of such vertices is nonempty (an odd number cannot be zero). Let \(v\) be an element of this nonempty set, so \(\operatorname {gaussFaultCount}(\mathrm{proc}, v, F) = d\).

For an arbitrary round \(r\), we need to show the corresponding time-fault is in \(F.\mathrm{timeFaults}\). Consider round \(r_0 = 0\) (which exists since \(d {\gt} 0\) by oddness). By \(\operatorname {syndromeFree\_ gauss\_ all\_ or\_ none}\), for vertex \(v\), either all Gauss measurements at all rounds are in \(F.\mathrm{timeFaults}\), or none are. If the round-\(0\) measurement were absent, then by \(\operatorname {gaussFaultCount\_ zero\_ or\_ d}\), the count would be either \(0\) or \(d\). Since round \(0\) is absent, the count cannot be \(d\) (as the filter would have strictly fewer than \(|\operatorname {Fin}(d)|\) elements), so it would be \(0\), contradicting \(\operatorname {gaussFaultCount} = d {\gt} 0\). Therefore the round-\(0\) measurement is present, and by the all-or-none property, all rounds including \(r\) are present.

We proveeach part separately.

1. The decomposition is obtained from \(\operatorname {spaceTime\_ decomposition}\), extracting \(F_S\), \(F_T\), \(S\) and their properties (dropping the nontriviality clause which is not needed here).

2. The sign independence follows from the first component of \(\operatorname {space\_ time\_ independent\_ effects}(\mathrm{proc}, F)\).

3. The Pauli error independence follows from the second component of \(\operatorname {space\_ time\_ independent\_ effects}(\mathrm{proc}, F)\).

By \(\operatorname {compose\_ pureSpace\_ pureTime\_ weight}\), \(\operatorname {weight}(F_S \cdot F_T) = \operatorname {weight}(F_S) + \operatorname {weight}(F_T)\), and rewriting gives the inequality (which is in fact an equality).