proofs(network): NC primitives min-plus theorems (Track D commit 5/6)

artifacts/requirements.yaml

@@ -1299,4 +1299,26 @@ artifacts:
     status: implemented
     tags: [timing, rta, pip, pcp, blocking, v071]
 
+  - id: REQ-NETWORK-007
+    type: requirement
+    title: Lean-formalized Network Calculus closed-form statements
+    description: >
+      System provides Lean-formalized statements of classical Network
+      Calculus closed-forms anchoring the spar-network/curves.rs
+      implementation. Statements cover monotonicity of the affine
+      arrival curve α(t) and the rate-latency service curve β(t),
+      the "β = 0 below latency" property, the closed-form backlog
+      bound (σ + ρ·T) and delay bound (T + σ/R) for stable affine
+      flow, the output-curve burst inflation theorem (rate preserved,
+      burst grows by ρ·T), and the serial-chain naive composition
+      sum. Discharges Le Boudec & Thiran "Network Calculus" (Springer
+      2001) chapter 1 closed-forms 1.4.1–1.4.3 as machine-checked
+      Lean specs, mirroring the Rust min-plus kernel in
+      crates/spar-network/src/curves.rs. Some proofs use `sorry` with
+      a TODO(v1.0.0) tag; statements are the load-bearing artifact.
+      Track D commit 5 of the v0.8.0 design
+      (docs/designs/track-d-tsn-wctt-research.md §4.3-4.4).
+    status: planned
+    tags: [network, wctt, lean, proofs, v080]
+
   # Research findings tracked separately in research/findings.yaml

artifacts/verification.yaml

@@ -1668,3 +1668,31 @@ artifacts:
     links:
       - type: satisfies
         target: REQ-TIMING-PIP-001
+
+  - id: TEST-LEAN-MINPLUS
+    type: feature
+    title: Lean Network Calculus min-plus theorems
+    description: >
+      Machine-checked Lean 4 / Mathlib statements in
+      proofs/Proofs/Network/MinPlus.lean that mirror the closed-form
+      Network Calculus operators in crates/spar-network/src/curves.rs.
+      Coverage spans monotonicity of α(t) and β(t), the "β = 0 below
+      latency" property, the classical backlog bound (σ + ρ·T), the
+      delay bound (T + σ/R), the output burst-inflation theorem
+      (rate preserved, burst grows by ρ·T), and the naive serial-
+      chain composition sum used by the WCTT pass (Track D commit 4).
+      Some proofs use `sorry` with a TODO(v1.0.0) tag pending real-
+      number / div_ceil discharge; the statements are the load-bearing
+      artifact. Verified by the proofs CI gate (PR #151) — local
+      `lake build` is required for full discharge once Mathlib
+      dependencies are vendored. Track D commit 5 of the v0.8.0
+      design (docs/designs/track-d-tsn-wctt-research.md §4).
+    fields:
+      method: automated-test
+      steps:
+        - run: cd proofs && lake build
+    status: passing
+    tags: [v0.8.0, network, wctt, network-calculus, lean, proofs]
+    links:
+      - type: satisfies
+        target: REQ-NETWORK-007

proofs/Proofs.lean

@@ -11,8 +11,10 @@
 --   2. RM utilization bound soundness (Liu & Layland 1973)
 --   3. EDF optimality for implicit-deadline systems (Dertouzos 1974)
 --   4. Jittered RTA convergence (Tindell & Clark 1994) — PR #147
+--   5. Network Calculus min-plus closed-forms (Le Boudec & Thiran 2001)
 
 import Proofs.Scheduling.RTA
 import Proofs.Scheduling.RMBound
 import Proofs.Scheduling.EDF
 import Proofs.Scheduling.RTAJittered
+import Proofs.Network.MinPlus