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

NautilusConfig

show as:
view Lean formalization →

NautilusConfig collects the core engineering parameters for a Nautilus-class device as an integer stiffness value kappa, a positive coil count, and a default of eight commutation phases. Modelers of Class C technological access paths cite this structure when specifying hardware in the superhuman tier system. The declaration is a direct structure definition with no attached computation or lemmas.

claimA Nautilus configuration consists of an integer stiffness parameter $k$, a positive natural number $n$ of coils, and a natural number of commutation phases that defaults to 8.

background

The module encodes the Nautilus-class technological access path for Class C powers, treating power tiers as structural model definitions and engineering parameters as drawn from the NTL provisional patent stack. Upstream definitions supply the kappa field: one sets kappa(k) = phi^k for thermal conductivity regimes on the phi-ladder, while another defines kappa as (log phi)^2 for annular cost. The cellular automata radius supplies a unit neighborhood but is not referenced in the structure fields.

proof idea

The declaration is a direct structure definition that introduces the four fields kappa as an integer, n_coils as a natural number together with its positivity witness, and commutation_phases defaulting to 8. No lemmas or tactics are applied.

why it matters in Recognition Science

This structure supplies the concrete engineering parameters required by the Nautilus power tiers inside the Class C technological access path. It links to the Recognition framework through the phi-ladder via the kappa parameter, which inherits its interpretation from upstream phi-power and log-phi definitions. No downstream uses are recorded, leaving open its integration with full tier mappings and Gap-45 safety.

scope and limits

formal statement (Lean)

  60structure NautilusConfig where
  61  kappa : ℤ
  62  n_coils : ℕ
  63  n_coils_pos : 0 < n_coils
  64  commutation_phases : ℕ := 8

proof body

Definition body.

  65
  66/-- The φ-log-spiral radius function: r(θ) = r₀ · φ^(κθ/2π). -/

depends on (3)

Lean names referenced from this declaration's body.