Nonuniform circuit size for promise problems

This module proves that completion-based promise SIZE is exactly explicit circuit-family solvability on the promised sides. It also distinguishes pointwise from eventual size bounds and proves that finitely many exceptional lengths do not affect polynomial-size promise circuits.

theorem Complexity.mem_PromiseSIZEWithBasis_iff (problem : PromiseProblem) (B : Basis) (bound : ℕ → ℕ) : problem ∈ PromiseSIZEWithBasis B bound ↔ ∃ (family : CircuitFamily B), problem.SolvedBy family.evalList ∧ family.SizeBoundedBy bound

Completion-based promise SIZE is equivalent to one explicit circuit family that solves both promised sides and meets the pointwise bound.

theorem Complexity.mem_PromiseSIZE_iff (problem : PromiseProblem) (bound : ℕ → ℕ) : problem ∈ PromiseSIZE bound ↔ ∃ (family : CircuitFamily Basis.andOr2), problem.SolvedBy family.evalList ∧ family.SizeBoundedBy bound

Specialized explicit-solver characterization over Basis.andOr2.

theorem Complexity.mem_PromisePPoly_iff (problem : PromiseProblem) : problem ∈ PromisePPoly ↔ ∃ (family : CircuitFamily Basis.andOr2), problem.SolvedBy family.evalList ∧ family.PolynomialSize

A promise has a P/poly completion exactly when one polynomial-size circuit family solves both promised sides.

theorem Complexity.CircuitFamily.SizeBoundedBy.eventuallySizeBoundedBy {B : Basis} {family : CircuitFamily B} {bound : ℕ → ℕ} (hbound : family.SizeBoundedBy bound) : family.EventuallySizeBoundedBy bound

A pointwise size bound is also an eventual size bound.

theorem Complexity.CircuitFamily.EventuallySizeBoundedBy.mono {B : Basis} {family : CircuitFamily B} {first second : ℕ → ℕ} (hbound : family.EventuallySizeBoundedBy first) (hle : ∀ (n : ℕ), first n ≤ second n) : family.EventuallySizeBoundedBy second

An eventual size bound is monotone under pointwise enlargement.

theorem Complexity.CircuitFamily.EventuallySizeBoundedBy.trans_eventually {B : Basis} {family : CircuitFamily B} {first second : ℕ → ℕ} (hbound : family.EventuallySizeBoundedBy first) (hle : ∀ᶠ (n : ℕ) in Filter.atTop, first n ≤ second n) : family.EventuallySizeBoundedBy second

An eventual size bound composes with an eventually valid comparison.

theorem Complexity.CircuitFamily.EventuallySizeBoundedBy.polynomialSize {B : Basis} {family : CircuitFamily B} {p : Polynomial ℕ} (hbound : family.EventuallySizeBoundedBy fun (n : ℕ) => Polynomial.eval n p) : family.PolynomialSize

A polynomial bound outside a finite prefix can be enlarged by a constant polynomial to cover every length.

theorem Complexity.PromiseSIZEWithBasis_subset_PromiseEventuallySIZEWithBasis (B : Basis) (bound : ℕ → ℕ) : PromiseSIZEWithBasis B bound ⊆ PromiseEventuallySIZEWithBasis B bound

Pointwise promise size is contained in eventual promise size over any basis.

theorem Complexity.PromiseSIZE_subset_PromiseEventuallySIZE (bound : ℕ → ℕ) : PromiseSIZE bound ⊆ PromiseEventuallySIZE bound

Pointwise promise size is contained in eventual promise size.

theorem Complexity.PromiseSIZEWithBasis_mono (B : Basis) {first second : ℕ → ℕ} (hle : ∀ (n : ℕ), first n ≤ second n) : PromiseSIZEWithBasis B first ⊆ PromiseSIZEWithBasis B second

Pointwise promise SIZE is monotone in its bound.

theorem Complexity.PromiseEventuallySIZEWithBasis_mono (B : Basis) {first second : ℕ → ℕ} (hle : ∀ (n : ℕ), first n ≤ second n) : PromiseEventuallySIZEWithBasis B first ⊆ PromiseEventuallySIZEWithBasis B second

Eventual promise SIZE is monotone in its bound.

theorem Complexity.PromiseSIZEWithBasis_mapBasis_subset {source target : Basis} (hom : source.Hom target) (bound : ℕ → ℕ) : PromiseSIZEWithBasis source bound ⊆ PromiseSIZEWithBasis target bound

Exact semantics-preserving basis relabeling preserves pointwise promise circuit size with no overhead.

theorem Complexity.PromiseEventuallySIZEWithBasis_mapBasis_subset {source target : Basis} (hom : source.Hom target) (bound : ℕ → ℕ) : PromiseEventuallySIZEWithBasis source bound ⊆ PromiseEventuallySIZEWithBasis target bound

Exact semantics-preserving basis relabeling preserves eventual promise circuit size with no overhead.

theorem Complexity.PromiseSIZEWithBasis_eq_of_homs {first second : Basis} (forward : first.Hom second) (reverse : second.Hom first) (bound : ℕ → ℕ) : PromiseSIZEWithBasis first bound = PromiseSIZEWithBasis second bound

Bases admitting exact semantics-preserving relabelings in both directions give the same pointwise promise-size class at every bound.

theorem Complexity.PromiseEventuallySIZEWithBasis_eq_of_homs {first second : Basis} (forward : first.Hom second) (reverse : second.Hom first) (bound : ℕ → ℕ) : PromiseEventuallySIZEWithBasis first bound = PromiseEventuallySIZEWithBasis second bound

Bases admitting exact semantics-preserving relabelings in both directions give the same eventual promise-size class at every bound.

theorem Complexity.PromiseEventuallySIZE_polynomial_subset_PromisePPoly (p : Polynomial ℕ) : (PromiseEventuallySIZE fun (n : ℕ) => Polynomial.eval n p) ⊆ PromisePPoly

Finitely many exceptional lengths do not prevent a polynomially bounded promise solver from giving a P/poly completion.

theorem Complexity.ofLanguage_mem_PromiseSIZE_iff (L : Language) (bound : ℕ → ℕ) : PromiseProblem.ofLanguage L ∈ PromiseSIZE bound ↔ L ∈ SIZE bound

The promise-size lift agrees with ordinary SIZE on total languages.

theorem Complexity.ofLanguage_mem_PromisePPoly_iff (L : Language) : PromiseProblem.ofLanguage L ∈ PromisePPoly ↔ L ∈ PPoly

The promise-P/poly lift agrees with ordinary P/poly on total languages.