CubicPathwidthProofs

Source file CubicPathwidthProofs.lean of the Lean project (how it is built).

import CubicPathwidth.Coefficients
import CubicPathwidth.GaussianEstimates
import CubicPathwidth.AsymptoticTransfer
import CubicPathwidth.BagOperations
import CubicPathwidth.BisectionLimit
import CubicPathwidth.GraphSections
import CubicPathwidth.CutConnector
import CubicPathwidth.Relabelling
import CubicPathwidth.CutGluing
import CubicPathwidth.UniformStep
import CubicPathwidth.BalanceRepair
import CubicPathwidth.GraphLocality
import CubicPathwidth.GraphGaussianCoefficients
import CubicPathwidth.BisectionMoments
import CubicPathwidth.ExpectedCut
import CubicPathwidth.GaussianField
import CubicPathwidth.GaussianBisection
import CubicPathwidth.GaussianPlanar
import CubicPathwidth.GaussianSign

import CubicPathwidth.BoundaryInduction
import CubicPathwidth.BoundaryAsymptotics
import CubicPathwidth.CoreCounting
import CubicPathwidth.CorePruning
import CubicPathwidth.SectionAssembly
import CubicPathwidth.BoundaryAssembly
import CubicPathwidth.FiniteComponents
import CubicPathwidth.ForestStructure
import CubicPathwidth.ForestDecomposition
import CubicPathwidth.PseudotreeDecomposition
import CubicPathwidth.CorePieces
import CubicPathwidth.SectionInsertion
import CubicPathwidth.CoreTorso
import CubicPathwidth.CoreLifting
import CubicPathwidth.Bootstrap
import CubicPathwidth.Completion
import CubicPathwidth.EndpointTransfer
import CubicPathwidth.C3Spec
import CubicPathwidth.C3.All
import CubicPathwidth.T2Spec
import CubicPathwidth.T2.All
import CubicPathwidth.T3Spec
import CubicPathwidth.T3.Targets
import CubicPathwidth.T4Spec
import CubicPathwidth.T4.Targets
import CubicPathwidth.Alg.Proofs.Targets
import CubicPathwidth.Alg.Proofs2.Targets
import CubicPathwidth.PwSeq.Targets
import CubicPathwidth.Sw4.Targets
import CubicPathwidth.CutSweep.All
/-!
# Complete proof of the existential pathwidth bound

`CubicPathwidth.mainClaim` proves the original specification without extra
mathematical hypotheses. The boundary/core constructions, Gaussian bisection,
a self-contained starting bound, and uniform coefficient iteration are all
checked. The axiom reports below inspect the proof's foundations.
Algorithm correctness and runtime proofs remain deferred at Serge Gaspers's
explicit request.
-/

#check CubicPathwidth.pathwidthCoefficient_lt_one_sixth
#check CubicPathwidth.mainClaim_of_baseline_and_step
#check CubicPathwidth.uniformBisectionBound_of_finite
#check CubicPathwidth.pathwidth_of_cut_sections
#check CubicPathwidth.mainClaim_of_graph_inputs
#check CubicPathwidth.finiteGaussianBisection_of_signDisagreement
#check CubicPathwidth.gaussianSignDisagreement
#check CubicPathwidth.finiteGaussianBisection
#check CubicPathwidth.uniformGaussianBisection
#check CubicPathwidth.mainClaim_of_remaining_graph_inputs

#print axioms CubicPathwidth.bisectionCoefficient_nonneg
#print axioms CubicPathwidth.pathwidthCoefficient_nonneg
#print axioms CubicPathwidth.PathDecomposition.WidthAtMost.mono
#print axioms CubicPathwidth.HasPathwidthAtMost.mono
#print axioms CubicPathwidth.transferRatio_pos
#print axioms CubicPathwidth.transferRatio_lt_one
#print axioms CubicPathwidth.iteratedCoefficient_zero
#print axioms CubicPathwidth.iteratedCoefficient_nonneg
#print axioms CubicPathwidth.iteratedCoefficient_le_one_sixth
#print axioms CubicPathwidth.iteratedCoefficient_succ
#print axioms CubicPathwidth.BagPath.hold
#print axioms CubicPathwidth.BagPath.reverse_width
#print axioms CubicPathwidth.BagPath.toDecomposition_width
#print axioms CubicPathwidth.BagPath.concat_bag_left
#print axioms CubicPathwidth.BagPath.concat_bag_right

/-! Axiom inspection for all public declarations added in the graph continuation. -/
#print axioms CubicPathwidth.BagPath.single
#print axioms CubicPathwidth.BagPath.append
#print axioms CubicPathwidth.BagPath.append_last
#print axioms CubicPathwidth.BagPath.append_width
#print axioms CubicPathwidth.BagPath.WidthAtMost.mono
#print axioms CubicPathwidth.BagPath.concat_last
#print axioms CubicPathwidth.SectionDecomposition.restrict
#print axioms CubicPathwidth.SectionDecomposition.restrict_width
#print axioms CubicPathwidth.SectionDecomposition.restrict_last
#print axioms CubicPathwidth.SectionDecomposition.toFull
#print axioms CubicPathwidth.SectionDecomposition.toFull_width
#print axioms CubicPathwidth.SectionDecomposition.restoreVertex
#print axioms CubicPathwidth.SectionDecomposition.restoreVertex_last
#print axioms CubicPathwidth.SectionDecomposition.restoreVertex_width
#print axioms CubicPathwidth.SectionDecomposition.endAtSubset
#print axioms CubicPathwidth.SectionDecomposition.endAtSubset_last
#print axioms CubicPathwidth.SectionDecomposition.endAtSubset_width
#print axioms CubicPathwidth.SectionDecomposition.restore_zero_outside
#print axioms CubicPathwidth.SectionDecomposition.restore_one_outside
#print axioms CubicPathwidth.SectionDecomposition.reverse
#print axioms CubicPathwidth.SectionDecomposition.reverse_start
#print axioms CubicPathwidth.SectionDecomposition.reverse_width
#print axioms CubicPathwidth.CutConnector.cutBag
#print axioms CubicPathwidth.CutConnector.cutBag_subset
#print axioms CubicPathwidth.CutConnector.cutBag_start
#print axioms CubicPathwidth.CutConnector.cutBag_end
#print axioms CubicPathwidth.CutConnector.path
#print axioms CubicPathwidth.CutConnector.edge_covered
#print axioms CubicPathwidth.CutConnector.cutBag_card_le
#print axioms CubicPathwidth.CutConnector.path_width
#print axioms CubicPathwidth.CutConnector.edges
#print axioms CubicPathwidth.CutConnector.mem_edges
#print axioms CubicPathwidth.CutConnector.edges_card
#print axioms CubicPathwidth.CutConnector.left_subset
#print axioms CubicPathwidth.CutConnector.right_not_mem
#print axioms CubicPathwidth.CutConnector.sides_disjoint
#print axioms CubicPathwidth.CutConnector.graph_path_width
#print axioms CubicPathwidth.SectionDecomposition.enumerate
#print axioms CubicPathwidth.SectionDecomposition.mem_iff_enumerate
#print axioms CubicPathwidth.SectionDecomposition.inducedOnFin
#print axioms CubicPathwidth.SectionDecomposition.inducedOnFin_subcubic
#print axioms CubicPathwidth.SectionDecomposition.lift
#print axioms CubicPathwidth.SectionDecomposition.lift_width
#print axioms CubicPathwidth.SectionDecomposition.lift_last
#print axioms CubicPathwidth.SectionDecomposition.boundaryPreimage
#print axioms CubicPathwidth.SectionDecomposition.boundaryPreimage_image
#print axioms CubicPathwidth.SectionDecomposition.boundaryPreimage_card
#print axioms CubicPathwidth.SectionDecomposition.ending_section_of_relabelled
#print axioms CubicPathwidth.pathwidth_of_cut_sections
#print axioms CubicPathwidth.pathwidth_of_cut_endpoint_bounds
#print axioms CubicPathwidth.coefficient_step_of_endpoint
#print axioms CubicPathwidth.mainClaim_of_graph_inputs

/-! Complete axiom inspection for the finite-Gaussian continuation.
Its modular assembly is discharged by GaussianSign below. -/
#print axioms CubicPathwidth.crossingEdges_compl
#print axioms CubicPathwidth.crossingEdges_subset_le
#print axioms CubicPathwidth.exists_bisection_of_large_side
#print axioms CubicPathwidth.exists_bisection_repair
#print axioms CubicPathwidth.Locality.sphere
#print axioms CubicPathwidth.Locality.ball
#print axioms CubicPathwidth.Locality.mem_sphere
#print axioms CubicPathwidth.Locality.mem_ball
#print axioms CubicPathwidth.Locality.sphere_zero
#print axioms CubicPathwidth.Locality.ball_zero
#print axioms CubicPathwidth.Locality.exists_predecessor
#print axioms CubicPathwidth.Locality.next_neighbors_card_le
#print axioms CubicPathwidth.Locality.sphere_card_succ_le
#print axioms CubicPathwidth.Locality.sphere_one
#print axioms CubicPathwidth.Locality.sphere_card_le
#print axioms CubicPathwidth.Locality.ball_succ
#print axioms CubicPathwidth.Locality.ball_card_add_two_le
#print axioms CubicPathwidth.Locality.disjoint_balls_of_not_mem
#print axioms CubicPathwidth.Locality.geometric
#print axioms CubicPathwidth.Locality.geometric_pos
#print axioms CubicPathwidth.Locality.geometric_zero
#print axioms CubicPathwidth.Locality.geometric_sq
#print axioms CubicPathwidth.Locality.geometric_step
#print axioms CubicPathwidth.Locality.geometric_antitone
#print axioms CubicPathwidth.Locality.layerMass
#print axioms CubicPathwidth.Locality.mass
#print axioms CubicPathwidth.Locality.sphere_mass
#print axioms CubicPathwidth.Locality.ball_disjoint_sphere_succ
#print axioms CubicPathwidth.Locality.mass_eq_layers
#print axioms CubicPathwidth.Locality.mass_pos
#print axioms CubicPathwidth.Locality.layerMass_antitone
#print axioms CubicPathwidth.Locality.outer_mass_fraction
#print axioms CubicPathwidth.Locality.lost_ball_subset_sphere
#print axioms CubicPathwidth.Locality.retained_mass
#print axioms CubicPathwidth.Locality.coefficient_ratio
#print axioms CubicPathwidth.Locality.coefficient
#print axioms CubicPathwidth.Locality.coefficient_nonneg
#print axioms CubicPathwidth.Locality.coefficient_norm_sq
#print axioms CubicPathwidth.Locality.coefficient_inner
#print axioms CubicPathwidth.Locality.graph_correlation_lower
#print axioms CubicPathwidth.integral_abs_le_sqrt_secondMoment
#print axioms CubicPathwidth.exists_bisection_of_cut_moments
#print axioms CubicPathwidth.cutSign
#print axioms CubicPathwidth.sum_cutSign
#print axioms CubicPathwidth.abs_cutSign
#print axioms CubicPathwidth.secondMoment_sum_le
#print axioms CubicPathwidth.secondMoment_sum_le_graph
#print axioms CubicPathwidth.crossIndicator
#print axioms CubicPathwidth.edgeDisagreement
#print axioms CubicPathwidth.sum_crossIndicator
#print axioms CubicPathwidth.edgeDisagreement_eq
#print axioms CubicPathwidth.sum_edgeDisagreement
#print axioms CubicPathwidth.crossIndicator_integrable
#print axioms CubicPathwidth.cut_integrable
#print axioms CubicPathwidth.expected_cut_le
#print axioms CubicPathwidth.GaussianField.Sample
#print axioms CubicPathwidth.GaussianField.vector
#print axioms CubicPathwidth.GaussianField.vector_inner
#print axioms CubicPathwidth.GaussianField.vector_inner_self
#print axioms CubicPathwidth.GaussianField.field
#print axioms CubicPathwidth.GaussianField.field_apply
#print axioms CubicPathwidth.GaussianField.field_gaussian
#print axioms CubicPathwidth.GaussianField.field_joint_gaussian
#print axioms CubicPathwidth.GaussianField.field_mean
#print axioms CubicPathwidth.GaussianField.field_covariance
#print axioms CubicPathwidth.GaussianField.field_variance
#print axioms CubicPathwidth.GaussianField.field_variance_pos
#print axioms CubicPathwidth.GaussianField.field_independent
#print axioms CubicPathwidth.GaussianField.thresholdSign
#print axioms CubicPathwidth.GaussianField.thresholdSign_measurable
#print axioms CubicPathwidth.GaussianField.thresholdSign_abs
#print axioms CubicPathwidth.GaussianField.thresholdSign_neg
#print axioms CubicPathwidth.GaussianField.gaussian_sign_mean
#print axioms CubicPathwidth.GaussianField.field_sign_mean
#print axioms CubicPathwidth.GaussianField.field_sign_memLp
#print axioms CubicPathwidth.GaussianField.distant_sign_product_mean
#print axioms CubicPathwidth.GaussianField.field_sign_secondMoment
#print axioms CubicPathwidth.GaussianSignDisagreementClaim
#print axioms CubicPathwidth.GaussianField.signCut
#print axioms CubicPathwidth.GaussianField.mem_signCut
#print axioms CubicPathwidth.GaussianField.signCut_measurable
#print axioms CubicPathwidth.GaussianField.signCut_imbalance
#print axioms CubicPathwidth.GaussianField.signCut_imbalance_memLp
#print axioms CubicPathwidth.GaussianField.signCut_secondMoment
#print axioms CubicPathwidth.GaussianField.signCut_edge_bound
#print axioms CubicPathwidth.GaussianField.signCut_expected_bound
#print axioms CubicPathwidth.finiteGaussianBisection_of_signDisagreement

/-! Complete axiom inspection for the sign identity and its consequences. -/
#print axioms CubicPathwidth.GaussianAngle.normal2
#print axioms CubicPathwidth.GaussianAngle.radial
#print axioms CubicPathwidth.GaussianAngle.density_polar
#print axioms CubicPathwidth.GaussianAngle.integral_normal2
#print axioms CubicPathwidth.GaussianAngle.integral_angular
#print axioms CubicPathwidth.GaussianAngle.radial_integral
#print axioms CubicPathwidth.GaussianAngle.sin_pos_iff
#print axioms CubicPathwidth.GaussianAngle.sin_neg_iff
#print axioms CubicPathwidth.GaussianAngle.angularDisagreement
#print axioms CubicPathwidth.GaussianAngle.angularDisagreement_eq
#print axioms CubicPathwidth.GaussianAngle.angular_integral
#print axioms CubicPathwidth.GaussianAngle.planar_sign_disagreement
#print axioms CubicPathwidth.GaussianAngle.projection_gaussian
#print axioms CubicPathwidth.GaussianAngle.projection_mean
#print axioms CubicPathwidth.GaussianAngle.projection_covariance
#print axioms CubicPathwidth.GaussianAngle.projection_variance
#print axioms CubicPathwidth.GaussianAngle.unit_projection_map
#print axioms CubicPathwidth.GaussianAngle.orthogonal_pair_map
#print axioms CubicPathwidth.GaussianAngle.unit_projection_ne_zero_ae
#print axioms CubicPathwidth.GaussianAngle.disagreement
#print axioms CubicPathwidth.GaussianAngle.disagreement_self
#print axioms CubicPathwidth.GaussianAngle.disagreement_neg
#print axioms CubicPathwidth.GaussianAngle.unit_sign_disagreement
#print axioms CubicPathwidth.GaussianAngle.normalize_halfspace
#print axioms CubicPathwidth.GaussianAngle.normalized_inner_self
#print axioms CubicPathwidth.GaussianAngle.sign_disagreement
#print axioms CubicPathwidth.gaussianSignDisagreement
#print axioms CubicPathwidth.finiteGaussianBisection
#print axioms CubicPathwidth.uniformGaussianBisection
#print axioms CubicPathwidth.mainClaim_of_remaining_graph_inputs

/-! Modular boundary/core assembly; CoreLifting now discharges both inputs. -/
#check CubicPathwidth.exists_core_branch_bound
#check CubicPathwidth.boundaryTransfer_of_tree_and_core
#print axioms CubicPathwidth.HasEndingSection
#print axioms CubicPathwidth.HasEndingSection.mono
#print axioms CubicPathwidth.sectionNeighbors
#print axioms CubicPathwidth.mem_sectionNeighbors
#print axioms CubicPathwidth.StableBoundary
#print axioms CubicPathwidth.endingSection_induction
#print axioms CubicPathwidth.endingSection_of_stable
#print axioms CubicPathwidth.endpointBudget
#print axioms CubicPathwidth.endpointBudget_mono
#print axioms CubicPathwidth.endpointBudget_ge_size
#print axioms CubicPathwidth.AffinePathwidthBound
#print axioms CubicPathwidth.FiniteEndpointTransfer
#print axioms CubicPathwidth.SublinearError
#print axioms CubicPathwidth.affinePathwidthBound_of_uniform
#print axioms CubicPathwidth.boundaryTransfer_of_finite
#print axioms CubicPathwidth.finiteEndpointTransfer_of_stable
#print axioms CubicPathwidth.incidence
#print axioms CubicPathwidth.incidence_symm
#print axioms CubicPathwidth.incidence_union_left
#print axioms CubicPathwidth.incidence_union_right
#print axioms CubicPathwidth.incidence_le_subcubic
#print axioms CubicPathwidth.degreeExcess
#print axioms CubicPathwidth.incidence_singleton
#print axioms CubicPathwidth.incidence_insert
#print axioms CubicPathwidth.degreeExcess_insert
#print axioms CubicPathwidth.sectionNeighbors_erase_self
#print axioms CubicPathwidth.degreeExcess_erase_leaf
#print axioms CubicPathwidth.stable_degreeExcess_bound
#print axioms CubicPathwidth.degreeExcess_eq_branch_card
#print axioms CubicPathwidth.ClosedIn
#print axioms CubicPathwidth.NonnegativeComponentExcess
#print axioms CubicPathwidth.nonnegativeComponentExcess_degree_pos
#print axioms CubicPathwidth.nonnegativeComponentExcess_erase_leaf
#print axioms CubicPathwidth.LeafPrunes
#print axioms CubicPathwidth.LeafPrunes.subset
#print axioms CubicPathwidth.LeafPrunes.excess_eq
#print axioms CubicPathwidth.exists_leafPrunes_minDegree_two
#print axioms CubicPathwidth.exists_core_branch_bound
#print axioms CubicPathwidth.SectionDecomposition.hold
#print axioms CubicPathwidth.SectionDecomposition.hold_width
#print axioms CubicPathwidth.SectionDecomposition.hold_bag
#print axioms CubicPathwidth.SectionDecomposition.concat
#print axioms CubicPathwidth.SectionDecomposition.concat_width
#print axioms CubicPathwidth.SectionDecomposition.concat_last
#print axioms CubicPathwidth.SectionDecomposition.ending_hold
#print axioms CubicPathwidth.SectionDecomposition.append_component
#print axioms CubicPathwidth.coreOverhead
#print axioms CubicPathwidth.coreOverhead_nonneg
#print axioms CubicPathwidth.coreOverhead_mono
#print axioms CubicPathwidth.coreOverhead_sublinear
#print axioms CubicPathwidth.ForestComponentBound
#print axioms CubicPathwidth.CoreLiftingBound
#print axioms CubicPathwidth.finiteEndpointTransfer_of_tree_and_core
#print axioms CubicPathwidth.boundaryTransfer_of_tree_and_core

/-! All named public declarations added in the completion session. -/
#print axioms CubicPathwidth.SectionConnected
#print axioms CubicPathwidth.closed_sdiff
#print axioms CubicPathwidth.closed_trans
#print axioms CubicPathwidth.component
#print axioms CubicPathwidth.component_subset
#print axioms CubicPathwidth.mem_component_self
#print axioms CubicPathwidth.component_min
#print axioms CubicPathwidth.component_closed
#print axioms CubicPathwidth.component_eq_of_mem
#print axioms CubicPathwidth.component_connected
#print axioms CubicPathwidth.component_eq_of_connected
#print axioms CubicPathwidth.components
#print axioms CubicPathwidth.mem_components
#print axioms CubicPathwidth.components_disjoint
#print axioms CubicPathwidth.components_cover
#print axioms CubicPathwidth.sum_component_cards
#print axioms CubicPathwidth.connected_subset_or_disjoint
#print axioms CubicPathwidth.connected_cross_edge
#print axioms CubicPathwidth.ForestSection
#print axioms CubicPathwidth.ForestSection.mono
#print axioms CubicPathwidth.connected_excess_mono
#print axioms CubicPathwidth.connected_excess_lower
#print axioms CubicPathwidth.forest_of_connected_negative
#print axioms CubicPathwidth.forest_component_neighbors_le_one
#print axioms CubicPathwidth.connected_component_neighbor
#print axioms CubicPathwidth.largestBranch
#print axioms CubicPathwidth.forest_centroid
#print axioms CubicPathwidth.section_of_components
#print axioms CubicPathwidth.sqrt_half_bound
#print axioms CubicPathwidth.forest_section_decomposition
#print axioms CubicPathwidth.degreeExcess_eq_sum
#print axioms CubicPathwidth.sum_component_excess
#print axioms CubicPathwidth.forestComponentBound
#print axioms CubicPathwidth.sectionNeighbors_mono
#print axioms CubicPathwidth.forest_restore_leaf
#print axioms CubicPathwidth.connected_erase_leaf
#print axioms CubicPathwidth.LeafPrunes.connected
#print axioms CubicPathwidth.LeafPrunes.forest_erase
#print axioms CubicPathwidth.connected_nonnegativeComponentExcess
#print axioms CubicPathwidth.incidence_positive
#print axioms CubicPathwidth.degree_two_erase_forest
#print axioms CubicPathwidth.pseudotree_section_decomposition
#print axioms CubicPathwidth.branchVertices
#print axioms CubicPathwidth.attachment
#print axioms CubicPathwidth.mem_attachment
#print axioms CubicPathwidth.attachment_subset
#print axioms CubicPathwidth.attachment_card_le
#print axioms CubicPathwidth.incidence_mono_right
#print axioms CubicPathwidth.incidence_insert_left
#print axioms CubicPathwidth.incidence_insert_right
#print axioms CubicPathwidth.LeafPrunes.closed_incidence_le_two
#print axioms CubicPathwidth.incidence_closed_split
#print axioms CubicPathwidth.core_piece_bounds
#print axioms CubicPathwidth.BagPath.takeUntil
#print axioms CubicPathwidth.BagPath.suffix
#print axioms CubicPathwidth.BagPath.takeUntil_width
#print axioms CubicPathwidth.BagPath.suffix_width
#print axioms CubicPathwidth.BagPath.concat_subset
#print axioms CubicPathwidth.SectionDecomposition.insert_at_bag
#print axioms CubicPathwidth.coreTorso
#print axioms CubicPathwidth.two_attachment_unique
#print axioms CubicPathwidth.torso_edge_witness
#print axioms CubicPathwidth.coreTorso_subcubic
#print axioms CubicPathwidth.liftTorso
#print axioms CubicPathwidth.liftTorso_width
#print axioms CubicPathwidth.liftTorso_bag
#print axioms CubicPathwidth.torso_attachment_bag
#print axioms CubicPathwidth.insert_components
#print axioms CubicPathwidth.coreLiftingBound
#print axioms CubicPathwidth.boundaryTransfer
#print axioms CubicPathwidth.pathwidth_of_cut_unanchored
#print axioms CubicPathwidth.uniformPathwidthBound_twice_of_bisection
#print axioms CubicPathwidth.pathwidthCoefficient_le_twice_bisection
#print axioms CubicPathwidth.bootstrapCoefficient
#print axioms CubicPathwidth.bootstrapCoefficient_zero
#print axioms CubicPathwidth.bootstrapCoefficient_nonneg
#print axioms CubicPathwidth.bootstrapCoefficient_le_twice
#print axioms CubicPathwidth.bootstrapCoefficient_succ
#print axioms CubicPathwidth.exists_bootstrapCoefficient_lt
#print axioms CubicPathwidth.uniformBootstrapCoefficient
#print axioms CubicPathwidth.uniformImprovedPathwidth
#print axioms CubicPathwidth.mainClaim
#print axioms CubicPathwidth.uniformOneSixthPathwidth
#print axioms CubicPathwidth.fixedSaving
#print axioms CubicPathwidth.coefficient_step_of_endpoint_general
#check CubicPathwidth.mainClaim
#check CubicPathwidth.fixedSaving

/-! The `c3` theorem (approved specification `CubicPathwidth/C3Spec.lean`). -/
#check CubicPathwidth.C3.c3MainClaim
#print axioms CubicPathwidth.C3.c3MainClaim

/-! Theorem 2, maximum degree 4 (approved specification `CubicPathwidth/T2Spec.lean`). -/
#check CubicPathwidth.T2.target2a
#check CubicPathwidth.T2.target2b
#check CubicPathwidth.T2.target2c
#print axioms CubicPathwidth.T2.target2a
#print axioms CubicPathwidth.T2.target2b
#print axioms CubicPathwidth.T2.target2c

/-! Theorem 3, maximum degree 5 (approved specification `CubicPathwidth/T3Spec.lean`). -/
#check CubicPathwidth.T3.target3P
#check CubicPathwidth.T3.target3R
#check CubicPathwidth.T3.target3S
#print axioms CubicPathwidth.T3.target3P
#print axioms CubicPathwidth.T3.target3R
#print axioms CubicPathwidth.T3.target3S

/-! Theorem 4 and Corollary 5 (approved specification `CubicPathwidth/T4Spec.lean`). -/
#check CubicPathwidth.T4.target4
#check CubicPathwidth.T4.target5
#print axioms CubicPathwidth.T4.target4
#print axioms CubicPathwidth.T4.target5

/-! Algorithms, stage 1: validity of the Lean port of `sweep.py`
(approved specification). -/
#check (CubicPathwidth.Alg.algoT1Valid : CubicPathwidth.Alg.AlgoT1Valid)
#check (CubicPathwidth.Alg.algoT2aValid : CubicPathwidth.Alg.AlgoT2aValid)
#check (CubicPathwidth.Alg.algoMixedValid : CubicPathwidth.Alg.AlgoMixedValid)
#check (CubicPathwidth.Alg.algoT4Valid : CubicPathwidth.Alg.AlgoT4Valid)
#check (CubicPathwidth.Alg.algoT1Exported : CubicPathwidth.Alg.AlgoT1Exported)
#check (CubicPathwidth.Alg.algoT2aExported : CubicPathwidth.Alg.AlgoT2aExported)
#check (CubicPathwidth.Alg.algoMixedExported : CubicPathwidth.Alg.AlgoMixedExported)
#check (CubicPathwidth.Alg.algoT4Exported : CubicPathwidth.Alg.AlgoT4Exported)
#print axioms CubicPathwidth.Alg.algoT1Valid
#print axioms CubicPathwidth.Alg.algoT2aValid
#print axioms CubicPathwidth.Alg.algoMixedValid
#print axioms CubicPathwidth.Alg.algoT4Valid
#print axioms CubicPathwidth.Alg.algoT1Exported
#print axioms CubicPathwidth.Alg.algoT2aExported
#print axioms CubicPathwidth.Alg.algoMixedExported
#print axioms CubicPathwidth.Alg.algoT4Exported

/-! Algorithms, stage 2: no fallbacks, widths, and Theorems 1–4 and Corollary 5 realized by
the port (approved specification). -/
#check (CubicPathwidth.Alg.connectorNoFallback : CubicPathwidth.Alg.ConnectorNoFallback)
#check (CubicPathwidth.Alg.reduceRecordNoFallback : CubicPathwidth.Alg.ReduceRecordNoFallback)
#check (CubicPathwidth.Alg.pdTw2NoFallback : CubicPathwidth.Alg.PdTw2NoFallback)
#check (CubicPathwidth.Alg.algoT1NoFallback : CubicPathwidth.Alg.AlgoT1NoFallback)
#check (CubicPathwidth.Alg.algoMixedNoFallback : CubicPathwidth.Alg.AlgoMixedNoFallback)
#check (CubicPathwidth.Alg.algoT4NoFallback : CubicPathwidth.Alg.AlgoT4NoFallback)
#check (CubicPathwidth.Alg.reduceRecordMaximal : CubicPathwidth.Alg.ReduceRecordMaximal)
#check (CubicPathwidth.Alg.undoNoFallback : CubicPathwidth.Alg.UndoNoFallback)
#check (CubicPathwidth.Alg.t4LoopNoFallback : CubicPathwidth.Alg.T4LoopNoFallback)
#check (CubicPathwidth.Alg.plainLayoutWidth : CubicPathwidth.Alg.PlainLayoutWidth)
#check (CubicPathwidth.Alg.connectorLemma10 : CubicPathwidth.Alg.ConnectorLemma10)
#check (CubicPathwidth.Alg.switchedLayoutWidth : CubicPathwidth.Alg.SwitchedLayoutWidth)
#check (CubicPathwidth.Alg.pdTw2Width : CubicPathwidth.Alg.PdTw2Width)
#check (CubicPathwidth.Alg.undoWidth : CubicPathwidth.Alg.UndoWidth)
#check (CubicPathwidth.Alg.deletionProcessBound : CubicPathwidth.Alg.DeletionProcessBound)
#check (CubicPathwidth.Alg.algoT1Width : CubicPathwidth.Alg.AlgoT1Width)
#check (CubicPathwidth.Alg.algoT2aWidth : CubicPathwidth.Alg.AlgoT2aWidth)
#check (CubicPathwidth.Alg.algoMixedWidth : CubicPathwidth.Alg.AlgoMixedWidth)
#check (CubicPathwidth.Alg.algoT4Width : CubicPathwidth.Alg.AlgoT4Width)
#check (CubicPathwidth.Alg.thinComponentWidth : CubicPathwidth.Alg.ThinComponentWidth)
#check (CubicPathwidth.Alg.algoT1RealizesTheorem1 : CubicPathwidth.Alg.AlgoT1RealizesTheorem1)
#check (CubicPathwidth.Alg.algoT2aRealizesTheorem2a : CubicPathwidth.Alg.AlgoT2aRealizesTheorem2a)
#check (CubicPathwidth.Alg.algoMixedRealizesTheorem2b : CubicPathwidth.Alg.AlgoMixedRealizesTheorem2b)
#check (CubicPathwidth.Alg.algoMixedRealizesTheorem2c : CubicPathwidth.Alg.AlgoMixedRealizesTheorem2c)
#check (CubicPathwidth.Alg.algoMixedRealizesTheorem3P : CubicPathwidth.Alg.AlgoMixedRealizesTheorem3P)
#check (CubicPathwidth.Alg.algoMixedRealizesTheorem3R : CubicPathwidth.Alg.AlgoMixedRealizesTheorem3R)
#check (CubicPathwidth.Alg.algoMixedRealizesTheorem3S : CubicPathwidth.Alg.AlgoMixedRealizesTheorem3S)
#check (CubicPathwidth.Alg.algoT4RealizesTheorem4 : CubicPathwidth.Alg.AlgoT4RealizesTheorem4)
#check (CubicPathwidth.Alg.algoT4RealizesCorollary5 : CubicPathwidth.Alg.AlgoT4RealizesCorollary5)
#print axioms CubicPathwidth.Alg.connectorNoFallback
#print axioms CubicPathwidth.Alg.reduceRecordNoFallback
#print axioms CubicPathwidth.Alg.pdTw2NoFallback
#print axioms CubicPathwidth.Alg.algoT1NoFallback
#print axioms CubicPathwidth.Alg.algoMixedNoFallback
#print axioms CubicPathwidth.Alg.algoT4NoFallback
#print axioms CubicPathwidth.Alg.reduceRecordMaximal
#print axioms CubicPathwidth.Alg.undoNoFallback
#print axioms CubicPathwidth.Alg.t4LoopNoFallback
#print axioms CubicPathwidth.Alg.plainLayoutWidth
#print axioms CubicPathwidth.Alg.connectorLemma10
#print axioms CubicPathwidth.Alg.switchedLayoutWidth
#print axioms CubicPathwidth.Alg.pdTw2Width
#print axioms CubicPathwidth.Alg.undoWidth
#print axioms CubicPathwidth.Alg.deletionProcessBound
#print axioms CubicPathwidth.Alg.algoT1Width
#print axioms CubicPathwidth.Alg.algoT2aWidth
#print axioms CubicPathwidth.Alg.algoMixedWidth
#print axioms CubicPathwidth.Alg.algoT4Width
#print axioms CubicPathwidth.Alg.thinComponentWidth
#print axioms CubicPathwidth.Alg.algoT1RealizesTheorem1
#print axioms CubicPathwidth.Alg.algoT2aRealizesTheorem2a
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem2b
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem2c
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem3P
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem3R
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem3S
#print axioms CubicPathwidth.Alg.algoT4RealizesTheorem4
#print axioms CubicPathwidth.Alg.algoT4RealizesCorollary5

-- Pathwidth sequences
#check (CubicPathwidth.PwSeq.targetRhoForm : CubicPathwidth.PwSeq.TargetRhoForm)
#check (CubicPathwidth.PwSeq.targetMono : CubicPathwidth.PwSeq.TargetMono)
#check (CubicPathwidth.PwSeq.targetBootSeq : CubicPathwidth.PwSeq.TargetBootSeq)
#check (CubicPathwidth.PwSeq.targetBootstrapLemma : CubicPathwidth.PwSeq.TargetBootstrapLemma)
#check (CubicPathwidth.PwSeq.targetLemma2 : CubicPathwidth.PwSeq.TargetLemma2)
#check (CubicPathwidth.PwSeq.targetSeedHyps : CubicPathwidth.PwSeq.TargetSeedHyps)
#check (CubicPathwidth.PwSeq.targetThm1C : CubicPathwidth.PwSeq.TargetThm1C)
#check (CubicPathwidth.PwSeq.targetThm1F : CubicPathwidth.PwSeq.TargetThm1F)
#check (CubicPathwidth.PwSeq.targetThm1P : CubicPathwidth.PwSeq.TargetThm1P)
#check (CubicPathwidth.PwSeq.targetThm1R : CubicPathwidth.PwSeq.TargetThm1R)
#check (CubicPathwidth.PwSeq.targetThm1S : CubicPathwidth.PwSeq.TargetThm1S)
#print axioms CubicPathwidth.PwSeq.targetRhoForm
#print axioms CubicPathwidth.PwSeq.targetMono
#print axioms CubicPathwidth.PwSeq.targetBootSeq
#print axioms CubicPathwidth.PwSeq.targetBootstrapLemma
#print axioms CubicPathwidth.PwSeq.targetLemma2
#print axioms CubicPathwidth.PwSeq.targetSeedHyps
#print axioms CubicPathwidth.PwSeq.targetThm1C
#print axioms CubicPathwidth.PwSeq.targetThm1F
#print axioms CubicPathwidth.PwSeq.targetThm1P
#print axioms CubicPathwidth.PwSeq.targetThm1R
#print axioms CubicPathwidth.PwSeq.targetThm1S

-- thm:switched4 and thm:pw-seq for the seed M
#check (CubicPathwidth.Sw4.targetThm62 : CubicPathwidth.Sw4.TargetThm62)
#check (CubicPathwidth.Sw4.targetThm1M : CubicPathwidth.Sw4.TargetThm1M)
#print axioms CubicPathwidth.Sw4.targetThm62
#print axioms CubicPathwidth.Sw4.targetThm1M

-- thm:cut-sweep, the cut sweep
#check (CubicPathwidth.CutSweep.cutSweep : CubicPathwidth.CutSweep.CutSweepClaim)
#print axioms CubicPathwidth.CutSweep.cutSweep