Document external AD proof backend setup

Author: jishengyang-cal

README.md

@@ -105,3 +105,8 @@ named command. The activation gate opens only when the boundary manifest is
 valid, the backend probe is production-ready, and the probed command matches
 the manifest `commandRef`. This repo still does not execute proof jobs or hold
 proof credentials.
+
+`gatl-ad-proof-backend` is now the standalone v0.1 command that satisfies this
+external command boundary. It validates derivative golden fixture intake and
+emits an external AD proof result, but it reports `validated-not-proved` until
+real proof-term checking is implemented.

docs/architecture.md

@@ -50,6 +50,11 @@ make that external boundary explicit:
 The gate is a deployment handoff artifact. It does not execute proof jobs,
 manage proof credentials, start workers, or modify `gatl-core`.
 
+The standalone `gatl-ad-proof-backend` repo now provides the external command
+referenced by `cmd://gatl-ad-proof-backend`. In v0.1 it validates derivative
+golden fixture intake and emits a result artifact, but it deliberately does not
+claim formal AD proof success.
+
 ## Primitive Semantics
 
 Supported scalar primitives:
@@ -72,7 +77,7 @@ Non-smooth or nondeterministic primitives remain outside this lab.
 - No production AD engine.
 - No TensorFlow, PyTorch, JAX, ONNX, or autograd integration.
 - No proof assistant integration.
-- No production formal proof backend.
+- No production formal proof backend execution in this repo.
 - No proof backend execution in this repo.
 - No network access.
 - No secret handling.

docs/production-proof-backend-setup.md

@@ -0,0 +1,46 @@
+# Production Proof Backend Setup
+
+`gatl-ad-lab` expects the AD proof backend to remain external. The production
+boundary manifest names:
+
+```text
+cmd://gatl-ad-proof-backend
+```
+
+## Local Activation Probe
+
+Install the standalone backend:
+
+```bash
+cd /home/jisheng-yang/projects/gatl-ad-proof-backend
+cargo install --path . --force
+gatl-ad-proof-backend --version
+```
+
+Then run the `gatl-ad-lab` gate:
+
+```bash
+cd /home/jisheng-yang/projects/gatl-ad-lab
+cargo run -- validate-proof-boundary examples/proof-backend-boundary.valid.json \
+  --out target/production-probes/proof-backend-boundary-validation.after-backend.json
+cargo run -- doctor-proof-backend \
+  --checked-at 2026-06-14T00:00:00Z \
+  --out target/production-probes/proof-backend-environment.after-backend.json
+cargo run -- gate-proof-backend \
+  examples/proof-backend-boundary.valid.json \
+  target/production-probes/proof-backend-environment.after-backend.json \
+  --out target/production-probes/proof-backend-activation-gate.after-backend.json
+```
+
+Expected result:
+
+- boundary validation is valid;
+- backend environment is production-ready;
+- activation gate is open.
+
+## Boundary
+
+This setup only proves that the external backend command exists and satisfies
+the v0.1 command boundary. It does not move proof execution into `gatl-ad-lab`.
+The v0.1 backend result remains `validated-not-proved` until real proof-term
+checking is added.