Current circuit claim register (C01–C08)
Quantum and Circuits
CLAIMS.md
1 # Claim register
2
3 C01–C08 remain the closed mathematical scope in version 1.2.0. C01, the maintained NCT degree dependency, and the C02 lower-bound component receive formal verification. The rest of C02 is not marked Lean proved. Older archives are historical evidence, not automatic additions to this register. “Written” means a supplied self-reviewed argument; “finite” means execution in the exact range stated.
4
5 ## C01 — Exact cut-comparison cover
6
7 **Statement.** For every restored classical oracle and every cut, H_i<=f and OR_i H_i=f.
8
9 **Proof.** [FOUNDATIONS.md](FOUNDATIONS.md), section F2; [Lean Block 01](formalization/LEAN_BLOCK_01.md). **Status:** LEAN, FINITE and WRITTEN.
10
11 **Lean.** `CircuitObstructions.complete_safe_cover` and `CircuitObstructions.canonical_complete_safe_cover`; pinned toolchain 4.34.0-rc2. Supporting declarations are not additional maintained claim groups.
12
13 **Computation.** All 276 functions through three inputs, with explicitly constructed restored circuits.
14
15 **Boundary.** No universal circuit-size lower bound follows solely from packet count.
16
17 ## C02 — Complete-cover lower bound and dual certificates
18
19 **Statement.** T>=max(0,deg(f)-1,2 beta*(f)-3), with exact evaluation-span characterization of beta_v.
20
21 **Proof.** [THEORY.md](THEORY.md), section 1; [Lean Block 02](formalization/LEAN_BLOCK_02.md). **Status:** PARTIAL LEAN, FINITE and WRITTEN.
22
23 **Lean subset.** `restored_degree_and_cover_bound` proves a degree-(T+1) polynomial certificate and `2 * betaStar f <= T+3`. Existence and least-bound properties of beta and betaStar, and `betaStar<=n`, are proved. The evaluation-span dual, affine input invariance, and general monotone ideal are not formalized.
24
25 **Computation.** Full four-input profile table; independent rank checks only on the documented 765 cases.
26
27 **Boundary.** beta*<=n is itself formalized. This does not yield a superpolynomial lower bound; the dual-certificate claims keep their distinct status.
28
29 ## C03 — Unbalanced-OR calibration
30
31 **Statement.** For k>=2, F_k=ab OR product(z_i): max affine alpha_1=3 and beta*=k+1.
32
33 **Proof.** [THEORY.md](THEORY.md), section 2. **Status:** FINITE and WRITTEN.
34
35 **Computation.** Full designated family tables through nine inputs; all affine masks only through eight.
36
37 **Boundary.** Easy linear-size family; no exact optimum claimed when lower and upper bounds differ.
38
39 ## C04 — Optimal small restored oracles
40
41 **Statement.** The complete-cover bound is attained by explicit classical implementations for all functions on one, two, or three inputs.
42
43 **Proof.** [THEORY.md](THEORY.md), section 2. **Status:** FINITE and WRITTEN.
44
45 **Computation.** All 276 functions; 28 zero-, 120 one-, and 128 three-Toffoli implementations.
46
47 **Boundary.** Optimality combines the written lower bound and constructed witnesses; not exhaustive circuit search.
48
49 ## C05 — Projection cost and safety counterexample
50
51 **Statement.** A family with n=2^m-2 has T(P_m)=2m-3 and T([P_m]_2)=n/2; the extracted grade can be unsafe.
52
53 **Proof.** [THEORY.md](THEORY.md), section 3. **Status:** COUNTEREXAMPLE, FINITE and WRITTEN.
54
55 **Computation.** Ranks and pair coefficients through m=10; full truth tables only m=2,3,4.
56
57 **Boundary.** Exponential in m, linear in n; not an exponential total-gate separation.
58
59 ## C06 — Faithful flat gluing dimension
60
61 **Statement.** A linear multiplicative witness-algebra map retaining every primitive witness idempotent has target dimension at least 2^m.
62
63 **Proof.** [THEORY.md](THEORY.md), section 4. **Status:** FINITE controls and WRITTEN.
64
65 **Computation.** Small scalar-map controls; the universal argument is orthogonal-idempotent independence.
66
67 **Boundary.** Restricted fixed-summary theorem; dimension is not arbitrary circuit cost.
68
69 ## C07 — Weighted witness fingerprint
70
71 **Statement.** Distinct witness monomials give an exact nonzero/satisfiable equivalence and Boolean top-coefficient identity.
72
73 **Proof.** [THEORY.md](THEORY.md), section 5. **Status:** FINITE and WRITTEN; algorithmic implication CONDITIONAL.
74
75 **Computation.** All designated verifiers through three witness bits; exact GF16 evaluation and specified extraction grids.
76
77 **Boundary.** Implemented evaluator is exponential. An efficient evaluator would give the stated randomized implication, not a deterministic P=NP proof.
78
79 ## C08 — Overlap obstruction to multiplicative trace
80
81 **Statement.** The weighted trace multiplies on disjoint variables and fails on the displayed overlapping one-bit predicates.
82
83 **Proof.** [THEORY.md](THEORY.md), section 5. **Status:** COUNTEREXAMPLE, FINITE and WRITTEN.
84
85 **Computation.** Exact GF16 counterexamples and 4,096 disjoint controls.
86
87 **Boundary.** Does not exclude context-dependent nonlinear algorithms.
88
89 Machine-readable form: [claims.json](claims.json). Finite output records are in `evidence/baseline/`; the release replay is documented in `evidence/closure/`.