Lab041: remove non-modelled metrics and cite value sources

Audit found seven numbers in simulate_trial that were neither modelled by
Lab041 nor traceable to their claimed source. Video fraction 0.910 did not
match Lab040 (0.9603); base queue length 31 did not match Lab040 (36-38).

- drop video/telemetry/control delivered fractions and queue length: these
  belong to Lab037 and Lab040 and are not modelled here
- drop lab041_traffic_impact.png, which plotted only those metrics
- drop negative_speed_cases and speed_limit_exceeded_cases, never computed,
  along with the tautological asserts that checked them
- bind braking parameters to the Lab039 nominal profile via named constants
  instead of the literals 0.250 and the divisor 6.0
- cite Lab038 as the source of the transferred video and telemetry loads
- rewrite the invariants section: nine architecture-derived properties now
  carry functional-check references, five unmeasurable ones move to their
  own section
- extend check 04 with negative speed and the 15 m/s boundary
- state explicitly what the matrix rolls, what the architecture fixes and
  what is not modelled at all

Regenerated: 180 combinations, 24/24 checks, five CSV and seven PNG.
Six columns removed, no retained value changed.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

data/processed/lab041/lab041_report.txt

@@ -57,6 +57,10 @@ Lab041 — сеансы связи, безопасный запуск и защ
 Ограничение модели
 - Исследуются задержки, дубликаты, перестановка, старые пакеты и потеря оперативного состояния при перезапуске.
 - Намеренная подделка не моделируется. Идентификаторы сеанса не доказывают отправителя, поэтому эта защита не заменяет криптографическую аутентификацию.
+- Что именно моделируется розыгрышем: моменты потерь по экспоненциальной модели Good-Bad, доставка и повтор служебных сообщений сеанса, время до безопасного согласования и до разрешения движения, объём эпизодической служебной нагрузки. Только эти величины являются результатом моделирования Lab041.
+- Что задано архитектурой, а не разыгрывается: исход обработки старого пакета, разрешено ли движение после перезапуска и сохраняется ли аварийное намерение. Матрица перебирает эти случаи, а поведение реализации проверяется отдельно функциональными проверками.
+- Что не моделируется вовсе: транспорт видео, планировщик очередей, доставка телеметрии и доставка команд по радиоканалу. Соответствующие показатели относятся к Lab037 и Lab040 и в Lab041 не пересчитываются.
+- Оценка пути после перезапуска получена по замкнутой формуле при параметрах профиля nominal Lab039 и одинакова во всех повторах; это расчёт, а не результат розыгрыша.
 
 Матрица 180 сочетаний
 архитектура | канал | сценарий | повторы | безопасный сеанс, % | разрешение, % | нарушения, % | старые пакеты приняты, % | потеря намерения, % | управление, кбит/с | эпизодическая служебная, кбит/с | полный поток, кбит/с
@@ -244,10 +248,13 @@ Lab041 — сеансы связи, безопасный запуск и защ
 Перезапуски и безопасное состояние
 - В основном режиме движение до синхронизации: 0; до подтверждения разрешения: 0; без новой команды оператора: 0.
 - Максимальный путь после перезапуска в основном режиме: 9.7737 м; это путь безопасного торможения, а не продолжение старой команды.
+- Величина рассчитана по формуле v*t + v^2/(2a) при v = 6.9444 м/с, t = 0.250 с и a = 3.0 м/с^2 из профиля nominal Lab039. Оценка одноступенчатая и не учитывает предварительное замедление Stage1, поэтому она консервативнее двухступенчатой модели Lab039.
 - Продолжение движения после перезапуска: 0; запуск по старой команде: 0.
 
 Пакеты предыдущего сеанса
 - Основной режим: введено 2807, отклонено 2807, ошибочно принято 0.
+- Эти числа получены перебором таблицы сценариев: семь сценариев со старым пакетом умножаются на число повторов, а исход перебора задан архитектурой, а не розыгрышем помех. Они показывают охват перебора, а не измеренную вероятность отклонения.
+- Что старый пакет действительно отклоняется реализацией, показывают проверки 06, 07, 08, 10 и 19: они вызывают receive_control и receive_reset настоящих автоматов и сверяют причину отказа.
 - Отрицательный уровень без идентификаторов: ошибочно принято 2807 старых пакетов.
 - Причины отказа основного режима: сеанс станции=401, запуск ровера=401, период управления=401, номер сообщения=802, событие аварии=401, запрос сброса=401.
 - Неоднозначных delta=2^31 отклонено: 401.
@@ -259,20 +266,24 @@ Lab041 — сеансы связи, безопасный запуск и защ
 - Потеря EMERGENCY_ACK не снимает аварийное намерение; потеря RESET_ACK вызывает повтор того же идемпотентного запроса.
 
 Инварианты безопасности основного режима
-- Движение до синхронизации: 0.
-- Движение до подтверждения разрешения: 0.
-- Движение без новой команды оператора: 0.
-- Принятие команды старого сеанса станции: 0.
-- Принятие команды старого запуска ровера: 0.
-- Использование старого периода управления: 0.
-- Снятие аварийной фиксации обычной командой: 0.
-- Потеря аварийного намерения после перезапуска станции: 0.
-- Движение до подтверждения сброса: 0.
-- Автоматическое восстановление старой команды после сброса: 0.
-- Принятие старого запроса сброса: 0.
-- Принятие неоднозначного номера: 0.
-- Отрицательная скорость: 0.
-- Превышение разрешённой скорости: 0.
+- Что означают числа ниже. Счётчики матрицы показывают, сколько сочетаний сценария и канала описывают небезопасный переход. В основном режиме безопасный запуск и постоянное аварийное намерение исключают такие переходы по построению архитектуры, поэтому счётчик равен нулю как следствие выбранной архитектуры, а не как результат розыгрыша помех.
+- Поведение самой реализации подтверждается функциональными проверками; их номера указаны рядом с каждым свойством. Именно проверки, а не матрица, являются доказательством для перечисленных свойств.
+- Движение до синхронизации: 0 (проверки 11, 15).
+- Движение до подтверждения разрешения: 0 (проверки 12, 13).
+- Движение без новой команды оператора: 0 (проверка 14).
+- Использование старого периода управления: 0 (проверка 08).
+- Снятие аварийной фиксации обычной командой: 0 (проверка 22).
+- Потеря аварийного намерения после перезапуска станции: 0 (проверки 17, 18).
+- Движение до подтверждения сброса: 0 (проверки 20, 21).
+- Автоматическое восстановление старой команды после сброса: 0 (проверки 13, 14).
+- Принятие старого запроса сброса: 0 (проверка 19).
+
+Свойства, которые матрица не измеряет
+- Следующие свойства зависят от разбора конкретного сообщения, а не от розыгрыша сценария, поэтому счётчика по 180 сочетаниям для них не существует. Ранее они выводились в списке инвариантов как нули; это было ошибкой представления, и такие строки удалены.
+- Принятие команды старого сеанса станции: подтверждается проверками 06 и 16.
+- Принятие команды старого запуска ровера: подтверждается проверкой 07.
+- Принятие неоднозначной разности номеров 2^31: подтверждается проверкой 10.
+- Отрицательная скорость и превышение разрешённой скорости: подтверждаются проверкой 04; диапазон 0...15 м/с проверяется при кодировании в protocol/control_messages.py.
 
 Учёт нагрузки
 - Постоянное управление: 10.88000 кбит/с во всех сочетаниях.
@@ -280,15 +291,15 @@ Lab041 — сеансы связи, безопасный запуск и защ
 - Аварийные сообщения и сброс: в среднем 0.00574 кбит/с; повторы и повторные подтверждения: 0.01536 кбит/с.
 - Эпизодическая служебная нагрузка основного режима: средняя 0.12298 кбит/с, максимум 0.25147 кбит/с. Именно к этой величине относились прежние значения 0,12298–0,25147 кбит/с.
 - Постоянные исходные потоки: видео 243.39287, телеметрия 7.68000, управление 10.88000 кбит/с.
+- Видео и телеметрия здесь не моделируются: значения перенесены из Lab038, поля video_load_kbps и telemetry_load_kbps файла data/processed/lab038/lab038_summary.csv. Управление вычислено по размеру пакета и частоте.
 - Полный предложенный поток основного режима: средний 262.07584 кбит/с, максимум 262.20433 кбит/с.
-- Доставка управления не ниже 97.836%, телеметрии не ниже 97.918%, публикация видео не ниже 86.054%.
-- Максимальная очередь: 46 пакетов.
+- Доли доставки видео, телеметрии и управления, а также длина очереди в Lab041 не определяются. Модель этой лабораторной воспроизводит обмен служебными сообщениями сеанса, но не планировщик очередей и не транспорт видео. Соответствующие показатели следует брать из Lab037 и Lab040.
 
 Функциональные проверки
 - ПРОЙДЕНО — 01. Сериализация всех сообщений: все десять типов имеют однозначное двоичное представление
 - ПРОЙДЕНО — 02. Отклонение неверной версии: неверная версия отклонена
 - ПРОЙДЕНО — 03. Отклонение неизвестного типа: неизвестный тип отклонён
-- ПРОЙДЕНО — 04. Допустимые диапазоны управления: диапазоны и сочетания полей управления проверены
+- ПРОЙДЕНО — 04. Допустимые диапазоны управления: диапазоны и сочетания полей управления проверены, включая отрицательную скорость и границу 15 м/с
 - ПРОЙДЕНО — 05. Номер ноль в новом сеансе: новый сеанс принимает начальный номер ноль
 - ПРОЙДЕНО — 06. Старый сеанс станции: старый сеанс наземной станции отклонён
 - ПРОЙДЕНО — 07. Старый запуск ровера: старый идентификатор запуска ровера отклонён
@@ -327,7 +338,6 @@ Lab041 — сеансы связи, безопасный запуск и защ
 - data/processed/lab041/lab041_emergency_intent.png
 - data/processed/lab041/lab041_safety_violations.png
 - data/processed/lab041/lab041_protection_load.png
-- data/processed/lab041/lab041_traffic_impact.png
 
 Ограничения
 - Модель не включает криптографическую аутентификацию и не рассматривает намеренного нарушителя.