RationalSTCutCertificate

Abstract

Exact flow conservation and capacity checks certify a global minimum cut.

Vertex is an arbitrary finite type. capacity is Vertex to Vertex to Q; source and sink are Vertex to Q; side is Vertex to Bool. All sums cover the entire finite carrier. True labels are on the source side.

Definition 1.1 (Directed cut energy).

$$\forall Vertex,capacity,source,sink,side,(\mathrm{stCutValue}(capacity,source,sink,side))=((\sum _i(\mathrm{ite}(\mathrm{apply}(side,i),\mathrm{sink}(i),\mathrm{source}(i))))+(\sum _i(\sum _j(\mathrm{ite}(((\mathrm{apply}(side,i))=(true))\wedge ((\mathrm{apply}(side,j))=(false)),\mathrm{capacity}(i,j),0)))))$$

Formalization. D5/S0/Certificates/RationalSTCutCertificate.stCutValue (✓ std3).

Source. Repository-derived.

Commentary.

The source is fixed on the true side and the sink on the false side. All vertex assignments are allowed.

Definition 1.2 (Untrusted flow and cut data).

Lean statement: D5/S0/Certificates/RationalSTCutCertificate.STCutCertificate

Formalization. D5/S0/Certificates/RationalSTCutCertificate.STCutCertificate (✓ std3).

Source. Repository-derived.

Commentary.

The fields are internal : Vertex to Vertex to Q; fromSource and toSink : Vertex to Q; side : Vertex to Bool. No proof or claimed optimality field is supplied.

Definition 1.3 (Value leaving the source).

$$\forall Vertex,certificate,(\mathrm{flowValue}(certificate))=(\sum _i(\mathrm{fromSource}(certificate,i)))$$

Formalization. D5/S0/Certificates/RationalSTCutCertificate.flowValue (✓ std3).

Source. Repository-derived.

Commentary.

The flow value is recomputed from terminal flows.

Definition 1.4 (Capacity, conservation and equality).

$$\forall Vertex,capacity,source,sink,certificate,(\mathrm{ValidSTCutCertificate}(capacity,source,sink,certificate))\iff ((\forall i,j,((0)\le (\mathrm{internal}(certificate,i,j)))\wedge ((\mathrm{internal}(certificate,i,j))\le (\mathrm{capacity}(i,j))))\wedge (\forall i,((0)\le (\mathrm{fromSource}(certificate,i)))\wedge ((\mathrm{fromSource}(certificate,i))\le (\mathrm{source}(i))))\wedge (\forall i,((0)\le (\mathrm{toSink}(certificate,i)))\wedge ((\mathrm{toSink}(certificate,i))\le (\mathrm{sink}(i))))\wedge (\forall i,((\mathrm{fromSource}(certificate,i))+(\sum _j(\mathrm{internal}(certificate,j,i))))=((\mathrm{toSink}(certificate,i))+(\sum _j(\mathrm{internal}(certificate,i,j)))))\wedge ((\mathrm{stCutValue}(capacity,source,sink,\mathrm{side}(certificate)))=(\mathrm{flowValue}(certificate))))$$

Formalization. D5/S0/Certificates/RationalSTCutCertificate.ValidSTCutCertificate (✓ std3).

Source. Repository-derived.

Commentary.

Each capacity condition and each conservation equation is checked on the actual finite arrays; the supplied cut must match the flow value.

Definition 1.5 (Executable exact check).

$$\forall Vertex,capacity,source,sink,certificate,(\mathrm{checkSTCutCertificate}(capacity,source,sink,certificate))=(\mathrm{decide}(\mathrm{ValidSTCutCertificate}(capacity,source,sink,certificate)))$$

Formalization. D5/S0/Certificates/RationalSTCutCertificate.checkSTCutCertificate (✓ std3).

Source. Repository-derived.

Commentary.

No floating acceptance tolerance or exhaustive Boolean search is used by the checker.

Theorem 1.6 (Acceptance reflection).

$$\forall Vertex,capacity,source,sink,certificate,((\mathrm{checkSTCutCertificate}(capacity,source,sink,certificate))=(true))\iff (\mathrm{ValidSTCutCertificate}(capacity,source,sink,certificate))$$

Proof. Machine-checked in Lean as D5/S0/Certificates/RationalSTCutCertificate.checkSTCutCertificate_eq_true_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

Connects Boolean acceptance to the exact finite arithmetic contract.

Theorem 1.7 (Conservation across any cut).

$$\forall Vertex,certificate,side,(\forall i,((\mathrm{fromSource}(certificate,i))+(\sum _j(\mathrm{internal}(certificate,j,i))))=((\mathrm{toSink}(certificate,i))+(\sum _j(\mathrm{internal}(certificate,i,j)))))\Rightarrow ((\mathrm{flowValue}(certificate))=((\sum _i(\mathrm{ite}(\mathrm{apply}(side,i),\mathrm{toSink}(certificate,i),\mathrm{fromSource}(certificate,i))))+(\sum _i(\sum _j((\mathrm{internal}(certificate,i,j))\cdot ((\mathrm{ite}(\mathrm{apply}(side,i),1,0))-(\mathrm{ite}(\mathrm{apply}(side,j),1,0))))))))$$

Proof. Machine-checked in Lean as D5/S0/Certificates/RationalSTCutCertificate.flow_cut_accounting (✓ std3). ∎

Source. Repository-derived.

Commentary.

Only flow conservation is required by this identity. Opposite directed terms cancel when summing over all vertices.

Theorem 1.8 (Global weak flow-cut duality).

$$\forall Vertex,capacity,source,sink,certificate,side,((\forall i,j,((0)\le (\mathrm{internal}(certificate,i,j)))\wedge ((\mathrm{internal}(certificate,i,j))\le (\mathrm{capacity}(i,j))))\wedge (\forall i,(\mathrm{fromSource}(certificate,i))\le (\mathrm{source}(i)))\wedge (\forall i,(\mathrm{toSink}(certificate,i))\le (\mathrm{sink}(i)))\wedge (\forall i,((\mathrm{fromSource}(certificate,i))+(\sum _j(\mathrm{internal}(certificate,j,i))))=((\mathrm{toSink}(certificate,i))+(\sum _j(\mathrm{internal}(certificate,i,j))))))\Rightarrow ((\mathrm{flowValue}(certificate))\le (\mathrm{stCutValue}(capacity,source,sink,side)))$$

Proof. Machine-checked in Lean as D5/S0/Certificates/RationalSTCutCertificate.flowValue_le_every_cut (✓ std3). ∎

Source. Repository-derived.

Commentary.

The lower bound covers every cut, including those never visited by a solver.

Theorem 1.9 (Attained minimum certificate).

$$\forall Vertex,capacity,source,sink,certificate,((\mathrm{checkSTCutCertificate}(capacity,source,sink,certificate))=(true))\Rightarrow (((\mathrm{stCutValue}(capacity,source,sink,\mathrm{side}(certificate)))=(\mathrm{flowValue}(certificate)))\wedge (\forall side,(\mathrm{flowValue}(certificate))\le (\mathrm{stCutValue}(capacity,source,sink,side))))$$

Proof. Machine-checked in Lean as D5/S0/Certificates/RationalSTCutCertificate.checkSTCutCertificate_sound (✓ std3). ∎

Source. Repository-derived.

Commentary.

A single accepted pair proves that its cut is a global minimum; no optimal flow premise or algorithmic discovery theorem is assumed.

References

• Truth anchor: D5/S0/Certificates/RationalSTCutCertificate.STCutCertificate
• Truth anchor: D5/S0/Certificates/RationalSTCutCertificate.ValidSTCutCertificate
• Truth anchor: D5/S0/Certificates/RationalSTCutCertificate.checkSTCutCertificate
• Truth anchor: D5/S0/Certificates/RationalSTCutCertificate.checkSTCutCertificate_eq_true_iff
• Truth anchor: D5/S0/Certificates/RationalSTCutCertificate.checkSTCutCertificate_sound
• Truth anchor: D5/S0/Certificates/RationalSTCutCertificate.flowValue
• Truth anchor: D5/S0/Certificates/RationalSTCutCertificate.flowValue_le_every_cut
• Truth anchor: D5/S0/Certificates/RationalSTCutCertificate.flow_cut_accounting
• Truth anchor: D5/S0/Certificates/RationalSTCutCertificate.stCutValue
• Dependency: D5/S0/Certificates/LinearObjectiveDual