Combinatorics / CONCEPT
PositiveCircuitSupplier
The exact supplier exists_simpleSignedCircuit_decomposition is retained from Maths/Multitubes/Additive/CirculationDecomposition.lean at elazarg/multitubes commit 20d22aa7ca67f9843e5adf9edf173403a2f4033a. A normalized nonnegative real signed-incidence certificate has a finite convex decomposition into simple circuits, with exact coordinate reconstruction. This does not itself supply a greedy support-decreasing certificate; that certificate is proved in LayeredFlow. Copyright, the upstream license notice, full Apache-2.0 text and the retirement condition against this repository pinned mathlib are in the Lean sources.
sum edgeMultiplicity eq length
RELATIONSHIP ATLAS
Every connection, in context.
Certified topology / UPSTREAM
Prerequisites
Certified topology / DOWNSTREAM
Consequences
RELATED KNOWLEDGE
Structural connections
- Finite Farkas Alternativesstructural-affinity · Closed
- LayeredFlowstructural-affinity · Closed
- LocalOptimumstructural-affinity · Closed
- Minimum directed-cycle mean and zero-temperature pressurestructural-affinity · Closed
- Refuting the binary detection threshold conjecturestructural-affinity · Closed
- SupplierDualstructural-affinity · Closed
- SupplierGraphstructural-affinity · Closed
- The labelled circle action and balanced negative incidencestructural-affinity · Closed
Documents & exposition
None recorded in this release.
Other authored & advisory relationships
None recorded in this release.
LIBRARY / RELEASE VERSIONS
Content history
Certified provenance