Finite checking for one-vertex cuts

This is a passive boundary for finite cut data emitted by an external search. Every condition of OneVertexCut is replayed by a transparent computation.

structure Utilities.Certificate.OneVertexCutCheck.Data (K : CFGraph) : Type u

The proof-free part of a proposed one-vertex cut.

• left : Finset K.V

  The proposed left vertex set of the one-vertex cut; cut properties are imposed by Valid.

• right : Finset K.V

  The proposed right vertex set, whose coverage and overlap with the left are checked separately.

• glue : K.V

  The proposed glue vertex intended to be the two sides' unique overlap.

def Utilities.Certificate.OneVertexCutCheck.Data.Valid {K : CFGraph} (c : Data K) : Prop

The exact conditions required by OneVertexCut.

Equations

• One or more equations did not get rendered due to their size.

def Utilities.Certificate.OneVertexCutCheck.Data.check {K : CFGraph} (c : Data K) : Bool

Executable replay of Valid.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Utilities.Certificate.OneVertexCutCheck.Data.check_eq_true_iff {K : CFGraph} (c : Data K) : c.check = true ↔ c.Valid

def Utilities.Certificate.OneVertexCutCheck.Data.toOneVertexCut {K : CFGraph} (c : Data K) (h : c.Valid) : OneVertexCut K

Turn verified finite data into the corresponding mathematical cut.

Equations

• c.toOneVertexCut h = { left := c.left, right := c.right, glue := c.glue, glue_mem_left := ⋯, glue_mem_right := ⋯, vertex_cover := ⋯, only_overlap := ⋯, no_cross := ⋯ }

def Utilities.Certificate.OneVertexCutCheck.Data.cutOfCheck {K : CFGraph} (c : Data K) (h : c.check = true) : OneVertexCut K

An accepted finite check constructs the corresponding one-vertex cut.

Equations

• c.cutOfCheck h = c.toOneVertexCut ⋯

noncomputable def Utilities.Certificate.OneVertexCutCheck.Data.presentationOfCheck {K : CFGraph} (c : Data K) (h : c.check = true) : VertexWedgePresentation K (c.cutOfCheck h).leftGraph (c.cutOfCheck h).rightGraph (c.cutOfCheck h).leftGlue (c.cutOfCheck h).rightGlue

The vertex-wedge presentation extracted from accepted cut data.

Equations

• c.presentationOfCheck h = (c.cutOfCheck h).presentation

noncomputable def Utilities.Certificate.OneVertexCutCheck.Data.graphIsoOfCheck {K : CFGraph} (c : Data K) (h : c.check = true) : CFGraphIso (vertexWedge (c.cutOfCheck h).leftGraph (c.cutOfCheck h).rightGraph (c.cutOfCheck h).leftGlue (c.cutOfCheck h).rightGlue) K

The occurrence-safe graph isomorphism extracted from accepted cut data.

Equations

• c.graphIsoOfCheck h = (c.cutOfCheck h).graphIso

theorem Utilities.Certificate.OneVertexCutCheck.Data.graph_connected_factors_of_check {K : CFGraph} (c : Data K) (h : c.check = true) (hK : graphConnected K) : graphConnected (c.cutOfCheck h).leftGraph ∧ graphConnected (c.cutOfCheck h).rightGraph

Connectedness of the ambient graph automatically supplies connectedness of both checked induced factors.

theorem Utilities.Certificate.OneVertexCutCheck.Data.BNExists_iff_of_check {K : CFGraph} (c : Data K) (h : c.check = true) (r d : ℤ) : BNExists K r d ↔ BNExists (vertexWedge (c.cutOfCheck h).leftGraph (c.cutOfCheck h).rightGraph (c.cutOfCheck h).leftGlue (c.cutOfCheck h).rightGlue) r d

Brill--Noether existence transfers across an accepted cut check.

theorem Utilities.Certificate.OneVertexCutCheck.Data.transmissionExists_of_profile_of_check {K : CFGraph} (c : Data K) (h : c.check = true) (u : (c.cutOfCheck h).leftGraph.V) (v : (c.cutOfCheck h).rightGraph.V) (tau : AspPerm) (D : CFDiv (c.cutOfCheck h).leftGraph) (E : CFDiv (c.cutOfCheck h).rightGraph) (hProfile : WedgeTransmissionProfile (c.cutOfCheck h).leftGraph (c.cutOfCheck h).rightGraph (c.cutOfCheck h).leftGlue (c.cutOfCheck h).rightGlue D E u v tau) : TransmissionExists K (↑u) (↑v) tau

An arbitrary-ASP wedge profile transfers to the ambient graph after an accepted cut check.

theorem Utilities.Certificate.OneVertexCutCheck.Data.transmissionExists_sameLeft_of_profile_of_check {K : CFGraph} (c : Data K) (h : c.check = true) (p q : (c.cutOfCheck h).leftGraph.V) (tau : AspPerm) (D : CFDiv (c.cutOfCheck h).leftGraph) (E : CFDiv (c.cutOfCheck h).rightGraph) (hProfile : WedgeSameLeftTransmissionProfile (c.cutOfCheck h).leftGraph (c.cutOfCheck h).rightGraph (c.cutOfCheck h).leftGlue (c.cutOfCheck h).rightGlue D E p q tau) : TransmissionExists K (↑p) (↑q) tau

A checked cut transports a same-left arbitrary-ASP factor profile to the ambient graph.

theorem Utilities.Certificate.OneVertexCutCheck.Data.satisfiesTransmission_map_wedgeAddDivisor_sameLeft_of_profile_of_check {K : CFGraph} (c : Data K) (h : c.check = true) (p q : (c.cutOfCheck h).leftGraph.V) (tau : AspPerm) (D : CFDiv (c.cutOfCheck h).leftGraph) (E : CFDiv (c.cutOfCheck h).rightGraph) (hProfile : WedgeSameLeftTransmissionProfile (c.cutOfCheck h).leftGraph (c.cutOfCheck h).rightGraph (c.cutOfCheck h).leftGlue (c.cutOfCheck h).rightGlue D E p q tau) : SatisfiesTransmission K (↑p) (↑q) tau ((c.cutOfCheck h).graphIso.mapDiv (wedgeAddDivisor (c.cutOfCheck h).leftGraph (c.cutOfCheck h).rightGraph (c.cutOfCheck h).leftGlue (c.cutOfCheck h).rightGlue D E))

Explicit ambient divisor supplied by a same-left profile after a checked cut.

theorem Utilities.Certificate.OneVertexCutCheck.Data.transmissionExists_sameRight_of_profile_of_check {K : CFGraph} (c : Data K) (h : c.check = true) (p q : (c.cutOfCheck h).rightGraph.V) (tau : AspPerm) (D : CFDiv (c.cutOfCheck h).leftGraph) (E : CFDiv (c.cutOfCheck h).rightGraph) (hProfile : WedgeSameRightTransmissionProfile (c.cutOfCheck h).leftGraph (c.cutOfCheck h).rightGraph (c.cutOfCheck h).leftGlue (c.cutOfCheck h).rightGlue D E p q tau) : TransmissionExists K (↑p) (↑q) tau

A checked cut transports a same-right arbitrary-ASP factor profile to the ambient graph.

theorem Utilities.Certificate.OneVertexCutCheck.Data.satisfiesTransmission_map_wedgeAddDivisor_sameRight_of_profile_of_check {K : CFGraph} (c : Data K) (h : c.check = true) (p q : (c.cutOfCheck h).rightGraph.V) (tau : AspPerm) (D : CFDiv (c.cutOfCheck h).leftGraph) (E : CFDiv (c.cutOfCheck h).rightGraph) (hProfile : WedgeSameRightTransmissionProfile (c.cutOfCheck h).leftGraph (c.cutOfCheck h).rightGraph (c.cutOfCheck h).leftGlue (c.cutOfCheck h).rightGlue D E p q tau) : SatisfiesTransmission K (↑p) (↑q) tau ((c.cutOfCheck h).graphIso.mapDiv (wedgeAddDivisor (c.cutOfCheck h).leftGraph (c.cutOfCheck h).rightGraph (c.cutOfCheck h).leftGlue (c.cutOfCheck h).rightGlue D E))

Explicit ambient divisor supplied by a same-right profile after a checked cut.

Closed regression