# All four cuts and an equal-value two-sided certificate

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-max-flow-min-cut-theorem/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-max-flow-min-cut-theorem-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Enumerate every s-t cut of a four-vertex network and give a feasible flow of value 5 together with a cut of capacity 5.

A complete finite certificate, without augmenting-path correctness, integrality or a general theorem from instances.





## Givens and symbols


- algebra
- sets
- flow_def
- cut_def


- G1 — V={s,a,b,t}; edges sa,sb,ab,at,bt,ba in that order have capacities (3,2,1,2,3,1) and flows (3,2,1,2,3,0).


- S^c — cut complement relative to V
- c(S) — outgoing-only cut capacity





## Rules and sources


- mko_definition · cited — Enumerate each vertex subset S containing the source and excluding the sink. Its capacity sums only directed edges from S to its complement; incoming edges are not counted. Every feasible flow value is at most every cut capacity. Complete cut enumeration determines the minimum cut. If a feasible flow and a cut have equal values, this bound immediately certifies both a maximum flow and a minimum cut. An arbitrary feasible flow or single cut is not automatically optimal. This slice does not claim integral flow, an augmenting-path algorithm proof or a general theorem proof from finitely many instances. · mko-max-flow-min-cut-theorem
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- sets · prerequisite — Compute unions, intersections, complements, inclusion and preimages element by element.
- flow_def · prerequisite — A finite simple directed network has no self-loop or duplicate ordered pair, but permits antiparallel edges; feasible flows satisfy every capacity bound and internal conservation, with value equal to source net outflow and sink net inflow.
- cut_def · prerequisite — A legal s-t cut is a vertex subset S containing s and excluding t; its capacity sums only directed capacities from S to its complement.





## Main derivation

S01 · impliesBefore

E=\{sa,sb,ab,at,bt,ba\},\quad c=(3,2,1,2,3,1)

After

\text{all edges loop-free and unique},\quad0\le f\le c

Conditions: none

Rule: flow_def · Uses: G1

Leaf basis: flow_def

All six directed pairs are unique and loop-free, antiparallel edges are legal, and every flow obeys its capacity.



S02 · impliesBefore

\operatorname{in}(a)=3+0,\quad\operatorname{in}(b)=2+1

After

\operatorname{out}(a)=1+2=3,\quad\operatorname{out}(b)=3+0=3

Conditions: none

Rule: algebra · Uses: G1, S01

Leaf basis: algebra

Both internal vertices conserve flow, qualifying the flow as feasible.



S03 · impliesBefore

|f|=f_{sa}+f_{sb}=3+2

After

|f|=5=f_{at}+f_{bt}=2+3

Conditions: none

Rule: algebra · Uses: G1, S02

Leaf basis: algebra

Source and sink net values agree.



S04 · definitionBefore

s\in S,\quad t\notin S

After

S\in\{\{s\},\{s,a\},\{s,b\},\{s,a,b\}\}

Conditions: none

Rule: cut_def · Uses: G1

Leaf basis: cut_def

a,b may independently belong to S, giving exactly four subsets without confusing complementary sides.



S05 · impliesBefore

|h|=\sum_{e:S\to S^c}h_e-\sum_{e:S^c\to S}h_e\quad(h\text{ feasible})

After

|h|\le\sum_{e:S\to S^c}h_e\le\sum_{e:S\to S^c}c_e=c(S)

Conditions: h\text{ feasible},\ s\in S,\ t\notin S

Rule: algebra · Uses: S01, S02, S04

Leaf basis: algebra

Sum divergences over S: internal edges cancel, leaving cut net flow. Nonnegative incoming flow and capacities give the bound for every feasible flow.



S06 · impliesBefore

c(\{s\}),c(\{s,a\}),c(\{s,b\}),c(\{s,a,b\})

After

3+2=5,\quad2+1+2=5,\quad3+3+1=7,\quad2+3=5

Conditions: none

Rule: algebra · Uses: G1, S04

Leaf basis: algebra

Count only outgoing edges. For {s,a}, ba is incoming and excluded; for {s,b}, ba is outgoing and contributes one.



S07 · impliesBefore

\{c(S):s\in S,t\notin S\}=\{5,5,7,5\}

After

\min_S c(S)=5\text{ attained at }S=\{s\}

Conditions: none

Rule: algebra · Uses: S04, S06

Leaf basis: algebra

The complete list has minimum five, attained by the source-singleton cut.



S08 · impliesBefore

|f|=5=c(\{s\})

After

f\text{ maximum},\quad\{s\}\text{ minimum cut},\quad\max|h|=\min c(S)=5

Conditions: none

Rule: algebra · Uses: S03, S05, S07

Leaf basis: algebra

Every feasible h is bounded by the cut's five and f attains it; every cut is at least f's value, certifying both sides optimal.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S03, S05, S07 — This is an equal-value certificate for the supplied finite network, not an algorithm or general integral-flow claim.
- S07 · premise_audit · S04, S06 — A lone cut of capacity five would not prove minimality; the complete table or weak bound is needed.
- S06 · premise_audit · G1, S04 — All four cuts are computed with directions explicitly checked.
- S05 · premise_audit · S01, S02, S04 — The weak bound applies to arbitrary h, not only the candidate f, enabling optimality.
- S04 · premise_audit · G1 — The fixed membership of s,t leaves exactly 2^2 choices.
- S03 · premise_audit · G1, S02 — Every internal conservation check precedes the endpoint value computation.
- S02 · premise_audit · G1, S01 — ba is retained in a's inflow and b's outflow.
- S01 · premise_audit · G1 — Network qualification and per-edge feasibility come first.





## Error controls and negative controls

Cut directionCount only S to its complement, not incoming edges.

Arbitrary competing flowThe weak bound must cover every feasible h to prove a maximum.


- Add capacities in both cut directions. → reject — ba is incoming for the {s,a} cut and must be excluded.
- Any feasible flow is maximum. → reject — This proof certifies a candidate only when it attains the cut weak bound.
- This instance proves every augmenting-path algorithm correct. → reject — No algorithm or general termination proof is provided.





## Result and limitations

Maximum flow and minimum cut both have value five; all four cut capacities are 5,5,7,5.







## Verification and source binding

2 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: a3f6ca7038c79f9eea7d99baeadfe28a147465af5256279afd33c427ad4be560
- original source SHA-256: 05cf7399183d2ca5c249a6bc36b388edd4cd3634a6674052196c12852140714a
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-max-flow-min-cut-theorem-01.json)