feat(formal): add independent participant crossing models

[Brad-Edwards]

Summary

Construct independent finite participant-crossing models for one fresh operation and its retries. Export complete deterministic graphs and source-bound manifests for later equivalence checking.

Requirement UIDs

• SEM-232
• SEM-230
• API-423
• RUN-319

Related Issues

Refs #971

ADR Impact

• ADR-100 (amended)
• ADR-059
• ADR-061

Changes

• Add independently derived abstract and concrete transition models, with 88/107 and 178/197 states/transitions respectively.
• Publish a closed binary profile, schema fixtures, deterministic AUT/state maps, and drift validation; reject crossing profiles at opacity admission.
• Amend ADR-100 for the agreed rev2 semantics and retain SEM-232 as DRAFT pending equivalence and reproduction. Multiple operations are tracked in Model participant crossings across multiple operations and retries #1395.
• Merge current dev while preserving both research evidence histories; refresh evidence for the combined source.
• Update locked PyJWT from 2.13.0 to 2.14.0 to clear the dependency security gate.

Test Plan

• Unit tests pass
• Integration tests pass if applicable
• Full completion suite required in CI before merge
• No coverage regression

275 targeted tests passed after conflict resolution. After the dependency update, 124 MCP/authorization tests and 22 export/evidence checks passed; the dependency vulnerability scan passed. Evidence integrity and production replay checks passed. Schema generation parity, file-local policy, and ADR-059 amendment validation passed. No runtime retry behavior changes, mandatory author annotations, or request-time checker. No equivalence or runtime-realization result is claimed.

Ground Control Checks

• Repository policy checks required in CI before merge
• Pre-push Codex review completed; all findings fixed or dispositioned

Traceability

• IMPLEMENTS: SEM-230 ← implementations/formal/participant_crossing/abstract.py (bounded formal representation), API-423, RUN-319 ← implementations/formal/participant_crossing/concrete.py (bounded formal representation), SEM-232 construction only ← implementations/formal/participant_crossing/export.py; theorem remains unestablished
• TESTS: SEM-232, SEM-230, API-423, RUN-319 ← implementations/python/tests/test_issue_971_crossing_models.py, SEM-232 ← implementations/python/tests/test_issue_971_crossing_profile.py, implementations/python/tests/test_issue_971_crossing_export.py

Checklist

• Code follows the project's coding standards
• Changelog: owned by Release Please (generated from the Conventional Commit PR title; no per-PR fragment)
• Architectural docs updated if stack, package structure, or key behaviors changed

Documentation

Updated: see diff.

[Brad-Edwards]

Ground Control delivery — this pull request delivers issue #971; Phase E runs on merge.

[Brad-Edwards]

Ground Control delivery — this pull request delivers issue #971; Phase E runs on merge.