Flagship Lean Witness Chain

Goal: one end-to-end Lean theorem + deterministic certificate artifact.

Verification Status

Lean CI

Container Repro Witness

DOI

Quickstart (60 seconds)

./scripts/flagship demo

Flagship Lean Certification (Released)

This repository includes a released certification layer.

Scope:

• Reproducible Lean4 project structure
• CI-stable witness skeletons
• Deterministic build environment

Non-scope:

• No claim of proof completeness
• No claim of solving open problems
• No semantic guarantees beyond declared artifacts

Certification artifacts are immutable once released. Final Wall FO^k Locality Certification (Released) This repository includes a released certification layer recording the FO^k locality terminal obstruction (“Final Wall”). Scope: Declarative obstruction statements Formal boundary documentation Deterministic, verifier-checkable artifacts Non-scope: No resolution of open complexity problems No executable algorithms No inference, refinement, or search guarantees Certification artifacts are immutable once released.

Cycle Local Rigidity Certification (Released)

This repository includes a released certification layer for cycle-local rigidity and locality obstructions.

Scope:

• Declarative rigidity statements
• Formal locality and cycle-structure documentation
• Deterministic, verifier-checkable artifacts

Non-scope:

• No resolution of open complexity problems
• No executable algorithms or solvers
• No inference, refinement, or search guarantees

Certification artifacts are immutable once released.

DFM–MKC Cosmology Certification (Released)

This repository includes a released certification layer for the DFM–MKC cosmology framework.

Scope:

• Reproducible numerical consistency checks
• Bounded-resource execution and documentation
• Deterministic, verifier-checkable artifacts

Non-scope:

• No claim of fundamental cosmological truth
• No resolution of dark energy, dark matter, or ΛCDM definitively
• No guarantees beyond documented numerical behavior

Certification artifacts are immutable once released.

Overlap Rigidity Lean Certification (Released)

Conditional note

• notes/OVERLAP_RIGIDITY_CONDITIONAL_SCOPE_2026_04.md — conditional scope note aligned with the released overlap-rigidity certification layer.

This repository includes a released certification layer for the Lean formal foundation of overlap rigidity.

Scope:

• Lean definitions and local lemmas
• Deterministic kernel-verified proof checking
• Stable formal dependency for downstream projects

Non-scope:

• No claim of a complete overlap rigidity theorem
• No resolution of open complexity problems
• No guarantees beyond Lean kernel correctness

Certification artifacts are immutable once released.

Formal Status

Status: Toy Verified Skeleton

Build status:

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

Theorem status:

• The current theorem surface is intentionally toy-level.
• Current theorem content: payload length nonnegativity.
• Substantive URF theorem verified: no.

Current status:

• Strongest verified theorem: toy payload-length invariant only
• Weakest missing theorem: replace the string-payload toy invariant with a nontrivial mathematical invariant and prove it without definitional collapse
• Triviality boundary: docs/status/TRIVIALITY_BOUNDARY_2026_04_27.md

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.