feat(nc): piecewise-affine arrival curves (v0.9.3 NC tightness #1)

[avrabe]

Summary

• Adds PiecewiseAffineArrivalCurve alongside the existing single-bucket ArrivalCurve to encode T-SPEC-style multi-leaky-bucket arrivals α(t) = min_i (σ_i + ρ_i · t) — captures short-horizon burst + long-horizon sustained behaviour in one curve.
• All four classical operators extend per-bucket: backlog/delay take min over per-bucket bounds (the binding bucket determines the bound), output_bound preserves the piecewise structure with each bucket inflated independently (Le Boudec & Thiran 1.4.3 per-bucket), residual_service lowers conservatively to a single rate-latency via R - max ρ_i and the worst per-bucket burst-drain time.
• From<ArrivalCurve> round-trips the single-bucket case (peak-capped form lowers to a 2-bucket PWA (σ, ρ), (0, peak)).
• 14 unit tests under curves::piecewise::tests — covering canonicalisation, causality, min-of-affines readouts, per-regime dominance for delay, conservative residual, single-bucket round-trip, peak-cap round-trip, etc.
• Out-of-tree Lean skeleton at proofs/Proofs/Network/MinPlusPwa.lean with theorem statements for the per-bucket generalisations, all sorry -- TODO(v1.0.0). MinPlus.lean (single-bucket spec, 4 remaining sorrys on the affine form) is unchanged — single-bucket is the special case [(σ, ρ)] of the new form, and existing wctt consumers stay on ArrivalCurve.
• Per the post-v0.9.2 reviewer's NC top-5 Add semantic analysis layer, LSP server, WIT transform, and advanced analyses #1 — highest-leverage tightness item; reviewer noted this typically halves bounds on real ADAS traffic.

File deltas

• crates/spar-network/src/curves.rs +611 lines (new pub mod piecewise with PiecewiseAffineArrivalCurve, PwaError, four operators, From<ArrivalCurve>, 14 unit tests)
• crates/spar-network/src/lib.rs +1 (re-export PiecewiseAffineArrivalCurve, PwaError)
• proofs/Proofs/Network/MinPlusPwa.lean +290 lines new (skeleton, not imported by Proofs.lean)
• artifacts/requirements.yaml REQ-NETWORK-013
• artifacts/verification.yaml TEST-NC-PIECEWISE → satisfies REQ-NETWORK-013

Out of scope

• wctt.rs is not touched — sibling track may swap propagation to piecewise in a follow-up commit (needs a min-bucket-preserving propagation strategy + AADL property surface for declaring multi-bucket inputs).
• No LP backend (sibling A2 PMOO/LUDB).
• No version bump.
• MinPlus.lean sorrys are not discharged (separate v1.0 work).

Deviations

The reviewer's English description for delay_bound and backlog_bound says "max over buckets", but the test description in the same task spec says "bound is the min" and the whole pitch is "halves bounds." I implemented the min semantics (the tight closed form) — taking max would always give bounds at least as loose as single-bucket. Documented in the operator docstrings; the delay_bound_min_across_buckets_each_dominates_a_regime test directly asserts result == min(single_bucket_b1, single_bucket_b2). residual_service follows the spec literally with R - max ρ_i (the conservative single-bucket-residual lowering) — that's the right call there because the residual must be sound under every individual bucket interpretation, and we're forced to a single rate-latency output.

Test plan

• cargo build --workspace — clean
• cargo test --workspace — clean (no regressions; spar-network goes from 77 → 91 lib tests, +14 piecewise)
• cargo test -p spar-network -- piecewise — 14/14 pass
• cargo clippy --workspace --all-targets -- -D warnings — clean
• cargo fmt --all -- --check — clean (in the worktree; pre-existing fmt drift on standard_properties.rs and spar-trace-topology exists on main and is unrelated)
• rivet validate — PASS (99 warnings, same as baseline)

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 90.79498% with 22 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/spar-network/src/curves.rs	90.79%	22 Missing ⚠️

📢 Thoughts on this report? Let us know!