`OAI/Combinatorics/Ramsey/CycleClique/Construction/`

658199 declarations, 0 contain sorry, 0 declared as axioms; 259 files

Files

All.lean 53 imports, no declarations
AllCheckedCertificates.lean 1 declarations
AssignedAmounts.lean 6 declarations
AssignedCut.lean 1 declarations
AssignedCutProfile.lean 2 declarations
AssignedDeletion.lean 2 declarations
AssignedLabels.lean 6 declarations
AssignedProfileOperations.lean 2 declarations
AssignedSubcollection.lean 10 declarations
AssignedUniqueness.lean 5 declarations
AttachmentResidual.lean 2 declarations
BallGrowth.lean 8 declarations
BallRecurrence.lean 6 declarations
BallSeparation.lean 8 declarations
BallWeights.lean 4 declarations
BfsBranchPath.lean 5 declarations
BfsBranches.lean 1 declarations
BfsColouredCycle.lean 1 declarations
BfsOneBranch.lean 1 declarations
BfsParent.lean 8 declarations
CEConnectivity.lean 1 declarations
CECycleExtension.lean 14 declarations
CEHamiltonicity.lean 2 declarations
CanonicalProfiles.lean 15 declarations
CanonicalRawCoverage.lean 3 declarations
CertificateCoverage.lean 5 declarations
CertificateMatrixChunks.lean 4 declarations
CertificatesK10.lean 16376 declarations
CertificatesK11.lean 3 imports, no declarations
CertificatesK11Part000.lean 12092 declarations
CertificatesK11Part001.lean 7586 declarations
CertificatesK11Part002.lean 1704 declarations
CertificatesK12.lean 3 imports, no declarations
CertificatesK12Part000.lean 11897 declarations
CertificatesK12Part001.lean 9716 declarations
CertificatesK12Part002.lean 5827 declarations
CertificatesK13.lean 5 imports, no declarations
CertificatesK13Part000.lean 17688 declarations
CertificatesK13Part001.lean 10149 declarations
CertificatesK13Part002.lean 10220 declarations
CertificatesK13Part003.lean 11195 declarations
CertificatesK13Part004.lean 9469 declarations
CertificatesK14.lean 5 imports, no declarations
CertificatesK14Part000.lean 10057 declarations
CertificatesK14Part001.lean 11531 declarations
CertificatesK14Part002.lean 12727 declarations
CertificatesK14Part003.lean 11521 declarations
CertificatesK14Part004.lean 12025 declarations
CertificatesK15.lean 10 imports, no declarations
CertificatesK15Part000.lean 14835 declarations
CertificatesK15Part001.lean 18117 declarations
CertificatesK15Part002.lean 12053 declarations
CertificatesK15Part003.lean 13170 declarations
CertificatesK15Part004.lean 12799 declarations
CertificatesK15Part005.lean 12974 declarations
CertificatesK15Part006.lean 12307 declarations
CertificatesK15Part007.lean 13433 declarations
CertificatesK15Part008.lean 13792 declarations
CertificatesK15Part009.lean 5931 declarations
CertificatesK16.lean 8 imports, no declarations
CertificatesK16Part000.lean 11833 declarations
CertificatesK16Part001.lean 13236 declarations
CertificatesK16Part002.lean 13552 declarations
CertificatesK16Part003.lean 14427 declarations
CertificatesK16Part004.lean 14020 declarations
CertificatesK16Part005.lean 14907 declarations
CertificatesK16Part006.lean 15322 declarations
CertificatesK16Part007.lean 5210 declarations
CertificatesK17.lean 14 imports, no declarations
CertificatesK17Part000.lean 11780 declarations
CertificatesK17Part001.lean 18037 declarations
CertificatesK17Part002.lean 13955 declarations
CertificatesK17Part003.lean 14100 declarations
CertificatesK17Part004.lean 13942 declarations
CertificatesK17Part005.lean 15171 declarations
CertificatesK17Part006.lean 14803 declarations
CertificatesK17Part007.lean 15040 declarations
CertificatesK17Part008.lean 16338 declarations
CertificatesK17Part009.lean 17309 declarations
CertificatesK17Part010.lean 15300 declarations
CertificatesK17Part011.lean 17364 declarations
CertificatesK17Part012.lean 17997 declarations
CertificatesK17Part013.lean 14256 declarations
CertificatesK5.lean 303 declarations
CertificatesK6.lean 815 declarations
CertificatesK7.lean 2179 declarations
CertificatesK8.lean 4039 declarations
CertificatesK9.lean 11783 declarations
CertifiedRamseyReduction.lean 4 declarations
ChainCounts.lean 15 declarations
CliqueThree.lean 2 declarations
CliqueTraversal.lean 5 declarations
ClosedIndexed.lean 3 declarations
ClosureCertificates.lean 8 declarations
ClosureSteps.lean 13 declarations
ColouredPath.lean 2 declarations
ColouredPathFull.lean 5 declarations
ColouredPathStart.lean 4 declarations
ComponentVertices.lean 7 declarations
ConditionalMain.lean 5 declarations
ConnectedLongPath.lean 3 declarations
CoverageK10.lean 249 declarations
CoverageK11.lean 424 declarations
CoverageK12.lean 527 declarations
CoverageK13.lean 905 declarations
CoverageK14.lean 993 declarations
CoverageK15.lean 1709 declarations
CoverageK16.lean 1404 declarations
CoverageK17.lean 2395 declarations
CoverageK5.lean 26 declarations
CoverageK6.lean 47 declarations
CoverageK7.lean 81 declarations
CoverageK8.lean 115 declarations
CoverageK9.lean 190 declarations
CycleTwoPaths.lean 4 declarations
Definitions.lean 9 declarations
DeletedComponent.lean 4 declarations
DeletionOrder.lean 2 declarations
DenseLayers.lean 2 declarations
DenseSubgraph.lean 5 declarations
DistanceLayers.lean 11 declarations
EndpointAllowedAttachment.lean 3 declarations
EndpointAttachment.lean 6 declarations
EndpointDegreeCover.lean 2 declarations
EndpointFullAttachment.lean 3 declarations
EndpointStructure.lean 1 declarations
EndpointTail.lean 5 declarations
ExteriorCounts.lean 3 declarations
FastCertificateMatrix.lean 13 declarations
FastLayoutGraph.lean 4 declarations
FastMatrixRows.lean 4 declarations
FiniteAttachments.lean 10 declarations
FiniteBad.lean 4 declarations
FiniteBallBounds.lean 7 declarations
FiniteConstraints.lean 7 declarations
FiniteLayout.lean 4 declarations
FinitePacking.lean 4 declarations
FiniteRangeReduction.lean 1 declarations
FiniteTemplates.lean 19 declarations
FiveCycleDisjointStructure.lean 1 declarations
FiveCycleExteriorSix.lean 1 declarations
FiveCycleFourClique.lean 2 declarations
FiveCycleGeometry.lean 8 declarations
FiveCycleNoOverlap.lean 1 declarations
FiveCycleOverlapStructure.lean 1 declarations
FiveCycleTriangleCounts.lean 3 declarations
FiveCycleTriangleOverlap.lean 3 declarations
FourCycleClassCounts.lean 3 declarations
FourCycleCounts.lean 3 declarations
FourCycleResidual.lean 1 declarations
FullLargeClique.lean 2 declarations
GlobalLongest.lean 4 declarations
GraphCopies.lean 4 declarations
IndependentPacking.lean 7 declarations
InteriorChainSelection.lean 12 declarations
InteriorDetour.lean 1 declarations
InteriorOrientations.lean 4 declarations
InteriorRepresentativeGrowth.lean 2 declarations
InteriorSelectionPacking.lean 5 declarations
InteriorSystemSelection.lean 7 declarations
LargeClique.lean 6 declarations
LargeCycleRamsey.lean 3 declarations
LayerArithmetic.lean 2 declarations
LayerMinimal.lean 5 declarations
LayerSelection.lean 5 declarations
LayerStructure.lean 10 declarations
LayerSums.lean 14 declarations
LayoutCertificate.lean 8 declarations
LayoutRefutation.lean 1 declarations
ListSurgery.lean 7 declarations
LongestPaths.lean 5 declarations
LowerBound.lean 7 declarations
Main.lean 2 declarations
MissingCoverage.lean 1 declarations
Monotonicity.lean 3 declarations
NormalizeChains.lean 4 declarations
NormalizedIncident.lean 10 declarations
NormalizedRepresentatives.lean 3 declarations
OptimalPathSystem.lean 5 declarations
OptimalRepresentatives.lean 7 declarations
OrientedSingleton.lean 2 declarations
OrientedTerminalWeights.lean 2 declarations
OutsideChainTemplate.lean 1 declarations
OutsidePathRules.lean 12 declarations
OutsideTemplate.lean 6 declarations
PackingCertificate.lean 3 declarations
PackingOptions.lean 5 declarations
PathDetour.lean 4 declarations
PathEndpoints.lean 9 declarations
PathJoining.lean 2 declarations
PathProfiles.lean 6 declarations
PathRotation.lean 7 declarations
PathSystem.lean 12 declarations
PathSystemCounts.lean 5 declarations
PatternCounts.lean 42 declarations
Patterns.lean 20 declarations
ProfileMasks.lean 8 declarations
PublishedInputs.lean 1 declarations
RamseyFromFiniteCoverage.lean 5 declarations
RamseyMainReduction.lean 2 declarations
RamseyReduction.lean 9 declarations
RawCanonical.lean 9 declarations
RawCliqueCompletion.lean 4 declarations
RawEmbedding.lean 7 declarations
RawOrientations.lean 9 declarations
RawPathSystem.lean 11 declarations
RawPermutation.lean 6 declarations
RawReplacement.lean 3 declarations
RawReplacementProfiles.lean 5 declarations
RawRestrict.lean 1 declarations
RawReverse.lean 8 declarations
Reduction.lean 8 declarations
ReplacementOptimality.lean 3 declarations
ReplacementProfiles.lean 4 declarations
RepresentativeBallGrowth.lean 4 declarations
RepresentativeCuts.lean 5 declarations
RepresentativeExclusion.lean 2 declarations
RepresentativeExtraNeighbor.lean 2 declarations
RepresentativeOutside.lean 5 declarations
RepresentativePacking.lean 1 declarations
RepresentativeSuccessor.lean 2 declarations
Representatives.lean 12 declarations
RequiredCertificates.lean 9 declarations
ResidualPaths.lean 3 declarations
RestrictedLongest.lean 3 declarations
SameChainReplacement.lean 2 declarations
SevenEightCycleRamsey.lean 4 declarations
ShortRepresentativePath.lean 1 declarations
Shortening.lean 12 declarations
SingleAttachment.lean 3 declarations
SixCycleRamsey.lean 2 declarations
Size.lean 8 declarations
SmallCycleGeometry.lean 8 declarations
SmallCycleRamsey.lean 4 declarations
SmallFiveCycle.lean 1 declarations
SmallFourCycle.lean 1 declarations
SmallIndependent.lean 2 declarations
SmallPacking.lean 2 declarations
StartingIncident.lean 2 declarations
TemplateEmbedding.lean 5 declarations
TemplateMatrix.lean 3 declarations
TerminalArithmetic.lean 2 declarations
TerminalClassification.lean 4 declarations
TerminalContradiction.lean 1 declarations
TerminalEndpointGeometry.lean 3 declarations
TerminalIncrement.lean 2 declarations
TerminalIncrementProfiles.lean 1 declarations
TerminalPacking.lean 4 declarations
TerminalPackingCases.lean 2 declarations
TerminalPathClassification.lean 1 declarations
TerminalProfileMinimum.lean 4 declarations
TerminalRepresentative.lean 3 declarations
TerminalRepresentativeSets.lean 9 declarations
TerminalRepresentatives.lean 4 declarations
TerminalWeights.lean 4 declarations
Triangle.lean 1 declarations
TriangleFacts.lean 8 declarations
TriangleLabels.lean 2 declarations
WalkCycle.lean 2 declarations