Quantum and Circuits

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \section*{The purpose and evidence contract}
2 This companion explains the actual Lean source behind the Circuit Obstructions
3 main paper. It supplies the computational model, the meaning of its predicates,
4 the route from legal gates to the joint lower bound, and all 115 indexed
5 theorem types with exact source locations. The written arguments are explained
6 for a mathematical reader; the source proof terms remain authoritative.
7 
8 The formal source has 115 indexed theorem declarations across eight modules.\begin{statusbox}{Current formal verification}Fresh source compilation, axiom inspection, and replay of all eight modules passed. All eight deliberately invalid or forbidden controls were rejected. The source package preserves the complete current receipt and logs alongside historical evidence.\end{statusbox}
9 
10 The formal subset consists of C01, the maintained NCT sharing-degree dependency
11 from F3, and the numerical lower-bound part of C02. C02's evaluation-span dual,
12 affine-input invariance and general monotone ideal, together with C03--C08,
13 remain outside this block. A theorem-name count is not a count of independent
14 discoveries. Forty declarations were inherited and 75 added in Block 02.
15 
16 \begin{tabularx}{\textwidth}{@{}>{\raggedright\arraybackslash}p{1.35in}>{\raggedright\arraybackslash}X@{}}\toprule
17 Part & Reader's task\\\midrule
18 Explanatory body & Check the hypotheses and how the predicates represent Boolean mathematics\\
19 Proof dependencies & Follow legal reversibility, cut coverage, shared degree, balancing and affine compilation\\
20 Evidence chapters & Distinguish written reasoning, exact finite checks, text scans and archived kernel checking\\
21 Declaration register & Inspect each complete elaborated type, file, line, block and axiom set\\\bottomrule
22 \end{tabularx}
23 
24 The guide does not supply a new toolchain, an independent checker or independent
25 human review. It preserves the original rights record and the original release
26 files. There is no new publication-novelty or unrestricted hardness claim.
27 \clearpage
28 \section*{The formal endpoint}
29 \addcontentsline{toc}{section}{The formal endpoint}
30 Let $c$ be a finite legal classical NOT/CNOT/Toffoli circuit. For $n$ input bits and $a$ zero-initialized ancillas, assume for every $x$ and both initial target values $b$ that
31 \[
32 \operatorname{run}(c)(x,0^a,b)=(x,0^a,b\x f(x)).
33 \]
34 Write $T=\TC(c)$ for its number of Toffoli gates. The Block 02 joint endpoint is
35 \begin{statusbox}{Degree and complete-cover bound}
36 \[
37 \boxed{\Deg(T+1,f)\quad\text{and}\quad 2\beta^*(f)\le T+3.}
38 \]
39 \pathref{CircuitObstructions.restored_degree_and_cover_bound}
40 \end{statusbox}
41 The first conclusion is an explicit certificate that $f$ has a Boolean polynomial representation of degree at most $T+1$. The second is the affine-optimized complete safe-cover lower bound, equivalently $T\ge\max\{0,2\beta^*(f)-3\}$.
42 
43 This applies even when the output controls intermediate gates, the inputs are modified temporarily, and workspace is dirty internally. It requires restoration only at the boundary. It makes no restriction to clean intermediate representations.
44 
45 \subsection*{What changed}
46 Block 01 proved that discrepancies between a prefix and an inverse suffix form a complete safe cover. Block 02 supplies the missing degree dependency, proves that the cover parameters exist, constructs the balanced cut, and implements affine-output adjustment using legal zero-Toffoli circuits.
47 
48 \subsection*{What did not change}
49 The mathematical scope remains the eight maintained claim groups. C02 is still partial as a group: its dual-certificate theorem is not included. The formal source also proves
50 \[
51 \beta(f)\le\beta^*(f)\le n.
52 \]
53 This ceiling prevents the degree parameter alone from producing a superpolynomial lower bound. No new best-known bound or publication-novelty claim is made.
54 
55 \subsection*{Where the proof lives}
56 Every proof term is in \pathref{formalization/lean/CircuitObstructions/}. The source inventory, archived 21 September elaboration log, and archived axiom report identify the exact statements. The register in this document lists all 115 maintained theorem declarations, including the 40 inherited declarations. Imported standard-library theorems are not counted.
57 
58 \pagehead{Model and definitions}{THE ASSUMPTIONS ARE PART OF THE THEOREM}
59 A general register state is a Boolean function $W\to\mathrm{Bool}$ on any wire type with decidable equality. C01 does not assume that $W$ is finite. The canonical degree model has a finite wire set with $n$ input wires, $a$ ancillas, and one target. A NOT complements a bit. A CNOT adds one control to a distinct target. A Toffoli adds the product of two distinct controls to a third distinct wire. Gate constructors carry the required inequalities.
60 
61 All arithmetic is over $\mathbb F_2$, implemented using Boolean XOR and AND. Each gate is its own inverse. Circuit reversal, restoration, and every cut are inherited from the unchanged Block 01 source.
62 
63 \begin{tabularx}{\linewidth}{@{}>{\raggedright\arraybackslash}p{1.25in}>{\raggedright\arraybackslash}X@{}}\toprule
64 Quantity & Meaning in the formal source\\\midrule
65 $T$ & Toffoli count. NOT and CNOT have cost zero in this count only.\\
66 $\Deg(d,f)$ & $f$ is an XOR of finitely many monomials, each containing at most $d$ variable occurrences.\\
67 Safe detector & A Boolean $h$ with $h(x)=1\Rightarrow f(x)=1$.\\
68 Complete coverage & Every positive $v$ has a safe detector with $h(v)=1$.\\
69 $\beta(f)$ & Least degree bound sufficient for complete safe coverage.\\
70 $\beta^*(f)$ & Least upper bound on $\beta(f\x g)$ over all degree-one $g$.\\\bottomrule
71 \end{tabularx}
72 
73 \subsection*{Polynomial certificates are not postulated degree oracles}
74 The inductive certificate has three constructors: zero, a bounded-length monomial, and XOR of two certified functions. It is tied to the concrete evaluator
75 \[
76 \operatorname{polyEval}(p,x)=\bigoplus_{L\in p}\prod_{i\in L}x_i
77 \]
78 by a proved equivalence. A certificate yields an explicit finite monomial list, and such a list yields a certificate.
79 
80 Repeated variables are allowed in the list. Boolean idempotence reduces their repetitions without increasing degree. This is the representation form of the usual Boolean degree bound. The formal source does not separately implement canonical ANF normalization or claim that extracting every homogeneous grade is free.
81 
82 \subsection*{Boundary of the model}
83 There are no quantum phases, measurements, or discarded work registers. Inputs and zero ancillas restore for every logical input and both target values. Standard classical choice defines least semantic bounds, but supplies no polynomial-time procedure for finding their witnesses.
84 
85 \pagehead{Why sharing does not break the degree bound}{A STRONGER INVARIANT THAN SINGLE-REGISTER DEGREE}
86 For a current state $s(x)$ after $t$ Toffolis, the invariant is
87 \[
88 \forall L,\qquad
89 \Deg\!\left(t+|L|,\;x\mapsto\prod_{i\in L}s_i(x)\right).
90 \]
91 $L$ may be any finite list, including repeated registers. Initially each coordinate is a variable or a constant, so a product of $r$ coordinates has degree at most $r$.
92 
93 Suppose the next gate toggles target $u$ by the product of a control list of length $q$. A product that omits $u$ is unchanged. If $u$ occurs, idempotence removes all its repetitions. With $R$ the remaining list, the updated product is
94 \[
95 \left(s_u\prod_{i\in R}s_i\right)
96 \x
97 \left(\prod_{j\in\mathrm{controls}}s_j\prod_{i\in R}s_i\right).
98 \]
99 The two old-state products have certified degrees at most
100 \[
101 t+1+|R|\qquad\text{and}\qquad t+q+|R|.
102 \]
103 Since $|R|+1\le |L|$, the invariant's budget rises by at most $\max\{q-1,0\}$: zero for NOT and CNOT, one for Toffoli.
104 
105 Induction along the actual gate list gives
106 \[
107 \Deg\!\left(T+r,\;x\mapsto\prod_{i\in L}\operatorname{run}(c)(s(x))_i\right),
108 \qquad r=|L|.
109 \]
110 With $r=1$, every register has degree at most $T+1$.
111 
112 \begin{statusbox}{Why this handles a DAG rather than just a formula}
113 The proof never unfolds a reused intermediate value into duplicated computation. It estimates arbitrary products of the current registers in one shared state. The budget increases once per actual Toffoli, including when its controls share earlier work or its target participates in feedback.
114 \end{statusbox}
115 
116 The statements are \pathref{workspaceDegree_run} and \pathref{canonical_run_coordinate_degree}. This formalizes the maintained NCT specialization of F3. A separate generic XOR--AND circuit syntax and simulation theorem are not added here.
117 
118 \pagehead{From the cut to a numerical lower bound}{EXISTENCE, BALANCE, AND COMPLETE COVERAGE}
119 Write $c=p\mathbin{++}q$. At this cut, Block 01 defines
120 \[
121 H_i(x)=\operatorname{run}(p)(x,0^a,0)_i\x
122        \operatorname{run}(q^{-1})(x,0^a,0)_i
123 \]
124 and proves
125 \[
126 H_i\le f,\qquad f(x)=1\iff\exists i\;H_i(x)=1.
127 \]
128 Reversal does not change Toffoli count. The new coordinate degree theorem therefore gives
129 \[
130 \deg(H_i)\le\max\{\TC(p),\TC(q)\}+1.
131 \]
132 
133 \subsection*{The least safe degree exists}
134 For a positive $v$, take the point indicator
135 \[
136 \delta_v(x)=\prod_{i=1}^{n}
137 \begin{cases}
138 x_i,&v_i=1,\\
139 1+x_i,&v_i=0.
140 \end{cases}
141 \]
142 It is safe, detects $v$, and has a degree-$n$ certificate. Hence complete safe coverage exists at degree $n$ for every function. Strong induction proves the existence of a least admissible natural degree. The definition \pathref{beta} chooses this bound and its specification and minimality are proved.
143 
144 \subsection*{The balanced cut is constructed}
145 Because each gate has cost zero or one, a prefix can realize every Toffoli count from zero to $T$. The source proves this fact and extracts a cut with
146 \[
147 \max\{\TC(p),\TC(q)\}\le\left\lceil T/2\right\rceil.
148 \]
149 The complete safe cut cover then proves
150 \[
151 \beta(f)\le\left\lceil T/2\right\rceil+1,
152 \qquad\boxed{2\beta(f)\le T+3.}
153 \]
154 Natural-number arithmetic retains the floor/ceiling and small-$T$ cases. No balance assumption is added to the final theorem.
155 
156 \pagehead{Affine output adjustment is an actual circuit}{THE OPTIMIZATION DOES NOT ASSUME A CLEAN NORMAL FORM}
157 For every degree-one Boolean function $g$, the source constructs a restored implementation with zero Toffolis.
158 
159 A constant is computed by the empty circuit or target NOT. An input variable uses a legal input-to-target CNOT. XOR is implemented by concatenating restored circuits. Induction on a degree-one certificate gives the general construction.
160 
161 If $c$ restores $f$ and $d$ restores $g$, their concatenation restores $f\x g$. For the affine implementation,
162 \[
163 \TC(c\mathbin{++}d)=\TC(c).
164 \]
165 The unoptimized bound applies to every affine $g$ at the same $T$. Define $\beta^*(f)$ as the least upper bound of those $\beta(f\x g)$ values. Existence follows from their common upper bound $n$.
166 
167 Therefore
168 \[
169 \boxed{2\beta^*(f)\le T+3,\qquad \beta(f)\le\beta^*(f)\le n.}
170 \]
171 The final output at initial target zero is exactly $f$, so the forward coordinate theorem also gives $\Deg(T+1,f)$. The joint endpoint combines these two proved conclusions.
172 
173 \subsection*{Nonvacuity: two-input AND}
174 Every degree-one function on two inputs has zero XOR over the four corners of the input square. AND has corner XOR one. Thus AND has no degree-one certificate.
175 
176 A degree-one complete safe cover for AND would include a detector of its sole accepting input. Safety forces that detector to be AND itself, contradicting the corner-parity lemma. The degree-two monomial is a valid detector. The source proves
177 \[
178 \beta(\mathrm{AND}_2)=\beta^*(\mathrm{AND}_2)=2
179 \]
180 and therefore every restored implementation of AND$_2$ uses at least one Toffoli.
181 
182 This is a theorem about all implementations in the model, not an exhaustive search through circuits. It does not formalize the general $k$-input monomial optimum.
183 
184 \pagehead{Verification and proof boundaries}{UNIVERSAL PROOFS AND FINITE CONTROLS REMAIN DISTINCT}
185 \begin{tabularx}{\linewidth}{@{}>{\raggedright\arraybackslash}p{1.9in}r>{\raggedright\arraybackslash}X@{}}\toprule
186 Module & Count & Formal role\\\midrule
187 Gates & 16 & Inherited legal primitives and reversal\\
188 CutComparison & 13 & Inherited complete cut cover\\
189 Examples & 11 & Inherited dirty and output-active controls\\
190 Degree & 19 & Polynomial certificates and closure\\
191 MultiplicativeDegree & 12 & Degree invariant with sharing\\
192 SafeDegree & 22 & Least complete degree and balanced cuts\\
193 AffineOutput & 14 & Affine compiler and optimized bound\\
194 DegreeChecks & 8 & AND2 exclusion and exact parameters\\\midrule
195 Total & 115 & 75 new declarations, 40 inherited\\\bottomrule
196 \end{tabularx}
197 
198 The current audit rebuilt all source in a fresh project directory, treated warnings as errors, printed each declaration's type and axiom dependencies, and replayed all eight modules through the bundled checker. Its eight deliberately invalid or forbidden controls were rejected.
199 
200 Only \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound} occur in the archived audited dependencies. No custom axiom, admitted proof, native-decision oracle, or kernel bypass is used. Lean 4.34.0-rc2 and its bundled Std are pinned. This checker shares the toolchain's trust boundary and is not an independent implementation or human review.
201 
202 The separate Python checker, freshly reproduced in this edition, uses exact truth tables and integer M\"obius transforms. It covers all 278 functions on zero through three inputs; all words over the documented 12-gate three-wire alphabet through length three and the 28-gate four-wire alphabet through length two (2,698 words); 28,088 register-product checks; and 251 restored words. The universal theorems do not follow by extrapolation from those finite tests.
203 
204 \subsection*{What remains outside the formal block}
205 C02's evaluation-span dual, affine input invariance, and general monotone ideal are not formalized. C03--C08 retain their previous written and finite-check status. The original classical/reversible circuit-size comparison and general exact monomial-cost theorem are not newly formalized. The active claim register controls interpretation.
206 
207 
208 \pagehead{Reading the formal model literally}{QUANTIFIERS AND ENCODING CARRY THE HYPOTHESES}
209 The generic cut theory uses a logical-input type $X$, a wire type $W$ with
210 decidable equality, and a boundary structure. Its essential fields are an
211 encoding $\mathrm{encode}:X\to\mathrm{Bool}\to(W\to\mathrm{Bool})$, a target
212 wire, and the proof
213 \[
214  \mathrm{encode}(x,b)(\mathrm{target})=b.
215 \]
216 This target equation separates the two target branches for each fixed input.
217 It excludes an encoding that silently ignores its supplied target bit.
218 The source proves \code{Boundary.target_separated}; it does not assume an
219 injective encoding of every logical-input value as an additional hypothesis.
220 
221 The restoration predicate is
222 \[
223  \forall x\,b,\quad \mathrm{run}(c)(\mathrm{encode}(x,b))
224  =\mathrm{encode}(x,b+f(x)).
225 \]
226 It is a hypothesis of the conditional theorem. The code does not assert that
227 every gate list realizes a restored oracle. The canonical encoding sets each
228 input wire to its input bit, each ancillary wire to zero, and the target to $b$.
229 Its wire type is
230 \begin{lstlisting}
231 Sum (Fin n) (Sum (Fin a) Unit)
232 \end{lstlisting}
233 which has exactly $n+a+1$ wires.
234 
235 In the generic C01 theorem, completeness is the existential statement
236 \[
237  f(x)=1\quad\Longleftrightarrow\quad\exists i:W,\ H_i(x)=1.
238 \]
239 No finite disjunction is needed there. Specializing to the canonical finite
240 wires yields the finite complete family used in the main paper. Completeness
241 does not say that the XOR of all packets reconstructs $f$; detecting packets
242 can cancel under XOR. It states existence of a detecting coordinate at every
243 positive input.
244 
245 No clean-intermediate condition occurs in these predicates. Legal gates may
246 temporarily alter inputs, dirty scratch and use the target as a control. The
247 source examples exercise those allowances. Its compute/copy/uncompute AND
248 example uses two Toffolis and is a restoration witness, whereas direct AND
249 uses one Toffoli. Neither example is an unrestricted circuit-search result.
250 
251 \pagehead{Certificates, semantic minima and natural arithmetic}{WHAT THE FORMAL OBJECTS DO AND DO NOT COMPUTE}
252 \code{DegreeLE d f} is an inductive representation predicate. Its constructors
253 build zero, a monomial represented by a variable-occurrence list of length
254 at most $d$, and XOR of certified functions. The polynomial evaluator XORs
255 the monomial-list values. The source proves the equivalence between a degree
256 certificate and such a finite representation.
257 
258 Repeated indices are permitted. Boolean idempotence reduces their repetitions,
259 so the representation gives the usual multilinear degree bound. The formal
260 block supplies no separate canonical ANF normalization algorithm and no theorem
261 that extracting homogeneous grades is computationally free. Zero has a
262 degree-zero certificate. The Python degree helper's $-1$ convention for zero
263 is a mathematical convention outside the natural-valued formal bound.
264 
265 \code{CompleteSafeDegreeLE f d} says that every positive point has some degree-$d$
266 safe detector. It does not require one detector to cover all positives, and
267 it places no efficiency bound on finding those detectors. Point indicators
268 show that $d=n$ suffices. A least-bound existence theorem then permits the
269 noncomputable definition \code{beta}. Its specification supplies complete
270 coverage; its minimality compares it with every sufficient natural bound.
271 
272 \code{AffineSafeDegreeLE f d} universally quantifies every degree-one output
273 function $g$ and requires $\beta(f+g)\le d$. The definition \code{betaStar}
274 chooses its least common upper bound. There are finitely many Boolean functions
275 on $n$ inputs, so this least bound equals the main paper's maximum over affine
276 output masks. It is a maximum over mask values, not a minimum over masks.
277 
278 The source proves $\beta(f)\le\beta^*(f)\le n$. The zero mask supplies the
279 first inequality. The point-indicator bound supplies the second. Classical
280 choice in the definitions is not a polynomial-time algorithm for computing
281 these parameters.
282 
283 All counters and degree bounds in this block are natural numbers. In
284 \code{2 * betaStar f - 3}, subtraction saturates at zero. Thus
285 \[
286  2\beta^*(f)-3\le T
287 \]
288 in the formal natural-number statement is the integer inequality
289 $\max\{0,2\beta^*(f)-3\}\le T$. The nonsubtractive endpoint
290 $2\beta^*(f)\le T+3$ avoids ambiguity. Rounding at odd $T$ is retained;
291 the balanced cut is chosen by Toffoli count, not by half the gate-list length.
292 
293 \pagehead{The proof dependency route}{A SOURCE MAP RATHER THAN A NEW AXIOM}
294 \begin{tabularx}{\textwidth}{@{}>{\raggedright\arraybackslash}p{1.8in}>{\raggedright\arraybackslash}X@{}}\toprule
295 Stage & Source role and conclusion\\\midrule
296 Legal gates and reversal & Distinct-wire constructor proofs; each gate is self-inverse; reverse gate lists invert the run\\
297 Separated boundary & The two initial target branches remain distinct after every prefix\\
298 Cut transport & Inverse suffix meets the appropriate forward target branch; $H_i=fD_i$ gives safety and pointwise completeness\\
299 Polynomial certificates & Monomial evaluation and XOR/product closure connect concrete lists to degree bounds\\
300 Shared register products & Products of $r$ current registers have budget $t+r$ after $t$ Toffolis; repeats and feedback are allowed\\
301 Balanced cut & An attainable prefix cost gives both sides cost at most $\lceil T/2\rceil$; the complete family gives the beta bound\\
302 Affine-output circuit & Degree-one certificates compile to restored NOT/CNOT lists, giving zero extra Toffolis for every mask\\
303 Joint endpoint & The forward target at initial zero supplies $f$; degree and optimized-cover conclusions are conjoined\\\bottomrule
304 \end{tabularx}
305 
306 The strongest degree invariant concerns products of actual current registers.
307 It does not duplicate the histories of shared controls. This is why its
308 coordinate consequence applies to DAG reuse, temporary input modification and
309 target feedback in this gate model. The general XOR--AND syntax argument in
310 the main paper remains a separate written proof.
311 
312 The general run theorem needs degree-one certificates for the initial
313 register functions. The canonical boundary supplies these certificates;
314 restoration is used later to identify the final target with $f$. The affine
315 existence theorem constructs gate lists inside its proof. It does not expose
316 a separate executable compiler function or assert minimum total gate count.
317 
318 The balanced cut and least-degree facts are established dependencies. They
319 are not extra assumptions added to \code{restored_degree_and_cover_bound}.
320 That endpoint assumes a legal gate list and restoration in the canonical
321 boundary model. The register prints its full type as L107.
322 
323 \pagehead{Formal and computational evidence}{FRESH SOURCE CHECKING AND BOUNDED EXACT REPLAY}
324 The current pinned Lean replay passed for all 115 indexed theorem declarations and eight modules. The permitted axiom union is \code{propext}, \code{Classical.choice}, and \code{Quot.sound}. No project axiom or admitted proof occurs in the maintained source.
325 
326 The complete exact scientific replay also passed. Its finite domains are recorded in the claim-coverage appendix and in the emitted run manifest. The degree-profile checker counts 278 functions on zero through three inputs. The small-oracle construction suite counts 276 functions on one through three inputs. The two zero-arity functions explain the difference. Those totals are not added together as disjoint evidence.
327 
328 The package retains historical failures as historical records. Current source compilation, kernel replay, finite computation, source integrity, and PDF rendering each establish a different kind of fact.
329 
330 \pagehead{Negative controls and the trust boundary}{A REJECTION HAS A PRECISE ROLE}
331 The current audit deliberately tested the following controls:
332 
333 \begin{tabularx}{\textwidth}{@{}>{\raggedright\arraybackslash}p{2.05in}>{\raggedright\arraybackslash}X@{}}\toprule
334 Control & Why rejection matters\\\midrule
335 Illegal repeated wire & Legal gate constructors require distinct controls and target\\
336 Target-only cut reconstruction & A discrepancy can move to a data wire; completeness needs the entire coordinate family\\
337 False theorem & A false statement is not accepted merely because it has a theorem wrapper\\
338 Placeholder guard & The project rejects admitted or placeholder source constructs\\
339 False monomial degree & A two-occurrence monomial cannot satisfy the supplied length-at-most-one premise\\
340 False affine AND claim & The supplied degree-two proof has the wrong type for a degree-one target\\
341 False beta value & Complete safe detection for AND2 cannot have degree one\\
342 False betaStar bound & Optimization cannot erase the AND2 obstruction\\\bottomrule
343 \end{tabularx}
344 
345 All eight controls were freshly rejected. They help check that the audit detects these specified errors. They are not additional positive mathematical results or an exhaustive attack on every possible checker defect.
346 The separate positive four-corner theorem proves the semantic impossibility
347 of an affine AND2 certificate; it is not the mechanism of that particular
348 wrong-type negative test.
349 
350 The bundled checker shares the Lean toolchain's trust boundary. It is not an independently implemented proof checker. The restored runtime archive was checked against the recorded combined hash. The runtime remains a separately supplied dependency.
351 
352 Historical development failures, rejected negative controls, and successful current checks are retained as separate events in the evidence package.
353 
354 \pagehead{Reproduce and inspect the authoritative files}{COMMANDS AND SOURCE IDENTITY}
355 From \code{source/komorebi-circuit-obstructions-v1.2.0}, run
356 \begin{lstlisting}
357 python scripts/check_integrity.py
358 python scripts/verify.py --all
359 python scripts/verify_lean.py --toolchain /path/to/toolchain
360 \end{lstlisting}
361 The integrity check needs Python; the full scientific replay also needs a
362 C++17 compiler. The last command needs the pinned
363 Lean toolchain supplied separately. The verification scripts do not download
364 it. A missing toolchain fails before proof checking. The current completion pass restored the pinned runtime and successfully executed this verification.
365 
366 From the publication-set root, regenerate the exact declaration appendix and
367 the explanatory guide source with
368 \begin{lstlisting}
369 python scripts/build_lean_register.py
370 python scripts/build_lean_guide.py
371 python scripts/build_documents.py
372 python scripts/verify_publication.py
373 \end{lstlisting}
374 The register generator verifies all 115 source hashes and declaration lines
375 against the archived catalog, then copies each complete elaborated type.
376 The guide generator preserves the archived explanatory proof route and adds
377 this edition's evidence distinctions. Neither script compiles Lean.
378 
379 The unmodified source ZIP's SHA-256 is
380 \begin{lstlisting}
381 88628c8274660bd20e11fec83249fdc04960403b9d64d1e5068a476b8c025936
382 \end{lstlisting}
383 The complete publication package preserves that ZIP, the repository bundle,
384 original companions and current evidence. Its new manifest binds the revised
385 papers, generators and figure assets. Hash consistency is not an authorship
386 certificate or mathematical proof.
387 
388 The declaration register follows. It includes the 40 inherited results and
389 75 Block 02 additions. The ten non-ASCII logical glyphs in its exact type text
390 are rendered as mathematical glyphs for readability. The unchanged UTF-8
391 sidecar is \code{manuscripts/lean_statements_utf8.txt}; the original authoritative
392 catalog is \code{reference/lean-block02/declaration_catalog.json} in the source
393 release. Imported library declarations and explanatory prose are not counted
394 as new project theorems.
395 \clearpage\section*{Complete declaration register}
396 \addcontentsline{toc}{section}{Complete declaration register}
397 The following 115 types are transcribed from the archived Block 02 declaration catalog. Unicode logical operators are rendered as mathematical glyphs; the complete original UTF-8 statements are also supplied. Source files and line locators match the preserved source hashes. The current replay rechecked the source declarations. The transcribed types remain tied to the supplied declaration catalog.
398 \begingroup
399 \lstset{basicstyle=\ttfamily\scriptsize,breakatwhitespace=false,
400 literate={¬}{{\ensuremath{\neg}}}1 {×}{{\ensuremath{\times}}}1
401 {→}{{\ensuremath{\to}}}1 {↔}{{\ensuremath{\leftrightarrow}}}1
402 {∀}{{\ensuremath{\forall}}}1 {∃}{{\ensuremath{\exists}}}1
403 {∈}{{\ensuremath{\in}}}1 {∧}{{\ensuremath{\land}}}1
404 {≠}{{\ensuremath{\ne}}}1 {≤}{{\ensuremath{\le}}}1}
405 
406 \subsection*{Gates: 16 declarations}
407 \par\medskip\noindent\begin{minipage}{\textwidth}
408 {\small\bfseries L001\enspace\texttt{write\_same}\par}
409 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:17\par
410 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
411 \begin{lstlisting}
412 CircuitObstructions.write_same {W : Type} [DecidableEq W] (s : CircuitObstructions.State W) (t : W) (b : Bool) :
413   CircuitObstructions.write s t b t = b
414 \end{lstlisting}
415 \end{minipage}\par
416 
417 \par\medskip\noindent\begin{minipage}{\textwidth}
418 {\small\bfseries L002\enspace\texttt{write\_other}\par}
419 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:20\par
420 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
421 \begin{lstlisting}
422 CircuitObstructions.write_other {W : Type} [DecidableEq W] (s : CircuitObstructions.State W) (t i : W) (b : Bool)
423   (h : i ≠ t) : CircuitObstructions.write s t b i = s i
424 \end{lstlisting}
425 \end{minipage}\par
426 
427 \par\medskip\noindent\begin{minipage}{\textwidth}
428 {\small\bfseries L003\enspace\texttt{xor\_cancel\_right}\par}
429 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:23\par
430 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
431 \begin{lstlisting}
432 CircuitObstructions.xor_cancel_right (a b : Bool) : (a ^^ b ^^ b) = a
433 \end{lstlisting}
434 \end{minipage}\par
435 
436 \par\medskip\noindent\begin{minipage}{\textwidth}
437 {\small\bfseries L004\enspace\texttt{xor\_cancel\_left}\par}
438 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:26\par
439 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
440 \begin{lstlisting}
441 CircuitObstructions.xor_cancel_left (a b : Bool) : (a ^^ (a ^^ b)) = b
442 \end{lstlisting}
443 \end{minipage}\par
444 
445 \par\medskip\noindent\begin{minipage}{\textwidth}
446 {\small\bfseries L005\enspace\texttt{xor\_commute}\par}
447 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:29\par
448 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
449 \begin{lstlisting}
450 CircuitObstructions.xor_commute (a b : Bool) : (a ^^ b) = (b ^^ a)
451 \end{lstlisting}
452 \end{minipage}\par
453 
454 \par\medskip\noindent\begin{minipage}{\textwidth}
455 {\small\bfseries L006\enspace\texttt{xor\_true\_iff\_ne}\par}
456 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:32\par
457 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
458 \begin{lstlisting}
459 CircuitObstructions.xor_true_iff_ne (a b : Bool) : (a ^^ b) = true ↔ a ≠ b
460 \end{lstlisting}
461 \end{minipage}\par
462 
463 \par\medskip\noindent\begin{minipage}{\textwidth}
464 {\small\bfseries L007\enspace\texttt{eval\_involutive}\par}
465 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:48\par
466 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
467 \begin{lstlisting}
468 CircuitObstructions.Gate.eval_involutive {W : Type} [DecidableEq W] (g : CircuitObstructions.Gate W)
469   (s : CircuitObstructions.State W) : g.eval (g.eval s) = s
470 \end{lstlisting}
471 \end{minipage}\par
472 
473 \par\medskip\noindent\begin{minipage}{\textwidth}
474 {\small\bfseries L008\enspace\texttt{eval\_injective}\par}
475 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:67\par
476 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
477 \begin{lstlisting}
478 CircuitObstructions.Gate.eval_injective {W : Type} [DecidableEq W] (g : CircuitObstructions.Gate W)
479   {s t : CircuitObstructions.State W} (h : g.eval s = g.eval t) : s = t
480 \end{lstlisting}
481 \end{minipage}\par
482 
483 \par\medskip\noindent\begin{minipage}{\textwidth}
484 {\small\bfseries L009\enspace\texttt{run\_nil}\par}
485 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:78\par
486 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
487 \begin{lstlisting}
488 CircuitObstructions.run_nil {W : Type} [DecidableEq W] (s : CircuitObstructions.State W) :
489   CircuitObstructions.run [] s = s
490 \end{lstlisting}
491 \end{minipage}\par
492 
493 \par\medskip\noindent\begin{minipage}{\textwidth}
494 {\small\bfseries L010\enspace\texttt{run\_cons}\par}
495 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:81\par
496 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
497 \begin{lstlisting}
498 CircuitObstructions.run_cons {W : Type} [DecidableEq W] (g : CircuitObstructions.Gate W)
499   (gs : CircuitObstructions.Circuit W) (s : CircuitObstructions.State W) :
500   CircuitObstructions.run (g :: gs) s = CircuitObstructions.run gs (g.eval s)
501 \end{lstlisting}
502 \end{minipage}\par
503 
504 \par\medskip\noindent\begin{minipage}{\textwidth}
505 {\small\bfseries L011\enspace\texttt{run\_append}\par}
506 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:84\par
507 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
508 \begin{lstlisting}
509 CircuitObstructions.run_append {W : Type} [DecidableEq W] (p q : CircuitObstructions.Circuit W)
510   (s : CircuitObstructions.State W) :
511   CircuitObstructions.run (p ++ q) s = CircuitObstructions.run q (CircuitObstructions.run p s)
512 \end{lstlisting}
513 \end{minipage}\par
514 
515 \par\medskip\noindent\begin{minipage}{\textwidth}
516 {\small\bfseries L012\enspace\texttt{run\_reverse\_run}\par}
517 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:90\par
518 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
519 \begin{lstlisting}
520 CircuitObstructions.run_reverse_run {W : Type} [DecidableEq W] (c : CircuitObstructions.Circuit W)
521   (s : CircuitObstructions.State W) : CircuitObstructions.run (List.reverse c) (CircuitObstructions.run c s) = s
522 \end{lstlisting}
523 \end{minipage}\par
524 
525 \par\medskip\noindent\begin{minipage}{\textwidth}
526 {\small\bfseries L013\enspace\texttt{run\_run\_reverse}\par}
527 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:98\par
528 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
529 \begin{lstlisting}
530 CircuitObstructions.run_run_reverse {W : Type} [DecidableEq W] (c : CircuitObstructions.Circuit W)
531   (s : CircuitObstructions.State W) : CircuitObstructions.run c (CircuitObstructions.run (List.reverse c) s) = s
532 \end{lstlisting}
533 \end{minipage}\par
534 
535 \par\medskip\noindent\begin{minipage}{\textwidth}
536 {\small\bfseries L014\enspace\texttt{run\_injective}\par}
537 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:102\par
538 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
539 \begin{lstlisting}
540 CircuitObstructions.run_injective {W : Type} [DecidableEq W] (c : CircuitObstructions.Circuit W)
541   {s t : CircuitObstructions.State W} (h : CircuitObstructions.run c s = CircuitObstructions.run c t) : s = t
542 \end{lstlisting}
543 \end{minipage}\par
544 
545 \par\medskip\noindent\begin{minipage}{\textwidth}
546 {\small\bfseries L015\enspace\texttt{toffoliCount\_append}\par}
547 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:114\par
548 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
549 \begin{lstlisting}
550 CircuitObstructions.toffoliCount_append {W : Type} (p q : CircuitObstructions.Circuit W) :
551   CircuitObstructions.toffoliCount (p ++ q) = CircuitObstructions.toffoliCount p + CircuitObstructions.toffoliCount q
552 \end{lstlisting}
553 \end{minipage}\par
554 
555 \par\medskip\noindent\begin{minipage}{\textwidth}
556 {\small\bfseries L016\enspace\texttt{toffoliCount\_reverse}\par}
557 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Gates.lean}:118\par
558 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
559 \begin{lstlisting}
560 CircuitObstructions.toffoliCount_reverse {W : Type} (c : CircuitObstructions.Circuit W) :
561   CircuitObstructions.toffoliCount (List.reverse c) = CircuitObstructions.toffoliCount c
562 \end{lstlisting}
563 \end{minipage}\par
564 
565 \subsection*{CutComparison: 13 declarations}
566 \par\medskip\noindent\begin{minipage}{\textwidth}
567 {\small\bfseries L017\enspace\texttt{target\_separated}\par}
568 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:17\par
569 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
570 \begin{lstlisting}
571 CircuitObstructions.Boundary.target_separated {X W : Type} (e : CircuitObstructions.Boundary X W) (x : X) :
572   e.encode x false ≠ e.encode x true
573 \end{lstlisting}
574 \end{minipage}\par
575 
576 \par\medskip\noindent\begin{minipage}{\textwidth}
577 {\small\bfseries L018\enspace\texttt{canonical\_input}\par}
578 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:39\par
579 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
580 \begin{lstlisting}
581 CircuitObstructions.canonical_input (n a : Nat) (x : Fin n → Bool) (b : Bool) (i : Fin n) :
582   (CircuitObstructions.canonicalBoundary n a).encode x b (Sum.inl i) = x i
583 \end{lstlisting}
584 \end{minipage}\par
585 
586 \par\medskip\noindent\begin{minipage}{\textwidth}
587 {\small\bfseries L019\enspace\texttt{canonical\_ancilla}\par}
588 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:42\par
589 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
590 \begin{lstlisting}
591 CircuitObstructions.canonical_ancilla (n a : Nat) (x : Fin n → Bool) (b : Bool) (i : Fin a) :
592   (CircuitObstructions.canonicalBoundary n a).encode x b (Sum.inr (Sum.inl i)) = false
593 \end{lstlisting}
594 \end{minipage}\par
595 
596 \par\medskip\noindent\begin{minipage}{\textwidth}
597 {\small\bfseries L020\enspace\texttt{canonical\_target}\par}
598 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:45\par
599 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
600 \begin{lstlisting}
601 CircuitObstructions.canonical_target (n a : Nat) (x : Fin n → Bool) (b : Bool) :
602   (CircuitObstructions.canonicalBoundary n a).encode x b (Sum.inr (Sum.inr ())) = b
603 \end{lstlisting}
604 \end{minipage}\par
605 
606 \par\medskip\noindent\begin{minipage}{\textwidth}
607 {\small\bfseries L021\enspace\texttt{inverse\_suffix\_boundary}\par}
608 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:49\par
609 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
610 \begin{lstlisting}
611 CircuitObstructions.inverse_suffix_boundary {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
612   (p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) (x : X)
613   (b : Bool) :
614   CircuitObstructions.run (List.reverse q) (e.encode x b) = CircuitObstructions.run p (e.encode x (b ^^ f x))
615 \end{lstlisting}
616 \end{minipage}\par
617 
618 \par\medskip\noindent\begin{minipage}{\textwidth}
619 {\small\bfseries L022\enspace\texttt{direction\_nonzero}\par}
620 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:67\par
621 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
622 \begin{lstlisting}
623 CircuitObstructions.direction_nonzero {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
624   (p : CircuitObstructions.Circuit W) (x : X) : ∃ i, CircuitObstructions.direction e p x i = true
625 \end{lstlisting}
626 \end{minipage}\par
627 
628 \par\medskip\noindent\begin{minipage}{\textwidth}
629 {\small\bfseries L023\enspace\texttt{cut\_transport\_identity}\par}
630 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:82\par
631 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
632 \begin{lstlisting}
633 CircuitObstructions.cut_transport_identity {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
634   (p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) (x : X)
635   (i : W) : CircuitObstructions.packet e p q x i = (f x && CircuitObstructions.direction e p x i)
636 \end{lstlisting}
637 \end{minipage}\par
638 
639 \par\medskip\noindent\begin{minipage}{\textwidth}
640 {\small\bfseries L024\enspace\texttt{cut\_packet\_safe}\par}
641 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:91\par
642 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
643 \begin{lstlisting}
644 CircuitObstructions.cut_packet_safe {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
645   (p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) (x : X)
646   (i : W) : CircuitObstructions.packet e p q x i = true → f x = true
647 \end{lstlisting}
648 \end{minipage}\par
649 
650 \par\medskip\noindent\begin{minipage}{\textwidth}
651 {\small\bfseries L025\enspace\texttt{cut\_cover\_complete}\par}
652 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:99\par
653 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
654 \begin{lstlisting}
655 CircuitObstructions.cut_cover_complete {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
656   (p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) (x : X) :
657   f x = true ↔ ∃ i, CircuitObstructions.packet e p q x i = true
658 \end{lstlisting}
659 \end{minipage}\par
660 
661 \par\medskip\noindent\begin{minipage}{\textwidth}
662 {\small\bfseries L026\enspace\texttt{complete\_safe\_cover}\par}
663 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:111\par
664 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
665 \begin{lstlisting}
666 CircuitObstructions.complete_safe_cover {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
667   (p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) :
668   (∀ (x : X) (i : W), CircuitObstructions.packet e p q x i = true → f x = true) ∧
669     ∀ (x : X), f x = true ↔ ∃ i, CircuitObstructions.packet e p q x i = true
670 \end{lstlisting}
671 \end{minipage}\par
672 
673 \par\medskip\noindent\begin{minipage}{\textwidth}
674 {\small\bfseries L027\enspace\texttt{cut\_states\_equal\_iff\_reject}\par}
675 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:119\par
676 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
677 \begin{lstlisting}
678 CircuitObstructions.cut_states_equal_iff_reject {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
679   (p q : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e (p ++ q) f) (x : X) :
680   CircuitObstructions.run p (e.encode x false) = CircuitObstructions.run (List.reverse q) (e.encode x false) ↔
681     f x = false
682 \end{lstlisting}
683 \end{minipage}\par
684 
685 \par\medskip\noindent\begin{minipage}{\textwidth}
686 {\small\bfseries L028\enspace\texttt{every\_index\_cut}\par}
687 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:131\par
688 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
689 \begin{lstlisting}
690 CircuitObstructions.every_index_cut {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
691   (c : CircuitObstructions.Circuit W) (f : X → Bool) (hR : CircuitObstructions.Restores e c f) (k : Nat) (x : X) :
692   f x = true ↔ ∃ i, CircuitObstructions.packet e (List.take k c) (List.drop k c) x i = true
693 \end{lstlisting}
694 \end{minipage}\par
695 
696 \par\medskip\noindent\begin{minipage}{\textwidth}
697 {\small\bfseries L029\enspace\texttt{canonical\_complete\_safe\_cover}\par}
698 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/CutComparison.lean}:139\par
699 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
700 \begin{lstlisting}
701 CircuitObstructions.canonical_complete_safe_cover (n a : Nat)
702   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : (Fin n → Bool) → Bool)
703   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) (k : Nat) :
704   (∀ (x : Fin n → Bool) (i : CircuitObstructions.CanonicalWire n a),
705       CircuitObstructions.packet (CircuitObstructions.canonicalBoundary n a) (List.take k c) (List.drop k c) x i =
706           true →
707         f x = true) ∧
708     ∀ (x : Fin n → Bool),
709       f x = true ↔
710         ∃ i,
711           CircuitObstructions.packet (CircuitObstructions.canonicalBoundary n a) (List.take k c) (List.drop k c) x i =
712             true
713 \end{lstlisting}
714 \end{minipage}\par
715 
716 \subsection*{Examples: 11 declarations}
717 \par\medskip\noindent\begin{minipage}{\textwidth}
718 {\small\bfseries L030\enspace\texttt{andOracle\_restores}\par}
719 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Examples.lean}:27\par
720 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace Quot.sound\par}\nopagebreak
721 \begin{lstlisting}
722 CircuitObstructions.Examples.andOracle_restores :
723   CircuitObstructions.Restores CircuitObstructions.Examples.andBoundary CircuitObstructions.Examples.andOracle fun x =>
724     x.fst && x.snd
725 \end{lstlisting}
726 \end{minipage}\par
727 
728 \par\medskip\noindent\begin{minipage}{\textwidth}
729 {\small\bfseries L031\enspace\texttt{andOracle\_toffoli\_count}\par}
730 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Examples.lean}:33\par
731 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
732 \begin{lstlisting}
733 CircuitObstructions.Examples.andOracle_toffoli_count :
734   CircuitObstructions.toffoliCount CircuitObstructions.Examples.andOracle = 2
735 \end{lstlisting}
736 \end{minipage}\par
737 
738 \par\medskip\noindent\begin{minipage}{\textwidth}
739 {\small\bfseries L032\enspace\texttt{and\_scratch\_can\_be\_dirty}\par}
740 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Examples.lean}:36\par
741 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
742 \begin{lstlisting}
743 CircuitObstructions.Examples.and_scratch_can_be_dirty :
744   CircuitObstructions.run CircuitObstructions.Examples.andCompute
745       (CircuitObstructions.Examples.andBoundary.encode (true, true) false)
746       CircuitObstructions.Examples.WorkWire.scratch =
747     true
748 \end{lstlisting}
749 \end{minipage}\par
750 
751 \par\medskip\noindent\begin{minipage}{\textwidth}
752 {\small\bfseries L033\enspace\texttt{andOracle\_every\_cut}\par}
753 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Examples.lean}:40\par
754 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
755 \begin{lstlisting}
756 CircuitObstructions.Examples.andOracle_every_cut (k : Nat) (x : Bool × Bool) :
757   (x.fst && x.snd) = true ↔
758     ∃ i,
759       CircuitObstructions.packet CircuitObstructions.Examples.andBoundary
760           (List.take k CircuitObstructions.Examples.andOracle) (List.drop k CircuitObstructions.Examples.andOracle) x
761           i =
762         true
763 \end{lstlisting}
764 \end{minipage}\par
765 
766 \par\medskip\noindent\begin{minipage}{\textwidth}
767 {\small\bfseries L034\enspace\texttt{outputActiveOracle\_restores}\par}
768 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Examples.lean}:66\par
769 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace Quot.sound\par}\nopagebreak
770 \begin{lstlisting}
771 CircuitObstructions.Examples.outputActiveOracle_restores :
772   CircuitObstructions.Restores CircuitObstructions.Examples.swapBoundary CircuitObstructions.Examples.outputActiveOracle
773     fun x => true
774 \end{lstlisting}
775 \end{minipage}\par
776 
777 \par\medskip\noindent\begin{minipage}{\textwidth}
778 {\small\bfseries L035\enspace\texttt{outputActiveOracle\_length}\par}
779 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Examples.lean}:71\par
780 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
781 \begin{lstlisting}
782 CircuitObstructions.Examples.outputActiveOracle_length : List.length CircuitObstructions.Examples.outputActiveOracle = 7
783 \end{lstlisting}
784 \end{minipage}\par
785 
786 \par\medskip\noindent\begin{minipage}{\textwidth}
787 {\small\bfseries L036\enspace\texttt{outputActiveOracle\_toffoli\_count}\par}
788 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Examples.lean}:73\par
789 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
790 \begin{lstlisting}
791 CircuitObstructions.Examples.outputActiveOracle_toffoli_count :
792   CircuitObstructions.toffoliCount CircuitObstructions.Examples.outputActiveOracle = 0
793 \end{lstlisting}
794 \end{minipage}\par
795 
796 \par\medskip\noindent\begin{minipage}{\textwidth}
797 {\small\bfseries L037\enspace\texttt{moved\_discrepancy\_data}\par}
798 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Examples.lean}:76\par
799 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
800 \begin{lstlisting}
801 CircuitObstructions.Examples.moved_discrepancy_data (x : Bool) :
802   CircuitObstructions.packet CircuitObstructions.Examples.swapBoundary CircuitObstructions.Examples.swapCircuit
803       CircuitObstructions.Examples.swapSuffix x CircuitObstructions.Examples.SwapWire.data =
804     true
805 \end{lstlisting}
806 \end{minipage}\par
807 
808 \par\medskip\noindent\begin{minipage}{\textwidth}
809 {\small\bfseries L038\enspace\texttt{moved\_discrepancy\_target}\par}
810 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Examples.lean}:80\par
811 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
812 \begin{lstlisting}
813 CircuitObstructions.Examples.moved_discrepancy_target (x : Bool) :
814   CircuitObstructions.packet CircuitObstructions.Examples.swapBoundary CircuitObstructions.Examples.swapCircuit
815       CircuitObstructions.Examples.swapSuffix x CircuitObstructions.Examples.SwapWire.target =
816     false
817 \end{lstlisting}
818 \end{minipage}\par
819 
820 \par\medskip\noindent\begin{minipage}{\textwidth}
821 {\small\bfseries L039\enspace\texttt{target\_only\_reconstruction\_is\_false}\par}
822 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Examples.lean}:85\par
823 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
824 \begin{lstlisting}
825 CircuitObstructions.Examples.target_only_reconstruction_is_false :
826   ¬∀ (x : Bool),
827       CircuitObstructions.packet CircuitObstructions.Examples.swapBoundary CircuitObstructions.Examples.swapCircuit
828           CircuitObstructions.Examples.swapSuffix x CircuitObstructions.Examples.SwapWire.target =
829         true
830 \end{lstlisting}
831 \end{minipage}\par
832 
833 \par\medskip\noindent\begin{minipage}{\textwidth}
834 {\small\bfseries L040\enspace\texttt{degenerate\_encoding\_control}\par}
835 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Examples.lean}:93\par
836 \textbf{Block.}\enspace 01\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
837 \begin{lstlisting}
838 CircuitObstructions.Examples.degenerate_encoding_control :
839   have bad := fun x x_1 => false;
840   (∀ (y : Bool), CircuitObstructions.run [] (bad y) = bad (y ^^ true)) ∧
841     ∀ (i : CircuitObstructions.Examples.SwapWire), (bad false i ^^ bad false i) = false
842 \end{lstlisting}
843 \end{minipage}\par
844 
845 \subsection*{Degree: 19 declarations}
846 \par\medskip\noindent\begin{minipage}{\textwidth}
847 {\small\bfseries L041\enspace\texttt{bprod\_nil}\par}
848 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:19\par
849 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
850 \begin{lstlisting}
851 CircuitObstructions.bprod_nil {W : Type} (s : CircuitObstructions.State W) : CircuitObstructions.bprod [] s = true
852 \end{lstlisting}
853 \end{minipage}\par
854 
855 \par\medskip\noindent\begin{minipage}{\textwidth}
856 {\small\bfseries L042\enspace\texttt{bprod\_cons}\par}
857 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:20\par
858 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
859 \begin{lstlisting}
860 CircuitObstructions.bprod_cons {W : Type} (i : W) (is : List W) (s : CircuitObstructions.State W) :
861   CircuitObstructions.bprod (i :: is) s = (s i && CircuitObstructions.bprod is s)
862 \end{lstlisting}
863 \end{minipage}\par
864 
865 \par\medskip\noindent\begin{minipage}{\textwidth}
866 {\small\bfseries L043\enspace\texttt{bprod\_append}\par}
867 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:23\par
868 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
869 \begin{lstlisting}
870 CircuitObstructions.bprod_append {W : Type} (l k : List W) (s : CircuitObstructions.State W) :
871   CircuitObstructions.bprod (l ++ k) s = (CircuitObstructions.bprod l s && CircuitObstructions.bprod k s)
872 \end{lstlisting}
873 \end{minipage}\par
874 
875 \par\medskip\noindent\begin{minipage}{\textwidth}
876 {\small\bfseries L044\enspace\texttt{xor\_and\_right}\par}
877 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:29\par
878 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
879 \begin{lstlisting}
880 CircuitObstructions.xor_and_right (a b c : Bool) : ((a ^^ b) && c) = (a && c ^^ b && c)
881 \end{lstlisting}
882 \end{minipage}\par
883 
884 \par\medskip\noindent\begin{minipage}{\textwidth}
885 {\small\bfseries L045\enspace\texttt{and\_xor\_right}\par}
886 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:33\par
887 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
888 \begin{lstlisting}
889 CircuitObstructions.and_xor_right (a b c : Bool) : (a && (b ^^ c)) = (a && b ^^ a && c)
890 \end{lstlisting}
891 \end{minipage}\par
892 
893 \par\medskip\noindent\begin{minipage}{\textwidth}
894 {\small\bfseries L046\enspace\texttt{not\_as\_xor\_one}\par}
895 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:37\par
896 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
897 \begin{lstlisting}
898 CircuitObstructions.not_as_xor_one (a : Bool) : (!a) = (a ^^ true)
899 \end{lstlisting}
900 \end{minipage}\par
901 
902 \par\medskip\noindent\begin{minipage}{\textwidth}
903 {\small\bfseries L047\enspace\texttt{mono}\par}
904 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:47\par
905 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
906 \begin{lstlisting}
907 CircuitObstructions.DegreeLE.mono {n d e : Nat} {f : CircuitObstructions.BFun n} (h : CircuitObstructions.DegreeLE d f)
908   (hde : d ≤ e) : CircuitObstructions.DegreeLE e f
909 \end{lstlisting}
910 \end{minipage}\par
911 
912 \par\medskip\noindent\begin{minipage}{\textwidth}
913 {\small\bfseries L048\enspace\texttt{one}\par}
914 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:54\par
915 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
916 \begin{lstlisting}
917 CircuitObstructions.DegreeLE.one (n d : Nat) : CircuitObstructions.DegreeLE d fun x => true
918 \end{lstlisting}
919 \end{minipage}\par
920 
921 \par\medskip\noindent\begin{minipage}{\textwidth}
922 {\small\bfseries L049\enspace\texttt{constant}\par}
923 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:57\par
924 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
925 \begin{lstlisting}
926 CircuitObstructions.DegreeLE.constant (n d : Nat) (b : Bool) : CircuitObstructions.DegreeLE d fun x => b
927 \end{lstlisting}
928 \end{minipage}\par
929 
930 \par\medskip\noindent\begin{minipage}{\textwidth}
931 {\small\bfseries L050\enspace\texttt{variable}\par}
932 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:63\par
933 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
934 \begin{lstlisting}
935 CircuitObstructions.DegreeLE.variable {n : Nat} (i : Fin n) : CircuitObstructions.DegreeLE 1 fun x => x i
936 \end{lstlisting}
937 \end{minipage}\par
938 
939 \par\medskip\noindent\begin{minipage}{\textwidth}
940 {\small\bfseries L051\enspace\texttt{xor}\par}
941 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:67\par
942 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
943 \begin{lstlisting}
944 CircuitObstructions.DegreeLE.xor {n d e : Nat} {f g : CircuitObstructions.BFun n}
945   (hf : CircuitObstructions.DegreeLE d f) (hg : CircuitObstructions.DegreeLE e g) :
946   CircuitObstructions.DegreeLE (max d e) fun x => f x ^^ g x
947 \end{lstlisting}
948 \end{minipage}\par
949 
950 \par\medskip\noindent\begin{minipage}{\textwidth}
951 {\small\bfseries L052\enspace\texttt{not}\par}
952 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:72\par
953 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace Quot.sound\par}\nopagebreak
954 \begin{lstlisting}
955 CircuitObstructions.DegreeLE.not {n d : Nat} {f : CircuitObstructions.BFun n} (hf : CircuitObstructions.DegreeLE d f) :
956   CircuitObstructions.DegreeLE d fun x => !f x
957 \end{lstlisting}
958 \end{minipage}\par
959 
960 \par\medskip\noindent\begin{minipage}{\textwidth}
961 {\small\bfseries L053\enspace\texttt{monomial\_mul}\par}
962 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:76\par
963 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
964 \begin{lstlisting}
965 CircuitObstructions.DegreeLE.monomial_mul {n d e : Nat} (l : List (Fin n)) (hl : l.length ≤ d)
966   {g : CircuitObstructions.BFun n} (hg : CircuitObstructions.DegreeLE e g) :
967   CircuitObstructions.DegreeLE (d + e) fun x => CircuitObstructions.bprod l x && g x
968 \end{lstlisting}
969 \end{minipage}\par
970 
971 \par\medskip\noindent\begin{minipage}{\textwidth}
972 {\small\bfseries L054\enspace\texttt{mul}\par}
973 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:87\par
974 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
975 \begin{lstlisting}
976 CircuitObstructions.DegreeLE.mul {n d e : Nat} {f g : CircuitObstructions.BFun n}
977   (hf : CircuitObstructions.DegreeLE d f) (hg : CircuitObstructions.DegreeLE e g) :
978   CircuitObstructions.DegreeLE (d + e) fun x => f x && g x
979 \end{lstlisting}
980 \end{minipage}\par
981 
982 \par\medskip\noindent\begin{minipage}{\textwidth}
983 {\small\bfseries L055\enspace\texttt{product}\par}
984 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:96\par
985 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
986 \begin{lstlisting}
987 CircuitObstructions.DegreeLE.product {n : Nat} {W : Type} (l : List W)
988   (s : (Fin n → Bool) → CircuitObstructions.State W) (h : ∀ (i : W), CircuitObstructions.DegreeLE 1 fun x => s x i) :
989   CircuitObstructions.DegreeLE l.length fun x => CircuitObstructions.bprod l (s x)
990 \end{lstlisting}
991 \end{minipage}\par
992 
993 \par\medskip\noindent\begin{minipage}{\textwidth}
994 {\small\bfseries L056\enspace\texttt{polyEval\_append}\par}
995 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:109\par
996 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
997 \begin{lstlisting}
998 CircuitObstructions.polyEval_append {n : Nat} (p q : List (List (Fin n))) (x : Fin n → Bool) :
999   CircuitObstructions.polyEval (p ++ q) x = (CircuitObstructions.polyEval p x ^^ CircuitObstructions.polyEval q x)
1000 \end{lstlisting}
1001 \end{minipage}\par
1002 
1003 \par\medskip\noindent\begin{minipage}{\textwidth}
1004 {\small\bfseries L057\enspace\texttt{polynomial\_witness}\par}
1005 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:115\par
1006 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1007 \begin{lstlisting}
1008 CircuitObstructions.DegreeLE.polynomial_witness {n d : Nat} {f : CircuitObstructions.BFun n}
1009   (h : CircuitObstructions.DegreeLE d f) :
1010   ∃ p, (∀ (l : List (Fin n)), l ∈ p → l.length ≤ d) ∧ CircuitObstructions.polyEval p = f
1011 \end{lstlisting}
1012 \end{minipage}\par
1013 
1014 \par\medskip\noindent\begin{minipage}{\textwidth}
1015 {\small\bfseries L058\enspace\texttt{polynomial\_degree\_certificate}\par}
1016 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:134\par
1017 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
1018 \begin{lstlisting}
1019 CircuitObstructions.polynomial_degree_certificate {n d : Nat} (p : List (List (Fin n)))
1020   (hp : ∀ (l : List (Fin n)), l ∈ p → l.length ≤ d) : CircuitObstructions.DegreeLE d (CircuitObstructions.polyEval p)
1021 \end{lstlisting}
1022 \end{minipage}\par
1023 
1024 \par\medskip\noindent\begin{minipage}{\textwidth}
1025 {\small\bfseries L059\enspace\texttt{degreeLE\_iff\_polynomial}\par}
1026 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/Degree.lean}:142\par
1027 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1028 \begin{lstlisting}
1029 CircuitObstructions.degreeLE_iff_polynomial {n d : Nat} (f : CircuitObstructions.BFun n) :
1030   CircuitObstructions.DegreeLE d f ↔
1031     ∃ p, (∀ (l : List (Fin n)), l ∈ p → l.length ≤ d) ∧ CircuitObstructions.polyEval p = f
1032 \end{lstlisting}
1033 \end{minipage}\par
1034 
1035 \subsection*{MultiplicativeDegree: 12 declarations}
1036 \par\medskip\noindent\begin{minipage}{\textwidth}
1037 {\small\bfseries L060\enspace\texttt{withoutWire\_length\_le}\par}
1038 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:17\par
1039 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
1040 \begin{lstlisting}
1041 CircuitObstructions.withoutWire_length_le {W : Type} [DecidableEq W] (l : List W) (t : W) :
1042   (CircuitObstructions.withoutWire l t).length ≤ l.length
1043 \end{lstlisting}
1044 \end{minipage}\par
1045 
1046 \par\medskip\noindent\begin{minipage}{\textwidth}
1047 {\small\bfseries L061\enspace\texttt{withoutWire\_length\_lt}\par}
1048 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:21\par
1049 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1050 \begin{lstlisting}
1051 CircuitObstructions.withoutWire_length_lt {W : Type} [DecidableEq W] (l : List W) (t : W) (ht : t ∈ l) :
1052   (CircuitObstructions.withoutWire l t).length + 1 ≤ l.length
1053 \end{lstlisting}
1054 \end{minipage}\par
1055 
1056 \par\medskip\noindent\begin{minipage}{\textwidth}
1057 {\small\bfseries L062\enspace\texttt{bprod\_write}\par}
1058 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:33\par
1059 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1060 \begin{lstlisting}
1061 CircuitObstructions.bprod_write {W : Type} [DecidableEq W] (l : List W) (s : CircuitObstructions.State W) (t : W)
1062   (b : Bool) :
1063   CircuitObstructions.bprod l (CircuitObstructions.write s t b) =
1064     ((if t ∈ l then b else true) && CircuitObstructions.bprod (CircuitObstructions.withoutWire l t) s)
1065 \end{lstlisting}
1066 \end{minipage}\par
1067 
1068 \par\medskip\noindent\begin{minipage}{\textwidth}
1069 {\small\bfseries L063\enspace\texttt{bprod\_write\_absent}\par}
1070 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:48\par
1071 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
1072 \begin{lstlisting}
1073 CircuitObstructions.bprod_write_absent {W : Type} [DecidableEq W] (l : List W) (s : CircuitObstructions.State W) (t : W)
1074   (b : Bool) (ht : ¬t ∈ l) :
1075   CircuitObstructions.bprod l (CircuitObstructions.write s t b) = CircuitObstructions.bprod l s
1076 \end{lstlisting}
1077 \end{minipage}\par
1078 
1079 \par\medskip\noindent\begin{minipage}{\textwidth}
1080 {\small\bfseries L064\enspace\texttt{workspaceDegree\_initial}\par}
1081 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:62\par
1082 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1083 \begin{lstlisting}
1084 CircuitObstructions.workspaceDegree_initial {n : Nat} {W : Type} (s : (Fin n → Bool) → CircuitObstructions.State W)
1085   (h : ∀ (i : W), CircuitObstructions.DegreeLE 1 fun x => s x i) : CircuitObstructions.WorkspaceDegree s 0
1086 \end{lstlisting}
1087 \end{minipage}\par
1088 
1089 \par\medskip\noindent\begin{minipage}{\textwidth}
1090 {\small\bfseries L065\enspace\texttt{workspaceDegree\_toggle}\par}
1091 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:73\par
1092 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1093 \begin{lstlisting}
1094 CircuitObstructions.workspaceDegree_toggle {n : Nat} {W : Type} [DecidableEq W]
1095   (s : (Fin n → Bool) → CircuitObstructions.State W) (t : W) (controls : List W) (k : Nat)
1096   (h : CircuitObstructions.WorkspaceDegree s k) :
1097   CircuitObstructions.WorkspaceDegree (CircuitObstructions.toggleProduct s t controls) (k + (controls.length - 1))
1098 \end{lstlisting}
1099 \end{minipage}\par
1100 
1101 \par\medskip\noindent\begin{minipage}{\textwidth}
1102 {\small\bfseries L066\enspace\texttt{workspaceDegree\_gate}\par}
1103 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:104\par
1104 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1105 \begin{lstlisting}
1106 CircuitObstructions.workspaceDegree_gate {n : Nat} {W : Type} [DecidableEq W]
1107   (s : (Fin n → Bool) → CircuitObstructions.State W) (g : CircuitObstructions.Gate W) (k : Nat)
1108   (h : CircuitObstructions.WorkspaceDegree s k) :
1109   CircuitObstructions.WorkspaceDegree (fun x => g.eval (s x)) (k + g.toffoliCost)
1110 \end{lstlisting}
1111 \end{minipage}\par
1112 
1113 \par\medskip\noindent\begin{minipage}{\textwidth}
1114 {\small\bfseries L067\enspace\texttt{workspaceDegree\_run}\par}
1115 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:128\par
1116 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1117 \begin{lstlisting}
1118 CircuitObstructions.workspaceDegree_run {n : Nat} {W : Type} [DecidableEq W] (c : CircuitObstructions.Circuit W)
1119   (s : (Fin n → Bool) → CircuitObstructions.State W) (k : Nat) (h : CircuitObstructions.WorkspaceDegree s k) :
1120   CircuitObstructions.WorkspaceDegree (fun x => CircuitObstructions.run c (s x))
1121     (k + CircuitObstructions.toffoliCount c)
1122 \end{lstlisting}
1123 \end{minipage}\par
1124 
1125 \par\medskip\noindent\begin{minipage}{\textwidth}
1126 {\small\bfseries L068\enspace\texttt{run\_coordinate\_degree}\par}
1127 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:139\par
1128 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1129 \begin{lstlisting}
1130 CircuitObstructions.run_coordinate_degree {n : Nat} {W : Type} [DecidableEq W] (c : CircuitObstructions.Circuit W)
1131   (s : (Fin n → Bool) → CircuitObstructions.State W) (hs : ∀ (i : W), CircuitObstructions.DegreeLE 1 fun x => s x i)
1132   (i : W) :
1133   CircuitObstructions.DegreeLE (CircuitObstructions.toffoliCount c + 1) fun x => CircuitObstructions.run c (s x) i
1134 \end{lstlisting}
1135 \end{minipage}\par
1136 
1137 \par\medskip\noindent\begin{minipage}{\textwidth}
1138 {\small\bfseries L069\enspace\texttt{canonical\_boundary\_degree}\par}
1139 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:146\par
1140 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1141 \begin{lstlisting}
1142 CircuitObstructions.canonical_boundary_degree (n a : Nat) (b : Bool) (i : CircuitObstructions.CanonicalWire n a) :
1143   CircuitObstructions.DegreeLE 1 fun x => (CircuitObstructions.canonicalBoundary n a).encode x b i
1144 \end{lstlisting}
1145 \end{minipage}\par
1146 
1147 \par\medskip\noindent\begin{minipage}{\textwidth}
1148 {\small\bfseries L070\enspace\texttt{canonical\_run\_coordinate\_degree}\par}
1149 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:155\par
1150 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1151 \begin{lstlisting}
1152 CircuitObstructions.canonical_run_coordinate_degree (n a : Nat)
1153   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (b : Bool)
1154   (i : CircuitObstructions.CanonicalWire n a) :
1155   CircuitObstructions.DegreeLE (CircuitObstructions.toffoliCount c + 1) fun x =>
1156     CircuitObstructions.run c ((CircuitObstructions.canonicalBoundary n a).encode x b) i
1157 \end{lstlisting}
1158 \end{minipage}\par
1159 
1160 \par\medskip\noindent\begin{minipage}{\textwidth}
1161 {\small\bfseries L071\enspace\texttt{canonical\_cut\_packet\_degree}\par}
1162 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/MultiplicativeDegree.lean}:161\par
1163 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1164 \begin{lstlisting}
1165 CircuitObstructions.canonical_cut_packet_degree (n a : Nat)
1166   (p q : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a))
1167   (i : CircuitObstructions.CanonicalWire n a) :
1168   CircuitObstructions.DegreeLE (max (CircuitObstructions.toffoliCount p) (CircuitObstructions.toffoliCount q) + 1)
1169     fun x => CircuitObstructions.packet (CircuitObstructions.canonicalBoundary n a) p q x i
1170 \end{lstlisting}
1171 \end{minipage}\par
1172 
1173 \subsection*{SafeDegree: 22 declarations}
1174 \par\medskip\noindent\begin{minipage}{\textwidth}
1175 {\small\bfseries L072\enspace\texttt{mono}\par}
1176 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:16\par
1177 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace none\par}\nopagebreak
1178 \begin{lstlisting}
1179 CircuitObstructions.CompleteSafeDegreeLE.mono {n d e : Nat} {f : CircuitObstructions.BFun n}
1180   (h : CircuitObstructions.CompleteSafeDegreeLE f d) (hde : d ≤ e) : CircuitObstructions.CompleteSafeDegreeLE f e
1181 \end{lstlisting}
1182 \end{minipage}\par
1183 
1184 \par\medskip\noindent\begin{minipage}{\textwidth}
1185 {\small\bfseries L073\enspace\texttt{bprod\_true\_iff}\par}
1186 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:22\par
1187 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1188 \begin{lstlisting}
1189 CircuitObstructions.bprod_true_iff {W : Type} (l : List W) (s : CircuitObstructions.State W) :
1190   CircuitObstructions.bprod l s = true ↔ ∀ (i : W), i ∈ l → s i = true
1191 \end{lstlisting}
1192 \end{minipage}\par
1193 
1194 \par\medskip\noindent\begin{minipage}{\textwidth}
1195 {\small\bfseries L074\enspace\texttt{pointIndicator\_true\_iff}\par}
1196 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:31\par
1197 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1198 \begin{lstlisting}
1199 CircuitObstructions.pointIndicator_true_iff {n : Nat} (v x : Fin n → Bool) :
1200   CircuitObstructions.pointIndicator v x = true ↔ x = v
1201 \end{lstlisting}
1202 \end{minipage}\par
1203 
1204 \par\medskip\noindent\begin{minipage}{\textwidth}
1205 {\small\bfseries L075\enspace\texttt{pointIndicator\_degree}\par}
1206 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:44\par
1207 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1208 \begin{lstlisting}
1209 CircuitObstructions.pointIndicator_degree {n : Nat} (v : Fin n → Bool) :
1210   CircuitObstructions.DegreeLE n (CircuitObstructions.pointIndicator v)
1211 \end{lstlisting}
1212 \end{minipage}\par
1213 
1214 \par\medskip\noindent\begin{minipage}{\textwidth}
1215 {\small\bfseries L076\enspace\texttt{completeSafeDegree\_le\_inputs}\par}
1216 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:56\par
1217 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1218 \begin{lstlisting}
1219 CircuitObstructions.completeSafeDegree_le_inputs {n : Nat} (f : CircuitObstructions.BFun n) :
1220   CircuitObstructions.CompleteSafeDegreeLE f n
1221 \end{lstlisting}
1222 \end{minipage}\par
1223 
1224 \par\medskip\noindent\begin{minipage}{\textwidth}
1225 {\small\bfseries L077\enspace\texttt{exists\_least\_degree}\par}
1226 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:65\par
1227 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1228 \begin{lstlisting}
1229 CircuitObstructions.exists_least_degree (P : Nat → Prop) (n : Nat) (hn : P n) : ∃ r, P r ∧ ∀ (k : Nat), P k → r ≤ k
1230 \end{lstlisting}
1231 \end{minipage}\par
1232 
1233 \par\medskip\noindent\begin{minipage}{\textwidth}
1234 {\small\bfseries L078\enspace\texttt{beta\_exists}\par}
1235 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:83\par
1236 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1237 \begin{lstlisting}
1238 CircuitObstructions.beta_exists {n : Nat} (f : CircuitObstructions.BFun n) :
1239   ∃ r, CircuitObstructions.CompleteSafeDegreeLE f r ∧ ∀ (k : Nat), CircuitObstructions.CompleteSafeDegreeLE f k → r ≤ k
1240 \end{lstlisting}
1241 \end{minipage}\par
1242 
1243 \par\medskip\noindent\begin{minipage}{\textwidth}
1244 {\small\bfseries L079\enspace\texttt{beta\_spec}\par}
1245 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:90\par
1246 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1247 \begin{lstlisting}
1248 CircuitObstructions.beta_spec {n : Nat} (f : CircuitObstructions.BFun n) :
1249   CircuitObstructions.CompleteSafeDegreeLE f (CircuitObstructions.beta f)
1250 \end{lstlisting}
1251 \end{minipage}\par
1252 
1253 \par\medskip\noindent\begin{minipage}{\textwidth}
1254 {\small\bfseries L080\enspace\texttt{beta\_le\_of\_cover}\par}
1255 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:93\par
1256 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1257 \begin{lstlisting}
1258 CircuitObstructions.beta_le_of_cover {n d : Nat} {f : CircuitObstructions.BFun n}
1259   (h : CircuitObstructions.CompleteSafeDegreeLE f d) : CircuitObstructions.beta f ≤ d
1260 \end{lstlisting}
1261 \end{minipage}\par
1262 
1263 \par\medskip\noindent\begin{minipage}{\textwidth}
1264 {\small\bfseries L081\enspace\texttt{beta\_le\_iff}\par}
1265 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:97\par
1266 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1267 \begin{lstlisting}
1268 CircuitObstructions.beta_le_iff {n d : Nat} (f : CircuitObstructions.BFun n) :
1269   CircuitObstructions.beta f ≤ d ↔ CircuitObstructions.CompleteSafeDegreeLE f d
1270 \end{lstlisting}
1271 \end{minipage}\par
1272 
1273 \par\medskip\noindent\begin{minipage}{\textwidth}
1274 {\small\bfseries L082\enspace\texttt{beta\_le\_inputs}\par}
1275 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:103\par
1276 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1277 \begin{lstlisting}
1278 CircuitObstructions.beta_le_inputs {n : Nat} (f : CircuitObstructions.BFun n) : CircuitObstructions.beta f ≤ n
1279 \end{lstlisting}
1280 \end{minipage}\par
1281 
1282 \par\medskip\noindent\begin{minipage}{\textwidth}
1283 {\small\bfseries L083\enspace\texttt{beta\_zero}\par}
1284 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:106\par
1285 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1286 \begin{lstlisting}
1287 CircuitObstructions.beta_zero (n : Nat) : (CircuitObstructions.beta fun x => false) = 0
1288 \end{lstlisting}
1289 \end{minipage}\par
1290 
1291 \par\medskip\noindent\begin{minipage}{\textwidth}
1292 {\small\bfseries L084\enspace\texttt{canonical\_cut\_completeSafeDegree}\par}
1293 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:113\par
1294 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1295 \begin{lstlisting}
1296 CircuitObstructions.canonical_cut_completeSafeDegree (n a : Nat)
1297   (p q : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
1298   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) (p ++ q) f) :
1299   CircuitObstructions.CompleteSafeDegreeLE f
1300     (max (CircuitObstructions.toffoliCount p) (CircuitObstructions.toffoliCount q) + 1)
1301 \end{lstlisting}
1302 \end{minipage}\par
1303 
1304 \par\medskip\noindent\begin{minipage}{\textwidth}
1305 {\small\bfseries L085\enspace\texttt{toffoliCost\_le\_one}\par}
1306 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:124\par
1307 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1308 \begin{lstlisting}
1309 CircuitObstructions.Gate.toffoliCost_le_one {W : Type} (g : CircuitObstructions.Gate W) : g.toffoliCost ≤ 1
1310 \end{lstlisting}
1311 \end{minipage}\par
1312 
1313 \par\medskip\noindent\begin{minipage}{\textwidth}
1314 {\small\bfseries L086\enspace\texttt{toffoliCount\_nil}\par}
1315 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:127\par
1316 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
1317 \begin{lstlisting}
1318 CircuitObstructions.toffoliCount_nil {W : Type} : CircuitObstructions.toffoliCount [] = 0
1319 \end{lstlisting}
1320 \end{minipage}\par
1321 
1322 \par\medskip\noindent\begin{minipage}{\textwidth}
1323 {\small\bfseries L087\enspace\texttt{toffoliCount\_cons}\par}
1324 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:129\par
1325 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
1326 \begin{lstlisting}
1327 CircuitObstructions.toffoliCount_cons {W : Type} (g : CircuitObstructions.Gate W) (c : CircuitObstructions.Circuit W) :
1328   CircuitObstructions.toffoliCount (g :: c) = g.toffoliCost + CircuitObstructions.toffoliCount c
1329 \end{lstlisting}
1330 \end{minipage}\par
1331 
1332 \par\medskip\noindent\begin{minipage}{\textwidth}
1333 {\small\bfseries L088\enspace\texttt{exists\_cut\_with\_toffoliCount}\par}
1334 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:133\par
1335 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1336 \begin{lstlisting}
1337 CircuitObstructions.exists_cut_with_toffoliCount {W : Type} (c : CircuitObstructions.Circuit W) (k : Nat)
1338   (hk : k ≤ CircuitObstructions.toffoliCount c) : ∃ p q, c = p ++ q ∧ CircuitObstructions.toffoliCount p = k
1339 \end{lstlisting}
1340 \end{minipage}\par
1341 
1342 \par\medskip\noindent\begin{minipage}{\textwidth}
1343 {\small\bfseries L089\enspace\texttt{exists\_balanced\_toffoli\_cut}\par}
1344 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:155\par
1345 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1346 \begin{lstlisting}
1347 CircuitObstructions.exists_balanced_toffoli_cut {W : Type} (c : CircuitObstructions.Circuit W) :
1348   ∃ p q,
1349     c = p ++ q ∧
1350       max (CircuitObstructions.toffoliCount p) (CircuitObstructions.toffoliCount q) ≤
1351         (CircuitObstructions.toffoliCount c + 1) / 2
1352 \end{lstlisting}
1353 \end{minipage}\par
1354 
1355 \par\medskip\noindent\begin{minipage}{\textwidth}
1356 {\small\bfseries L090\enspace\texttt{canonical\_restored\_completeSafeDegree}\par}
1357 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:165\par
1358 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1359 \begin{lstlisting}
1360 CircuitObstructions.canonical_restored_completeSafeDegree (n a : Nat)
1361   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
1362   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
1363   CircuitObstructions.CompleteSafeDegreeLE f ((CircuitObstructions.toffoliCount c + 1) / 2 + 1)
1364 \end{lstlisting}
1365 \end{minipage}\par
1366 
1367 \par\medskip\noindent\begin{minipage}{\textwidth}
1368 {\small\bfseries L091\enspace\texttt{beta\_le\_half\_toffoliCount}\par}
1369 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:173\par
1370 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1371 \begin{lstlisting}
1372 CircuitObstructions.beta_le_half_toffoliCount (n a : Nat)
1373   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
1374   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
1375   CircuitObstructions.beta f ≤ (CircuitObstructions.toffoliCount c + 1) / 2 + 1
1376 \end{lstlisting}
1377 \end{minipage}\par
1378 
1379 \par\medskip\noindent\begin{minipage}{\textwidth}
1380 {\small\bfseries L092\enspace\texttt{beta\_restoration\_bound}\par}
1381 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:179\par
1382 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1383 \begin{lstlisting}
1384 CircuitObstructions.beta_restoration_bound (n a : Nat)
1385   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
1386   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
1387   2 * CircuitObstructions.beta f ≤ CircuitObstructions.toffoliCount c + 3
1388 \end{lstlisting}
1389 \end{minipage}\par
1390 
1391 \par\medskip\noindent\begin{minipage}{\textwidth}
1392 {\small\bfseries L093\enspace\texttt{toffoliCount\_ge\_two\_beta\_sub\_three}\par}
1393 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/SafeDegree.lean}:186\par
1394 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1395 \begin{lstlisting}
1396 CircuitObstructions.toffoliCount_ge_two_beta_sub_three (n a : Nat)
1397   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
1398   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
1399   2 * CircuitObstructions.beta f - 3 ≤ CircuitObstructions.toffoliCount c
1400 \end{lstlisting}
1401 \end{minipage}\par
1402 
1403 \subsection*{AffineOutput: 14 declarations}
1404 \par\medskip\noindent\begin{minipage}{\textwidth}
1405 {\small\bfseries L094\enspace\texttt{restores\_append}\par}
1406 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:12\par
1407 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
1408 \begin{lstlisting}
1409 CircuitObstructions.restores_append {X W : Type} [DecidableEq W] (e : CircuitObstructions.Boundary X W)
1410   (c d : CircuitObstructions.Circuit W) (f g : X → Bool) (hc : CircuitObstructions.Restores e c f)
1411   (hd : CircuitObstructions.Restores e d g) : CircuitObstructions.Restores e (c ++ d) fun x => f x ^^ g x
1412 \end{lstlisting}
1413 \end{minipage}\par
1414 
1415 \par\medskip\noindent\begin{minipage}{\textwidth}
1416 {\small\bfseries L095\enspace\texttt{canonical\_target\_not}\par}
1417 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:20\par
1418 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1419 \begin{lstlisting}
1420 CircuitObstructions.canonical_target_not (n a : Nat) (x : Fin n → Bool) (b : Bool) :
1421   (CircuitObstructions.Gate.not (CircuitObstructions.canonicalBoundary n a).target).eval
1422       ((CircuitObstructions.canonicalBoundary n a).encode x b) =
1423     (CircuitObstructions.canonicalBoundary n a).encode x (b ^^ true)
1424 \end{lstlisting}
1425 \end{minipage}\par
1426 
1427 \par\medskip\noindent\begin{minipage}{\textwidth}
1428 {\small\bfseries L096\enspace\texttt{canonical\_input\_to\_target}\par}
1429 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:34\par
1430 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1431 \begin{lstlisting}
1432 CircuitObstructions.canonical_input_to_target (n a : Nat) (i : Fin n) (x : Fin n → Bool) (b : Bool) :
1433   (CircuitObstructions.inputToTarget n a i).eval ((CircuitObstructions.canonicalBoundary n a).encode x b) =
1434     (CircuitObstructions.canonicalBoundary n a).encode x (b ^^ x i)
1435 \end{lstlisting}
1436 \end{minipage}\par
1437 
1438 \par\medskip\noindent\begin{minipage}{\textwidth}
1439 {\small\bfseries L097\enspace\texttt{affine\_restored\_exists}\par}
1440 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:45\par
1441 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1442 \begin{lstlisting}
1443 CircuitObstructions.affine_restored_exists (n a : Nat) (g : CircuitObstructions.BFun n)
1444   (hg : CircuitObstructions.DegreeLE 1 g) :
1445   ∃ d,
1446     CircuitObstructions.toffoliCount d = 0 ∧
1447       CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) d g
1448 \end{lstlisting}
1449 \end{minipage}\par
1450 
1451 \par\medskip\noindent\begin{minipage}{\textwidth}
1452 {\small\bfseries L098\enspace\texttt{betaStar\_exists}\par}
1453 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:76\par
1454 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1455 \begin{lstlisting}
1456 CircuitObstructions.betaStar_exists {n : Nat} (f : CircuitObstructions.BFun n) :
1457   ∃ r, CircuitObstructions.AffineSafeDegreeLE f r ∧ ∀ (k : Nat), CircuitObstructions.AffineSafeDegreeLE f k → r ≤ k
1458 \end{lstlisting}
1459 \end{minipage}\par
1460 
1461 \par\medskip\noindent\begin{minipage}{\textwidth}
1462 {\small\bfseries L099\enspace\texttt{betaStar\_spec}\par}
1463 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:85\par
1464 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1465 \begin{lstlisting}
1466 CircuitObstructions.betaStar_spec {n : Nat} (f : CircuitObstructions.BFun n) :
1467   CircuitObstructions.AffineSafeDegreeLE f (CircuitObstructions.betaStar f)
1468 \end{lstlisting}
1469 \end{minipage}\par
1470 
1471 \par\medskip\noindent\begin{minipage}{\textwidth}
1472 {\small\bfseries L100\enspace\texttt{betaStar\_le\_of\_bound}\par}
1473 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:88\par
1474 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1475 \begin{lstlisting}
1476 CircuitObstructions.betaStar_le_of_bound {n d : Nat} {f : CircuitObstructions.BFun n}
1477   (h : CircuitObstructions.AffineSafeDegreeLE f d) : CircuitObstructions.betaStar f ≤ d
1478 \end{lstlisting}
1479 \end{minipage}\par
1480 
1481 \par\medskip\noindent\begin{minipage}{\textwidth}
1482 {\small\bfseries L101\enspace\texttt{betaStar\_le\_inputs}\par}
1483 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:92\par
1484 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1485 \begin{lstlisting}
1486 CircuitObstructions.betaStar_le_inputs {n : Nat} (f : CircuitObstructions.BFun n) : CircuitObstructions.betaStar f ≤ n
1487 \end{lstlisting}
1488 \end{minipage}\par
1489 
1490 \par\medskip\noindent\begin{minipage}{\textwidth}
1491 {\small\bfseries L102\enspace\texttt{beta\_le\_betaStar}\par}
1492 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:97\par
1493 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1494 \begin{lstlisting}
1495 CircuitObstructions.beta_le_betaStar {n : Nat} (f : CircuitObstructions.BFun n) :
1496   CircuitObstructions.beta f ≤ CircuitObstructions.betaStar f
1497 \end{lstlisting}
1498 \end{minipage}\par
1499 
1500 \par\medskip\noindent\begin{minipage}{\textwidth}
1501 {\small\bfseries L103\enspace\texttt{betaStar\_le\_half\_toffoliCount}\par}
1502 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:101\par
1503 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1504 \begin{lstlisting}
1505 CircuitObstructions.betaStar_le_half_toffoliCount (n a : Nat)
1506   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
1507   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
1508   CircuitObstructions.betaStar f ≤ (CircuitObstructions.toffoliCount c + 1) / 2 + 1
1509 \end{lstlisting}
1510 \end{minipage}\par
1511 
1512 \par\medskip\noindent\begin{minipage}{\textwidth}
1513 {\small\bfseries L104\enspace\texttt{betaStar\_restoration\_bound}\par}
1514 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:112\par
1515 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1516 \begin{lstlisting}
1517 CircuitObstructions.betaStar_restoration_bound (n a : Nat)
1518   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
1519   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
1520   2 * CircuitObstructions.betaStar f ≤ CircuitObstructions.toffoliCount c + 3
1521 \end{lstlisting}
1522 \end{minipage}\par
1523 
1524 \par\medskip\noindent\begin{minipage}{\textwidth}
1525 {\small\bfseries L105\enspace\texttt{toffoliCount\_ge\_two\_betaStar\_sub\_three}\par}
1526 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:119\par
1527 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1528 \begin{lstlisting}
1529 CircuitObstructions.toffoliCount_ge_two_betaStar_sub_three (n a : Nat)
1530   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
1531   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
1532   2 * CircuitObstructions.betaStar f - 3 ≤ CircuitObstructions.toffoliCount c
1533 \end{lstlisting}
1534 \end{minipage}\par
1535 
1536 \par\medskip\noindent\begin{minipage}{\textwidth}
1537 {\small\bfseries L106\enspace\texttt{canonical\_restored\_output\_degree}\par}
1538 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:126\par
1539 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1540 \begin{lstlisting}
1541 CircuitObstructions.canonical_restored_output_degree (n a : Nat)
1542   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
1543   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
1544   CircuitObstructions.DegreeLE (CircuitObstructions.toffoliCount c + 1) f
1545 \end{lstlisting}
1546 \end{minipage}\par
1547 
1548 \par\medskip\noindent\begin{minipage}{\textwidth}
1549 {\small\bfseries L107\enspace\texttt{restored\_degree\_and\_cover\_bound}\par}
1550 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/AffineOutput.lean}:140\par
1551 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1552 \begin{lstlisting}
1553 CircuitObstructions.restored_degree_and_cover_bound (n a : Nat)
1554   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire n a)) (f : CircuitObstructions.BFun n)
1555   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary n a) c f) :
1556   CircuitObstructions.DegreeLE (CircuitObstructions.toffoliCount c + 1) f ∧
1557     2 * CircuitObstructions.betaStar f ≤ CircuitObstructions.toffoliCount c + 3
1558 \end{lstlisting}
1559 \end{minipage}\par
1560 
1561 \subsection*{DegreeChecks: 8 declarations}
1562 \par\medskip\noindent\begin{minipage}{\textwidth}
1563 {\small\bfseries L108\enspace\texttt{squareParity\_add}\par}
1564 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/DegreeChecks.lean}:17\par
1565 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext\par}\nopagebreak
1566 \begin{lstlisting}
1567 CircuitObstructions.squareParity_add (f g : CircuitObstructions.BFun 2) :
1568   (CircuitObstructions.squareParity fun x => f x ^^ g x) =
1569     (CircuitObstructions.squareParity f ^^ CircuitObstructions.squareParity g)
1570 \end{lstlisting}
1571 \end{minipage}\par
1572 
1573 \par\medskip\noindent\begin{minipage}{\textwidth}
1574 {\small\bfseries L109\enspace\texttt{affine\_squareParity\_zero}\par}
1575 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/DegreeChecks.lean}:22\par
1576 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1577 \begin{lstlisting}
1578 CircuitObstructions.affine_squareParity_zero (f : CircuitObstructions.BFun 2) (h : CircuitObstructions.DegreeLE 1 f) :
1579   CircuitObstructions.squareParity f = false
1580 \end{lstlisting}
1581 \end{minipage}\par
1582 
1583 \par\medskip\noindent\begin{minipage}{\textwidth}
1584 {\small\bfseries L110\enspace\texttt{andTwo\_degree\_two}\par}
1585 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/DegreeChecks.lean}:39\par
1586 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1587 \begin{lstlisting}
1588 CircuitObstructions.andTwo_degree_two : CircuitObstructions.DegreeLE 2 CircuitObstructions.andTwo
1589 \end{lstlisting}
1590 \end{minipage}\par
1591 
1592 \par\medskip\noindent\begin{minipage}{\textwidth}
1593 {\small\bfseries L111\enspace\texttt{andTwo\_not\_affine}\par}
1594 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/DegreeChecks.lean}:43\par
1595 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1596 \begin{lstlisting}
1597 CircuitObstructions.andTwo_not_affine : ¬CircuitObstructions.DegreeLE 1 CircuitObstructions.andTwo
1598 \end{lstlisting}
1599 \end{minipage}\par
1600 
1601 \par\medskip\noindent\begin{minipage}{\textwidth}
1602 {\small\bfseries L112\enspace\texttt{andTwo\_no\_degree\_one\_safe\_cover}\par}
1603 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/DegreeChecks.lean}:49\par
1604 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Quot.sound\par}\nopagebreak
1605 \begin{lstlisting}
1606 CircuitObstructions.andTwo_no_degree_one_safe_cover :
1607   ¬CircuitObstructions.CompleteSafeDegreeLE CircuitObstructions.andTwo 1
1608 \end{lstlisting}
1609 \end{minipage}\par
1610 
1611 \par\medskip\noindent\begin{minipage}{\textwidth}
1612 {\small\bfseries L113\enspace\texttt{beta\_andTwo}\par}
1613 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/DegreeChecks.lean}:64\par
1614 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1615 \begin{lstlisting}
1616 CircuitObstructions.beta_andTwo : CircuitObstructions.beta CircuitObstructions.andTwo = 2
1617 \end{lstlisting}
1618 \end{minipage}\par
1619 
1620 \par\medskip\noindent\begin{minipage}{\textwidth}
1621 {\small\bfseries L114\enspace\texttt{betaStar\_andTwo}\par}
1622 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/DegreeChecks.lean}:72\par
1623 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1624 \begin{lstlisting}
1625 CircuitObstructions.betaStar_andTwo : CircuitObstructions.betaStar CircuitObstructions.andTwo = 2
1626 \end{lstlisting}
1627 \end{minipage}\par
1628 
1629 \par\medskip\noindent\begin{minipage}{\textwidth}
1630 {\small\bfseries L115\enspace\texttt{restored\_andTwo\_needs\_toffoli}\par}
1631 {\footnotesize\raggedright\textbf{Source.}\enspace\code{CircuitObstructions/DegreeChecks.lean}:78\par
1632 \textbf{Block.}\enspace 02\quad\textbf{Axioms.}\enspace propext, Classical.choice, Quot.sound\par}\nopagebreak
1633 \begin{lstlisting}
1634 CircuitObstructions.restored_andTwo_needs_toffoli (a : Nat)
1635   (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire 2 a))
1636   (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary 2 a) c CircuitObstructions.andTwo) :
1637   1 ≤ CircuitObstructions.toffoliCount c
1638 \end{lstlisting}
1639 \end{minipage}\par
1640 
1641 \endgroup
1642 

Back to source controls

Back to Quantum and Circuits