First-party checked source

Source for Strong Papadimitriou–Ratajczak Conjecture

This pinned Lean source formalizes the following mathematical result: A paper and pinned Lean package give a proof candidate that every finite simple 3-connected plane graph has a convex greedy straight-line drawing preserving its prescribed embedding and outer face. Download the complete checked closure, open the endpoint, or browse its supporting modules to study the proof or develop an extension.

Read the theorem overview Complete checked Lean source · 499 Lean files · 1 evidence record · Download ZIP Open MainConjecture.lean

Immutable source commit: 2469f1b840e839355c948371bf614f5155349270

License and notice commit: 7d5a6e6c949fcf1f460db2e128b90ba8bc082bed

Each ZIP contains the checked first-party local Lean import closure, exact statements and boundaries, license, notice, evidence, a source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled; this is not a portable whole-repository release.

Proof and source

What is checked—and how much source supports it

Browse the counted source

Declarations covered by evidence: 1
First-party Lean files: 499
Lean source lines: 35,941
Main recorded file: 91 lines

How the source is counted

Line counts exclude blank lines; comments and documentation count. The total is the deduplicated, commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded. Declaration count means names covered by the artifact's recorded evidence, not every declaration in the source. Source footprint is not a difficulty or proof-quality score.

Exact theorem evidence

Strong Papadimitriou–Ratajczak Conjecture

StrongPR.strong_pr_conjecture

This is the hash-matched main Lean file. Its complete tracked local Lean import closure is browsable once below; checker evidence remains separate for this exact theorem.

Commit: 2469f1b840e839355c948371bf614f5155349270
Main Lean file: StrongPR/MainConjecture.lean
Main-file footprint: 91 lines
File SHA-256: sha256:c98946232141cae7f420dc3076b7c20b65e0925ae174aed35dc00963e5f2da2a
Complete Lean closure: 499 files · 35,941 lines
Toolchain: leanprover/lean4:v4.32.2

Open main Lean file Download main Lean file Download checker evidence (JSON)Download Apache-2.0 license Download Lech Mazur notice

Deduplicated checked source

Complete Lean import closure

This closure supports the theorem evidence record above.

Complete checked Lean closure

499 Lean files are available here

Start with the principal theorem and proof-architecture files below, or search the complete commit-pinned closure.

499Lean files

Search and browse all 499 checked Lean files

Every listed file is read from the same pinned Git commit. File links open raw source in a new tab; use the ZIP download for the complete package. External Mathlib modules are dependency-locked but are not copied into this first-party source tree.

Filter all 499 Lean files

Showing all 499 files

StrongPR499 files · 35,941 lines

StrongPR/MainConjecture.lean91 lines
StrongPR/AbsorbingMapPatch.lean91 lines
StrongPR/AffineActiveNeighborhood.lean50 lines
StrongPR/AffineBodyExterior.lean81 lines
StrongPR/AffineBodyRegions.lean70 lines
StrongPR/AffineEdgeContact.lean47 lines
StrongPR/AffineInwardDirection.lean56 lines
StrongPR/AffineSegmentZeros.lean43 lines
StrongPR/AlgebraicPlacement.lean101 lines
StrongPR/AmbientJoin.lean120 lines
StrongPR/AmbientJoinAssembly.lean97 lines
StrongPR/AmbientJoinChild.lean196 lines
StrongPR/AmbientPath.lean143 lines
StrongPR/AmbientPorts.lean91 lines
StrongPR/AmbientSeries.lean199 lines
StrongPR/AmbientTraceAssembly.lean102 lines
StrongPR/AmbientWalkTransport.lean29 lines
StrongPR/AugmentedBridge.lean161 lines
StrongPR/BarrierDirichlet.lean88 lines
StrongPR/BondySetMenger.lean703 lines
StrongPR/BondySetMengerContraction.lean934 lines
StrongPR/BorderedForestPartition.lean64 lines
StrongPR/BorderedSuccessorKernel.lean43 lines
StrongPR/BoundaryReplacementDet.lean63 lines
StrongPR/BridgeGraph.lean161 lines
StrongPR/CanonicalRootBlock.lean120 lines
StrongPR/CapJordanRegion.lean37 lines
StrongPR/ChildClassLabels.lean39 lines
StrongPR/ChildClosedFrontierEdges.lean47 lines
StrongPR/ChildFaceClasses.lean71 lines
StrongPR/ChildFrontierEdges.lean87 lines
StrongPR/ChildFrontierVertices.lean55 lines
StrongPR/ChildOrbitFrontier.lean77 lines
StrongPR/ChildOrbitRegions.lean44 lines
StrongPR/ChildOriginalDarts.lean56 lines
StrongPR/ChildOriginalEulerBound.lean62 lines
StrongPR/ChildRotationNoReverse.lean26 lines
StrongPR/ChildSimpleCycleModel.lean59 lines
StrongPR/ChildSimpleCycles.lean58 lines
StrongPR/ChildVertexRotation.lean59 lines
StrongPR/CircleCollarArc.lean65 lines
StrongPR/CircleCollarPair.lean58 lines
StrongPR/CircleJordanTransport.lean48 lines
StrongPR/CirclePrefixWindow.lean96 lines
StrongPR/ClockwiseExteriorAngle.lean44 lines
StrongPR/ClockwiseRayAngle.lean50 lines
StrongPR/ClockwiseRayInjectivity.lean43 lines
StrongPR/ClosedBodyComponent.lean26 lines
StrongPR/ClosedComponentPaths.lean77 lines
StrongPR/ClosedCrosscutCarrier.lean89 lines
StrongPR/ClosedCrosscutSeparation.lean59 lines
StrongPR/ClosingEdgeIndices.lean45 lines
StrongPR/ClosureCoverBounds.lean25 lines
StrongPR/ClosureCoverRegions.lean78 lines
StrongPR/CompactCommonFibers.lean35 lines
StrongPR/CompactJordanBody.lean43 lines
StrongPR/ComplexMapLift.lean71 lines
StrongPR/ComplexMapWinding.lean71 lines
StrongPR/ComplexPathIncrement.lean48 lines
StrongPR/ComplexPathWinding.lean30 lines
StrongPR/ComplexSegmentLog.lean73 lines
StrongPR/ComponentBridgeSuffix.lean168 lines
StrongPR/ComponentPartition.lean55 lines
StrongPR/ComponentPathVisits.lean40 lines
StrongPR/ConnectedChildOrbitClasses.lean52 lines
StrongPR/ConnectedChildOrbitRegions.lean69 lines
StrongPR/ConnectedDartLabels.lean36 lines
StrongPR/ConnectedMapEuler.lean49 lines
StrongPR/Connectivity.lean164 lines
StrongPR/ContinuousCrosscut.lean93 lines
StrongPR/ContinuousCrosscutRegions.lean159 lines
StrongPR/ContinuousLog.lean53 lines
StrongPR/ContinuousWinding.lean79 lines
StrongPR/ContinuousWindingHomotopy.lean53 lines
StrongPR/ContinuousWindingOrientation.lean49 lines
StrongPR/ConvexFrontierRay.lean34 lines
StrongPR/ConvexLocalBoundary.lean41 lines
StrongPR/ConvexSimpleWinding.lean62 lines
StrongPR/ConvexWindingOutside.lean38 lines
StrongPR/CoordinateKernelRestriction.lean71 lines
StrongPR/CornerEulerSaturation.lean84 lines
StrongPR/CorrelatedForestMinors.lean57 lines
StrongPR/CutVisibility.lean25 lines
StrongPR/CutVisibilityConnectivity.lean47 lines
StrongPR/CutVisibleCardinality.lean26 lines
StrongPR/CycleActiveNeighborhood.lean54 lines
StrongPR/CycleHeightIncrease.lean94 lines
StrongPR/CycleNonbacktracking.lean64 lines
StrongPR/CycleOppositePaths.lean35 lines
StrongPR/CycleRootHeightPaths.lean54 lines
StrongPR/CycleRootPaths.lean68 lines
StrongPR/CycleSupportedIncidence.lean94 lines
StrongPR/CycleSupportedRegion.lean93 lines
StrongPR/CyclicHeightOrder.lean56 lines
StrongPR/DartWindingCancellation.lean61 lines
StrongPR/DeletedEdgePaths.lean51 lines
StrongPR/DeletedIncidenceRank.lean62 lines
StrongPR/DenseCountTiling.lean79 lines
StrongPR/DisjointPathForest.lean92 lines
StrongPR/EarEndpointCycles.lean118 lines
StrongPR/EarExtension.lean86 lines
StrongPR/EarInteriorCycles.lean62 lines
StrongPR/EarVertexFibers.lean62 lines
StrongPR/EdgeInsertionConnectivity.lean36 lines
StrongPR/EdgeRotationDeletion.lean77 lines
StrongPR/EuclideanProgress.lean166 lines
StrongPR/ExponentialCapBoundary.lean59 lines
StrongPR/ExponentialCapContact.lean18 lines
StrongPR/ExponentialCapFrontierContact.lean30 lines
StrongPR/ExponentialCapSides.lean33 lines
StrongPR/ExponentialRectangle.lean45 lines
StrongPR/ExteriorCrosscut.lean57 lines
StrongPR/FaceRegionGluing.lean70 lines
StrongPR/FamilyEarSuccessors.lean70 lines
StrongPR/FamilyEarVertexActions.lean90 lines
StrongPR/FiniteAffineBody.lean73 lines
StrongPR/FiniteClosedAvoidance.lean38 lines
StrongPR/FiniteClosedCover.lean55 lines
StrongPR/FiniteClosedGluing.lean53 lines
StrongPR/FiniteInvariantCore.lean51 lines
StrongPR/FiniteLinearPreimage.lean29 lines
StrongPR/FiniteMergeCardinality.lean37 lines
StrongPR/FiniteOrbitLabels.lean29 lines
StrongPR/FiniteReturnInvariants.lean37 lines
StrongPR/FiniteReturnPermutation.lean61 lines
StrongPR/FirstBoundaryCrosscut.lean54 lines
StrongPR/FirstExit.lean63 lines
StrongPR/FirstReturnCycles.lean66 lines
StrongPR/ForestAreaPositivity.lean56 lines
StrongPR/ForestMinorExpansion.lean56 lines
StrongPR/ForestOriginalPaths.lean81 lines
StrongPR/ForestPlaneArea.lean62 lines
StrongPR/ForestRoot.lean32 lines
StrongPR/ForestRotationCycles.lean77 lines
StrongPR/ForestWeightPaths.lean41 lines
StrongPR/GraphReachTransport.lean25 lines
StrongPR/GreedyHeight.lean125 lines
StrongPR/HarmonicForestEvaluation.lean67 lines
StrongPR/HarmonicForestRatio.lean75 lines
StrongPR/HeightCover.lean153 lines
StrongPR/HeightTrace.lean101 lines
StrongPR/HomeomorphicCircleCaps.lean83 lines
StrongPR/HomeomorphSubsetRestriction.lean39 lines
StrongPR/JordanCircleCaps.lean66 lines
StrongPR/JordanWinding.lean53 lines
StrongPR/LinearProgress.lean104 lines
StrongPR/LocalCompactBody.lean40 lines
StrongPR/LocalIntegerRows.lean141 lines
StrongPR/LocalIntegerSystem.lean136 lines
StrongPR/LocalRowCertificate.lean69 lines
StrongPR/LocalRowForest.lean58 lines
StrongPR/LocalRowPlacement.lean100 lines
StrongPR/MaskedDirichlet.lean120 lines
StrongPR/MaskedForestRows.lean52 lines
StrongPR/MaskedMatrix.lean58 lines
StrongPR/MatchedJordanExtension.lean29 lines
StrongPR/MengerCarrier.lean96 lines
StrongPR/MengerFirstBoundary.lean86 lines
StrongPR/MengerThreePaths.lean43 lines
StrongPR/NativeActiveEuler.lean77 lines
StrongPR/NativeActiveFillings.lean72 lines
StrongPR/NativeAmbientPositiveSign.lean56 lines
StrongPR/NativeAnchoredRuns.lean95 lines
StrongPR/NativeBoundaryInheritance.lean31 lines
StrongPR/NativeChildBoundaryDarts.lean102 lines
StrongPR/NativeChildCarrier.lean59 lines
StrongPR/NativeChildCycleWinding.lean65 lines
StrongPR/NativeChildOuterSign.lean89 lines
StrongPR/NativeChildPathBoundary.lean163 lines
StrongPR/NativeChildWinding.lean99 lines
StrongPR/NativeClassAtFace.lean64 lines
StrongPR/NativeClassCancellation.lean105 lines
StrongPR/NativeClassWalkFrontier.lean57 lines
StrongPR/NativeClosureIntersections.lean57 lines
StrongPR/NativeConnectedChildCount.lean22 lines
StrongPR/NativeCornerEuler.lean103 lines
StrongPR/NativeCycleAlignment.lean178 lines
StrongPR/NativeCycleFrontierVertices.lean40 lines
StrongPR/NativeDeletedDual.lean55 lines
StrongPR/NativeDeletionEuler.lean48 lines
StrongPR/NativeDualSplit.lean83 lines
StrongPR/NativeEarSuccessors.lean53 lines
StrongPR/NativeEdgeSegment.lean82 lines
StrongPR/NativeFaceBoundaryKernel.lean53 lines
StrongPR/NativeFaceBoundaryMap.lean64 lines
StrongPR/NativeFaceClosureIncidence.lean90 lines
StrongPR/NativeFaceCounts.lean68 lines
StrongPR/NativeFaceCycleCount.lean85 lines
StrongPR/NativeFaceCycleEuler.lean50 lines
StrongPR/NativeFaceDual.lean65 lines
StrongPR/NativeFaceFamily.lean117 lines
StrongPR/NativeFaceFamilyEar.lean169 lines
StrongPR/NativeFaceFamilyExistence.lean30 lines
StrongPR/NativeFaceFamilyUpdate.lean97 lines
StrongPR/NativeFaceHeightPaths.lean67 lines
StrongPR/NativeFaceIncidence.lean53 lines
StrongPR/NativeFaceOrbits.lean51 lines
StrongPR/NativeFaceOrientation.lean99 lines
StrongPR/NativeFacePermutation.lean69 lines
StrongPR/NativeFaceRegionHomeomorph.lean46 lines
StrongPR/NativeFaceReversal.lean60 lines
StrongPR/NativeFaceWinding.lean106 lines
StrongPR/NativeForestFacialSigns.lean80 lines
StrongPR/NativeGlobalAmbientSign.lean49 lines
StrongPR/NativeInternalContact.lean63 lines
StrongPR/NativeLeafRootEdge.lean79 lines
StrongPR/NativeMissingRootTrace.lean127 lines
StrongPR/NativeOmittedFaceGraph.lean44 lines
StrongPR/NativeOpenEdgeContact.lean56 lines
StrongPR/NativeOppositeChildRequests.lean72 lines
StrongPR/NativeOuterContact.lean60 lines
StrongPR/NativeOuterCycleCanonicality.lean119 lines
StrongPR/NativeOwnBoundaryWinding.lean74 lines
StrongPR/NativeParentOuterRequests.lean77 lines
StrongPR/NativePathFibers.lean60 lines
StrongPR/NativePositiveChildBoundary.lean60 lines
StrongPR/NativePositiveOrientation.lean48 lines
StrongPR/NativeResidualBridge.lean114 lines
StrongPR/NativeReversedRotation.lean60 lines
StrongPR/NativeRootedFrontier.lean53 lines
StrongPR/NativeRootedRequests.lean59 lines
StrongPR/NativeSignedFaceRequests.lean56 lines
StrongPR/NativeSignedRootVertex.lean67 lines
StrongPR/NativeSupportedAmbientHomeomorph.lean97 lines
StrongPR/NativeSupportedClockwise.lean68 lines
StrongPR/NativeSupportedTiling.lean60 lines
StrongPR/NativeTargetExterior.lean57 lines
StrongPR/NativeTargetMultiplicity.lean40 lines
StrongPR/NativeTargetRegions.lean50 lines
StrongPR/NativeTargetTraceCover.lean76 lines
StrongPR/NativeTargetWinding.lean29 lines
StrongPR/NativeVertexCycleBase.lean46 lines
StrongPR/NativeVertexFibers.lean41 lines
StrongPR/NativeVertexSegment.lean52 lines
StrongPR/OmittedClassSupport.lean31 lines
StrongPR/OmittedFaceCoefficients.lean59 lines
StrongPR/OmittedFaceRuns.lean68 lines
StrongPR/OmittedFaceTransport.lean27 lines
StrongPR/OmittedVertexStar.lean79 lines
StrongPR/OppositeIntervalArcs.lean40 lines
StrongPR/OriginalActiveAdjacency.lean34 lines
StrongPR/OriginalBetaVisibility.lean93 lines
StrongPR/OriginalBetaVisibilityConverse.lean81 lines
StrongPR/OriginalBlockChain.lean174 lines
StrongPR/OriginalBlockPaths.lean54 lines
StrongPR/OriginalBlockPorts.lean57 lines
StrongPR/OriginalBoundaryChain.lean39 lines
StrongPR/OriginalBridgePartition.lean118 lines
StrongPR/OriginalBridgeSuffix.lean55 lines
StrongPR/OriginalChainCertificate.lean71 lines
StrongPR/OriginalChainTrace.lean69 lines
StrongPR/OriginalChildAttachments.lean186 lines
StrongPR/OriginalChildOutside.lean47 lines
StrongPR/OriginalChildRegionExistence.lean35 lines
StrongPR/OriginalChildRegions.lean41 lines
StrongPR/OriginalChildRootEdge.lean81 lines
StrongPR/OriginalClockwiseAmbientPlacement.lean155 lines
StrongPR/OriginalClockwiseAngle.lean34 lines
StrongPR/OriginalClockwiseCorner.lean67 lines
StrongPR/OriginalClockwiseSuccessor.lean48 lines
StrongPR/OriginalClosedSide.lean90 lines
StrongPR/OriginalClosedTiling.lean76 lines
StrongPR/OriginalConnectivityBridge.lean81 lines
StrongPR/OriginalConvexFacialPlacement.lean55 lines
StrongPR/OriginalCornerCount.lean44 lines
StrongPR/OriginalCornerLowerBounds.lean52 lines
StrongPR/OriginalCrosscutFaceSide.lean80 lines
StrongPR/OriginalCrosscutLabels.lean93 lines
StrongPR/OriginalCrosscutWinding.lean61 lines
StrongPR/OriginalCycleAmbientExtension.lean40 lines
StrongPR/OriginalCycleBridge.lean43 lines
StrongPR/OriginalCycleDarts.lean77 lines
StrongPR/OriginalCycleImages.lean91 lines
StrongPR/OriginalCycleJordan.lean59 lines
StrongPR/OriginalCycleOrientation.lean62 lines
StrongPR/OriginalCycleOwnWinding.lean81 lines
StrongPR/OriginalDartCurves.lean93 lines
StrongPR/OriginalDartPaths.lean64 lines
StrongPR/OriginalDartPermutations.lean71 lines
StrongPR/OriginalDartSum.lean39 lines
StrongPR/OriginalDrawing.lean85 lines
StrongPR/OriginalDrawingBridge.lean71 lines
StrongPR/OriginalDrawingFibers.lean61 lines
StrongPR/OriginalDrawingHomeomorph.lean92 lines
StrongPR/OriginalDrawingRestriction.lean64 lines
StrongPR/OriginalDualConnected.lean115 lines
StrongPR/OriginalEarCounts.lean89 lines
StrongPR/OriginalEarCycles.lean56 lines
StrongPR/OriginalEarFace.lean57 lines
StrongPR/OriginalEarFaceSplit.lean108 lines
StrongPR/OriginalEarInduction.lean62 lines
StrongPR/OriginalEarInheritance.lean65 lines
StrongPR/OriginalEarRegions.lean96 lines
StrongPR/OriginalEarRotations.lean56 lines
StrongPR/OriginalEarWords.lean86 lines
StrongPR/OriginalEdgeAvoidance.lean48 lines
StrongPR/OriginalEdgeDescent.lean119 lines
StrongPR/OriginalEdgeGradient.lean67 lines
StrongPR/OriginalEdgeImages.lean87 lines
StrongPR/OriginalEdgeOrientation.lean19 lines
StrongPR/OriginalEdgePartitionCount.lean54 lines
StrongPR/OriginalEdgeRootOrder.lean55 lines
StrongPR/OriginalEuler.lean60 lines
StrongPR/OriginalFaceBridge.lean59 lines
StrongPR/OriginalFaceRegionHomeomorph.lean52 lines
StrongPR/OriginalFacialChord.lean130 lines
StrongPR/OriginalFacialMultiplicity.lean69 lines
StrongPR/OriginalFirstBoundaryOrder.lean103 lines
StrongPR/OriginalFirstExitStar.lean77 lines
StrongPR/OriginalFrontierInheritance.lean24 lines
StrongPR/OriginalGraphImages.lean74 lines
StrongPR/OriginalGraphModel.lean87 lines
StrongPR/OriginalGraphRestrictions.lean66 lines
StrongPR/OriginalIncidenceRank.lean45 lines
StrongPR/OriginalLastBridge.lean67 lines
StrongPR/OriginalLeafVisibility.lean33 lines
StrongPR/OriginalLinkedEdgeOrder.lean74 lines
StrongPR/OriginalLiteralHeightTrace.lean85 lines
StrongPR/OriginalMissingEdgeData.lean81 lines
StrongPR/OriginalOuterClockwise.lean65 lines
StrongPR/OriginalOuterCrosscut.lean77 lines
StrongPR/OriginalOuterFace.lean47 lines
StrongPR/OriginalPositiveForest.lean69 lines
StrongPR/OriginalPositiveOuter.lean102 lines
StrongPR/OriginalProtectedBeta.lean68 lines
StrongPR/OriginalRemovedFrontier.lean54 lines
StrongPR/OriginalRootBlockPorts.lean90 lines
StrongPR/OriginalSegmentIncidence.lean106 lines
StrongPR/OriginalSharedDart.lean54 lines
StrongPR/OriginalSharedEdge.lean103 lines
StrongPR/OriginalSharedFaceSide.lean87 lines
StrongPR/OriginalStraightAngles.lean32 lines
StrongPR/OriginalStraightArc.lean47 lines
StrongPR/OriginalStraightCorner.lean65 lines
StrongPR/OriginalStraightDirections.lean46 lines
StrongPR/OriginalStraightDrawing.lean61 lines
StrongPR/OriginalStraightPaths.lean34 lines
StrongPR/OriginalStrictFacialPlacement.lean85 lines
StrongPR/OriginalStrongBridges.lean49 lines
StrongPR/OriginalStrongCircuitCuts.lean65 lines
StrongPR/OriginalSubgraphRecovery.lean93 lines
StrongPR/OriginalSubgraphTransport.lean112 lines
StrongPR/OriginalTargetRegions.lean83 lines
StrongPR/OriginalTauBlock.lean55 lines
StrongPR/OriginalThirdPath.lean94 lines
StrongPR/OriginalThreeConnectedHeight.lean64 lines
StrongPR/OriginalTrivialBridge.lean71 lines
StrongPR/OriginalUniversalEdgeOrder.lean42 lines
StrongPR/OriginalUniversalHeight.lean124 lines
StrongPR/OriginalUnpausedWalk.lean92 lines
StrongPR/OriginalVertexCycles.lean81 lines
StrongPR/OriginalWalkBoundaryHomeomorph.lean43 lines
StrongPR/OriginalWalkBridge.lean145 lines
StrongPR/OriginalWalkContacts.lean57 lines
StrongPR/OriginalWalkHomeomorph.lean33 lines
StrongPR/OriginalWalkImages.lean68 lines
StrongPR/OriginalWalkSimplicity.lean94 lines
StrongPR/OriginalWalkWinding.lean67 lines
StrongPR/OuterComponent.lean71 lines
StrongPR/ParabolicBodyBounds.lean93 lines
StrongPR/ParabolicChain.lean70 lines
StrongPR/ParabolicChord.lean63 lines
StrongPR/ParabolicCyclicRoots.lean39 lines
StrongPR/ParabolicEnvelope.lean88 lines
StrongPR/ParabolicFacets.lean91 lines
StrongPR/ParabolicFeasibility.lean85 lines
StrongPR/ParabolicFrontier.lean66 lines
StrongPR/ParabolicIncidence.lean75 lines
StrongPR/ParabolicLoop.lean73 lines
StrongPR/ParabolicSegments.lean66 lines
StrongPR/PatchConnectivity.lean48 lines
StrongPR/PathConnectivity.lean81 lines
StrongPR/PathEndpointCut.lean48 lines
StrongPR/PathInitialSegment.lean53 lines
StrongPR/PathRootEdge.lean18 lines
StrongPR/PathSimplicity.lean67 lines
StrongPR/PathSuccessor.lean55 lines
StrongPR/PathTailSeparation.lean41 lines
StrongPR/PermutationCycleDeletion.lean90 lines
StrongPR/PermutationCycleTransport.lean34 lines
StrongPR/PermutationDeletion.lean57 lines
StrongPR/PermutationFirstReturn.lean91 lines
StrongPR/PermutationPairDeletion.lean56 lines
StrongPR/PermutationSignCount.lean59 lines
StrongPR/PermutationSignFibers.lean31 lines
StrongPR/PermutationSingleDrop.lean35 lines
StrongPR/PermutationSwapClasses.lean65 lines
StrongPR/PermutationSwapCount.lean28 lines
StrongPR/PermutationSwapMerge.lean55 lines
StrongPR/PermutationSwapSplit.lean73 lines
StrongPR/PlaneCircleParam.lean62 lines
StrongPR/PlaneCircleRegions.lean35 lines
StrongPR/PlaneCircleWinding.lean48 lines
StrongPR/PlaneComplex.lean50 lines
StrongPR/PlaneExponentialCollar.lean33 lines
StrongPR/PlaneHomeomorphWinding.lean52 lines
StrongPR/PlaneOrientationSign.lean46 lines
StrongPR/PlanePathIncrement.lean41 lines
StrongPR/PlanePathWinding.lean80 lines
StrongPR/PlaneRegionTransport.lean55 lines
StrongPR/PlaneSegmentInterior.lean44 lines
StrongPR/PlaneSegmentLog.lean42 lines
StrongPR/PlaneSlackBounds.lean69 lines
StrongPR/PlaneSphereComponents.lean50 lines
StrongPR/PlaneSupportedFacets.lean62 lines
StrongPR/PlaneTurn.lean78 lines
StrongPR/PlaneTurnAffine.lean77 lines
StrongPR/PlaneWinding.lean44 lines
StrongPR/PlaneWindingLocal.lean39 lines
StrongPR/PlaneWindingOutside.lean43 lines
StrongPR/PortRows.lean171 lines
StrongPR/PositiveAmbientCalibration.lean19 lines
StrongPR/PositiveGraphLoop.lean56 lines
StrongPR/PositiveGraphLoopImage.lean47 lines
StrongPR/PositiveTestVector.lean66 lines
StrongPR/PositiveWalkWinding.lean64 lines
StrongPR/PrincipalIdentityDet.lean48 lines
StrongPR/QuadraticTest.lean67 lines
StrongPR/RankedMaximum.lean112 lines
StrongPR/RealParabolicInterior.lean81 lines
StrongPR/RealParabolicLoop.lean63 lines
StrongPR/RegularCellComponents.lean37 lines
StrongPR/RegularCellTrace.lean68 lines
StrongPR/RegularLocalContact.lean21 lines
StrongPR/ResidualBridgeChain.lean18 lines
StrongPR/RestoredEdgePrefixes.lean44 lines
StrongPR/RetainedFacePermutation.lean54 lines
StrongPR/RetainedVertexClasses.lean67 lines
StrongPR/RetainedVertexRotation.lean58 lines
StrongPR/RootBlock.lean106 lines
StrongPR/RootBlockAttachments.lean107 lines
StrongPR/RootBoundaryRotation.lean26 lines
StrongPR/RootBoundarySupport.lean49 lines
StrongPR/RootBridgeComponents.lean95 lines
StrongPR/RootedBlockLeaves.lean81 lines
StrongPR/RootedBorderEvaluation.lean81 lines
StrongPR/RootedForestPartition.lean80 lines
StrongPR/RootEdgeConnectivity.lean85 lines
StrongPR/RootEdgeCuts.lean58 lines
StrongPR/RootedLeafClosure.lean65 lines
StrongPR/RootedLeafPaths.lean83 lines
StrongPR/RootedSuccessorMatrix.lean87 lines
StrongPR/RootGuardedRuns.lean51 lines
StrongPR/RotationDeletionEuler.lean51 lines
StrongPR/RotationFaceBoundary.lean63 lines
StrongPR/RotationFaceFillings.lean86 lines
StrongPR/RotationNonbacktracking.lean18 lines
StrongPR/RowNormalization.lean55 lines
StrongPR/SameFamilyDual.lean81 lines
StrongPR/SelectedBoundaryRows.lean51 lines
StrongPR/SelectedEdgeCycleBound.lean36 lines
StrongPR/SelectedEdgeReversal.lean54 lines
StrongPR/SeriesChain.lean153 lines
StrongPR/SeriesHeight.lean135 lines
StrongPR/SeriesPaths.lean88 lines
StrongPR/SeriesRequestCoverage.lean55 lines
StrongPR/SharedArcJumps.lean74 lines
StrongPR/SharedArcWinding.lean40 lines
StrongPR/SharpJoin.lean274 lines
StrongPR/SharpJoinAssembly.lean252 lines
StrongPR/SmallCircleCollar.lean31 lines
StrongPR/SmallCirclePairCaps.lean53 lines
StrongPR/SmallPathPrefixes.lean41 lines
StrongPR/StraightTargetTrace.lean73 lines
StrongPR/StraightTargetWinding.lean80 lines
StrongPR/StraightTraceDensity.lean39 lines
StrongPR/StraightWindingReversal.lean40 lines
StrongPR/StrictConvexCycleInterface.lean24 lines
StrongPR/StrictRowComparison.lean53 lines
StrongPR/SuccessorMatrixKernel.lean64 lines
StrongPR/SupportedCarrierEuler.lean33 lines
StrongPR/SupportedComponentCount.lean74 lines
StrongPR/SupportedCycleJordanRegions.lean47 lines
StrongPR/SupportedCyclePolygon.lean29 lines
StrongPR/SupportedCycleWinding.lean76 lines
StrongPR/SupportedInduceDarts.lean36 lines
StrongPR/SupportedInduceRotation.lean60 lines
StrongPR/SupportedPermutationRegion.lean88 lines
StrongPR/SupportedSegments.lean72 lines
StrongPR/SupportedTargetWinding.lean43 lines
StrongPR/SupportedTripleCenter.lean45 lines
StrongPR/SupportedWalkPath.lean133 lines
StrongPR/TerminalCutChildren.lean146 lines
StrongPR/TerminalCutOrder.lean112 lines
StrongPR/TracedConstruction.lean109 lines
StrongPR/TracedParabolicBoundary.lean158 lines
StrongPR/TwoArcStraightening.lean75 lines
StrongPR/TwoTerminalCut.lean98 lines
StrongPR/VertexCycleInsertion.lean50 lines
StrongPR/VertexRotationDeletion.lean63 lines
StrongPR/VertexSuccessorInsertion.lean23 lines
StrongPR/VisibleCycleCuts.lean40 lines
StrongPR/WalkCarrierDeletion.lean57 lines
StrongPR/WalkCyclicHeightOrder.lean41 lines
StrongPR/WalkHeightTrace.lean24 lines
StrongPR/WalkPrefixEquality.lean27 lines
StrongPR/WalkSegmentTrace.lean66 lines
StrongPR/WalkTrace.lean76 lines
StrongPR/WordSpliceSuccessors.lean37 lines

Source hashMatches checked record

Lean buildPassed in recorded evidence

LicenseApache-2.0 · Lech Mazur

Provenance and reproducibility

Exact checked source, with reuse terms

The endpoint and every listed local import come from the exact recorded Git commit, and the endpoint matches the stored source hash byte for byte. The locally authored package material is licensed under Apache-2.0 by Lech Mazur; Mathlib and cited third-party material remain under their own terms. Machine-readable checker evidence is included.