diff --git a/.claude/tasks/0047-flake-check-hm-module-composition.md b/.claude/tasks/0047-flake-check-hm-module-composition.md
index c5905c8..e6dab45 100644
--- a/.claude/tasks/0047-flake-check-hm-module-composition.md
+++ b/.claude/tasks/0047-flake-check-hm-module-composition.md
@@ -26,11 +26,24 @@ This adds a module check alongside the existing package check in the flake's `ch
 
 ## Acceptance criteria
 
-- [ ] The flake has a home-manager input whose nixpkgs follows the flake's nixpkgs; `flake.lock` is updated.
-- [ ] A new check under the flake's `checks` output evaluates the real module through home-manager's standalone configuration entry point and builds the home files derivation — no Claude Code binary or running agent required.
-- [ ] The attribute-set-skills configuration asserts the module's Skill and the operator's skill both land, each at its own name.
-- [ ] The whole-directory-skills (path form) configuration asserts the module's Skill lands alongside the operator's directory contents; a non-recursive path-form install would fail this as a build-time collision.
-- [ ] The Claude-Code-disabled configuration asserts no gitea-axi Skill entry is written.
-- [ ] A configuration with an operator's own SessionStart hook asserts the module's hook merges into that list rather than replacing it.
-- [ ] The check asserts on the generation's file tree only, not on option values or store paths.
-- [ ] `nix flake check` runs the new check across the flake's systems and passes.
+- [x] The flake has a home-manager input whose nixpkgs follows the flake's nixpkgs; `flake.lock` is updated.
+- [x] A new check under the flake's `checks` output evaluates the real module through home-manager's standalone configuration entry point and builds the home files derivation — no Claude Code binary or running agent required.
+- [x] The attribute-set-skills configuration asserts the module's Skill and the operator's skill both land, each at its own name.
+- [x] The whole-directory-skills (path form) configuration asserts the module's Skill lands alongside the operator's directory contents; a non-recursive path-form install would fail this as a build-time collision.
+- [x] The Claude-Code-disabled configuration asserts no gitea-axi Skill entry is written.
+- [x] A configuration with an operator's own SessionStart hook asserts the module's hook merges into that list rather than replacing it.
+- [x] The check asserts on the generation's file tree only, not on option values or store paths.
+- [x] `nix flake check` runs the new check across the flake's systems and passes.
+
+## Implementation Notes
+
+The check lives in its own file, `checks/home-manager-module.nix`, imported from the flake's `checks` output beside the existing package check; the `forAllSystems` callback now destructures `{ pkgs, system }` because the check needs `pkgs` to build fixtures and the derivation.
+`home-manager` is added as a flake input with `inputs.nixpkgs.follows = "nixpkgs"`; it is a check-only development input with no bearing on the package or the module a consumer imports, and the comment in `flake.nix` says so.
+
+Each of the four configurations builds `config.home-files` — the home-manager file-linkage layer — and the final `runCommandLocal` asserts on that tree with `test`/`grep` only: skill files present or absent by path, and the two SessionStart commands present as quoted JSON string values in `settings.json`.
+The hook-merge assertion reads generated file content because that is the only place a list merge is observable; the spec's Testing Decisions name "the hook merges into the operator's own hooks" as a required assertion, so this stays within "assert on the file tree, not on option values or store paths".
+
+On the cross-system criterion: `nix flake check` builds the check for the host system and passes, and omits the incompatible systems (`aarch64-*`) with a warning — identical per-system semantics to the pre-existing package check, which also builds only natively.
+The check is import-from-derivation-bearing (the Claude Code module reads the fixture skill directories at evaluation time), so evaluating a foreign system's check forces a cross-platform fixture build rather than skipping cleanly; this is not exercised by the default `nix flake check` and does not affect the native run.
+
+Verified by `nix flake check` (passes, all outputs) and by inspecting each configuration's built `home-files` tree directly: the disabled-Claude-Code generation contains no `.claude` directory at all, and the merged-hook `settings.json` contains both hooks in the `SessionStart` array — confirming the assertions are not vacuous.
diff --git a/checks/home-manager-module.nix b/checks/home-manager-module.nix
new file mode 100644
index 0000000..e7c0a25
--- /dev/null
+++ b/checks/home-manager-module.nix
@@ -0,0 +1,139 @@
+# The first automated proof of the home-manager module's composition (ADR 0021).
+#
+# It evaluates the *real* module through home-manager's standalone configuration
+# entry point and builds the resulting home files derivation — the file-linkage
+# layer that actually decides whether two declarations collide — under several
+# operator configurations, then asserts on the tree each one produces. It never
+# reads module internals: not option values, not store paths, not the shape of
+# the file mechanism, only which files a generation contains. Building the home
+# files derivation needs neither the Claude Code binary nor a running agent.
+#
+# The configurations cover the composition risks the reshape introduced: the
+# Skill coexisting with an operator's own skills in both the attribute-set and
+# whole-directory forms, the explicit sibling-enable gate that keeps the Skill
+# off a host without Claude Code, and the hook merging into an operator's own
+# SessionStart list rather than replacing it.
+{
+  pkgs,
+  home-manager,
+  module,
+  package,
+}:
+let
+  inherit (pkgs) lib;
+
+  # A skill the operator declares as their own, as one attribute-set entry. Its
+  # SKILL.md is what the attribute-set assertion looks for beside the module's.
+  operatorAttrSkill = pkgs.runCommandLocal "operator-attr-skill" { } ''
+    mkdir -p "$out"
+    printf '%s\n' "the operator's own attribute-set skill" > "$out/SKILL.md"
+  '';
+
+  # A whole directory of skills, one folder per skill, for the path form of the
+  # operator's own `programs.claude-code.skills`. The Claude Code module installs
+  # this recursively; the module's own nested Skill entry has to drop in beside
+  # its contents rather than collide with a single link over the directory.
+  operatorSkillsDir = pkgs.runCommandLocal "operator-skills-dir" { } ''
+    mkdir -p "$out/operator-dir-skill"
+    printf '%s\n' "the operator's own whole-directory skill" \
+      > "$out/operator-dir-skill/SKILL.md"
+  '';
+
+  # A distinctive command so the merged-hook assertion can tell the operator's
+  # own SessionStart hook apart from gitea-axi's in the generated settings.json.
+  operatorHook = {
+    matcher = "";
+    hooks = [
+      {
+        type = "command";
+        command = "operator-own-session-hook";
+      }
+    ];
+  };
+
+  # Evaluate the real module through home-manager's standalone entry point and
+  # return the home files derivation — the tree home-manager would link into
+  # $HOME. `programs.gitea-axi.enable` is on in every configuration; the package
+  # is the flake's own build, so the check reuses the store path the package
+  # check already produces rather than building a second time.
+  homeFiles =
+    operatorConfig:
+    (home-manager.lib.homeManagerConfiguration {
+      inherit pkgs;
+      modules = [
+        module
+        {
+          home.username = "operator";
+          home.homeDirectory = "/home/operator";
+          home.stateVersion = "24.11";
+
+          programs.gitea-axi.enable = true;
+          programs.gitea-axi.package = package;
+        }
+        operatorConfig
+      ];
+    }).config.home-files;
+
+  # An operator on Claude Code who declares their own skill as an attribute-set
+  # entry: the module's Skill and theirs must both land, each at its own name.
+  attrSetSkills = homeFiles {
+    programs.claude-code.enable = true;
+    # A store path (not a bare derivation): the skills value type takes a path,
+    # and a derivation would be read as the attribute-set branch of the option.
+    programs.claude-code.skills.operator-attr-skill = "${operatorAttrSkill}";
+  };
+
+  # An operator who declares their own skills as a whole directory (path form):
+  # the module's Skill lands beside the directory's contents. A regression to a
+  # non-recursive path-form install would fail this build as a file collision.
+  wholeDirSkills = homeFiles {
+    programs.claude-code.enable = true;
+    programs.claude-code.skills = "${operatorSkillsDir}";
+  };
+
+  # Claude Code disabled: the explicit sibling-enable gate must leave no
+  # gitea-axi Skill entry in the generation.
+  claudeCodeOff = homeFiles {
+    programs.claude-code.enable = false;
+  };
+
+  # An operator with their own SessionStart hook: the module's hook must merge
+  # into that list rather than replace it.
+  mergedHook = homeFiles {
+    programs.claude-code.enable = true;
+    programs.claude-code.settings.hooks.SessionStart = [ operatorHook ];
+  };
+in
+pkgs.runCommandLocal "gitea-axi-home-manager-module-check"
+  {
+    # Forcing each derivation as a build input is what actually builds the home
+    # files tree under every configuration; the whole-directory build would fail
+    # here, before any assertion runs, on a non-recursive-install regression.
+    inherit
+      attrSetSkills
+      wholeDirSkills
+      claudeCodeOff
+      mergedHook
+      ;
+  }
+  ''
+    echo "attribute-set skills: module's Skill and operator's both land"
+    test -f "$attrSetSkills/.claude/skills/gitea-axi/SKILL.md"
+    test -f "$attrSetSkills/.claude/skills/operator-attr-skill/SKILL.md"
+
+    echo "whole-directory skills: module's Skill lands beside the directory"
+    test -f "$wholeDirSkills/.claude/skills/gitea-axi/SKILL.md"
+    test -f "$wholeDirSkills/.claude/skills/operator-dir-skill/SKILL.md"
+
+    echo "Claude Code disabled: no gitea-axi Skill entry is written"
+    test ! -e "$claudeCodeOff/.claude/skills/gitea-axi"
+
+    echo "operator's own SessionStart hook: the module's hook merges in"
+    # Match the commands as quoted JSON string values, not by their position or
+    # the emitter's colon spacing: both must be present for a merge (rather than
+    # a replacement) of the two SessionStart hooks.
+    grep -q '"operator-own-session-hook"' "$mergedHook/.claude/settings.json"
+    grep -q '"gitea-axi"' "$mergedHook/.claude/settings.json"
+
+    touch "$out"
+  ''
diff --git a/flake.lock b/flake.lock
index 301a9a7..99d37c7 100644
--- a/flake.lock
+++ b/flake.lock
@@ -1,5 +1,25 @@
 {
   "nodes": {
+    "home-manager": {
+      "inputs": {
+        "nixpkgs": [
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1784588016,
+        "narHash": "sha256-ouZe80aWEhMLVMkqICFDN+JUw+0FJtCr/bh+hHtRtMg=",
+        "owner": "nix-community",
+        "repo": "home-manager",
+        "rev": "deeb6b7eb7e0c44ae1819c051ce175bd92a85100",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-community",
+        "repo": "home-manager",
+        "type": "github"
+      }
+    },
     "nixpkgs": {
       "locked": {
         "lastModified": 1784356753,
@@ -18,6 +38,7 @@
     },
     "root": {
       "inputs": {
+        "home-manager": "home-manager",
         "nixpkgs": "nixpkgs"
       }
     }
diff --git a/flake.nix b/flake.nix
index 62d8ff6..c1187ec 100644
--- a/flake.nix
+++ b/flake.nix
@@ -6,8 +6,18 @@
   # only — never the deployed artifact.
   inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
 
+  # Present only so `nix flake check` can evaluate the home-manager module
+  # against real home-manager (the `home-manager-module` check). Its nixpkgs
+  # follows this flake's, so the module is checked against the same
+  # nixpkgs-and-home-manager pairing a consumer following this flake would get.
+  # It has no bearing on the package or the module a consumer imports — the
+  # module is a bare function that takes the importing configuration's own
+  # home-manager and pkgs.
+  inputs.home-manager.url = "github:nix-community/home-manager";
+  inputs.home-manager.inputs.nixpkgs.follows = "nixpkgs";
+
   outputs =
-    { self, nixpkgs }:
+    { self, nixpkgs, home-manager }:
     let
       # x86_64-darwin is deliberately absent: nixpkgs 26.11 dropped it, and
       # `legacyPackages.x86_64-darwin` now throws rather than merely failing to
@@ -79,16 +89,31 @@
         }
       );
 
-      # An alias for the package, so `nix flake check` builds it and thereby runs
-      # both its verification phases — the fast tier in `checkPhase`, the
-      # installed-binary tier in `installCheckPhase`.
+      # Two checks. `gitea-axi` is an alias for the package, so `nix flake check`
+      # builds it and thereby runs both its verification phases — the fast tier
+      # in `checkPhase`, the installed-binary tier in `installCheckPhase`.
       #
-      # No granular per-stage checks: the one stage that would add coverage the
-      # package build does not already have is the full typecheck, which spans
-      # `test/` and `bench/` and would therefore drag the benchmark harness into
-      # the derivation's inputs — undoing the source filtering that keeps
-      # benchmark churn from forcing a rebuild. That typecheck stays in
-      # continuous integration, where it already runs.
-      checks = forAllSystems ({ system, ... }: { inherit (self.packages.${system}) gitea-axi; });
+      # `home-manager-module` evaluates the home-manager module through real
+      # home-manager and builds the home files derivation it produces under
+      # several operator configurations, proving the module's composition (ADR
+      # 0021). It reuses the package check's store path rather than rebuilding.
+      #
+      # No granular per-stage checks for the package: the one stage that would
+      # add coverage the package build does not already have is the full
+      # typecheck, which spans `test/` and `bench/` and would therefore drag the
+      # benchmark harness into the derivation's inputs — undoing the source
+      # filtering that keeps benchmark churn from forcing a rebuild. That
+      # typecheck stays in continuous integration, where it already runs.
+      checks = forAllSystems (
+        { pkgs, system }: {
+          inherit (self.packages.${system}) gitea-axi;
+
+          home-manager-module = import ./checks/home-manager-module.nix {
+            inherit pkgs home-manager;
+            module = self.homeModules.gitea-axi;
+            package = self.packages.${system}.gitea-axi;
+          };
+        }
+      );
     };
 }