Topological graph-contraction certificates

GraphContractionCertificate.Valid records the quotient multiplicities. A topological contraction additionally has connected vertex fibres. This file expresses that condition by the same finite-cut criterion as graphConnected, so it admits an exact Boolean replay checker.

The fibre condition is deliberately separate from Valid: quotient multiplicities alone do not prevent a certificate from identifying two disconnected pieces of the source graph.

def Utilities.Certificate.GraphContractionCertificate.FibreConnectedAt {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (target : H.V) : Prop

The fibre over target is connected, expressed by finite cuts of the ambient source graph. Only cuts which split that fibre need be crossed, and the crossing edge is required to remain inside the fibre.

Equations

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

def Utilities.Certificate.GraphContractionCertificate.ConnectedFibres {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : Prop

Every vertex fibre is connected.

Equations

• c.ConnectedFibres = ∀ (target : H.V), c.FibreConnectedAt target

def Utilities.Certificate.GraphContractionCertificate.connectedFibresCheck {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : Bool

Exact finite Boolean replay of connectedness for every fibre.

Equations

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

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.connectedFibresCheck_eq_true_iff {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : c.connectedFibresCheck = true ↔ c.ConnectedFibres

def Utilities.Certificate.GraphContractionCertificate.TopologicalValid {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : Prop

A quotient certificate whose fibres are actual connected subgraphs.

Equations

• c.TopologicalValid = (c.Valid ∧ c.ConnectedFibres)

def Utilities.Certificate.GraphContractionCertificate.topologicalCheck {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : Bool

Exact Boolean checker for a topological contraction certificate.

Equations

• c.topologicalCheck = (c.check && c.connectedFibresCheck)

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.topologicalCheck_eq_true_iff {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : c.topologicalCheck = true ↔ c.TopologicalValid

theorem Utilities.Certificate.GraphContractionCertificate.exists_source_of_vertexMap_eq {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (target : H.V) : ∃ (source : G.V), c.vertexMap source = target

A valid contraction is onto on vertices. This small formulation keeps marked-lift arguments from having to unpack Valid directly.

theorem Utilities.Certificate.GraphContractionCertificate.graph_connected_of_topologicalValid {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hTopological : c.TopologicalValid) (hTarget : _root_.graphConnected H) : _root_.graphConnected G

A topological quotient of a connected graph cannot have a disconnected source. Indeed, a source cut with no crossing edge cannot split a connected fibre; it therefore descends to a nontrivial target cut, whose crossing edge lifts through the quotient multiplicity equation.

theorem Utilities.Certificate.GraphContractionCertificate.connectedFibres_precomposeLaplacianEquiv {G : CFGraph} {H : CFGraph} {G' : CFGraph} (c : GraphContractionCertificate G H) (equivalence : LaplacianEquiv G' G) (hFibres : c.ConnectedFibres) : (c.precomposeLaplacianEquiv equivalence).ConnectedFibres

Connected fibres are invariant under a checked relabeling of the source graph. A cut of a relabeled fibre is carried across the vertex equivalence, the original fibre condition supplies a crossing edge, and that edge is then pulled back.

theorem Utilities.Certificate.GraphContractionCertificate.topologicalValid_precomposeLaplacianEquiv {G : CFGraph} {H : CFGraph} {G' : CFGraph} (c : GraphContractionCertificate G H) (equivalence : LaplacianEquiv G' G) (hTopological : c.TopologicalValid) : (c.precomposeLaplacianEquiv equivalence).TopologicalValid

Topological validity is invariant under a checked relabeling of the source graph.

theorem Utilities.Certificate.GraphContractionCertificate.connectedFibres_postcomposeLaplacianEquiv {G : CFGraph} {H : CFGraph} {H' : CFGraph} (c : GraphContractionCertificate G H) (equivalence : LaplacianEquiv H H') (hFibres : c.ConnectedFibres) : (c.postcomposeLaplacianEquiv equivalence).ConnectedFibres

Connected fibres are invariant under a checked relabeling of the quotient target.

theorem Utilities.Certificate.GraphContractionCertificate.topologicalValid_postcomposeLaplacianEquiv {G : CFGraph} {H : CFGraph} {H' : CFGraph} (c : GraphContractionCertificate G H) (equivalence : LaplacianEquiv H H') (hTopological : c.TopologicalValid) : (c.postcomposeLaplacianEquiv equivalence).TopologicalValid

Topological validity is invariant under a checked relabeling of the quotient target.