Overlap Rigidity Counterexamples

This repository contains the counterexample constructions for Overlap Rigidity used in the Final Wall program.

Conditional note

• notes/COUNTEREXAMPLE_SCOPE_NOTE_2026_04.md — conditional note specifying the weakest certificate-level extension compatible with the repository's counterexample scope.

Contents

• *.tex — LaTeX expositions of counterexamples
• *.pdf — compiled outputs (not tracked)
• src/ — supporting source (if any)

Build

To compile the LaTeX sources locally:

pdflatex <file>.tex

## External status

This repository is governed by [`docs/status/EXTERNAL_STATUS_LOCK.md`](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`](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.