fullSafety
plain-language theorem explainer
fullSafety supplies the canonical SafetyRequirements record with every protection flag enabled. Engineers modeling Nautilus-class Class C systems cite it to instantiate the complete safety profile drawn from the NTL patent stack. The definition is a direct record construction that satisfies the conjunction of equality conditions by reflexivity.
Claim. The canonical safety configuration is the record with has_watchdog = true, has_overcurrent_protection = true, has_overvoltage_protection = true, has_thermal_protection = true, has_loss_of_load_detection = true, and has_deterministic_shutdown = true, together with a proof that all six equalities hold.
background
SafetyRequirements is the structure that encodes Nautilus safety requirements from NTL-008/018. It consists of six Boolean fields for watchdog, overcurrent protection, overvoltage protection, thermal protection, loss of load detection, and deterministic shutdown, plus a conjunction asserting that each field equals true. The module formalizes the Nautilus-class technological access path for Class C powers, treating power tiers and mappings as structural definitions while drawing engineering parameters from the NTL provisional patent stack.
proof idea
The definition constructs the SafetyRequirements record by assigning true to each of the six protection fields and supplying a six-element tuple of reflexivity proofs for the conjunction.
why it matters
This definition supplies the standard full-safety instance for the Nautilus technological access path. It supports the engineering parameters in the NTL patent stack and aligns with the proved Gap-45 safety imported from the Gap45 module. No downstream uses appear yet, leaving open its integration with tier power mappings and schedule definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.