Problem CX-003 — the sample complexity of PAC learning

Conjectura.Problems.CX003.Statement

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Conjectura.Defs.ComputerScience.Learning.HasFiniteVCDim
import Conjectura.Defs.ComputerScience.Learning.VCDimension

/-! # Problem CX-003 — the sample complexity of PAC learning

LOCKED: solvers cannot modify this file.
-/
namespace Conjectura.CX003
open Conjectura.Learning
/-- Is a class of finite VC dimension shattered by no set larger than that dimension?
The definitional direction is immediate; the content is that `vcDim` and
`HasFiniteVCDim` agree, which is the bridge between the two ways the corpus states
finiteness. A formalization target rather than an open question. -/
def goal : Prop :=
  ∀ (α : Type) (C : ConceptClass α Bool),
    HasFiniteVCDim C ↔ vcDim C ≠ ⊤
end Conjectura.CX003