From f952d4cf034d55950295b17a9c5f6c44b943d9f0 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sun, 26 Apr 2026 01:45:13 +0200
Subject: [PATCH] fix(proofs): use /- ... -/ block comment to match RTA.lean
 style
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Lean 4.29.0-rc6 rejects `import` after a `/-! ... -/` module-docstring
in this file's pattern, even though Mathlib uses module docstrings
throughout — likely an interaction with the closing `-/` being on the
same line as content text. The other working files in this directory
(RTA.lean, RMBound.lean, EDF.lean) all use a regular `/- ... -/`
block comment with the closing `-/` on its own line, so we match that
style.

#159 (the previous import-order fix) addressed the structural ordering
but introduced the `/-!` form. CI surfaced that in #151's first run
that actually reached our in-tree files via mathlib-cache.

Body unchanged. Format-only edit.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 proofs/Proofs/Scheduling/RTAJittered.lean | 67 ++++++++++++-----------
 1 file changed, 34 insertions(+), 33 deletions(-)

diff --git a/proofs/Proofs/Scheduling/RTAJittered.lean b/proofs/Proofs/Scheduling/RTAJittered.lean
index 34547e4..73677c5 100644
--- a/proofs/Proofs/Scheduling/RTAJittered.lean
+++ b/proofs/Proofs/Scheduling/RTAJittered.lean
@@ -1,36 +1,37 @@
-/-! # Jittered Response Time Analysis — convergence theorems
-
-Mirrors `compute_response_time_jittered` in
-`crates/spar-analysis/src/scheduling_verified.rs` (PR #147).
-The Rust implementation is checked against this spec via property tests
-in that file's `#[cfg(test)] mod tests`.
-
-Reference: Tindell & Clark, "Holistic schedulability analysis for
-distributed hard real-time systems", Microprocessing & Microprogramming,
-1994.  Joseph & Pandya 1986 for the un-jittered baseline.
-
-We extend the RTA recurrence in `RTA.lean` with three new ingredients:
-  1. The task under analysis has a release jitter `J_i` added as a
-     constant offset to its response window.
-  2. Each higher-priority task `j` has its own release jitter `J_j`
-     which inflates the ceiling count: ⌈(R + J_j) / T_j⌉ × C_j.
-  3. Periodic ISR overhead enters as an extra monotone term
-     `IsrOverhead : Nat → Nat`.
-
-Recurrence:
-
-  R(0)   = C_i + J_i
-  R(n+1) = C_i + J_i
-         + Σ_j ⌈(R(n) + J_j) / T_j⌉ × C_j
-         + IsrOverhead(R(n))
-
-When all `J_j = 0`, `J_i = 0`, and `IsrOverhead = fun _ => 0`, this
-reduces to `Spar.Scheduling.RTA.rtaStep` modulo packaging.
-
-This file states the theorems anchoring the Rust implementation in
-`compute_response_time_jittered`.  Convergence is established under
-the same termination argument as the un-jittered case — monotone
-non-decreasing sequence bounded by the deadline. -/
+/-
+  Jittered Response Time Analysis — Fixed-Point Convergence
+
+  Mirrors `compute_response_time_jittered` in
+  `crates/spar-analysis/src/scheduling_verified.rs` (PR #147).
+  The Rust implementation is checked against this spec via property tests
+  in that file's `#[cfg(test)] mod tests`.
+
+  Reference: Tindell & Clark, "Holistic schedulability analysis for
+  distributed hard real-time systems", Microprocessing & Microprogramming,
+  1994.  Joseph & Pandya 1986 for the un-jittered baseline.
+
+  We extend the RTA recurrence in `RTA.lean` with three new ingredients:
+    1. The task under analysis has a release jitter `J_i` added as a
+       constant offset to its response window.
+    2. Each higher-priority task `j` has its own release jitter `J_j`
+       which inflates the ceiling count: ⌈(R + J_j) / T_j⌉ × C_j.
+    3. Periodic ISR overhead enters as an extra monotone term
+       `IsrOverhead : Nat → Nat`.
+
+  Recurrence:
+    R(0)   = C_i + J_i
+    R(n+1) = C_i + J_i
+           + Σ_j ⌈(R(n) + J_j) / T_j⌉ × C_j
+           + IsrOverhead(R(n))
+
+  When all `J_j = 0`, `J_i = 0`, and `IsrOverhead = fun _ => 0`, this
+  reduces to `Spar.Scheduling.RTA.rtaStep` modulo packaging.
+
+  This file states the theorems anchoring the Rust implementation in
+  `compute_response_time_jittered`.  Convergence is established under
+  the same termination argument as the un-jittered case — monotone
+  non-decreasing sequence bounded by the deadline.
+-/
 
 import Mathlib.Tactic
 import Proofs.Scheduling.RTA