19structure AlignmentProtocol where 20 protocol : Protocol 21 /-- Invariants that must be preserved under alignment (e.g., dominant mode, total Z, etc.). -/ 22 invariants : List String := []
proof body
Definition body.
23 24namespace AlignmentProtocol 25
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.