Proof Backlog Validation Report

Generated: 2026-02-10 18:57:26

Summary

Progress: 2/11 (18%)

Near-term (P1-P6): 2/6 proved

Long-term (L1-L5): 0/5 complete

Detailed Status

IDFileStatusTestsIssues
P1 morphism/lab/proofs/Morphism/SheafTheory.lean Axiomatized -> Proved X Test file missing Test file not found
P2 morphism/lab/proofs/Morphism/SheafTheory.lean Axiomatized -> Proved X Test file missing Test file not found
P3 morphism/lab/proofs/Morphism/GOVERNANCE_BELL_INEQUALITY.lean Axiomatized -> Proved X Test file missing Test file not found
P4 morphism/lab/proofs/Morphism/GOVERNANCE_BELL_INEQUALITY.lean Axiomatized -> Proved X Test file missing Test file not found
P5 morphism/lab/proofs/Morphism/AgentUncertainty.lean Proved N/A None
P6 morphism/lab/proofs/Morphism/AgentUncertainty.lean Proved N/A None
L1 morphism/lab/proofs/Morphism/ProbabilisticUncertainty.lean Open N/A None
L2 morphism/lab/proofs/Morphism/ContinuousUncertainty.lean Open N/A None
L3 morphism/lab/proofs/Morphism/Computability.lean Open N/A None
L4 morphism/lab/proofs/Morphism/CategoricalEquivalence.lean Open N/A None
L5 morphism/lab/proofs/Morphism/HigherCohomology.lean Open N/A None

Validation Issues

• P1: File morphism/lab/proofs/Morphism/SheafTheory.lean not found

• P2: File morphism/lab/proofs/Morphism/SheafTheory.lean not found

• P3: File morphism/lab/proofs/Morphism/GOVERNANCE_BELL_INEQUALITY.lean not found

• P4: File morphism/lab/proofs/Morphism/GOVERNANCE_BELL_INEQUALITY.lean not found

• P5: File morphism/lab/proofs/Morphism/AgentUncertainty.lean not found

• P6: File morphism/lab/proofs/Morphism/AgentUncertainty.lean not found