Guided Labs

Download the offline combinatorics and graph kit. Extract it and work inside combinatorics-graphs. Python 3.10+ and the standard library suffice. The README specifies inputs, bounds, ordering and error behavior.

python check.py starter
python run_labs.py starter

The unfinished starter fails intentionally. Implement the eight contracts before consulting reference.py; use python check.py reference to calibrate afterward. Save a hand-derived fixture, first attempt, general argument, failing test and changed-assumption result in the evidence template.

Lab	Implementations	Proof obligation	Planning time
1	Bounded distributions, onto maps	Disjoint last-coordinate cases; inclusion-exclusion with empty functions	4–6 h
2	No-adjacent-one words, coin coefficients	State/base definitions; ordered versus unordered construction	4–6 h
3	Graph report, walk-count matrix	Components and bridge deletion; walk decomposition by last edge	4–6 h
4	Proper-coloring count, maximum matching	Exhaustive coverage; valid witness plus a matching upper bound	4–6 h

All graph vertices, including isolates, are explicit. The graph reporter classifies Euler existence but does not return a route. Proper coloring uses labeled colors; the matching report includes a left subset and its neighborhood certifying its optimal size. Explain each output without running the code.

The independent checks enumerate small objects, cycles, walks and edge trails; coloring counts are cross-checked with inclusion-exclusion on monochromatic edges, and matching optima with subsets of edges. These checks establish finite evidence, not a general theorem. No planarity or Hamilton solver is included: those lessons require proofs, drawings or explicitly verified witnesses.

The demonstration is a worked version of the workshop project. Attempt its model and numerical predictions before reading that implementation.