SafetyRequirements
plain-language theorem explainer
SafetyRequirements packages six boolean safety interlocks with an explicit conjunction requiring each to equal true for Nautilus-class systems. Engineers working on Class C power tiers under NTL-008/018 would cite this record when checking compliance in the superhuman access path. The declaration is a pure structure definition with no lemmas or tactics.
Claim. A safety requirements record consists of six boolean fields (watchdog, overcurrent protection, overvoltage protection, thermal protection, loss-of-load detection, deterministic shutdown) together with the assertion that all six equal true.
background
The module formalizes the Nautilus-class technological access path for Class C powers. Power tiers and mappings count as structural models while engineering parameters come from the NTL provisional patent stack and Gap-45 safety is imported as proved. Upstream canonical arithmetic supplies realization-independent Peano content, Gap45.Beat.canonical supplies the eight-tick and 45-cycle synchronization, and NonParasitism.canonical supplies the prime-based non-resonant schedule.
proof idea
This is a structure definition that directly assembles the six boolean safety indicators with the conjunction requiring each to be true. No lemmas are applied; the all_satisfied field is part of the structure itself.
why it matters
This definition supplies the type for the canonical fullSafety instance used in Nautilus power tier verification. It fills the engineering safety slot in the Technological Access Path, drawing on NTL-008/018 and the proved Gap-45 safety imported from the Gap45 module. It touches the open question of how these structural requirements translate to physical implementations in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.