docs: DSLTrans cutoff analysis + Forge protocol + v0.9.x milestone draft

[avrabe]

Summary

Three docs-only deliverables wrapping the v0.9.x cycle:

• docs/research/cutoff-theorem-modal-filtering.md (~1900 words) — applies Lucio's Cutoff Theorem (arXiv 2604.18792) to spar's modal filter (crates/spar-analysis/src/modal.rs). Derives K_filter = 1 + max(C, E) for the positive existence property "every element declared in modes (s) is preserved in the SOM-projection". Worked K=3 estimate on test-data/parser/modes_test.aadl. Discharge plan (Kani harness vs capped proptest). Honest about gaps: negative properties, cartesian-product SOM enumeration, fixed-point downstream passes (RTA/WCTT), mode reachability — the theorem does not compose through any of those.
• docs/research/forge-replication-protocol.md (~1700 words) + docs/research/forge-replication/ scaffold (descriptor.sexp, descriptor.aadl, tasks.json with 24 paired tasks pinned to bad85e6, run_trial.sh driving claude --print --output-format stream-json, empty RESULTS.md template) — mirrors Jin et al. (arXiv 2604.13108) for a self-target replication on spar. Pre-registration discipline; no numbers reported — protocol only.
• docs/blog/v0.9.x-milestone.md (~1600 words) — recaps v0.9.0..v0.9.3 (MCP + spar-insight; gPTP ε + frame quantization; RTA→WCTT coupling, Context_Switch_Time, sensitivity, ARINC severity; piecewise-affine arrival curves + PMOO/LUDB) and previews v0.10.x trace-topology (4 parsers all landed, 5 deterministic checks, v1 contract URL https://pulseengine.eu/spar-trace-topology/v1). 5/5 reviewer NC top-5 items closed across v0.9.1–v0.9.3.

Every claim about spar's code cites file:line. Every claim about the papers references the arXiv ID + section. No code under crates/ modified.

Test plan

• CI green (docs-only — no Rust/Lean compilation involved).
• Internal markdown links resolve: docs/blog/v0.9.x-milestone.md → CHANGELOG anchors + ../research/*.md + ../designs/v0.10.0-trace-topology.md; docs/research/forge-replication/RESULTS.md → ../forge-replication-protocol.md.
• chmod +x docs/research/forge-replication/run_trial.sh (the chmod was denied during agent execution; the file is functional via bash run_trial.sh).
• Manual review of word counts — D1=1924, D2=1718, D3=1568.
• Forge replication trials are out-of-scope for this PR — they land later when someone drives the scaffold and fills RESULTS.md.

🤖 Generated with Claude Code

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!