diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 7df2a638..deb9fa70 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -17,6 +17,14 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       - uses: ./.github/actions/setup-lean
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.x'
+      - name: Regenerate Rules.lean and RuleData.lean from pinned phino
+        run: |
+          pip install pyyaml
+          bash scripts/regen-rules.sh
+          bash scripts/regen-rule-data.sh
       - name: Build the library and executables
         run: |
           lake build
diff --git a/.github/workflows/difftest.yml b/.github/workflows/difftest.yml
index defc60c1..cfb47762 100644
--- a/.github/workflows/difftest.yml
+++ b/.github/workflows/difftest.yml
@@ -16,9 +16,10 @@ jobs:
     runs-on: ubuntu-24.04
     steps:
       - uses: actions/checkout@v4
-      - name: Install phino (latest)
+      - name: Install phino (pinned via .phino-version)
         run: |
-          sudo curl -fsSL -o /usr/local/bin/phino http://phino.objectionary.com/releases/ubuntu-24.04/phino-latest
+          version="$(cat .phino-version)"
+          sudo curl -fsSL -o /usr/local/bin/phino "http://phino.objectionary.com/releases/ubuntu-24.04/phino-$version"
           sudo chmod +x /usr/local/bin/phino
           phino --version
       - uses: ./.github/actions/setup-lean
diff --git a/.github/workflows/ruff.yml b/.github/workflows/ruff.yml
new file mode 100644
index 00000000..60b99290
--- /dev/null
+++ b/.github/workflows/ruff.yml
@@ -0,0 +1,18 @@
+# SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+name: ruff
+'on':
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - master
+jobs:
+  ruff:
+    timeout-minutes: 15
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v4
+      - uses: astral-sh/ruff-action@v3
diff --git a/.github/workflows/rules-in-sync.yml b/.github/workflows/rules-in-sync.yml
deleted file mode 100644
index c98473a7..00000000
--- a/.github/workflows/rules-in-sync.yml
+++ /dev/null
@@ -1,29 +0,0 @@
-# SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com
-# SPDX-License-Identifier: MIT
-
-name: rules-in-sync
-on:
-  push:
-    branches: [master]
-  pull_request:
-
-concurrency:
-  group: rules-in-sync-${{ github.ref }}
-  cancel-in-progress: true
-
-jobs:
-  rules-in-sync:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-      - uses: actions/setup-python@v5
-        with:
-          python-version: '3.x'
-      - run: pip install pyyaml
-      - name: Regenerate rules from phino (latest) and detect drift
-        run: |
-          bash scripts/regen-rules.sh
-          if ! git diff --exit-code PhiConfluence/Rules.lean; then
-            echo "::error::PhiConfluence/Rules.lean is out of sync with phino — run scripts/regen-rules.sh and commit"
-            exit 1
-          fi
diff --git a/.phino-version b/.phino-version
new file mode 100644
index 00000000..4b9517ee
--- /dev/null
+++ b/.phino-version
@@ -0,0 +1 @@
+0.0.0.74
diff --git a/PhiConfluence.lean b/PhiConfluence.lean
index a89b9120..40a441ac 100644
--- a/PhiConfluence.lean
+++ b/PhiConfluence.lean
@@ -13,6 +13,8 @@ import PhiConfluence.Step
 import PhiConfluence.Reduce
 import PhiConfluence.Render
 import PhiConfluence.Rules
+import PhiConfluence.RuleSchema
+import PhiConfluence.RuleData
 import PhiConfluence.Parallel
 import PhiConfluence.Preservation
 import PhiConfluence.Diamond
diff --git a/PhiConfluence/RuleData.lean b/PhiConfluence/RuleData.lean
new file mode 100644
index 00000000..ccff5ffc
--- /dev/null
+++ b/PhiConfluence/RuleData.lean
@@ -0,0 +1,33 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+-- AUTO-GENERATED by scripts/gen-rule-data.py from objectionary/phino resources/*.yaml.
+-- DO NOT EDIT BY HAND. Regenerate after phino's rules change.
+
+import PhiConfluence.RuleSchema
+
+/-!
+# Normalization rules as structured data, generated from phino
+
+The eleven rules as `RuleEntry` tags (types in PhiConfluence/RuleSchema.lean), emitted
+by the fidelity-lock deriver `scripts/gen-rule-data.py`. The CI build regenerates this
+file from pinned phino and compiles it, so the proof builds against phino's rules.
+-/
+
+namespace PhiConfluence
+
+/-- The φ-calculus normalization rules as structured, interpretable data. -/
+def normalizationRuleData : List RuleEntry :=
+  [ { name := "alpha", shape := .appForm, conds := [.alphaVoidOrdinal], rhs := .alphaRename }
+  , { name := "copy", shape := .appForm, conds := [.slotVoid, .argXiFree, .argNf], rhs := .copyFill }
+  , { name := "dc", shape := .appBot, conds := [], rhs := .bot }
+  , { name := "dd", shape := .dispatchBot, conds := [], rhs := .bot }
+  , { name := "dot", shape := .dispatchForm, conds := [.slotAttached, .valNf], rhs := .dotFeedback }
+  , { name := "miss", shape := .appForm, conds := [.slotAbsent, .attrNotAlpha], rhs := .bot }
+  , { name := "null", shape := .dispatchForm, conds := [.slotVoid], rhs := .bot }
+  , { name := "over", shape := .appForm, conds := [.slotAttached, .attrNeRho], rhs := .bot }
+  , { name := "phi", shape := .dispatchForm, conds := [.phiPresent, .slotAbsent], rhs := .phiExpand }
+  , { name := "stay", shape := .appForm, conds := [.attrIsRho, .slotAttached], rhs := .formSame }
+  , { name := "stop", shape := .dispatchForm, conds := [.slotAbsent, .phiAbsent, .noLambda], rhs := .bot } ]
+
+end PhiConfluence
diff --git a/PhiConfluence/RuleSchema.lean b/PhiConfluence/RuleSchema.lean
new file mode 100644
index 00000000..69918115
--- /dev/null
+++ b/PhiConfluence/RuleSchema.lean
@@ -0,0 +1,43 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+/-!
+# Schema for the generated rule data
+
+The typed vocabulary that `PhiConfluence/RuleData.lean` (generated from phino by
+`scripts/gen-rule-data.py`) is written in: each normalization rule is a `RuleEntry` of
+tags — the redex it fires on, its side-conditions, and its contractum. These are *data*
+describing the eleven `phino` rules; the proof relation `Step` (`Step.lean`) is the
+authoritative hand-written object, and `RuleData.lean` is kept identical to phino by the
+`rule-data-in-sync` CI job.
+-/
+
+namespace PhiConfluence
+
+/-- Which redex a rule fires on: `⊥.a`, `⊥(a↦arg)`, `⟦bs⟧.a`, or `⟦bs⟧(a↦arg)`. -/
+inductive RedexShape where
+  | dispatchBot | appBot | dispatchForm | appForm
+  deriving Repr, DecidableEq
+
+/-- A side condition on the redex's formation, attribute, and argument. -/
+inductive Cond where
+  | slotVoid | slotAttached | slotAbsent
+  | attrNeRho | attrIsRho | attrNotAlpha
+  | phiAbsent | phiPresent | noLambda
+  | valNf | argXiFree | argNf | alphaVoidOrdinal
+  deriving Repr, DecidableEq
+
+/-- The contractum a rule rewrites its redex to. -/
+inductive Contractum where
+  | bot | formSame | phiExpand | dotFeedback | copyFill | alphaRename
+  deriving Repr, DecidableEq
+
+/-- One normalization rule as structured data. (Named `RuleEntry`, not `RuleSpec`,
+to avoid colliding with `Render.lean`'s display-string `RuleSpec`.) -/
+structure RuleEntry where
+  name  : String
+  shape : RedexShape
+  conds : List Cond
+  rhs   : Contractum
+
+end PhiConfluence
diff --git a/REUSE.toml b/REUSE.toml
index 0355a763..54ef9512 100644
--- a/REUSE.toml
+++ b/REUSE.toml
@@ -5,6 +5,7 @@ version = 1
 [[annotations]]
 path = [
     ".gitignore",
+    ".phino-version",
     ".yamllint",
     "**.json",
     "**.md",
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index 9ac385c9..6682e8d5 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -150,8 +150,8 @@ independent directions:
 * **Tiny, human-readable trusted surface.** Only `Syntax`, `Step`, `↝∗`, and the
   `confluence` statement must be read and endorsed (a few dozen lines — the M0 spec).
 * **Rule transcription vs phino.** The eleven-rule *display* table (`Rules.lean`) is
-  **generated** from phino's `resources/*.yaml` by `gen-rules.py` and pinned by the
-  `rules-in-sync` CI job, so the displayed rules cannot drift from phino/the paper. The
+  **generated** from phino's `resources/*.yaml` by `gen-rules.py` and regenerated from
+  pinned phino in the CI build, so the displayed rules cannot drift from phino/the paper. The
   *proof relation* `Step` is hand-written (constructors are needed for case-analysis) and
   pinned to phino **behaviorally** by `difftest`.
 * **Differential testing against phino.** `Difftest.lean` + `scripts/difftest.sh` normalize
@@ -232,13 +232,15 @@ relation the confluence theorem governs.
 from phino's `resources/*.yaml` — the same source the paper's Fig. 4 is rendered from — so
 the displayed rules cannot drift from phino/the paper by construction.
 
-**CI** (single-purpose workflows, each on push to `master` + PRs, tracking phino-latest):
+**CI** (single-purpose workflows, each on push to `master` + PRs, against pinned phino):
 
-* **build** — install elan, `lake exe cache get`, `lake build`; then a `sorry`/`admit`/
-  `axiom` source gate **and** a `#print axioms` gate on the headline results.
-* **rules-in-sync** — `scripts/regen-rules.sh` clones `objectionary/phino` and regenerates
-  `Rules.lean`; `git diff --exit-code` fails if our committed table has drifted from phino.
-* **difftest** — install the `phino-latest` binary, build `difftest`, run
+* **build** — install elan and `lake exe cache get`; regenerate `Rules.lean` and
+  `RuleData.lean` from the pinned phino (`scripts/regen-rules.sh`,
+  `scripts/regen-rule-data.sh`) so the proof compiles against phino-derived rules; `lake
+  build`; then a `sorry`/`admit`/`axiom` source gate **and** a `#print axioms` gate on the
+  headline results. (`gen-rule-data.py`'s fidelity lock fails the build on rule-structure
+  drift.)
+* **difftest** — install the pinned phino binary (`.phino-version`), build `difftest`, run
   `scripts/difftest.sh`; fails if our reducer disagrees with phino.
 
 The two Lean workflows share a composite action (`.github/actions/setup-lean`) that caches
diff --git a/scripts/confluence-probe.sh b/scripts/confluence-probe.sh
index a5fc6903..9746f223 100755
--- a/scripts/confluence-probe.sh
+++ b/scripts/confluence-probe.sh
@@ -31,6 +31,7 @@ cd "$(dirname "$0")/.."
 ITERS="${ITERS:-24}"
 
 command -v phino >/dev/null 2>&1 || { echo "phino not on PATH; skipping" >&2; exit 0; }
+PHINO_VERSION="$(cat .phino-version)"
 
 RESOURCES="${PHINO_RESOURCES:-}"
 if [ -z "$RESOURCES" ]; then
@@ -50,7 +51,7 @@ total=0
 # Normal form of a file, or the sentinel <diverge>/<error> for an unfinished/failed run.
 norm() {
   local out ec
-  out=$($TO phino rewrite --normalize --depth-sensitive --flat "$1" 2>&1); ec=$?
+  out=$($TO phino --pin="$PHINO_VERSION" rewrite --normalize --depth-sensitive --flat "$1" 2>&1); ec=$?
   if [ "$ec" = 124 ]; then echo "<diverge>"
   elif [ "$ec" = 0 ]; then echo "$out"
   elif printf '%s' "$out" | grep -q 'depth-sensitive'; then echo "<diverge>"
@@ -71,16 +72,16 @@ probe() {
 
   local i s ec
   for ((i = 1; i <= ITERS; i++)); do
-    s=$($TO phino rewrite --normalize --shuffle --depth-sensitive --flat "$file" 2>&1); ec=$?
+    s=$($TO phino --pin="$PHINO_VERSION" rewrite --normalize --shuffle --depth-sensitive --flat "$file" 2>&1); ec=$?
     [ "$ec" = 0 ] && [ -n "$s" ] && samples+=("shuffle	$s")
   done
 
-  local canon; canon=$($TO phino rewrite --flat "$file" 2>&1)
+  local canon; canon=$($TO phino --pin="$PHINO_VERSION" rewrite --flat "$file" 2>&1)
   local rule forced nfr tmp
   tmp="$(mktemp)"
   for rule in $RULES; do
     [ -f "$RESOURCES/$rule.yaml" ] || continue
-    forced=$($TO phino rewrite --rule "$RESOURCES/$rule.yaml" --max-depth 1 --max-cycles 1 --flat "$file" 2>&1)
+    forced=$($TO phino --pin="$PHINO_VERSION" rewrite --rule "$RESOURCES/$rule.yaml" --max-depth 1 --max-cycles 1 --flat "$file" 2>&1)
     { [ -z "$forced" ] || [ "$forced" = "$canon" ]; } && continue
     printf '%s\n' "$forced" > "$tmp"
     nfr=$(norm "$tmp")
diff --git a/scripts/difftest.sh b/scripts/difftest.sh
index 7cc00a16..a7818d36 100755
--- a/scripts/difftest.sh
+++ b/scripts/difftest.sh
@@ -4,11 +4,13 @@
 #
 # Differential test: for each example program, check that phino's normal form
 # (`phino rewrite --normalize`) equals our reducer's normal form. The behavioral
-# pin between this prover's Step relation and phino. Requires `phino` on PATH.
+# pin between this prover's Step relation and phino. Requires `phino` on PATH,
+# pinned via `--pin` to the version in .phino-version (phino aborts on a mismatch).
 
 set -uo pipefail
 cd "$(dirname "$0")/.."
 export PATH="$HOME/.elan/bin:$PATH"
+PHINO_VERSION="$(cat .phino-version)"
 
 if ! command -v phino >/dev/null 2>&1; then
   echo "FATAL: phino not found on PATH; the differential test requires it (fail-fast, not skip)" >&2
@@ -22,7 +24,7 @@ count=0
 while IFS=$'\t' read -r input expected; do
   [ -z "${input:-}" ] && continue
   count=$((count + 1))
-  out=$(printf '%s\n' "$input" | phino rewrite --normalize --flat 2>/dev/null)
+  out=$(printf '%s\n' "$input" | phino --pin="$PHINO_VERSION" rewrite --normalize --flat 2>/dev/null)
   pn=$(printf '%s' "$out" | tr -d '[:space:]'); pn=${pn#Φ↦}
   ours=$(printf '%s' "$expected" | tr -d '[:space:]')
   if [ "$pn" = "$ours" ]; then
diff --git a/scripts/gen-rule-data.py b/scripts/gen-rule-data.py
new file mode 100644
index 00000000..a87cf31a
--- /dev/null
+++ b/scripts/gen-rule-data.py
@@ -0,0 +1,220 @@
+#!/usr/bin/env python3
+# SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com
+# SPDX-License-Identifier: MIT
+"""
+Generate PhiConfluence/RuleData.lean from phino's resources/*.yaml.
+
+Unlike `gen-rules.py` (which emits *display strings* for the demo), this emits the
+**structured** rule data: each rule becomes a `RuleEntry` of typed tags (redex shape,
+side-conditions, contractum), whose types are defined in PhiConfluence/RuleSchema.lean.
+The CI build regenerates PhiConfluence/RuleData.lean from pinned phino and then compiles
+it, so the proof always builds against phino-derived rules and a phino change that breaks
+compilation (or trips the fidelity lock below) fails the build.
+
+DESIGN — a *fidelity lock*, not a general translator.
+  phino's rule semantics live in its Haskell (`contextualize`, `isNF`, ordinals …),
+  not in the YAML, so the YAML cannot be mechanically translated into a Lean relation.
+  Instead this script carries one *locked interpretation*
+  per rule (the structured tags below) and ASSERTS that phino's current YAML still
+  renders to the pattern/result/condition this interpretation assumes — failing loudly
+  on any mismatch. The locked tags are emitted into RuleData.lean, which the CI build
+  regenerates from pinned phino and compiles — so phino-drift trips this assertion and
+  fails the build.
+
+This intentionally duplicates `gen-rules.py`'s `when`/`where` rendering (keep in sync) so
+the asserted condition strings match the display table's — one rendering, two consumers.
+
+Usage:
+    gen-rule-data.py <phino-resources-dir> <output-RuleData.lean>
+"""
+import glob
+import os
+import re
+import sys
+
+import yaml
+
+
+# --- condition/where rendering: identical to gen-rules.py (kept in sync on purpose) ---
+
+def rterm(x):
+    return str(x)
+
+
+def rcmp(x):
+    if isinstance(x, dict):
+        k = next(iter(x))
+        v = x[k]
+        if k == "index":
+            return f"index({rterm(v)})"
+        if k == "length":
+            return f"|{rterm(v)}|"
+        if k == "domain":
+            return f"domain({rterm(v)})"
+        return f"{k}({rterm(v)})"
+    return rterm(x)
+
+
+def rcond(w):
+    if w is None:
+        return ""
+    if not isinstance(w, dict):
+        return rterm(w)
+    k = next(iter(w))
+    v = w[k]
+    if k == "and":
+        return " and ".join(p for p in (rcond(x) for x in v) if p)
+    if k == "or":
+        return " or ".join(p for p in (rcond(x) for x in v) if p)
+    if k == "not":
+        return "¬(" + rcond(v) + ")"
+    if k == "in":
+        return f"{rterm(v[0])} ∈ {rterm(v[1])}"
+    if k == "nf":
+        return f"nf({rterm(v)})"
+    if k == "alpha":
+        return f"α-attr({rterm(v)})"
+    if k == "eq":
+        return f"{rcmp(v[0])} = {rcmp(v[1])}"
+    return f"{k}({rterm(v)})"
+
+
+def rwhere(ws):
+    parts = []
+    for w in ws or []:
+        meta = w.get("meta")
+        fn = w.get("function")
+        args = w.get("args", [])
+        parts.append(f"{meta} := {fn}({', '.join(rterm(a) for a in args)})")
+    return " and ".join(parts)
+
+
+def norm(s):
+    """Whitespace-insensitive comparison key (phino's pattern strings have stray spaces)."""
+    return re.sub(r"\s+", " ", s or "").strip()
+
+
+# --- the locked interpretation: one entry per phino rule -------------------------------
+#
+# Each entry asserts phino's rendered (pattern, result, cond, where) and, on a match,
+# contributes the structured Lean tags. `shape`/`conds`/`rhs` are Lean `RuleSpec` field
+# expressions; they MUST stay in step with PhiConfluence/RuleSchema.lean's inductives.
+# `expect` strings are phino's current YAML as rendered above (== the gen-rules.py table).
+#
+# If phino's YAML drifts from `expect`, this script aborts (see `check`) — that is the
+# point. If the *interpretation* (tags) is what changed, the Lean `conformance` theorem
+# is what fails. Adding/removing a phino rule trips the name-set assertion in `main`.
+
+LOCK = {
+    "dd": dict(
+        expect=("⊥.𝜏", "⊥", "", ""),
+        shape=".dispatchBot", conds="[]", rhs=".bot"),
+    "dc": dict(
+        expect=("⊥(𝜏 ↦ 𝑒)", "⊥", "", ""),
+        shape=".appBot", conds="[]", rhs=".bot"),
+    "null": dict(
+        expect=("⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧.𝜏", "⊥", "", ""),
+        shape=".dispatchForm", conds="[.slotVoid]", rhs=".bot"),
+    "over": dict(
+        expect=("⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧(𝜏 ↦ 𝑒2)", "⊥", "¬(𝜏 = ρ)", ""),
+        shape=".appForm", conds="[.slotAttached, .attrNeRho]", rhs=".bot"),
+    "stop": dict(
+        expect=("⟦𝐵⟧.𝜏", "⊥", "¬(𝜏 ∈ 𝐵) and ¬(φ ∈ 𝐵) and ¬(λ ∈ 𝐵)", ""),
+        shape=".dispatchForm", conds="[.slotAbsent, .phiAbsent, .noLambda]", rhs=".bot"),
+    "miss": dict(
+        expect=("⟦𝐵⟧(𝜏 ↦ 𝑒)", "⊥", "¬(𝜏 ∈ 𝐵) and ¬(α-attr(𝜏))", ""),
+        shape=".appForm", conds="[.slotAbsent, .attrNotAlpha]", rhs=".bot"),
+    "stay": dict(
+        expect=("⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧(ρ ↦ 𝑒2)", "⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧", "", ""),
+        shape=".appForm", conds="[.attrIsRho, .slotAttached]", rhs=".formSame"),
+    "phi": dict(
+        expect=("⟦𝐵⟧.𝜏", "⟦𝐵⟧.φ.𝜏", "φ ∈ 𝐵 and ¬(𝜏 ∈ 𝐵)", ""),
+        shape=".dispatchForm", conds="[.phiPresent, .slotAbsent]", rhs=".phiExpand"),
+    "alpha": dict(
+        expect=("⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏2 ↦ 𝑒)", "⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒)",
+                "index(𝜏2) = domain(𝐵1)", ""),
+        shape=".appForm", conds="[.alphaVoidOrdinal]", rhs=".alphaRename"),
+    "dot": dict(
+        expect=("⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧.𝜏", "𝑒2(ρ ↦ ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧)", "nf(𝑒1)",
+                "𝑒2 := contextualize(𝑒1, ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧)"),
+        shape=".dispatchForm", conds="[.slotAttached, .valNf]", rhs=".dotFeedback"),
+    # NOTE — copy keeps phino's `xi-free` guard in the DATA (Step.copy carries `xiFree`);
+    # only the DISPLAY table (gen-rules.py) strips ξ for paper-figure parity.
+    "copy": dict(
+        expect=("⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑒)", "⟦ 𝐵1, 𝜏 ↦ 𝑒, 𝐵2 ⟧",
+                "xi-free(𝑒) and nf(𝑒)", ""),
+        shape=".appForm", conds="[.slotVoid, .argXiFree, .argNf]", rhs=".copyFill"),
+}
+
+
+def check(name, got, want):
+    g = tuple(norm(x) for x in got)
+    w = tuple(norm(x) for x in want)
+    if g != w:
+        raise SystemExit(
+            f"FIDELITY-LOCK BREACH for rule '{name}': phino's YAML no longer matches the "
+            f"locked interpretation in gen-rule-data.py.\n  phino : {g}\n  locked: {w}\n"
+            f"Re-read the phino rule, update LOCK['{name}'] AND the matching tags, and "
+            f"re-verify PhiConfluence/RuleConform.lean's `conformance` against `Step`.")
+
+
+def main():
+    if len(sys.argv) != 3:
+        raise SystemExit("Usage: gen-rule-data.py <phino-resources-dir> <output-RuleData.lean>")
+    res_dir, out = sys.argv[1], sys.argv[2]
+    found = {}
+    for path in sorted(glob.glob(os.path.join(res_dir, "*.yaml"))):
+        with open(path, encoding="utf-8") as f:
+            d = yaml.safe_load(f)
+        name = str(d["name"])
+        if name in found:
+            raise SystemExit(f"duplicate rule name '{name}' in {res_dir}")
+        got = (str(d["pattern"]), str(d["result"]), rcond(d.get("when")), rwhere(d.get("where")))
+        if name not in LOCK:
+            raise SystemExit(f"phino has an UNLOCKED rule '{name}' — add it to LOCK and to Step/conformance")
+        check(name, got, LOCK[name]["expect"])
+        found[name] = LOCK[name]
+    missing = set(LOCK) - set(found)
+    if missing:
+        raise SystemExit(f"locked rules absent from phino's resources: {sorted(missing)}")
+    lines = [
+        # REUSE-IgnoreStart
+        "-- SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com",
+        "-- SPDX-License-Identifier: MIT",
+        # REUSE-IgnoreEnd
+        "",
+        "-- AUTO-GENERATED by scripts/gen-rule-data.py from objectionary/phino resources/*.yaml.",
+        "-- DO NOT EDIT BY HAND. Regenerate after phino's rules change.",
+        "",
+        "import PhiConfluence.RuleSchema",
+        "",
+        "/-!",
+        "# Normalization rules as structured data, generated from phino",
+        "",
+        "The eleven rules as `RuleEntry` tags (types in PhiConfluence/RuleSchema.lean), emitted",
+        "by the fidelity-lock deriver `scripts/gen-rule-data.py`. The CI build regenerates this",
+        "file from pinned phino and compiles it, so the proof builds against phino's rules.",
+        "-/",
+        "",
+        "namespace PhiConfluence",
+        "",
+        "/-- The φ-calculus normalization rules as structured, interpretable data. -/",
+        "def normalizationRuleData : List RuleEntry :=",
+    ]
+    entries = []
+    for name in sorted(found):
+        e = found[name]
+        entries.append(
+            '  { name := "%s", shape := %s, conds := %s, rhs := %s }'
+            % (name, e["shape"], e["conds"], e["rhs"]))
+    lines.append("  [ " + "\n  , ".join(x.strip() for x in entries) + " ]")
+    lines.append("")
+    lines.append("end PhiConfluence")
+    lines.append("")
+    with open(out, "w", encoding="utf-8") as f:
+        f.write("\n".join(lines))
+    print(f"wrote {out} with {len(found)} rules (fidelity lock held)")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/scripts/gen-rules.py b/scripts/gen-rules.py
index ddae3fc9..73358e73 100644
--- a/scripts/gen-rules.py
+++ b/scripts/gen-rules.py
@@ -18,7 +18,10 @@
 Usage:
     gen-rules.py <phino-resources-dir> <output-Rules.lean>
 """
-import sys, os, glob
+import glob
+import os
+import sys
+
 import yaml
 
 
@@ -28,7 +31,8 @@ def rterm(x):
 
 def rcmp(x):
     if isinstance(x, dict):
-        k = next(iter(x)); v = x[k]
+        k = next(iter(x))
+        v = x[k]
         if k == "index":
             return f"index({rterm(v)})"
         if k == "length":
@@ -42,7 +46,8 @@ def rcond(w):
         return ""
     if not isinstance(w, dict):
         return rterm(w)
-    k = next(iter(w)); v = w[k]
+    k = next(iter(w))
+    v = w[k]
     if k == "and":
         return " and ".join(p for p in (rcond(x) for x in v) if p)
     if k == "or":
@@ -65,7 +70,9 @@ def rcond(w):
 def rwhere(ws):
     parts = []
     for w in ws or []:
-        meta = w.get("meta"); fn = w.get("function"); args = w.get("args", [])
+        meta = w.get("meta")
+        fn = w.get("function")
+        args = w.get("args", [])
         parts.append(f"{meta} := {fn}({', '.join(rterm(a) for a in args)})")
     return " and ".join(parts)
 
diff --git a/scripts/regen-rule-data.sh b/scripts/regen-rule-data.sh
new file mode 100644
index 00000000..b5194db2
--- /dev/null
+++ b/scripts/regen-rule-data.sh
@@ -0,0 +1,27 @@
+#!/usr/bin/env bash
+# SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com
+# SPDX-License-Identifier: MIT
+#
+# Regenerate PhiConfluence/RuleData.lean from the PINNED phino rules on GitHub
+# (objectionary/phino at the tag in .phino-version). The fidelity lock in
+# scripts/gen-rule-data.py aborts if phino's rules drift from the locked interpretation.
+# The CI build runs this before `lake build`, so the proof compiles against phino's rules.
+#
+# Usage: bash scripts/regen-rule-data.sh
+
+set -euo pipefail
+cd "$(dirname "$0")/.."
+
+PHINO_REPO="${PHINO_REPO:-https://github.com/objectionary/phino}"
+PHINO_VERSION="$(cat .phino-version)"
+# phino's package/binary version is 4-part (0.0.0.74), but its git tags drop the
+# leading component (0.0.74).
+PHINO_TAG="${PHINO_VERSION#0.}"
+tmp="$(mktemp -d)"
+trap 'rm -rf "$tmp"' EXIT
+
+echo "cloning $PHINO_REPO at tag $PHINO_TAG (phino $PHINO_VERSION, pinned via .phino-version) ..."
+git clone --depth 1 --branch "$PHINO_TAG" "$PHINO_REPO" "$tmp/phino" >/dev/null 2>&1
+
+python3 scripts/gen-rule-data.py "$tmp/phino/resources" PhiConfluence/RuleData.lean
+echo "done — PhiConfluence/RuleData.lean regenerated from phino $PHINO_VERSION"
diff --git a/scripts/regen-rules.sh b/scripts/regen-rules.sh
index 4200faf4..eac72e89 100755
--- a/scripts/regen-rules.sh
+++ b/scripts/regen-rules.sh
@@ -2,9 +2,10 @@
 # SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com
 # SPDX-License-Identifier: MIT
 #
-# Regenerate PhiConfluence/Rules.lean from the LATEST phino rules on GitHub
-# (objectionary/phino master). The rule source is phino's repo — the same source the
-# paper's Fig. 4 is generated from — not any local checkout.
+# Regenerate PhiConfluence/Rules.lean from the PINNED phino rules on GitHub
+# (objectionary/phino at the tag in .phino-version). The rule source is phino's repo —
+# the same source the paper's Fig. 4 is generated from — not any local checkout. Pinning
+# keeps regeneration deterministic: tracking master let phino drift break this in CI.
 #
 # Usage: bash scripts/regen-rules.sh
 
@@ -12,11 +13,15 @@ set -euo pipefail
 cd "$(dirname "$0")/.."
 
 PHINO_REPO="${PHINO_REPO:-https://github.com/objectionary/phino}"
+PHINO_VERSION="$(cat .phino-version)"
+# phino's package/binary version is 4-part (0.0.0.74 — what --pin and the release
+# artifacts use), but its git tags drop the leading component (0.0.74).
+PHINO_TAG="${PHINO_VERSION#0.}"
 tmp="$(mktemp -d)"
 trap 'rm -rf "$tmp"' EXIT
 
-echo "cloning $PHINO_REPO (master = latest) ..."
-git clone --depth 1 "$PHINO_REPO" "$tmp/phino" >/dev/null 2>&1
+echo "cloning $PHINO_REPO at tag $PHINO_TAG (phino $PHINO_VERSION, pinned via .phino-version) ..."
+git clone --depth 1 --branch "$PHINO_TAG" "$PHINO_REPO" "$tmp/phino" >/dev/null 2>&1
 
 python3 scripts/gen-rules.py "$tmp/phino/resources" PhiConfluence/Rules.lean
-echo "done — PhiConfluence/Rules.lean regenerated from phino master"
+echo "done — PhiConfluence/Rules.lean regenerated from phino $PHINO_VERSION"