Claim register
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.
C01 — Exact cut-comparison cover
Statement. For every restored classical oracle and every cut, H_i<=f and OR_i H_i=f.
Proof. FOUNDATIONS.md, section F2; Lean Block 01. Status: LEAN, FINITE and WRITTEN.
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.
Computation. All 276 functions through three inputs, with explicitly constructed restored circuits.
Boundary. No universal circuit-size lower bound follows solely from packet count.
C02 — Complete-cover lower bound and dual certificates
Statement. T>=max(0,deg(f)-1,2 beta*(f)-3), with exact evaluation-span characterization of beta_v.
Proof. THEORY.md, section 1; Lean Block 02. Status: PARTIAL LEAN, FINITE and WRITTEN.
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.
Computation. Full four-input profile table; independent rank checks only on the documented 765 cases.
Boundary. beta*<=n is itself formalized. This does not yield a superpolynomial lower bound; the dual-certificate claims keep their distinct status.
C03 — Unbalanced-OR calibration
Statement. For k>=2, F_k=ab OR product(z_i): max affine alpha_1=3 and beta*=k+1.
Proof. THEORY.md, section 2. Status: FINITE and WRITTEN.
Computation. Full designated family tables through nine inputs; all affine masks only through eight.
Boundary. Easy linear-size family; no exact optimum claimed when lower and upper bounds differ.
C04 — Optimal small restored oracles
Statement. The complete-cover bound is attained by explicit classical implementations for all functions on one, two, or three inputs.
Proof. THEORY.md, section 2. Status: FINITE and WRITTEN.
Computation. All 276 functions; 28 zero-, 120 one-, and 128 three-Toffoli implementations.
Boundary. Optimality combines the written lower bound and constructed witnesses; not exhaustive circuit search.
C05 — Projection cost and safety counterexample
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.
Proof. THEORY.md, section 3. Status: COUNTEREXAMPLE, FINITE and WRITTEN.
Computation. Ranks and pair coefficients through m=10; full truth tables only m=2,3,4.
Boundary. Exponential in m, linear in n; not an exponential total-gate separation.
C06 — Faithful flat gluing dimension
Statement. A linear multiplicative witness-algebra map retaining every primitive witness idempotent has target dimension at least 2^m.
Proof. THEORY.md, section 4. Status: FINITE controls and WRITTEN.
Computation. Small scalar-map controls; the universal argument is orthogonal-idempotent independence.
Boundary. Restricted fixed-summary theorem; dimension is not arbitrary circuit cost.
C07 — Weighted witness fingerprint
Statement. Distinct witness monomials give an exact nonzero/satisfiable equivalence and Boolean top-coefficient identity.
Proof. THEORY.md, section 5. Status: FINITE and WRITTEN; algorithmic implication CONDITIONAL.
Computation. All designated verifiers through three witness bits; exact GF16 evaluation and specified extraction grids.
Boundary. Implemented evaluator is exponential. An efficient evaluator would give the stated randomized implication, not a deterministic P=NP proof.
C08 — Overlap obstruction to multiplicative trace
Statement. The weighted trace multiplies on disjoint variables and fails on the displayed overlapping one-bit predicates.
Proof. THEORY.md, section 5. Status: COUNTEREXAMPLE, FINITE and WRITTEN.
Computation. Exact GF16 counterexamples and 4,096 disjoint controls.
Boundary. Does not exclude context-dependent nonlinear algorithms.
Machine-readable form: claims.json. Finite output records are in evidence/baseline/; the release replay is documented in evidence/closure/.