Lean files

The modules, in compile order, followed by the verification log, the README and two reports. Back to the page.

AvoidedDefs.lean
AvoidedPeelTools.lean
AvoidedClosure.lean
AvoidedGen.lean
AvoidedPeel.lean
AvoidedTransfer.lean
Projection.lean
Statements.lean
Conjectures.lean
ClusterProperty.lean
Statements6.lean
Conjecture6Reduction.lean
PairSource.lean
GuardedDefs.lean
GuardedBasic.lean
GuardedKernel.lean
GuardedDecoy.lean
GuardedTwoCluster.lean
PairGuardedCSH.lean
PairSurplus.lean
PairSurplusClosure.lean
PairFixedMin.lean
Conjecture6Proof.lean
Question5Dual.lean
Question5.lean
Question8Defs.lean
Question8Cases.lean
Question8Counterexample.lean
Question8Equivalence.lean
Question8Interior.lean
Question8Sufficient.lean
SourceGeneralCSH.lean
SourceSurplus.lean
SourceProjection.lean
Statements9.lean
Question9Reduction.lean
Question9.lean
AvoidedClosure.REPORT.md
Projection.REPORT.md
README.md
VERIFICATION.log