  28  deriving DecidableEq, Repr
  29
  30/-- Power range for each tier (in watts). -/
  31def tierPowerRange : NautilusTier → ℝ × ℝ
  32  | .quietRoom => (10, 100)
  33  | .temple    => (5000, 10000)
  34  | .ignition  => (100000, 1000000)
  35
  36/-- Each tier's lower bound is positive. -/
  37theorem tier_power_positive (t : NautilusTier) : 0 < (tierPowerRange t).1 := by
  38  cases t <;> simp [tierPowerRange] <;> norm_num
  39
  40/-! ## Power-to-Tier Mapping -/
  41
  42/-- Maps each Class C power to its minimum required Nautilus tier. -/
  43def requiredTier : Power → Option NautilusTier
  44  | .flight          => some .ignition
  45  | .invulnerability => some .temple
  46  | .superStrength   => some .temple
  47  | .forceFields     => some .temple
  48  | .energyProjection => some .ignition
  49  | .transmutation   => some .ignition
  50  | _                => none
  51
  52/-- All Class C powers have a required tier. -/
  53theorem classC_has_tier (p : Power) (h : powerClass p = .NautilusClass) :
  54    (requiredTier p).isSome = true := by
  55  cases p <;> simp_all [powerClass, requiredTier]
  56
  57/-! ## Nautilus Architecture Parameters -/
  58
  59/-- Core architectural parameters for a Nautilus device. -/
  60structure NautilusConfig where
  61  kappa : ℤ

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.