Proof of `Deterministic undirected product flow–cut algorithm`
groundedproofs/Lax455465Proofs/ProductCorollaries.lean · lax-455465
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Specialize the general algorithm to undirected input words and symmetric capacities. The program, resource bounds and joint output are unchanged.
Proof strategy
Apply the general certificate guarantee with the undirected mode. The symmetry implication is discharged by the input's symmetry hypothesis.