requiredTier
plain-language theorem explainer
This definition assigns a minimum Nautilus tier to each Class C power from the canonical list of 27 superhuman powers. Researchers modeling technological requirements for superhuman capabilities cite it to set hardware thresholds for entries such as flight or force fields. The implementation is a direct pattern match on the Power inductive type that returns some tier for the six Class C cases and none otherwise.
Claim. Let $P$ be the inductive type of the 27 canonical superhuman powers and $N$ the inductive type of Nautilus tiers. The function $r : P → Option(N)$ is defined by $r(flight) = some(ignition)$, $r(invulnerability) = some(temple)$, $r(superStrength) = some(temple)$, $r(forceFields) = some(temple)$, $r(energyProjection) = some(ignition)$, $r(transmutation) = some(ignition)$, and $r(p) = none$ for all other $p ∈ P$.
background
The module formalizes the Nautilus-class technological access path for Class C powers. NautilusTier is the inductive type with three constructors: quietRoom (~10–100 W for meditation amplification), temple (~5–10 kW for healing fields and group coherence), and ignition (>100 kW pulsed for metric editing and flight). Power is the inductive type imported from Core that enumerates the 27 canonical powers drawn from mythology, comics, and folklore, with a subset marked NautilusClass. The module documentation states that power tiers and mappings are MODEL structural definitions while engineering parameters come from the NTL provisional patent stack.
proof idea
This is a definition by exhaustive pattern matching on the Power inductive type. It directly returns the corresponding Option NautilusTier for each of the six Class C constructors and none for the remainder, with no lemmas or tactics applied.
why it matters
The definition is used by the downstream theorem classC_has_tier, which proves that every power satisfying powerClass p = NautilusClass has (requiredTier p).isSome = true. It supplies the concrete mapping required by the Nautilus architecture parameters section. Within the Recognition Science framework it extends the core structural layer for technological access without touching the T0–T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.