Overlap Rigidity Lean Dev

Lean 4 development repository for overlap rigidity interfaces.

Formal Status

Status: INTENDED_GRAPH_FRONTIER_REDUCED / GRAPH_ORL_OPEN

Build status:

• A successful build means the checked root target compiles.
• It does not imply intended ORL or global overlap rigidity.

Theorem status:

• The repository closes formal constructor obligations under permissive semantics.
• The repository closes formal semantic obligations under permissive semantics.
• The repository reduces intended graph-theoretic ORL to explicit intended graph obligations.
• Intended graph-theoretic ORL verified: no.
• Global overlap-rigidity theorem verified: no.

Current strongest checked theorem:

• intended_graph_obligations_exist_give_every_problem_certificate

Current missing theorem/object:

• Construct IntendedGraphTheoreticORLObligations.

Status documents:

• docs/status/FORMAL_SEMANTIC_ORL_CLOSURE_2026_05_03.md
• docs/status/INTENDED_GRAPH_ORL_FRONTIER_2026_05_03.md

Boundary

This repository does not prove intended graph-theoretic ORL. This repository does not prove global Overlap Rigidity. This repository does not prove a nontrivial quotient-rank bound.