Overlap Rigidity (Lean)

Canonical frozen Lean dependency for the Final Wall. Status: conditional (single axiom isolated). Tag: overlap-rigidity-frozen-v1

Conditional note

• docs/DEV_BOUNDARY_NOTE_2026_04.md — conditional note specifying the weakest dependency-audit extension compatible with the current dev-scaffold status.

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.

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.

Formal Status

Status: Placeholder / Scaffold

Build status:

• A successful build means the checked root target compiles.
• It does not imply that the current theorem surface proves overlap rigidity.

Theorem status:

• The current theorem surface is placeholder-level.
• Substantive overlap-rigidity theorem verified: no.
• Placeholder theorems such as True := trivial do not constitute theorem-level verification.

Current status:

• Strongest verified theorem: placeholder theorem only
• Weakest missing theorem: state and prove a nontrivial overlap-rigidity theorem without placeholder collapse
• Scaffold boundary: docs/status/SCAFFOLD_STATUS_2026_04_27.md