pith. machine review for the scientific record. sign in
structure definition def or abbrev high

SafetyRequirements

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  96structure SafetyRequirements where
  97  has_watchdog : Bool
  98  has_overcurrent_protection : Bool
  99  has_overvoltage_protection : Bool
 100  has_thermal_protection : Bool
 101  has_loss_of_load_detection : Bool
 102  has_deterministic_shutdown : Bool
 103  all_satisfied :
 104    has_watchdog = true ∧
 105    has_overcurrent_protection = true ∧
 106    has_overvoltage_protection = true ∧
 107    has_thermal_protection = true ∧
 108    has_loss_of_load_detection = true ∧
 109    has_deterministic_shutdown = true
 110
 111/-- The canonical safety configuration. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.