By definition, \(\operatorname {gaussStringFault}(v)\) has empty space-faults, so \(\operatorname {isPureTime}\) holds by simplification.

Let \(r_1, r_2 \in \operatorname {Fin}(d)\) and suppose the images are equal. By injectivity of the \(\operatorname {phase2}\) and \(\operatorname {gaussLaw}\) constructors, we extract \(r_1 = r_2\).

Rewriting using the definition of \(\operatorname {gaussMeasFaults}\), the cardinality of the image of an injective function equals the cardinality of the domain, which is \(|\operatorname {Fin}(d)| = d\).

By simplification using the definitions of weight and \(\operatorname {gaussStringFault}\), the weight equals \(|\emptyset | + |\operatorname {gaussMeasFaults}(v)| = 0 + d = d\).

By simplification of the membership condition in the image finset. Both directions follow by exhibiting the witness \(r\).

This holds by reflexivity (definitional equality).

Rewriting using \(\operatorname {gaussStringFault\_ timeFaults\_ eq}\) and \(\operatorname {mem\_ gaussMeasFaults}\), the witness \(r\) itself suffices.

Rewriting using \(\operatorname {gaussStringFault\_ timeFaults\_ eq}\) and \(\operatorname {mem\_ gaussMeasFaults}\), we push the negation inward. For any candidate round \(r'\), the equality hypothesis forces \(v = w\) by injectivity of the \(\operatorname {gaussLaw}\) constructor, contradicting \(v \neq w\).

Unfolding \(\operatorname {gaussSignFlip}\), we establish that for each vertex \(w\), the inner sum \(\sum _{r \in \operatorname {Fin}(d)} [\langle \operatorname {phase2}(\operatorname {gaussLaw}(w,r))\rangle \in F.\mathrm{timeFaults}]\) equals \(d \pmod{2}\) if \(w = v\) and \(0\) otherwise. For \(w = v\): by \(\operatorname {gaussStringFault\_ mem\_ gauss}\), every indicator is \(1\), and the constant sum gives \(d \cdot 1 = d\). For \(w \neq v\): by \(\operatorname {gaussStringFault\_ no\_ other\_ gauss}\), every indicator is \(0\). Substituting these values, the outer sum over \(V\) reduces to a single term at \(v\) by \(\sum _{w \in V} [\! [w = v]\! ] \cdot (d \bmod 2) = d \pmod{2}\).

Rewriting \(\operatorname {FlipsGaugingSign}\) and applying \(\operatorname {gaussStringFault\_ signFlip}\), the goal becomes \(d \pmod{2} = 1\), which holds since \(d\) is odd.

We verify that no detector is violated by case analysis on the detector index type:

Case \(\operatorname {phase1Repeated}(j, r, r', hr)\): The Phase 1 repeated detector involves Phase 1 measurements, which are disjoint from the Gauss Phase 2 measurements in the \(A_v\) string. We apply \(\operatorname {not\_ isViolated\_ disjoint}\): for each measurement \(m\) in the detector, it cannot be a Gauss \(A_v\) measurement at any round, established by simplification of the constructors.

Case \(\operatorname {phase2GaussRepeated}(w, r, r', hr)\): This detector compares \(A_w\) at consecutive rounds \(r\) and \(r'\). Rewriting using \(\operatorname {isViolated\_ iff\_ flipParity}\) and unfolding the detector, the flip parity is a sum over a pair of measurements. If \(v = w\): both measurements are in the string by \(\operatorname {gaussStringFault\_ mem\_ gauss}\), so both indicators are \(1\) and the sum is \(1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) (by the characteristic-two identity). If \(v \neq w\): both measurements are absent by \(\operatorname {gaussStringFault\_ no\_ other\_ gauss}\), so both indicators are \(0\) and the sum is \(0\).

Case \(\operatorname {phase2FluxRepeated}(p, r, r', hr)\): The flux repeated detector involves flux measurements \(B_p\), which are disjoint from Gauss \(A_v\) measurements. We apply \(\operatorname {not\_ isViolated\_ disjoint}\) with the observation that no flux measurement equals a Gauss measurement.

Case \(\operatorname {phase2DeformedRepeated}(j, r, r', hr)\): The deformed repeated detector involves deformed check measurements \(\tilde{s}_j\), which are disjoint from Gauss \(A_v\) measurements. We apply \(\operatorname {not\_ isViolated\_ disjoint}\) similarly.

Case \(\operatorname {phase3Repeated}(j, r, r', hr)\): The Phase 3 repeated detector involves Phase 3 measurements, disjoint from Phase 2 Gauss measurements. We apply \(\operatorname {not\_ isViolated\_ disjoint}\).

Case \(\operatorname {fluxInit}(p)\): The flux initialization detector involves edge initialization and flux measurements, both disjoint from Gauss \(A_v\) measurements. We apply \(\operatorname {not\_ isViolated\_ disjoint}\).

Case \(\operatorname {deformedInit}(j)\): The deformed initialization detector involves edge initialization, Phase 1, and deformed measurements, all disjoint from Gauss \(A_v\) measurements. We apply \(\operatorname {not\_ isViolated\_ disjoint}\).

Case \(\operatorname {fluxUngauge}(p)\): The flux ungauge detector involves Phase 3 and flux measurements, disjoint from Gauss measurements. We apply \(\operatorname {not\_ isViolated\_ disjoint}\).

Case \(\operatorname {deformedUngauge}(j)\): The deformed ungauge detector involves Phase 3, deformed, and edge-\(Z\) measurements, all disjoint from Gauss measurements. We apply \(\operatorname {not\_ isViolated\_ disjoint}\).

The fault is syndrome-free by \(\operatorname {gaussStringFault\_ syndromeFree}\). It does not preserve the gauging sign because, rewriting \(\operatorname {PreservesGaugingSign}\) and applying \(\operatorname {gaussStringFault\_ signFlip}\), we get \(\operatorname {gaussSignFlip} = d \pmod{2} = 1 \neq 0\) since \(d\) is odd.

Unfolding the definition of \(d_{\mathrm{time}}\) as an infimum, we apply \(\operatorname {Nat.sInf\_ le}\) with the witness \(\operatorname {gaussStringFault}(v)\). This fault is pure-time (by \(\operatorname {gaussStringFault\_ isPureTime}\)), is a gauging logical fault (by \(\operatorname {gaussStringFault\_ isLogicalFault}\)), and has weight \(d\) (by \(\operatorname {gaussStringFault\_ weight\_ eq\_ d}\)).

By \(\operatorname {isPureTime}\), the space-faults are empty: \(F.\mathrm{spaceFaults} = \emptyset \). Thus \(\operatorname {weight}(F) = |\emptyset | + |F.\mathrm{timeFaults}| = |F.\mathrm{timeFaults}|\).

Unfolding both definitions, we apply congruence. For each vertex \(v\), rewriting the cardinality of the filter using \(\operatorname {Finset.card\_ filter}\) and simplifying with \(\operatorname {Finset.sum\_ boole}\) gives the equality.

The syndrome-freeness hypothesis applied to the detector \(\operatorname {phase2GaussRepeated}(v, r, r', hr)\) gives that this detector is not violated. Rewriting using \(\operatorname {isViolated\_ iff\_ flipParity}\) and unfolding the Gauss repeated detector, the flip parity is a sum over the pair \(\{ m_r, m_{r'}\} \). Since \(r \neq r'\) (as \(r + 1 = r'\)), this is a two-element sum. We perform case analysis on whether each measurement is in \(F.\mathrm{timeFaults}\): if both are present or both absent, the sum is \(0\) (consistent with non-violation); if exactly one is present, the sum is \(1\) (contradicting non-violation). This establishes the biconditional.

It suffices to show the claim for \(r \leq r'\) (the other direction follows by symmetry of the biconditional). We proceed by induction on the difference \(k = r' - r\).

Base case (\(k = 0\)): Then \(r = r'\) by \(\operatorname {Fin.ext}\), so the biconditional holds by reflexivity.

Inductive step (\(k = n + 1\)): We have \(r' = r + n + 1\). By the induction hypothesis, the fault status at round \(r\) equals that at round \(r + n\). By \(\operatorname {syndromeFree\_ gauss\_ consecutive}\), the fault status at round \(r + n\) equals that at round \(r + n + 1 = r'\). Composing these two biconditionals via transitivity gives the result.

Unfolding \(\operatorname {gaussFaultCount}\), if \(d = 0\) then the filter over \(\operatorname {Fin}(0)\) is empty, giving count \(0\). Otherwise, \(d {\gt} 0\) and we let \(r_0 = 0 \in \operatorname {Fin}(d)\). By case analysis on whether \(A_v\) at round \(r_0\) is faulted:

If faulted: by \(\operatorname {syndromeFree\_ gauss\_ all\_ or\_ none}\), every round \(r\) is faulted, so the filter equals \(\operatorname {Fin}(d)\) and the count is \(d\).

If not faulted: by \(\operatorname {syndromeFree\_ gauss\_ all\_ or\_ none}\), no round \(r\) is faulted (any faulted round would imply \(r_0\) is faulted), so the filter is empty and the count is \(0\).

By \(\operatorname {gaussFaultCount\_ zero\_ or\_ d}\), the count is \(0\) or \(d\). In either case, the corresponding congruence modulo \(2\) follows by simplification.

Rewriting \(\operatorname {FlipsGaugingSign}\) and applying \(\operatorname {gaussSignFlip\_ eq\_ sum\_ parities}\), we have \(\sum _{v \in V} \operatorname {gaussFaultCount}(v, F) \equiv 1 \pmod{2}\). Since \(d\) is odd, \(d \equiv 1 \pmod{2}\). By \(\operatorname {gaussFaultParity\_ zero\_ or\_ d}\), each summand is either \(0\) or \(1\) in \(\mathbb {Z}/2\mathbb {Z}\). The sum therefore equals the cardinality (mod 2) of the set \(\{ v \mid \operatorname {gaussFaultCount}(v,F) \equiv 1 \pmod{2}\} \). We verify this filter equals \(\{ v \mid \operatorname {gaussFaultCount}(v,F) = d\} \) using \(\operatorname {gaussFaultCount\_ zero\_ or\_ d}\): count \(= 0\) gives parity \(0\), and count \(= d\) gives parity \(1\) (since \(d\) is odd). The cardinality being \(1 \pmod{2}\) means the set has odd cardinality, as verified by \(\operatorname {ZMod.natCast\_ eq\_ one\_ iff\_ odd}\).

Rewriting the weight as \(|F.\mathrm{timeFaults}|\) using \(\operatorname {pureTime\_ weight\_ eq\_ card}\), we show that the biUnion of the mapped Gauss faults (over all vertices) is a subset of \(F.\mathrm{timeFaults}\): each element of the biUnion is obtained from some \(\langle \operatorname {phase2}(\operatorname {gaussLaw}(v,r)) \rangle \) that is in \(F.\mathrm{timeFaults}\) by the filter condition. The sum of cardinalities of the per-vertex image sets equals the cardinality of their disjoint union (since different vertices produce distinct measurement labels by injectivity of the \(\operatorname {gaussLaw}\) constructor). Thus \(\sum _v \operatorname {gaussFaultCount}(v,F) = |\text{biUnion}| \leq |F.\mathrm{timeFaults}|\) by monotonicity of cardinality.

By a chain of inequalities:

where the first inequality uses that a single term of a nonneg sum is at most the total sum (\(\operatorname {Finset.single\_ le\_ sum}\)), and the second is \(\operatorname {pureTime\_ weight\_ ge\_ gauss\_ sum}\).

By \(\operatorname {sign\_ flip\_ implies\_ odd\_ full\_ strings}\), the set \(\{ v \mid \operatorname {gaussFaultCount}(v, F) = d\} \) has odd cardinality, hence is nonempty. Let \(v\) be an element of this set. Then \(\operatorname {gaussFaultCount}(v, F) = d\), and by \(\operatorname {pureTime\_ weight\_ ge\_ d\_ of\_ full\_ string}\), we conclude \(d \leq \operatorname {weight}(F)\).

Unfolding \(d_{\mathrm{time}}\) as an infimum, we perform case analysis on whether the set of pure-time logical fault weights is nonempty.

If nonempty: we apply \(\operatorname {le\_ csInf}\) and take an arbitrary element \(w\) with witness \(F\) satisfying \(\operatorname {IsPureTimeFault}(F)\), \(\operatorname {IsGaugingLogicalFault}(F)\), and \(\operatorname {weight}(F) = w\). The gauging logical fault condition gives syndrome-freeness and non-preservation of the sign. By \(\operatorname {gaussSignFlip\_ zero\_ or\_ one}\), the sign flip is either \(0\) or \(1\); since it is not \(0\) (non-preservation), it is \(1\), meaning the fault flips the sign. By \(\operatorname {pureTime\_ logicalFault\_ weight\_ ge\_ d}\), \(d \leq \operatorname {weight}(F) = w\).

If empty: we derive a contradiction, since \(\operatorname {gaussStringFault}(v)\) (for \(v \in V\) from nonemptiness) is a pure-time logical fault of weight \(d\), so \(d\) belongs to the weight set, contradicting emptiness.

By antisymmetry: \(d_{\mathrm{time}} \leq d\) from \(\operatorname {timeFaultDistance\_ le\_ d}\) and \(d \leq d_{\mathrm{time}}\) from \(\operatorname {timeFaultDistance\_ ge\_ d}\).

This follows directly from \(\operatorname {spacetimeStabilizer\_ completeness}\) applied to \(F\) with the pair of hypotheses (syndrome-freeness and sign preservation).

By \(\operatorname {flipsOrPreserves}\), either \(F\) flips or preserves the gauging sign. In the first case, the left disjunct holds. In the second case, we combine the preservation hypothesis with \(\operatorname {pureTime\_ preservesSign\_ decomposes\_ into\_ generators}\) to obtain the generator decomposition.

The fault is syndrome-free by hypothesis. Suppose for contradiction that the sign is not preserved. By \(\operatorname {gaussSignFlip\_ zero\_ or\_ one}\), the sign flip is \(0\) or \(1\); since it is not \(0\), it is \(1\), meaning the fault flips the sign. By \(\operatorname {pureTime\_ logicalFault\_ weight\_ ge\_ d}\), \(d \leq \operatorname {weight}(F)\), contradicting \(\operatorname {weight}(F) {\lt} d\).

This is exactly \(\operatorname {gaussFaultCount\_ zero\_ or\_ d}\).

Rewriting using \(\operatorname {timeFaultDistance\_ eq\_ d}\) and \(\operatorname {phase2\_ duration}\).

By \(\operatorname {sign\_ flip\_ implies\_ odd\_ full\_ strings}\), the set \(S = \{ v \mid \operatorname {gaussFaultCount}(v, F) = d\} \) has odd cardinality, hence \(|S| \geq 1\). We show \(|S| \leq 1\) by contradiction: if \(|S| \geq 2\), there exist distinct \(v_1, v_2 \in S\) with \(\operatorname {gaussFaultCount}(v_i, F) = d\). Then

where the second inequality is \(\operatorname {pureTime\_ weight\_ ge\_ gauss\_ sum}\), giving \(2d \leq d\). Since \(d {\gt} 0\) (as \(d\) is odd), this is a contradiction. Therefore \(|S| = 1\).