# Claim register

Only C01–C08 are active mathematical claims in version 1.0.0. 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](FOUNDATIONS.md), section F2. **Status:** FINITE and WRITTEN.

**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](THEORY.md), section 1. **Status:** FINITE and WRITTEN.

**Computation.** Full four-input profile table; independent rank checks only on the documented 765 cases.

**Boundary.** beta*<=n; bounded controls are not universal machine checking.

## 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](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](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](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](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](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](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](claims.json). Finite output records are in `evidence/baseline/`; the release replay is documented in `evidence/closure/`.