diff --git a/4-Infrastructure/netcup-vps/configuration.nix b/4-Infrastructure/netcup-vps/configuration.nix
new file mode 100644
index 00000000..9ca5d969
--- /dev/null
+++ b/4-Infrastructure/netcup-vps/configuration.nix
@@ -0,0 +1,278 @@
+{ config, pkgs, lib, ... }:
+
+{
+  imports = [
+    # Hardware configuration (if needed)
+  ];
+
+  # ── System identity ───────────────────────────────────────────────────────
+  networking.hostName = "rs-vps";
+  time.timeZone = "Europe/Berlin";
+
+  # ── Boot ──────────────────────────────────────────────────────────────────
+  boot.loader.grub.enable = lib.mkDefault true;
+  boot.loader.grub.device = "/dev/vda";
+  boot.loader.grub.efiSupport = true;
+  boot.loader.grub.efiInstallAsRemovable = true;
+
+  # ── Filesystems ────────────────────────────────────────────────────────────
+  fileSystems = {
+    "/" = {
+      device = "/dev/vda1";
+      fsType = "ext4";
+      autoMount = true;
+    };
+    "/boot/efi" = {
+      device = "/dev/vda2";
+      fsType = "vfat";
+      autoMount = true;
+    };
+  };
+
+  swapDevices = [
+    { device = "/dev/vda3"; size = 65536; }
+  ];
+
+  # ── Users ─────────────────────────────────────────────────────────────────
+  users.users.researcher = {
+    isNormalUser = true;
+    description = "Research Stack developer";
+    extraGroups = [
+      "wheel"
+      "docker"
+      "keys"
+    ];
+    openssh.authorizedKeys.keys = [
+      # Add SSH keys here
+    ];
+  };
+
+  # ── OpenSSH ────────────────────────────────────────────────────────────────
+  services.openssh = {
+    enable = true;
+    settings = {
+      PermitRootLogin = "yes";
+      PasswordAuthentication = false;
+    };
+    # listenAddresses = [{ port = 22; }];
+  };
+
+  # ── nix-ld (run x86_64 binaries on ARM64) ────────────────────────────────
+  programs.nix-ld.enable = true;
+
+  # ── uv is installed via environment.systemPackages ──────────────────────
+
+  # ── Lean LSP services ──────────────────────────────────────────────────────
+  # Lean 4.19.0 LSP on port 8765 (streamable-http)
+  systemd.services.lean-lsp-mcp = {
+    description = "Lean LSP MCP server (v4.19.0)";
+    after = [ "network.target" ];
+    wantedBy = [ "multi-user.target" ];
+
+    script = let
+      lean-lsp = pkgs.writeShellScriptBin "lean-lsp-run" ''
+        #!${pkgs.bash}/bin/bash
+        set -euo pipefail
+        export ELAN_TOOLCHAIN=4.19.0
+        export SSL_CERT_FILE=${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt
+        export PATH="${pkgs.uv}/bin:$HOME/.elan/bin:$PATH"
+        exec uv tool run --from lean-lsp-mcp lean-lsp-mcp --port 8765 --stdio
+      '';
+    in ''
+      exec ${lean-lsp}/bin/lean-lsp-run
+    '';
+
+    serviceConfig = {
+      Type = "simple";
+      Restart = "always";
+      RestartSec = "5s";
+      User = "researcher";
+      Group = "researcher";
+      WorkingDirectory = "/home/researcher";
+      Environment = [
+        "ELAN_TOOLCHAIN=4.19.0"
+        "HOME=/home/researcher"
+        "SSL_CERT_FILE=${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt"
+      ];
+    };
+  };
+
+  # Lean 4.30.0-rc2 LSP on port 8766 (for mathlib)
+  systemd.services.lean-lsp-mathlib = {
+    description = "Lean LSP MCP server (v4.30.0-rc2, mathlib)";
+    after = [ "network.target" ];
+    wantedBy = [ "multi-user.target" ];
+
+    script = let
+      lean-lsp-mathlib = pkgs.writeShellScriptBin "lean-lsp-mathlib-run" ''
+        #!${pkgs.bash}/bin/bash
+        set -euo pipefail
+        export ELAN_TOOLCHAIN=4.30.0-rc2
+        export SSL_CERT_FILE=${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt
+        export PATH="${pkgs.uv}/bin:$HOME/.elan/bin:$PATH"
+        exec uv tool run --from lean-lsp-mcp lean-lsp-mcp --port 8766 --stdio
+      '';
+    in ''
+      exec ${lean-lsp-mathlib}/bin/lean-lsp-mathlib-run
+    '';
+
+    serviceConfig = {
+      Type = "simple";
+      Restart = "always";
+      RestartSec = "5s";
+      User = "researcher";
+      Group = "researcher";
+      WorkingDirectory = "/home/researcher";
+      Environment = [
+        "ELAN_TOOLCHAIN=4.30.0-rc2"
+        "HOME=/home/researcher"
+        "SSL_CERT_FILE=${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt"
+      ];
+    };
+  };
+
+  # ── Python LSP TCP on port 8767 ──────────────────────────────────────────
+  systemd.services.pylsp = {
+    description = "Python LSP server (TCP)";
+    after = [ "network.target" ];
+    wantedBy = [ "multi-user.target" ];
+
+    script = let
+      pythonEnv = pkgs.python311.withPackages (ps: with ps; [
+        numpy scipy sympy pandas matplotlib seaborn
+        uncertainties pint
+        beautifulsoup4 lxml
+        requests httpx
+        fastapi uvicorn pydantic
+        python-dateutil
+      ]);
+      pylsp-script = pkgs.writeShellScriptBin "pylsp-run" ''
+        #!${pkgs.bash}/bin/bash
+        set -euo pipefail
+        exec ${pythonEnv}/bin/python -m pylsp --host 0.0.0.0 --port 8767
+      '';
+    in ''
+      exec ${pylsp-script}/bin/pylsp-run
+    '';
+
+    serviceConfig = {
+      Type = "simple";
+      Restart = "always";
+      RestartSec = "5s";
+      User = "researcher";
+      Group = "researcher";
+      WorkingDirectory = "/home/researcher";
+      Environment = [
+        "HOME=/home/researcher"
+        "SSL_CERT_FILE=${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt"
+      ];
+    };
+  };
+
+  # ── Ollama inference server on port 11434 ─────────────────────────────────
+  systemd.services.ollama = {
+    description = "Ollama LLM inference server";
+    after = [ "network.target" ];
+    wantedBy = [ "multi-user.target" ];
+
+    script = ''
+      #!${pkgs.bash}/bin/bash
+      set -euo pipefail
+      export OLLAMA_HOST=0.0.0.0:11434
+      export OLLAMA_MODELS=/home/researcher/.ollama/models
+      mkdir -p $OLLAMA_MODELS
+      exec ${pkgs.ollama}/bin/ollama serve
+    '';
+
+    serviceConfig = {
+      Type = "simple";
+      Restart = "always";
+      RestartSec = "5s";
+      User = "researcher";
+      Group = "researcher";
+      WorkingDirectory = "/home/researcher";
+      Environment = [
+        "HOME=/home/researcher"
+        "PATH=${pkgs.ollama}/bin:${pkgs.curl}/bin"
+      ];
+    };
+  };
+
+  # ── Ollama model puller helper ─────────────────────────────────────────────
+  # Run with: sudo -u researcher /var/lib/ollama/model-pull.sh deepseek-r1:7b
+  systemd.services.ollama-model-pull = {
+    description = "Ollama model puller";
+    after = [ "ollama.service" ];
+    wantedBy = [ "multi-user.target" ];
+    script = ''
+      #!${pkgs.bash}/bin/bash
+      MODEL="''${1:-deepseek-r1:7b}"
+      exec ${pkgs.ollama}/bin/ollama pull "$MODEL"
+    '';
+    serviceConfig = {
+      Type = "oneshot";
+      User = "researcher";
+      RemainAfterExit = true;
+    };
+  };
+
+  # ── Docker (for x86_64 images via nix-ld) ────────────────────────────────
+  virtualisation.docker = {
+    enable = true;
+    autoPrune.enable = true;
+    enableOnBoot = true;
+    # Store images on a larger disk if available
+    # dataRoot = "/var/lib/docker";
+  };
+
+  # ── Networking ─────────────────────────────────────────────────────────────
+  networking.firewall = {
+    enable = true;
+    allowedTCPPorts = [
+      22    # SSH
+      80    # HTTP
+      443   # HTTPS
+      8765  # Lean LSP (v4.19.0)
+      8766  # Lean LSP (v4.30.0-rc2)
+      8767  # Python LSP
+      11434 # Ollama
+    ];
+    allowedUDPPorts = [ ];
+  };
+
+  # ── Packages ────────────────────────────────────────────────────────────────
+  environment.systemPackages = with pkgs; [
+    # Core utilities
+    git git-lfs
+    bash bashInteractive coreutils findutils gnugrep gnused gawk
+    util-linux
+    curl wget rsync zstd xz gnutar gzip
+    ripgrep jq
+    gnumake
+    nodejs_22
+    uv
+    elan
+    texliveFull
+    gnuplot maxima octave
+    typst
+    openssh cacert
+    less which file procps htop
+    glibc binutils
+    openssl pkg-config
+    graphviz
+    postgresql_16
+    docker containerd
+  ];
+
+  # ── Performance tuning for 64GB RAM / 18 cores ─────────────────────────────
+  # Aggressive transparent hugepage for memory-heavy workloads
+  boot.kernel.sysctl = {
+    "vm.nr_hugepages" = 1024;
+  };
+
+  # ── Security ────────────────────────────────────────────────────────────────
+  security.sudo.wheelNeedsPassword = false;
+
+  # ── System state ────────────────────────────────────────────────────────────
+  system.stateVersion = "25.11";
+}
diff --git a/4-Infrastructure/netcup-vps/flake.lock b/4-Infrastructure/netcup-vps/flake.lock
new file mode 100644
index 00000000..65ec8bdc
--- /dev/null
+++ b/4-Infrastructure/netcup-vps/flake.lock
@@ -0,0 +1,44 @@
+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1779796641,
+        "narHash": "sha256-ZsIrKmhp4vbBXoXXmR/tBXA/UCsAQiJL9vsgZEduhVY=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "25f538306313eae3927264466c70d7001dcea1df",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-25.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-stable": {
+      "locked": {
+        "lastModified": 1751274312,
+        "narHash": "sha256-/bVBlRpECLVzjV19t5KMdMFWSwKLtb5RyXdjz3LJT+g=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "50ab793786d9de88ee30ec4e4c24fb4236fc2674",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-24.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nixpkgs": "nixpkgs",
+        "nixpkgs-stable": "nixpkgs-stable"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/4-Infrastructure/netcup-vps/flake.nix b/4-Infrastructure/netcup-vps/flake.nix
new file mode 100644
index 00000000..4edacd36
--- /dev/null
+++ b/4-Infrastructure/netcup-vps/flake.nix
@@ -0,0 +1,199 @@
+{
+  description = "Research Stack — netcup VPS (Ampere ARM64, 64GB RAM)";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.11";
+    nixpkgs-stable.url = "github:NixOS/nixpkgs/nixos-24.11";
+  };
+
+  outputs = { self, nixpkgs, nixpkgs-stable }:
+    let
+      system = "aarch64-linux";
+      pkgs = import nixpkgs {
+        inherit system;
+        config.allowUnfree = false;
+      };
+
+      # ── Lean 4 toolchains via elan ─────────────────────────────────────────
+      # elan-lsp overlays lean4 onto PATH for a given toolchain.
+      # Multiple toolchains can coexist; default is set via ELAN_TOOLCHAIN.
+      elan-lsp = { toolchain ? "4.19.0", port ? 8765 }:
+        let
+          elan-init = pkgs.runCommand "elan-init-${toolchain}" {
+            nativeBuildInputs = [ pkgs.curl ];
+            SSL_CERT_FILE = "${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt";
+          } ''
+            mkdir -p $out/etc/profile.d
+            cat > $out/etc/profile.d/elan-${toolchain}.sh << 'PROFILE'
+            export ELAN_TOOLCHAIN=${toolchain}
+            export PATH="$HOME/.elan/toolchains/lean4-${toolchain}/bin:$PATH"
+            PROFILE
+          '';
+        in pkgs.writeShellScriptBin "lean-lsp-mcp" ''
+          #! ${pkgs.bash}/bin/bash
+          set -euo pipefail
+          export ELAN_TOOLCHAIN=${toolchain}
+          export PATH="$HOME/.elan/toolchains/lean4-${toolchain}/bin:$PATH"
+          export SSL_CERT_FILE=${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt
+          exec uvx lean-lsp-mcp --port=${toString port} --stdio
+        '';
+
+      # ── Python LSP server ─────────────────────────────────────────────────
+      pylsp-tcp = { port ? 8767, extras ? [ "all" ] }:
+        let
+          pythonEnv = pkgs.python311.withPackages (ps: with ps; [
+            numpy scipy sympy pandas matplotlib seaborn
+            uncertainties pint
+            beautifulsoup4 lxml
+            requests httpx
+            fastapi uvicorn pydantic
+            python-dateutil
+          ]);
+        in pkgs.writeShellScriptBin "pylsp-tcp" ''
+          #! ${pkgs.bash}/bin/bash
+          set -euo pipefail
+          exec ${pythonEnv}/bin/python -m pylsp --host 0.0.0.0 --port ${toString port}
+        '';
+
+      # ── Ollama for inference ─────────────────────────────────────────────
+      ollama-service = pkgs.writeShellScriptBin "ollama-service" ''
+        #! ${pkgs.bash}/bin/bash
+        set -euo pipefail
+        export OLLAMA_HOST=0.0.0.0:11434
+        exec ${pkgs.ollama}/bin/ollama serve
+      '';
+
+      # ── Core packages ─────────────────────────────────────────────────────
+      corePackages = with pkgs; [
+        # Version control
+        git git-lfs
+        # Shells & core utils
+        bash bashInteractive coreutils findutils gnugrep gnused gawk
+        util-linux
+        # File transfer & compression
+        curl wget rsync zstd xz gnutar gzip
+        # Search & text processing
+        ripgrep jq
+        # Build essentials
+        gnumake
+        # Node (for any JS tooling)
+        nodejs_22
+        # Python: uv for runtime package management
+        uv
+        # Elan for Lean 4 toolchains
+        elan
+        # LaTeX
+        texliveFull
+        # Math CLI tools
+        gnuplot maxima wxmaxima octave
+        # CAS
+        # sage  # too heavy for server; use lean + sympy
+        # Typesetting
+        typst
+        # Network / TLS
+        openssh cacert
+        # Shell helpers
+        less which file procps htop
+        # glibc / binutils
+        glibc binutils
+        # SSL / crypto
+        openssl pkg-config
+        # Graphviz
+        graphviz
+        # PostgreSQL client
+        postgresql_16
+        # Docker (for running pre-built x86_64 images via nix-ld)
+        docker
+        # Containerd for docker
+        containerd
+        # nix-ld for running x86_64 binaries on ARM64
+        # (built from nixpkgs-stable to ensure binary cache availability)
+        (import nixpkgs-stable {
+          system = "x86_64-linux";
+          config.allowUnfree = false;
+        }).nix-ld
+      ];
+
+      # ── Python packages (full science stack) ──────────────────────────────
+      pythonPackages = with pkgs.python311Packages; [
+        numpy scipy sympy pandas matplotlib seaborn
+        uncertainties pint
+        beautifulsoup4 lxml
+        requests httpx
+        fastapi uvicorn pydantic
+        python-dotenv pyyaml rich
+        python-dateutil urllib3
+        boto3 botocore
+        psycopg2
+        biopython networkx
+        pycryptodome
+        zstandard
+        z3
+        pywavelets
+        polars
+        scikit-learn
+        notion-client
+        pytest
+      ];
+
+      # ── Custom etc for researcher user ───────────────────────────────────
+      customEtc = pkgs.runCommand "custom-etc" {} ''
+        mkdir -p $out/etc
+        echo 'root:x:0:0:root user:/var/empty:/bin/sh' > $out/etc/passwd
+        echo 'nobody:x:65534:65534:nobody:/var/empty:/bin/sh' >> $out/etc/passwd
+        echo 'researcher:x:1000:1000:Research Stack developer:/home/researcher:/bin/bash' >> $out/etc/passwd
+        echo 'root:x:0:' > $out/etc/group
+        echo 'nobody:x:65534:' >> $out/etc/group
+        echo 'researcher:x:1000:' >> $out/etc/group
+        echo 'passwd: files' > $out/etc/nsswitch.conf
+        echo 'group: files' >> $out/etc/nsswitch.conf
+        echo 'hosts: files dns' >> $out/etc/nsswitch.conf
+      '';
+
+      researcherSetup = pkgs.runCommand "researcher-home" {} ''
+        mkdir -p $out/home/researcher/stack
+        mkdir -p $out/home/researcher/.elan/toolchains
+        mkdir -p $out/home/researcher/.cache
+        mkdir -p -m 1777 $out/tmp
+        chmod 755 $out/home/researcher
+        chmod 700 $out/home/researcher/.elan
+      '';
+
+    in rec {
+      packages.${system} = {
+        inherit corePackages pythonPackages;
+
+        # ── Lean LSP service (port 8765) ──────────────────────────────────
+        lean-lsp-mcp = elan-lsp { toolchain = "4.19.0"; port = 8765; };
+
+        # ── Lean LSP with mathlib toolchain (port 8766) ───────────────────
+        lean-lsp-mathlib = elan-lsp { toolchain = "4.30.0-rc2"; port = 8766; };
+
+        # ── Python LSP TCP (port 8767) ───────────────────────────────────
+        pylsp = pylsp-tcp { port = 8767; };
+
+        # ── Ollama inference server ───────────────────────────────────────
+        ollama = ollama-service;
+      };
+
+      # ── NixOS configuration for the VPS ──────────────────────────────────
+      nixosConfigurations.netcup-vps = nixpkgs.lib.nixosSystem {
+        inherit system;
+        modules = [
+          ./configuration.nix
+        ];
+      };
+
+      # Convenience: nix build .#packages.aarch64-linux.lean-lsp-mcp
+      defaultPackage.${system} = packages.${system}.lean-lsp-mcp;
+
+      # ── Dev shell ────────────────────────────────────────────────────────
+      devShells.${system}.default = pkgs.mkShell {
+        packages = corePackages ++ pythonPackages;
+        shellHook = ''
+          echo "Research Stack — netcup VPS dev shell (ARM64, NixOS 25.11)"
+          export PS1='\[\033[1;34m\][rs-vps]\[\033[0m\] \w \$ '
+        '';
+      };
+    };
+}