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 
2 \chapter{Claim coverage and theorem index}
3 \label{c:app:index}
4 The source register has eight maintained claim groups. This reference expands the maintained arguments into individually numbered statements and adds the later register-product invariant. Prose statement counts and formal lemma counts have different meanings. The Lean guide lists all 115 formal declarations; the original theorem companion and its historical theorem map remain preserved.
5 
6 \section{Coverage of the maintained register}
7 \small
8 \begin{longtable}{@{}>{\RaggedRight\arraybackslash}p{0.40in}>{\RaggedRight\arraybackslash}p{1.77in}>{\RaggedRight\arraybackslash}p{2.24in}>{\RaggedRight\arraybackslash}p{1.40in}@{}}
9 \toprule
10 \textbf{ID} & \textbf{Maintained subject} & \textbf{Results in this reference} & \textbf{Source location}\\\midrule\endhead
11 C01 & Exact cut-comparison cover & Theorem~\ref{c:thm:cut} & Foundations F2\\
12 C02 & Complete-cover bound and dual certificates & Results~\ref{c:prop:beta-bounds}--\ref{c:cor:monomial} & Theory \S1; Foundations F4\\
13 C03 & Unbalanced-OR calibration & Results~\ref{c:prop:raw-family}--\ref{c:cor:family-cost} & Theory \S2\\
14 C04 & Optimal small restored oracles & Theorem~\ref{c:thm:small-oracles} & Theory \S2\\
15 C05 & Projection cost and safety & Results~\ref{c:lem:affine-subspace}--\ref{c:ce:unsafe} & Theory \S3\\
16 C06 & Faithful flat gluing dimension & Theorem~\ref{c:thm:gluing-dim}; Corollary~\ref{c:cor:scalar-eval} & Theory \S4\\
17 C07 & Weighted witness fingerprint & Results~\ref{c:thm:fingerprint}--\ref{c:prop:conditional-sat} & Theory \S5\\
18 C08 & Overlap obstruction & Proposition~\ref{c:prop:disjoint}; Counterexample~\ref{c:ce:overlap} & Theory \S5\\
19 \bottomrule
20 \end{longtable}
21 \normalsize
22 The foundational simulation and degree results, Theorem~\ref{c:thm:simulation} and Lemma~\ref{c:lem:degree}, support the active claims. The conditional status of Proposition~\ref{c:prop:conditional-sat} is unchanged from C07. Counterexamples are deliberately indexed as counterexamples, rather than presented as successful universal compression theorems.
23 
24 \section{Dependency structure}
25 The main proof dependencies are:
26 \[
27 \begin{gathered}
28 \text{restored oracle convention}\ \Longrightarrow\ \text{cut comparison},\\
29 \text{cut comparison}+\text{degree per multiplication}\
30 \Longrightarrow\ \text{complete-cover lower bound},\\
31 \text{safe ideal}+\text{finite linear duality}\
32 \Longrightarrow\ \text{evaluation-span certificates},\\
33 \text{monotone ideal}+\text{affine input/output changes}\
34 \Longrightarrow\ \text{calibration formulas},\\
35 \text{affine restriction}+\text{quadratic polar rank}\
36 \Longrightarrow\ \text{projection-cost lower bound},\\
37 \text{orthogonal idempotents}\ \Longrightarrow\ \text{gluing dimension},\\
38 \text{Boolean coefficient identity}+\text{root bound}\
39 \Longrightarrow\ \text{conditional fingerprint test}.
40 \end{gathered}
41 \]
42 The gluing-dimension theorem and fingerprint construction are separate from the circuit-cut theorem. No proof step identifies algebra dimension with unrestricted circuit size.
43 
44 \clearpage
45 \section{Complete numbered-result index}
46 \small
47 \begin{longtable}{@{}>{\RaggedRight\arraybackslash}p{0.40in}>{\RaggedRight\arraybackslash}p{4.15in}>{\RaggedRight\arraybackslash}p{0.74in}r@{}}
48 \toprule
49 \textbf{No.} & \textbf{Result} & \textbf{Scope} & \textbf{Page}\\\midrule\endhead
50 \resultrow{c:thm:simulation}{Classical/restored simulation comparison}{Base}{}
51 \resultrow{c:lem:degree}{Degree per multiplication}{Base}{}
52 \resultrow{c:thm:register-products}{Register-product degree invariant}{Base / formal}{}
53 \resultrow{c:thm:cut}{Cut-comparison identity and complete coverage}{C01}{}
54 \resultrow{c:prop:beta-bounds}{Basic size bounds}{C02}{}
55 \resultrow{c:prop:affine-invariance}{Affine input invariance}{C02}{}
56 \resultrow{c:thm:complete-bound}{Affine-optimized complete-cover bound}{C02}{}
57 \resultrow{c:thm:dual}{Dual certificate for failure of safe detection}{C02}{}
58 \resultrow{c:cor:dual-witness}{Finite support of a dual witness}{C02}{}
59 \resultrow{c:thm:monotone}{Safe monomial ideal for a monotone function}{C02}{}
60 \resultrow{c:cor:monomial}{Exact monomial oracle cost}{C02}{}
61 \resultrow{c:prop:raw-family}{Raw calibration parameters}{C03}{}
62 \resultrow{c:thm:family-alpha}{Affine optimization of the one-packet parameter}{C03}{}
63 \resultrow{c:thm:family-beta}{Affine optimization of complete coverage}{C03}{}
64 \resultrow{c:cor:family-cost}{Restored cost interval for the calibration family}{C03}{}
65 \resultrow{c:thm:small-oracles}{Exact small restored-oracle calibration}{C04}{}
66 \resultrow{c:lem:affine-subspace}{Affine subspace after multiplication restrictions}{C05}{}
67 \resultrow{c:prop:quadratic-cost}{Exact cost of a nondegenerate paired quadratic}{C05}{}
68 \resultrow{c:thm:whole-cost}{Exact nonlinear cost of the whole function}{C05}{}
69 \resultrow{c:thm:grade-cost}{Exact cost of the extracted grade}{C05}{}
70 \resultrow{c:ce:unsafe}{Projection does not preserve safe support}{C05}{}
71 \resultrow{c:thm:gluing-dim}{Dimension of a faithful multiplicative summary}{C06}{}
72 \resultrow{c:cor:scalar-eval}{Scalar unital summaries are evaluations}{C06}{}
73 \resultrow{c:thm:fingerprint}{Exact witness fingerprint}{C07}{}
74 \resultrow{c:lem:top-coeff}{Top coefficient as a Boolean-cube sum}{C07}{}
75 \resultrow{c:thm:weighted-top}{Weighted top-coefficient identity}{C07}{}
76 \resultrow{c:lem:roots}{Finite-field root bound}{C07}{}
77 \resultrow{c:prop:conditional-sat}{Conditional randomized satisfiability test}{C07}{}
78 \resultrow{c:prop:disjoint}{Disjoint-variable factorization}{C08}{}
79 \resultrow{c:ce:overlap}{Shared-variable multiplication fails}{C08}{}
80 \bottomrule
81 \end{longtable}
82 \normalsize
83 
84 
85 \section{Baseline domains reproduced by the full run}\label{c:app:evidence}
86 The exact mathematical outputs below were compared with the preserved baseline. The historical runner also reproduced its seven scientific output records. These finite ranges remain part of the evidence even where a universal written theorem accompanies them.
87 \small
88 \begin{longtable}{@{}>{\RaggedRight\arraybackslash}p{1.57in}>{\RaggedRight\arraybackslash}p{2.27in}>{\RaggedRight\arraybackslash}p{2.00in}@{}}
89 \toprule
90 \textbf{Evidence area} & \textbf{Executed domain in the baseline} & \textbf{Limit of the evidence}\\\midrule\endhead
91 Small functions & All 276 functions on one, two, or three inputs; 4,240 scalar input/target cases; 2,344 cuts & Exact constructions plus proved lower bounds, not exhaustive circuit search\\
92 Four-input profiles & All 65,536 truth tables; all 168 monotone functions & Independent evaluation-span method checks only the declared 765 cases\\
93 Unbalanced-OR family & Designated truth tables through nine inputs; all affine masks through eight & No exhaustive ninth-input affine-mask claim\\
94 Projection coefficients & 693,965 pair coefficients and nine exact rank cases, through 1,022 inputs & Full truth tables only at $m=2,3,4$\\
95 Projection oracle checks & 65,808 logical-input/target cases across the two constructed oracle families in the stated small domains & Large entries use symbolic formulas, exact rank, and construction counts\\
96 Weighted fingerprints & 1,052,736 verifier/field-point evaluations & Enumerated verifiers have at most three witness bits\\
97 Independent coefficient extraction & 20,544 cases & All field points for $m\le2$; restricted coordinate grid at $m=3$\\
98 Disjoint product rule & 4,096 exact controls & Does not extend the rule to shared variables\\
99 Scalar algebra maps & 66,048 linear maps over the three specified witness/field domains & Controls the scalar special case; general dimension theorem has a written proof\\
100 \bottomrule
101 \end{longtable}
102 \normalsize
103 
104 The field used in the fingerprint checker is
105 \[
106  \mathrm{GF}(16)=\F[t]/(t^4+t+1).
107 \]
108 All mathematical arithmetic in these tests is Boolean, exact integer, or finite-field arithmetic. Runtime is not presented as a complexity benchmark. Equality of checksums certifies matching bytes, not mathematical truth.
109 
110 
111 
112 \section{Excluded inferences}
113 The following boundaries are retained from the release's failure register. They are part of the closed scope, not a promise to finish every exploratory route.
114 
115 \textbf{Semantic elimination curvature.} Exact existential eliminations commute. A nonzero semantic commutator cannot be asserted for those exact operators.
116 
117 \textbf{Expanded-state counting.} Exponentially many residuals or obstruction descriptions can arise from a small circuit. The number of expanded objects is not their shared construction cost.
118 
119 \textbf{Small-case equality.} Agreement of affine-optimized one-packet and complete-cover degrees through four inputs does not extend to all sizes. Chapter~\ref{c:ch:calibration} gives an exact separating family.
120 
121 \textbf{Free homogeneous extraction.} A projected grade may have greater nonlinear cost than the whole and can fail to remain safe. Chapter~\ref{c:ch:projection} keeps the input length and total affine cost explicit.
122 
123 \textbf{Unrestricted gluing.} The exponential dimension theorem applies to a fixed faithful linear multiplicative map. It does not exclude succinct, nonlinear, or context-dependent algorithms.
124 
125 \textbf{Context-free trace multiplication.} The disjoint-variable product rule fails at shared witness variables. A short expression containing an extraction operator is not an efficient implementation of that extraction.
126 

Back to source controls

Back to Quantum and Circuits