proof: sweep stall ladder windows and retention

[Abdk4Moura]

Update the merged stall-ladder model to avoid circularly naming an outcome-based measurement.

• Sweep transient windows of 0.5, 1, 2, 3, and 5+ rungs.
• Evaluate fail-fast and preserve-state candidates for each window.
• Make retention boundedness explicit; unbounded preserve-state is marked unsafe.
• Report the divergence band: bounded retention diverges for 0.5-5 rungs; unbounded retention makes preserve-state unsafe.
• Print the retention precondition: if retention cannot be bounded, condition measurement is unnecessary and fail-fast wins by default; if bounded, condition measurement remains worth taking.
• Inventory current retention candidates in proofs/README.md as BOUNDED TODAY, BOUNDABLE, or NOT OURS TO BOUND.
• Close the ICE/conntrack half of feat: Windows warm-path parity via named-pipe ControlChannel (needs design repair) #63 using host-specific sysctl arithmetic: nf_conntrack_udp_timeout=30s for UNREPLIED, nf_conntrack_udp_timeout_stream=120s for ASSURED, and 5 ladder rungs = 75s. fix: linux-gate warm_all integration test (macOS hyperkit limitation) #50 observed UNREPLIED entries and no reply, so they cannot become ASSURED and expire before rung 3. This does not close QUIC fd/port or fix: signalling reliability + web time-to-connect #31 transport-level data-freeze cases. The values are operator-configurable and explicitly labeled as host-specific.
• Replace the separating measurement with direct condition instrumentation: when ICE becomes usable and when conntrack reappears, not when the file arrives.
• Keep Gate 0 and source coherence unchanged.

Verification: python3 proofs/stall_ladder_model.py, python3 -m py_compile proofs/stall_ladder_model.py, and git diff --check pass. No build required.