W1.3: MILP scheduling backend (E4) with formal liveness and slot-reuse validation

[AtlantisPleb]

Workstream W1 deliverable 3 of the unified research plan
(openagents docs/tassadar/RESEARCH_PLAN.md); phase E4 of the original
design (docs/tassadar/2026-06-10-psionic-alm-compiler-design-speculation.md),
the one phase of that design still unlanded.

Scope

1. A Mixed-Integer Linear Program scheduler for the four-phase layer
   structure: decision variables assign each gate to layer/phase;
   constraints encode precedence, type compatibility (LookUp→attention,
   ReGLU→FFN), and co-location; objective fits a layer budget while
   minimizing peak simultaneous liveness (which determines d_model).
   Reference: transformer-vm scheduler/.
2. Formal validation of liveness intervals and slot reuse — prove every
   stale-slot subtraction is present and no live value is overwritten —
   as an independent checker alongside the existing allocator-safety
   check in the bounded harness.
3. Width/depth/token-rate deltas reported against the greedy
   interval-coloring baseline (tassadar_alm_backend.rs) on
   profile-versioned benchmarks, including the branch-capable
   interpreter graph.

Honest framing (from the plan)

Plausibly vanity at current scale — the design doc says so — but H4's
module economics change if compiled modules are materially narrower, and
the formal-validation half is a deliverable regardless of the solver
outcome. Scope-bound per the external analysis's warning: restrict to
versioned benchmarks; do not let compiler engineering consume the agenda.

Acceptance

MILP schedule achieving d_model parity-or-better versus greedy on the
interpreter graph, solver verdict cross-checked, formal checker green on
every committed workload, deltas published in the lane docs.