This follows from \(\texttt{Nat.sub\_ pos\_ iff\_ lt}\) applied to the hypothesis \(t_i {\lt} t_o\).

This follows directly from \(t_i {\lt} t_o\) by \(\texttt{Nat.le\_ of\_ lt}\).

We unfold \(\texttt{SpacetimeFault.weight}\). Since \(F\) is a pure time fault, we establish that \(F.\mathrm{spaceErrorLocations}(\mathrm{times}) = \emptyset \): for any pair \((q, t)\), the pure time condition ensures all space errors are trivial, so the filter yields the empty set. Simplifying with \(|\emptyset | = 0\) and \(0 + \cdot \), the weight equals \(|F.\mathrm{timeErrorLocations}(\mathrm{times})|\).

We unfold the definition of \(\texttt{violatesComparisonDetector}\). The hypothesis \(\neg \mathrm{violates}\) gives us (after simplifying the double negation) that the two parity predicates are equal. Using \(t \neq 0\) to resolve the conditional, we obtain the biconditional by \(\texttt{Iff.of\_ eq}\).

Without loss of generality, assume \(t_1 \leq t_2\) (symmetry handles the other case). Write \(t_2 = t_1 + d\) for some \(d \geq 0\). We proceed by induction on \(d\).

Base case (\(d = 0\)): The statement is trivial by reflexivity.

Inductive step (\(d \to d+1\)): By the inductive hypothesis, \(\mathrm{Odd}(\mathrm{timeFaultCountAt}(F, m, t_1)) \Leftrightarrow \mathrm{Odd}(\mathrm{timeFaultCountAt}(F, m, t_1 + d))\). Since \(t_1 + d + 1\) is in the interior (by arithmetic from \(t_i {\lt} t_1 + d + 1 {\lt} t_o\)) and the detector at \(t_1 + d + 1\) is not violated, Lemma 911 gives that \(\mathrm{Odd}(\mathrm{timeFaultCountAt}(F, m, t_1 + d + 1)) \Leftrightarrow \mathrm{Odd}(\mathrm{timeFaultCountAt}(F, m, t_1 + d))\). Chaining the two biconditionals yields the result after simplifying \((t_1 + d + 1) - 1 = t_1 + d\).

Let \(t \in [t_i, t_o)\). By Lemma 912, \(\mathrm{Odd}(\mathrm{timeFaultCountAt}(F, m, t_0)) \Leftrightarrow \mathrm{Odd}(\mathrm{timeFaultCountAt}(F, m, t))\). Since the count at \(t_0\) is odd, so is the count at \(t\). From \(\mathrm{Odd}(k)\), we obtain \(k = 2j + 1\) for some \(j\), hence \(k {\gt} 0\) by arithmetic (\(\omega \)).

Let \(m\), \(t_0\), \(h_{t_0 \geq }\), \(h_{t_0 {\lt}}\), and \(h_{\mathrm{odd}}\) be obtained from the existence hypothesis. We rewrite the weight using Lemma 907 (since \(F\) is pure time), reducing the goal to \(I.\mathrm{numRounds} \leq |F.\mathrm{timeErrorLocations}(\mathrm{times})|\).

By Lemma 913, for every \(t \in [t_i, t_o)\), the fault count at \((m, t)\) is positive, so \(F.\mathrm{timeErrors}(m, t) = \mathrm{true}\). We define the injection \(f(t) = (m, t)\), which is injective since the second component determines \(t\). The image of the interval rounds \(\mathrm{Ico}(t_i, t_o)\) under \(f\) is contained in \(F.\mathrm{timeErrorLocations}(\mathrm{times})\), since each \(t \in [t_i, t_o)\) is in \(\mathrm{times}\) (by the interval inclusion hypothesis) and has \(F.\mathrm{timeErrors}(m, t) = \mathrm{true}\).

Therefore:

This holds by definitional equality (reflexivity).

Let \(q\) and \(t\) be arbitrary. By the definition of \(\mathrm{Av\_ chain}\), the space errors are all identity, so \(F.\mathrm{isPureTime}\) holds by simplification.

By simplification of the \(\mathrm{Av\_ chain\_ timeErrors}\) equation: the decision procedure yields true since \(m = m\), \(t_i \leq t\), and \(t {\lt} t_o\) all hold.

We unfold \(\mathrm{timeFaultCountAt}\) and rewrite using Lemma 920, which gives \(\mathrm{timeErrors}(m, t) = \mathrm{true}\). The conditional evaluates to \(1\).

We unfold \(\mathrm{timeFaultCountAt}\) and simplify \(\mathrm{Av\_ chain\_ timeErrors}\). If the decision procedure returns true, we obtain \(t_i \leq t\) and \(t {\lt} t_o\), which contradicts \(t {\lt} t_i\) (in the first case) or \(t_o \leq t\) (in the second case) by irreflexivity of \({\lt}\) on \(\mathbb {N}\). Otherwise, the conditional evaluates to \(0\) by reflexivity.

Let \(t\) with \(t_i {\lt} t {\lt} t_o\). We unfold \(\mathrm{violatesComparisonDetector}\) and show equality of parities. Since \(t_i \leq t\) and \(t_i \leq t - 1\) (from \(t_i {\lt} t\)), and both \(t {\lt} t_o\) and \(t - 1 {\lt} t_o\) hold, Lemma 921 gives both counts equal to \(1\). Since \(t \neq 0\) (from \(t_i {\lt} t\) and \(t_i \geq 0\)), the previous-time conditional resolves, and the two counts being equal implies equal parities.

We first rewrite the weight using Lemma 907 (applicable since the \(A_v\) chain is pure time by Lemma 919). We then show that \(\mathrm{timeErrorLocations}(\mathrm{times})\) equals the image of \(\mathrm{intervalRounds}(I)\) under \(t \mapsto (m, t)\): by extensionality on pairs \((m', t)\), the forward direction uses the time error characterization and the reverse uses the interval inclusion hypothesis. After this identification, \(|\mathrm{map}(f, \mathrm{Ico}(t_i, t_o))| = |\mathrm{Ico}(t_i, t_o)| = t_o - t_i = I.\mathrm{numRounds}\).

We unfold \(\mathrm{gaugingLogicalEffect}\) and witness \(m\). The filter of times \(t \in [t_i, t_o)\) with \(\mathrm{timeErrors}(m, t) = \mathrm{true}\) equals the full interval \(\mathrm{Ico}(t_i, t_o)\): by extensionality, for any \(t\) with \(t_i \leq t {\lt} t_o\), the \(A_v\) chain has \(\mathrm{timeErrors}(m, t) = \mathrm{true}\) (by Lemma 918 with \(m = m\)). Rewriting and using \(|\mathrm{Ico}(t_i, t_o)| = t_o - t_i = I.\mathrm{numRounds}\), the result follows from the hypothesis that \(I.\mathrm{numRounds}\) is odd.

We unfold \(\mathrm{gaugingLogicalEffect'}\) and witness \(m\). We rewrite using \(\texttt{Finset.nonempty\_ iff\_ ne\_ empty}\) and \(\texttt{Finset.filter\_ nonempty\_ iff}\). We use \(t_i\) as witness: \(t_i \in \mathrm{Ico}(t_i, t_o)\) since \(t_i \leq t_i\) and \(t_i {\lt} t_o\) (by \(I.\mathrm{initial\_ lt\_ final}\)), and \(\mathrm{Av\_ chain\_ timeErrors}\) evaluates to true with \(m = m\), \(t_i \leq t_i\), and \(t_i {\lt} t_o\).

We verify the two conditions of \(\mathrm{IsSpacetimeLogicalFault}\) using \(\texttt{constructor}\).

Empty syndrome: We rewrite using \(\texttt{hasEmptySyndrome\_ iff}\). For each detector \(D\) in the collection, the hypothesis \(\texttt{h\_ all\_ detectors}\) provides an interior time \(t\) with \(t_i {\lt} t {\lt} t_o\) and a biconditional relating detector satisfaction to non-violation of the comparison detector. By Lemma 923, the comparison detector is not violated, so the detector is satisfied.

Affects logical: This follows directly from Lemma 928.

The result is the pair \(\langle h_{\mathrm{empty}}, h_{\mathrm{preserves}}\rangle \) of the two hypotheses: empty syndrome and preservation of logical information.

We use the canonical decomposition \(\mathrm{type2\_ decomposition}(s)\). The three properties follow directly from the fields \(\mathrm{propagatorGens\_ are\_ propagators}\), \(\mathrm{initialGen\_ is\_ initial}\), and \(\mathrm{finalGen\_ is\_ final}\) of the decomposition.

This follows directly from Theorem 916 applied to \(F\), \(I\), \(\mathrm{times}\), and the given hypotheses.

We use \(\texttt{refine}\) to split into the three parts.

Part 1 (The \(A_v\) chain is a pure time logical fault): We construct the pair. The first component follows from Theorem 929 applied with the detector hypotheses. The second component follows from Lemma 919.

Part 2 (Weight equals \(\mathrm{numRounds}\)): This is exactly Theorem 924 applied to \(m\), \(I\), \(\mathrm{times}\), and the interval inclusion hypothesis.

Part 3 (Lower bound for all pure time logical faults): Let \(F\) be a pure time logical fault with the given properties. Decomposing the membership \(F \in \mathrm{pureTimeLogicalFaults}\) yields \(\mathrm{IsSpacetimeLogicalFault}\) and \(\mathrm{isPureTimeFault}\). The bound follows from Theorem 916 applied to \(F\), \(I\), \(\mathrm{times}\), the pure time hypothesis, the interval inclusion, the no-violation hypothesis, and the fault existence hypothesis.

This follows directly from Theorem 924.