Lean project

The Lean 4 project that proves the formalised statements of the paper. The formalisation page maps each statement to its Lean theorems and says how the project was checked. All declarations live in the namespace CubicPathwidth.

Comments in the sources are those of the development. References to unpublished working notes were removed or replaced by the corresponding statement of the paper. Where a comment names a statement of the paper by its label in backticks, its number in this version of the paper is added. Other statement numbers in comments are those of the research version or of earlier drafts: in particular, Theorems 2, 3 and 4 and Corollary 5 there (and in declaration names such as target4) are Theorems 7.1, 7.2 and 1.3 and Corollary 1.4 of the paper.

The specification files (*Spec.lean, called the approval surface in comments) state the theorems in Lean. The author reviewed and approved each of them before the proofs were written, and the proofs did not change them; approved in comments refers to that review, and the STATUS lines record its date.

Project files

Modules

“Built” says whether lake build builds the module (the roots CubicPathwidth and CubicPathwidthProofs and what they import). The theorems that the paper cites are in the modules with paper statements listed.

Module Built Paper statements
CubicPathwidth yes
CubicPathwidth.Alg.DiffMain no
CubicPathwidth.Alg.Graph yes
CubicPathwidth.Alg.Plan2 yes
CubicPathwidth.Alg.Plan2Deletion yes
CubicPathwidth.Alg.Port yes
CubicPathwidth.Alg.Proofs.A12Top yes
CubicPathwidth.Alg.Proofs.A3T4 yes
CubicPathwidth.Alg.Proofs.B1Bridge yes
CubicPathwidth.Alg.Proofs.B2OfSimpleGraph yes
CubicPathwidth.Alg.Proofs.C1Perm yes
CubicPathwidth.Alg.Proofs.C2PlainLayout yes
CubicPathwidth.Alg.Proofs.C3Connector yes
CubicPathwidth.Alg.Proofs.C4Switched yes
CubicPathwidth.Alg.Proofs.C5ReduceRecord yes
CubicPathwidth.Alg.Proofs.C6PdTw2 yes
CubicPathwidth.Alg.Proofs.C7Undo yes
CubicPathwidth.Alg.Proofs.E14Exported yes
CubicPathwidth.Alg.Proofs.G1WFBasics yes
CubicPathwidth.Alg.Proofs.G2AddEdge yes
CubicPathwidth.Alg.Proofs.G3RemoveNode yes
CubicPathwidth.Alg.Proofs.G4Induced yes
CubicPathwidth.Alg.Proofs.G5Components yes
CubicPathwidth.Alg.Proofs.G6UnionAll yes
CubicPathwidth.Alg.Proofs.G7Concat yes
CubicPathwidth.Alg.Proofs.G8SeparatorGlue yes
CubicPathwidth.Alg.Proofs.T1AppendIsolated yes
CubicPathwidth.Alg.Proofs.T2InitInv yes
CubicPathwidth.Alg.Proofs.T3LoopPreserves yes
CubicPathwidth.Alg.Proofs.Targets yes Theorem 10.1
CubicPathwidth.Alg.Proofs2.A1TopWidth yes
CubicPathwidth.Alg.Proofs2.A2MixedWidth yes
CubicPathwidth.Alg.Proofs2.A3T4Width yes
CubicPathwidth.Alg.Proofs2.AlgoT4Cor5 yes
CubicPathwidth.Alg.Proofs2.AlgoT4Internal yes
CubicPathwidth.Alg.Proofs2.AlgoT4NoFallback yes
CubicPathwidth.Alg.Proofs2.AlgoT4Thm4 yes
CubicPathwidth.Alg.Proofs2.CommitBound yes
CubicPathwidth.Alg.Proofs2.D1KeyStepAt yes
CubicPathwidth.Alg.Proofs2.D4LoopFuel yes
CubicPathwidth.Alg.Proofs2.DeletionBound yes
CubicPathwidth.Alg.Proofs2.K1Theorem1 yes
CubicPathwidth.Alg.Proofs2.K2Theorem2a yes
CubicPathwidth.Alg.Proofs2.K3Mixed yes
CubicPathwidth.Alg.Proofs2.L1PlainBags yes
CubicPathwidth.Alg.Proofs2.L2PlainWidth yes
CubicPathwidth.Alg.Proofs2.L3Connected yes
CubicPathwidth.Alg.Proofs2.L4Connector yes Lemma A.33
CubicPathwidth.Alg.Proofs2.L5SwitchedWidth yes
CubicPathwidth.Alg.Proofs2.N1ConnectorNoFallback yes Lemma A.33
CubicPathwidth.Alg.Proofs2.N2AlgoT1NoFallback yes
CubicPathwidth.Alg.Proofs2.N3MixedNoFallback yes
CubicPathwidth.Alg.Proofs2.OpsRecordFrame yes
CubicPathwidth.Alg.Proofs2.R1ReduceFuel yes
CubicPathwidth.Alg.Proofs2.R2ReduceMaximal yes
CubicPathwidth.Alg.Proofs2.R3Records yes
CubicPathwidth.Alg.Proofs2.R4TorsoSim yes
CubicPathwidth.Alg.Proofs2.R5RecordMono yes
CubicPathwidth.Alg.Proofs2.R6Confluent yes
CubicPathwidth.Alg.Proofs2.R7Balanced yes
CubicPathwidth.Alg.Proofs2.R8Attach yes
CubicPathwidth.Alg.Proofs2.SweepBound yes
CubicPathwidth.Alg.Proofs2.T4LoopInit yes
CubicPathwidth.Alg.Proofs2.T4LoopRun yes
CubicPathwidth.Alg.Proofs2.T4LoopStep yes
CubicPathwidth.Alg.Proofs2.Targets yes Theorem 10.1, Lemma A.28, Lemma A.34
CubicPathwidth.Alg.Proofs2.TorsoBridge yes
CubicPathwidth.Alg.Proofs2.TorsoLocal yes
CubicPathwidth.Alg.Proofs2.U1PdTw2Width yes
CubicPathwidth.Alg.Proofs2.U2PdTw2NoFallback yes
CubicPathwidth.Alg.Proofs2.U3UndoNoFallback yes
CubicPathwidth.Alg.Proofs2.U4UndoWidth yes
CubicPathwidth.Alg.Proofs2.U5ThinWidth yes
CubicPathwidth.Alg.Proofs2.X1Relabel yes
CubicPathwidth.Alg.Proofs2.X2RelabelExists yes
CubicPathwidth.Alg.Proofs2.X3DegreeTransfer yes
CubicPathwidth.Alg.Proofs2.X4LabelTransfer yes
CubicPathwidth.Alg.Spec yes
CubicPathwidth.Alg.Spec2 yes
CubicPathwidth.AsymptoticTransfer yes
CubicPathwidth.BagOperations yes
CubicPathwidth.BalanceRepair yes
CubicPathwidth.BisectionLimit yes
CubicPathwidth.BisectionMoments yes
CubicPathwidth.Bootstrap yes
CubicPathwidth.BoundaryAssembly yes
CubicPathwidth.BoundaryAsymptotics yes
CubicPathwidth.BoundaryInduction yes
CubicPathwidth.C3.All yes Theorem 1.1, Theorem 8.1
CubicPathwidth.C3.Assembly yes
CubicPathwidth.C3.Concentration yes
CubicPathwidth.C3.Connector yes
CubicPathwidth.C3.Constants yes
CubicPathwidth.C3.Defs yes
CubicPathwidth.C3.Disintegration yes
CubicPathwidth.C3.EqMin yes
CubicPathwidth.C3.Families yes
CubicPathwidth.C3.GaussianTools yes
CubicPathwidth.C3.GoodLabels yes
CubicPathwidth.C3.GramLaw yes
CubicPathwidth.C3.Grid yes
CubicPathwidth.C3.IdealBounds yes
CubicPathwidth.C3.IdealStar yes
CubicPathwidth.C3.Intervals yes
CubicPathwidth.C3.Labels yes
CubicPathwidth.C3.MinBound yes
CubicPathwidth.C3.Planar yes
CubicPathwidth.C3.RotBase yes
CubicPathwidth.C3.RotClosed yes
CubicPathwidth.C3.RotForm yes
CubicPathwidth.C3.RotIBP yes
CubicPathwidth.C3.RotMono yes
CubicPathwidth.C3.RotSign yes
CubicPathwidth.C3.Sheppard yes
CubicPathwidth.C3.StarFrontier yes
CubicPathwidth.C3.Switch yes
CubicPathwidth.C3.SwitchedLayout yes
CubicPathwidth.C3.Triangle yes
CubicPathwidth.C3.VertexBounds yes
CubicPathwidth.C3Spec yes
CubicPathwidth.Coefficients yes
CubicPathwidth.Completion yes
CubicPathwidth.CoreCounting yes
CubicPathwidth.CoreLifting yes
CubicPathwidth.CorePieces yes
CubicPathwidth.CorePruning yes
CubicPathwidth.CoreTorso yes
CubicPathwidth.CutConnector yes
CubicPathwidth.CutGluing yes
CubicPathwidth.CutSweep.All yes Theorem 3.1
CubicPathwidth.CutSweep.Assembly yes
CubicPathwidth.CutSweep.Crossing yes
CubicPathwidth.CutSweep.Defs yes
CubicPathwidth.CutSweep.Deterministic yes
CubicPathwidth.CutSweep.Sweep yes
CubicPathwidth.CutSweep.SweepConc yes
CubicPathwidth.CutSweep.SweepGrid yes
CubicPathwidth.CutSweep.SweepMean yes
CubicPathwidth.CutSweepSpec yes
CubicPathwidth.EndpointTransfer yes
CubicPathwidth.ExpectedCut yes
CubicPathwidth.FiniteComponents yes
CubicPathwidth.ForestDecomposition yes
CubicPathwidth.ForestStructure yes
CubicPathwidth.GaussianBisection yes
CubicPathwidth.GaussianEstimates yes
CubicPathwidth.GaussianField yes
CubicPathwidth.GaussianPlanar yes
CubicPathwidth.GaussianSign yes
CubicPathwidth.GraphGaussianCoefficients yes Lemma 5.4
CubicPathwidth.GraphLocality yes
CubicPathwidth.GraphSections yes
CubicPathwidth.PseudotreeDecomposition yes
CubicPathwidth.PwSeq.Assembly yes
CubicPathwidth.PwSeq.Basic yes Definition 9.1
CubicPathwidth.PwSeq.BootComp yes
CubicPathwidth.PwSeq.BootDeletion yes
CubicPathwidth.PwSeq.BootSeq yes
CubicPathwidth.PwSeq.Bootstrap yes
CubicPathwidth.PwSeq.Defs yes
CubicPathwidth.PwSeq.Extension yes
CubicPathwidth.PwSeq.Seeds yes
CubicPathwidth.PwSeq.Targets yes Theorem 9.2, Lemma 9.3
CubicPathwidth.PwSeqSpec yes
CubicPathwidth.Relabelling yes
CubicPathwidth.SectionAssembly yes
CubicPathwidth.SectionInsertion yes
CubicPathwidth.Sw4.Assembly yes
CubicPathwidth.Sw4.Defs yes
CubicPathwidth.Sw4.FrontierVertex yes
CubicPathwidth.Sw4.FrontierVertexNum yes
CubicPathwidth.Sw4.GoodLabels yes
CubicPathwidth.Sw4.GoodLabelsA yes
CubicPathwidth.Sw4.GoodLabelsB yes
CubicPathwidth.Sw4.Layout4 yes
CubicPathwidth.Sw4.PsiLower yes
CubicPathwidth.Sw4.Targets yes Theorem 8.2, Theorem 9.2
CubicPathwidth.Sw4.ZeroVertex yes
CubicPathwidth.Sw4.ZeroVertexNum yes
CubicPathwidth.Sw4Spec yes
CubicPathwidth.T2.All yes
CubicPathwidth.T2.AssemblyA yes
CubicPathwidth.T2.AssemblyB yes
CubicPathwidth.T2.Bridge yes
CubicPathwidth.T2.Charging yes
CubicPathwidth.T2.Concentration4 yes
CubicPathwidth.T2.Defs yes
CubicPathwidth.T2.DefsB yes
CubicPathwidth.T2.DegreeLabels yes
CubicPathwidth.T2.DegreeLabelsAmp yes
CubicPathwidth.T2.DegreeLabelsCut yes
CubicPathwidth.T2.DegreeLabelsShell yes
CubicPathwidth.T2.FcubicBounds yes
CubicPathwidth.T2.GoodLabels4 yes
CubicPathwidth.T2.GoodLabelsCount yes
CubicPathwidth.T2.GoodLabelsCountA yes
CubicPathwidth.T2.GoodLabelsCountB yes
CubicPathwidth.T2.HetStar yes
CubicPathwidth.T2.IdealLimit yes
CubicPathwidth.T2.Labels4 yes
CubicPathwidth.T2.LayoutS yes
CubicPathwidth.T2.Locality4 yes
CubicPathwidth.T2.PhiTail yes
CubicPathwidth.T2.Reduction yes
CubicPathwidth.T2.ReductionPieces yes
CubicPathwidth.T2.Slepian yes
CubicPathwidth.T2.SlepianSmooth yes
CubicPathwidth.T2.SlepianStein yes
CubicPathwidth.T2.StarBoundCont yes
CubicPathwidth.T2.StarFour yes
CubicPathwidth.T2.TargetA yes Theorem 1.1, Theorem 7.1
CubicPathwidth.T2.TargetBC yes Theorem 7.1
CubicPathwidth.T2Spec yes
CubicPathwidth.T3.Assembly yes
CubicPathwidth.T3.Charging5 yes
CubicPathwidth.T3.Constants yes
CubicPathwidth.T3.Defs yes
CubicPathwidth.T3.DegreeLabels5 yes
CubicPathwidth.T3.GoodLabelsCount5 yes
CubicPathwidth.T3.GoodLabelsCount5A yes
CubicPathwidth.T3.GoodLabelsCount5B yes
CubicPathwidth.T3.PhiTail5 yes
CubicPathwidth.T3.Reduction5 yes
CubicPathwidth.T3.Targets yes Theorem 7.2
CubicPathwidth.T3Spec yes
CubicPathwidth.T4.Assembly yes
CubicPathwidth.T4.Basic yes
CubicPathwidth.T4.BasicComp yes
CubicPathwidth.T4.BasicGlue yes
CubicPathwidth.T4.BasicPsi yes
CubicPathwidth.T4.Cor5S yes
CubicPathwidth.T4.Defs yes
CubicPathwidth.T4.DeletionX yes
CubicPathwidth.T4.DeletionXArith yes
CubicPathwidth.T4.DeletionXKey yes
CubicPathwidth.T4.DeletionXLoc yes
CubicPathwidth.T4.Lift yes
CubicPathwidth.T4.Process yes
CubicPathwidth.T4.ProcessDefs yes
CubicPathwidth.T4.SeqH yes
CubicPathwidth.T4.Targets yes Theorem 1.3, Corollary 1.4
CubicPathwidth.T4.TorsoDyn yes
CubicPathwidth.T4Spec yes
CubicPathwidth.UniformStep yes
CubicPathwidthProofs yes
Back to top