[Tristan-Stoltz-ERC]

Summary

Adds a bounded exact packing solver stacked on PR #2718 and PR #2717.

Paradigm shift: proof-carrying outcome semantics

The solver deliberately distinguishes:

• Feasible: a complete layout was found in the declared finite model;
• ProvenInfeasible: every candidate branch was exhausted for this model;
• BudgetExceeded: the solver stopped before it could find a layout or exhaust the search.

It uses deterministic minimum-remaining-values (MRV) branching rather than relying only on request order, with y-major/x-major candidate order and stable tie breaks. The search is limited to four requests and yards no larger than 5x5 integer placement units. Out-of-scope inputs and geometry errors fail closed.

Frozen greedy-failure benchmark

In a 4x4 yard, two 1x1 squares followed by a 1x3 bar are a constructed counterexample for the first-fit ordering. Exact-polygon first-fit places the squares at (0,0) and (2,0), then leaves the bar unplaced. MRV exact search can fit all three by placing the bar at (0,0) and the squares at (2,0) and (2,2). A separate integer-cell and boundary-contact oracle checks the returned layout.

This is a deterministic completeness demonstration, not a runtime or industrial-quality claim. An independent finite-grid reference calculation reproduced the intended positions. The exact-head Rust suite remains the authoritative confirmation.

Other conformance targets

• Prove that two 2x2 square blocks cannot both fit in a 2x2 yard under the fixed-orientation/contact-as-conflict model.
• Return BudgetExceeded after a one-candidate-check budget instead of relabeling search exhaustion as infeasibility.
• Reject out-of-scope yard size, more than four requests, duplicate IDs and a zero evaluation budget.

Engineering

Dependency-only links to the polygon geometry and first-fit baseline prototypes; no third-party runtime. Rust 1.96 formatting, offline tests and Clippy-with-warnings-denied gates are included.

Verification boundary

No local Rust toolchain was available for this authoring session. Keep this draft until the exact-head format/test/Clippy workflows pass. The mathematical proof, if confirmed by implementation, applies only to fixed-orientation polygon footprints on the finite integer translation grid, with the declared yard bounds and boundary-contact policy.