Status: Frozen

• Witness scope: Closed at repository scope

Status: Frozen (see FREEZE.md)

OWC Counterexamples

Canonical counterexamples and boundary constructions for OWC-style claims.

Repo goals

• Store explicit witnesses (constructors + parameters)
• Provide verifiers that check a witness against a stated target property
• Keep results reproducible via CI

Structure

• docs/ : specification + policy
• witnesses/ : explicit witness constructions
• verify/ : verification scripts + tests
• metrics/ : summaries produced by verification runs

Quickstart

python3 -m venv .venv source .venv/bin/activate python -m pip install -U pip pip install -r requirements.txt pytest -q python verify/verify_witness.py witnesses/witness_0001/parameters.json

Conditional note

• docs/WITNESS_SCOPE_NOTE_2026_04.md — closed witness-scope note specifying the weakest witness-integrity extension compatible with the repository's frozen witness-and-verifier scope.

External status

This repository is governed by docs/status/EXTERNAL_STATUS_LOCK.md. Build success, CI success, dashboards, ledgers, axioms, admits, sorry, or placeholder witnesses do not constitute theorem-level closure.

Lean proof portfolio classification

This repository is governed by docs/status/LEAN_PROOF_PORTFOLIO_CLASSIFICATION.md. Its role in the portfolio is explicitly classified as proof-facing, conditional frontier, infrastructure/documentation, or legacy/scaffold.