diff --git a/.github/workflows/eqy.yml b/.github/workflows/eqy.yml
new file mode 100644
index 0000000..3e205d1
--- /dev/null
+++ b/.github/workflows/eqy.yml
@@ -0,0 +1,188 @@
+name: eqy
+
+# =============================================================================
+# Yosys EQY formal equivalence gate — Wave-24 RVR-017 · Issue #4 Change N
+#
+# Purpose:
+#   Verify that hand-written src/*.v modules are formally equivalent to the
+#   reference Verilog generated by `t27c gen-verilog` from the t27 spec
+#   (repository gHashTag/t27 @ T27C_COMMIT).
+#
+# Verdicts:
+#   PASS    — EQY confirmed equivalence (blocks merge if any FAIL)
+#   FAIL    — EQY found non-equivalence  ← blocks merge
+#   PENDING — t27c reference file missing (warns, does NOT block)
+#
+# Anchor: phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877
+# =============================================================================
+
+on:
+  push:
+    branches:
+      - '**'
+  pull_request:
+    branches:
+      - main
+      - 'feat/**'
+
+jobs:
+  eqy-check:
+    name: Yosys EQY t27c↔src equivalence
+    runs-on: ubuntu-22.04
+
+    env:
+      # Pinned gHashTag/t27 commit that owns the reference Verilog files.
+      # Update this when a new t27c gen-verilog run produces build/t27c/*.v
+      T27C_COMMIT: "9752bab4b81fe1a3abc66b13749c4ac412a74ee6"
+      # EQY_STRICT=0 — PENDING verdicts warn but do not fail CI
+      # Set to "1" after build/t27c/*.v are committed to block on PENDING
+      EQY_STRICT: "0"
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Install system dependencies
+        run: |
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends \
+            build-essential \
+            python3 \
+            python3-pip \
+            tcl \
+            libreadline-dev \
+            bison \
+            flex \
+            wget \
+            ca-certificates
+
+      - name: Install Yosys (pinned apt package)
+        run: |
+          # Install Yosys from apt — Ubuntu 22.04 ships Yosys 0.9 (uses -V not --version)
+          sudo apt-get install -y --no-install-recommends yosys
+          # Yosys 0.9 uses -V flag; newer versions support --version
+          yosys -V 2>/dev/null || yosys --version 2>/dev/null || echo "yosys installed (version flag varies)"
+
+      - name: Install Yosys EQY
+        # Non-fatal: if eqy is unavailable, script marks modules PENDING (R5-honest)
+        # EQY_STRICT=0 means PENDING verdicts warn but do not block CI
+        continue-on-error: true
+        run: |
+          # Install eqy from YosysHQ/eqy source (pip package name varies by version)
+          # Try multiple install methods in order; non-fatal per continue-on-error
+          pip3 install --user yosys-eqy 2>&1 && echo "Installed via pip yosys-eqy" && exit 0
+          echo "pip yosys-eqy failed, trying pip eqy..."
+          pip3 install --user eqy 2>&1 && echo "Installed via pip eqy" && exit 0
+          echo "Both pip methods failed. EQY will be marked NOT_INSTALLED."
+          echo "Modules will receive PENDING verdict (acceptable with EQY_STRICT=0)."
+          exit 0  # always succeed — script handles missing eqy gracefully
+
+      - name: Show toolchain versions
+        run: |
+          echo "=== Yosys version ==="
+          yosys -V 2>/dev/null || yosys --version 2>/dev/null || echo "yosys not found"
+          echo "=== EQY version ==="
+          eqy --version 2>/dev/null || echo "eqy not found (will mark PENDING)"
+          echo "=== Python version ==="
+          python3 --version
+          echo "=== T27C_COMMIT ==="
+          echo "${T27C_COMMIT}"
+
+      - name: Create evidence directory
+        run: mkdir -p evidence
+
+      - name: Run EQY equivalence check
+        id: eqy_run
+        run: |
+          bash scripts/eqy_check.sh
+        continue-on-error: true
+
+      - name: Evaluate verdict (FAIL blocks, PENDING warns)
+        run: |
+          echo "=== Evidence files written ==="
+          ls -la evidence/eqy_*.json 2>/dev/null || echo "(no evidence files)"
+
+          # Parse verdicts from JSON evidence
+          FAIL_COUNT=0
+          PENDING_COUNT=0
+          PASS_COUNT=0
+
+          for f in evidence/eqy_*.json; do
+            if [[ -f "$f" ]]; then
+              MODULE=$(python3 -c "import json; print(json.load(open('$f'))['module'])")
+              VERDICT=$(python3 -c "import json; print(json.load(open('$f'))['verdict'])")
+              echo "  ${MODULE}: ${VERDICT}"
+              case "${VERDICT}" in
+                PASS)    PASS_COUNT=$((PASS_COUNT + 1)) ;;
+                FAIL)    FAIL_COUNT=$((FAIL_COUNT + 1)) ;;
+                PENDING) PENDING_COUNT=$((PENDING_COUNT + 1)) ;;
+              esac
+            fi
+          done
+
+          echo ""
+          echo "=== Summary ==="
+          echo "  PASS:    ${PASS_COUNT}"
+          echo "  PENDING: ${PENDING_COUNT}"
+          echo "  FAIL:    ${FAIL_COUNT}"
+          echo ""
+          echo "Anchor: phi^2 + phi^-2 = 3 · Wave-24 RVR-017"
+
+          # PENDING warning (R5-honest)
+          if [[ ${PENDING_COUNT} -gt 0 ]]; then
+            echo ""
+            echo "::warning::${PENDING_COUNT} module(s) are PENDING — t27c gen-verilog output"
+            echo "::warning::not yet committed to build/t27c/. See docs/EQY_CHECK.md for status."
+            echo "::warning::Set EQY_STRICT=1 in workflow env once build/t27c/*.v are committed."
+          fi
+
+          # FAIL is a hard blocker
+          if [[ ${FAIL_COUNT} -gt 0 ]]; then
+            echo "::error::${FAIL_COUNT} module(s) FAILED formal equivalence check."
+            echo "::error::Merge is BLOCKED until all modules pass EQY."
+            exit 1
+          fi
+
+          echo "EQY gate PASSED (no FAIL verdicts)."
+
+      - name: Upload evidence artifacts
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: eqy-evidence-${{ github.sha }}
+          path: evidence/eqy_*.json
+          retention-days: 90
+
+      - name: Generate GitHub Step Summary
+        if: always()
+        run: |
+          echo "## Yosys EQY Formal Equivalence — Wave-24 RVR-017" >> $GITHUB_STEP_SUMMARY
+          echo "" >> $GITHUB_STEP_SUMMARY
+          echo "| Module | Verdict | t27c SHA | src SHA |" >> $GITHUB_STEP_SUMMARY
+          echo "|--------|---------|----------|---------|" >> $GITHUB_STEP_SUMMARY
+
+          for f in evidence/eqy_*.json; do
+            if [[ -f "$f" ]]; then
+              python3 - <<'PYEOF'
+          import json, sys, os
+          f = sys.argv[1] if len(sys.argv) > 1 else None
+          import glob
+          files = glob.glob('evidence/eqy_*.json')
+          for fp in sorted(files):
+              d = json.load(open(fp))
+              v = d['verdict']
+              icon = {'PASS': '✅', 'FAIL': '❌', 'PENDING': '⏳'}.get(v, '?')
+              t_sha = d.get('t27c_sha', 'MISSING')[:16] if d.get('t27c_sha') != 'MISSING' else 'MISSING'
+              s_sha = d.get('src_sha', 'MISSING')[:16]
+              print(f"| {d['module']} | {icon} {v} | {t_sha} | {s_sha} |")
+          PYEOF
+              break
+            fi
+          done >> $GITHUB_STEP_SUMMARY || true
+
+          echo "" >> $GITHUB_STEP_SUMMARY
+          echo "**T27C_COMMIT:** \`${T27C_COMMIT}\`" >> $GITHUB_STEP_SUMMARY
+          echo "" >> $GITHUB_STEP_SUMMARY
+          echo "> Anchor: \`phi^2 + phi^-2 = 3 · Wave-24 RVR-017 · DOI 10.5281/zenodo.19227877\`" >> $GITHUB_STEP_SUMMARY
diff --git a/docs/EQY_CHECK.md b/docs/EQY_CHECK.md
new file mode 100644
index 0000000..2b444a3
--- /dev/null
+++ b/docs/EQY_CHECK.md
@@ -0,0 +1,242 @@
+# EQY_CHECK.md — Yosys Formal Equivalence Manifest
+
+**Wave-24 · RVR-017 · Issue #4 Change N**
+**Anchor:** `phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877`
+**R5-honest disclosure required in "Current Status" section — see below.**
+
+---
+
+## Purpose
+
+This document is the reproducibility manifest for the **Yosys EQY formal
+equivalence gate** between two Verilog representations of the GoldenFloat-16
+silicon modules:
+
+| Representation | Description | Path |
+|---|---|---|
+| **GOLD** (reference) | Generated by `t27c gen-verilog` from the `.t27`/`.tri` algebraic spec in `gHashTag/t27` | `build/t27c/<module>.v` |
+| **GATE** (submission) | Hand-written RTL targeting TTSKY26c silicon submission | `src/<module>.v` |
+
+**Why this matters for the PhD defense (Glava 35 R14):**
+
+The Trinity thesis claim is `φ² + φ⁻² = 3` — a Coq-proven algebraic identity
+that flows from theorem to generated Verilog to silicon. The chain is:
+
+```
+Coq theorem (t27/trios-coq/)
+      │ t27c gen-verilog
+      ▼
+build/t27c/<module>.v   ←──  EQY  ──→   src/<module>.v
+                                          │
+                              TTSKY26c silicon submission
+```
+
+Without EQY, the hand-written RTL is an **unverified translation** of the
+proven spec. EQY closes this gap formally.
+
+---
+
+## Algebraic Anchor (φ²+φ⁻²=3)
+
+The golden ratio φ = (1+√5)/2 satisfies the identity:
+
+```
+φ² + φ⁻² = 3
+```
+
+This is the structural constant that determines the GoldenFloat-16 (GF16) format:
+- 1 sign bit
+- 6 exponent bits (bias 31, φ-derived)
+- 9 mantissa bits
+
+All arithmetic operations (`gf16_mul`, `gf16_add`, `gf16_dot4`) are derived
+from properties of this identity. The EQY equivalence check confirms that
+the synthesisable RTL preserves these properties bit-exactly.
+
+**DOI:** `10.5281/zenodo.19227877`
+**Coq base:** `gHashTag/t27/trios-coq/` (canonical SoT, post-2026-05-12 consolidation)
+
+---
+
+## Modules Under Audit
+
+| Module | `src/` path | `build/t27c/` spec path | Coq theorem citation | Current verdict |
+|---|---|---|---|---|
+| `gf16_mul` | `src/gf16_mul.v` | `build/t27c/gf16_mul.v` | `t27/trios-coq/IGLA/gf16_precision.v::lucas_values_gf16_exact_n1` | ⏳ PENDING |
+| `gf16_add` | `src/gf16_add.v` | `build/t27c/gf16_add.v` | `t27/trios-coq/IGLA/lucas_closure_gf16.v::lucas_closure_phi_sq` | ⏳ PENDING |
+| `gf16_dot4` | `src/gf16_dot4.v` | `build/t27c/gf16_dot4.v` | `t27/trios-coq/IGLA/gf16_precision.v::lucas_4_eq_7` | ⏳ PENDING |
+| `trinity_gf16_tile` | `src/trinity_gf16_tile.v` | `build/t27c/trinity_gf16_tile.v` | `t27/trios-coq/IGLA/IGLA_ASHA_Bound.v::champion_survives_pruning` | ⏳ PENDING |
+
+**Verdict key:**
+- ✅ PASS — EQY formal proof of equivalence confirmed this run
+- ❌ FAIL — EQY found non-equivalence; merge blocked
+- ⏳ PENDING — `t27c gen-verilog` output not yet committed to `build/t27c/`
+
+---
+
+## Toolchain Pins
+
+| Tool | Pinned version | Source | Purpose |
+|---|---|---|---|
+| **Yosys** | ≥ 0.40 (apt ubuntu-22.04) | https://github.com/YosysHQ/yosys | Synthesis + EQY backend |
+| **Yosys EQY** | ≥ 0.1 (`pip install yosys-eqy`) | https://github.com/YosysHQ/eqy | Formal equivalence checker |
+| **t27c** (bootstrap) | commit `9752bab4b81fe1a3abc66b13749c4ac412a74ee6` | https://github.com/gHashTag/t27 | Reference Verilog generator |
+| **Python** | ≥ 3.10 | system | Evidence JSON writer |
+
+### t27c version pin rationale
+
+`t27c` is the bootstrap Python compiler at `gHashTag/t27/bootstrap/t27c.py`.
+At the time of this PR, the t27 repository HEAD is commit
+`9752bab4b81fe1a3abc66b13749c4ac412a74ee6`. The `t27c gen-verilog` command
+generates Verilog from `.t27` spec files; the output for the GF16 numeric
+modules lives in `gen/verilog/numeric/` in that repo.
+
+**The specific `build/t27c/<module>.v` files for `gf16_mul`, `gf16_add`,
+`gf16_dot4`, and `trinity_gf16_tile` are not yet committed to this repo** —
+see "Current Status" below for the tracker issue.
+
+---
+
+## Reproduction Recipe
+
+Three commands to reproduce the EQY check from scratch:
+
+```bash
+# 1. Install Yosys + EQY (Ubuntu 22.04)
+sudo apt-get install -y yosys && pip3 install yosys-eqy
+
+# 2. Run the equivalence check (set T27C_COMMIT to the pinned t27 commit)
+T27C_COMMIT=9752bab4b81fe1a3abc66b13749c4ac412a74ee6 bash scripts/eqy_check.sh
+
+# 3. Inspect evidence
+cat evidence/eqy_*.json | python3 -m json.tool
+```
+
+For strict mode (PENDING treated as failure):
+```bash
+EQY_STRICT=1 T27C_COMMIT=9752bab4b81fe1a3abc66b13749c4ac412a74ee6 \
+    bash scripts/eqy_check.sh
+```
+
+---
+
+## Evidence Schema
+
+Each run of `scripts/eqy_check.sh` writes one JSON file per module to
+`evidence/eqy_<GIT_SHA>_<module>.json` with the following schema:
+
+```json
+{
+  "module":        "<module name>",
+  "src_sha":       "<sha256 of src/<module>.v, or MISSING>",
+  "t27c_sha":      "<sha256 of build/t27c/<module>.v, or MISSING>",
+  "eqy_version":   "<eqy --version output, or NOT_INSTALLED>",
+  "yosys_version": "<yosys --version output, or NOT_INSTALLED>",
+  "verdict":       "PASS | FAIL | PENDING",
+  "timestamp_utc": "<ISO-8601>",
+  "evidence_path": "<path to this file>",
+  "anchor":        "phi^2 + phi^-2 = 3 · Wave-24 RVR-017 · DOI 10.5281/zenodo.19227877",
+  "t27c_commit":   "<T27C_COMMIT env var>",
+  "coq_citation":  "<Coq theorem file::theorem_name>",
+  "r5_note":       "PENDING = t27c gen-verilog output not yet committed to build/t27c/"
+}
+```
+
+**R5-honest rule:** the `verdict` field is `PASS` only if EQY exit code was 0
+in this run. No manual overrides. The script will not emit `PASS` unless it
+actually ran EQY to completion.
+
+---
+
+## Current Status (R5-honest)
+
+> **This section is required reading for PhD defense auditors and Wave-24 reviewers.**
+> R5 demands honest disclosure of what is and is not verified.
+
+### What is PASSING
+
+| Item | Status | Evidence |
+|---|---|---|
+| `scripts/eqy_check.sh` exits 0 for PENDING modules | ✅ | Script design: PENDING returns 0, FAIL returns 1 |
+| CI workflow `.github/workflows/eqy.yml` exists and runs | ✅ | This PR |
+| Evidence JSON schema is defined and written per run | ✅ | See above |
+
+### What is PENDING and Why
+
+| Module | Reason | Tracker |
+|---|---|---|
+| `gf16_mul` | `build/t27c/gf16_mul.v` not yet generated from t27 spec | Follow-up: commit t27c output |
+| `gf16_add` | `build/t27c/gf16_add.v` not yet generated from t27 spec | Follow-up: commit t27c output |
+| `gf16_dot4` | `build/t27c/gf16_dot4.v` not yet generated from t27 spec | Follow-up: commit t27c output |
+| `trinity_gf16_tile` | `build/t27c/trinity_gf16_tile.v` not yet generated from t27 spec | Follow-up: commit t27c output |
+
+**Root cause:** The `t27c gen-verilog` command in `gHashTag/t27/bootstrap/t27c.py`
+currently supports `gen-zig` and `parse` subcommands. The GF16 numeric modules
+exist as generated Verilog in `t27/gen/verilog/numeric/gf16.v` (for the
+`triformat_gf16` spec), but the specific module names `gf16_mul`, `gf16_add`,
+`gf16_dot4`, and `trinity_gf16_tile` corresponding to the hand-written `src/*.v`
+files have not yet been committed to `build/t27c/` in this repo.
+
+**Impact on the PhD defense claim:** The EQY scaffolding is fully in place.
+The claim "Coq→t27c→src EQY PASS" will be achievable once the `build/t27c/*.v`
+files are committed. The scaffolding itself (this PR) is the prerequisite
+deliverable for Change N of Issue #4.
+
+**Activation path:**
+1. Run `t27c gen-verilog` for each module from `gHashTag/t27` @ `9752bab`
+2. Commit output to `build/t27c/gf16_mul.v`, `build/t27c/gf16_add.v`, etc.
+3. Re-run `bash scripts/eqy_check.sh` — verdicts will upgrade from PENDING → PASS/FAIL
+4. Set `EQY_STRICT: "1"` in `.github/workflows/eqy.yml` to harden the CI gate
+
+### What is not covered by this PR
+
+- **Change A** (`gf16_mul.v` LUT replacement) — separate lane, see PR #35 sibling
+- **Change C** (Wallace-tree `gf16_dot4.v`) — Lane W, concurrent with this PR
+- **OpenLane2 synthesis** — not affected by this tooling PR (no RTL modified)
+
+---
+
+## Coq Citation Map (R14)
+
+Each module under EQY audit traces to one or more theorems in the
+`gHashTag/t27/trios-coq/` Coq library (canonical SoT, v1.3 mapping).
+
+| Module | Coq file (canonical path) | Theorem name | Status |
+|---|---|---|---|
+| `gf16_mul` | `t27/trios-coq/IGLA/gf16_precision.v` | `lucas_values_gf16_exact_n1`, `lucas_values_gf16_exact_n2` | Proven (Qed) |
+| `gf16_add` | `t27/trios-coq/IGLA/lucas_closure_gf16.v` | `lucas_closure_phi_sq`, `phi_sq_plus_phi_inv_sq` | Proven (Qed) |
+| `gf16_dot4` | `t27/trios-coq/IGLA/gf16_precision.v` | `lucas_4_eq_7`, `lucas_2_eq_3` | Proven (Qed) |
+| `trinity_gf16_tile` | `t27/trios-coq/IGLA/IGLA_ASHA_Bound.v` | `champion_survives_pruning`, `prune_threshold_from_trinity` | Proven (Qed) |
+
+The Coq theorems live in the canonical post-2026-05-12 consolidation SoT at
+[gHashTag/t27/trios-coq/IGLA/](https://github.com/gHashTag/t27/tree/main/trios-coq/IGLA).
+Pre-consolidation paths under `trinity-clara/proofs/igla/` are frozen mirrors —
+do not write new proofs there.
+
+---
+
+## Sibling Skills
+
+- **`coq-runtime-invariants` v1.3** — canonical SoT for the Coq→Rust proof bridge;
+  the Coq theorem citations in the table above follow its v1.3 path mapping from
+  `trinity-clara/proofs/igla/` → `t27/trios-coq/IGLA/`.
+- **Wave-24 Lane W** (Change C, Wallace-tree `gf16_dot4_wallace.v`) — concurrent PR,
+  no file overlap with this Lane E. Both PRs target `feat/silicon-g1-followup`.
+- **RVR-015 (Issue #34)** — formal audit that pre-registered Wave-24 changes A, C, N.
+
+---
+
+## References
+
+- Issue #4 Change N: https://github.com/gHashTag/tt-trinity-gf16/issues/4
+- Issue #34 RVR-015: https://github.com/gHashTag/tt-trinity-gf16/issues/34
+- Yosys EQY: https://github.com/YosysHQ/eqy
+- t27 upstream (canonical): https://github.com/gHashTag/t27
+- t27c bootstrap compiler: https://github.com/gHashTag/t27/blob/main/bootstrap/t27c.py
+- trios-coq canonical SoT: https://github.com/gHashTag/t27/tree/main/trios-coq/IGLA
+- Zenodo DOI: https://doi.org/10.5281/zenodo.19227877
+
+---
+
+*Wave-24 · RVR-017 · Vasilev Dmitrii <admin@t27.ai> · DO NOT MERGE PRE-TTSKY26c*
+*phi^2 + phi^-2 = 3 · NEVER STOP*
diff --git a/evidence/.gitkeep b/evidence/.gitkeep
new file mode 100644
index 0000000..e69de29
diff --git a/scripts/eqy_check.sh b/scripts/eqy_check.sh
new file mode 100755
index 0000000..afcf374
--- /dev/null
+++ b/scripts/eqy_check.sh
@@ -0,0 +1,325 @@
+#!/usr/bin/env bash
+# =============================================================================
+# scripts/eqy_check.sh — Yosys EQY formal equivalence checker
+# =============================================================================
+#
+# Wave-24 · RVR-017 · Issue #4 Change N
+# Anchor: phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877
+#
+# PURPOSE
+#   Wire Yosys EQY (open-source formal equivalence checking) between two
+#   Verilog implementations of each target module:
+#     GOLD  — build/t27c/<module>.v  (generated by `t27c gen-verilog`)
+#     GATE  — src/<module>.v          (hand-written, TTSKY26c submission target)
+#
+#   This closes the "Coq→silicon gap": Coq theorems prove the t27 spec correct;
+#   t27c emits Verilog from that spec; EQY proves the hand-written RTL is
+#   bit-exactly equivalent to the generated RTL.
+#
+# MODULES UNDER AUDIT
+#   gf16_mul         src/gf16_mul.v
+#   gf16_add         src/gf16_add.v
+#   gf16_dot4        src/gf16_dot4.v
+#   trinity_gf16_tile  src/trinity_gf16_tile.v
+#
+# VERDICT STATES (R5-honest)
+#   PASS    — EQY exited 0; formal equivalence confirmed this run
+#   FAIL    — EQY exited non-zero; equivalence NOT confirmed
+#   PENDING — t27c-generated reference file missing; check deferred
+#             (see docs/EQY_CHECK.md "Current Status" for tracker)
+#
+# EVIDENCE SCHEMA (written to evidence/eqy_<GIT_SHA>_<module>.json)
+#   {
+#     "module":        string,
+#     "src_sha":       string (SHA-256 of src file),
+#     "t27c_sha":      string (SHA-256 of build/t27c file, or "MISSING"),
+#     "eqy_version":   string (eqy --version output, or "NOT_INSTALLED"),
+#     "yosys_version": string (yosys --version output, or "NOT_INSTALLED"),
+#     "verdict":       "PASS" | "FAIL" | "PENDING",
+#     "timestamp_utc": ISO-8601,
+#     "evidence_path": string
+#   }
+#
+# USAGE
+#   bash scripts/eqy_check.sh
+#   EQY_STRICT=1 bash scripts/eqy_check.sh   # exit 1 on PENDING (default: warn)
+#
+# TOOLCHAIN PINS (override via environment)
+#   YOSYS_MIN_VERSION  default: "0.40"
+#   EQY_MIN_VERSION    default: "0.1"  (eqy is part of yosys-eqy)
+#   T27C_COMMIT        default: "9752bab4b81fe1a3abc66b13749c4ac412a74ee6" (HEAD at PR time)
+#                      Set to the gHashTag/t27 commit that generated build/t27c/*.v
+#
+# REPRODUCTION RECIPE
+#   1. pip install yosys-eqy  (or: nix-shell -p yosys-eqy)
+#   2. T27C_COMMIT=9752bab4b81fe1a3abc66b13749c4ac412a74ee6 bash scripts/eqy_check.sh
+#   3. cat evidence/eqy_*.json | python3 -m json.tool
+#
+# REFS
+#   Issue #4 Change N: https://github.com/gHashTag/tt-trinity-gf16/issues/4
+#   Issue #34 RVR-015: https://github.com/gHashTag/tt-trinity-gf16/issues/34
+#   Yosys EQY docs:    https://github.com/YosysHQ/eqy
+#   t27 upstream:      https://github.com/gHashTag/t27  commit T27C_COMMIT
+#
+# =============================================================================
+set -euo pipefail
+
+# ---------------------------------------------------------------------------
+# Configuration
+# ---------------------------------------------------------------------------
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+EVIDENCE_DIR="${REPO_ROOT}/evidence"
+BUILD_T27C_DIR="${REPO_ROOT}/build/t27c"
+SRC_DIR="${REPO_ROOT}/src"
+
+T27C_COMMIT="${T27C_COMMIT:-9752bab4b81fe1a3abc66b13749c4ac412a74ee6}"
+YOSYS_MIN_VERSION="${YOSYS_MIN_VERSION:-0.40}"
+EQY_MIN_VERSION="${EQY_MIN_VERSION:-0.1}"
+EQY_STRICT="${EQY_STRICT:-0}"   # if 1, PENDING exits non-zero
+
+# Modules under audit (Issue #4 Change N acceptance list)
+MODULES=(
+    "gf16_mul"
+    "gf16_add"
+    "gf16_dot4"
+    "trinity_gf16_tile"
+)
+
+# Coq theorem citations per module (R14 — Coq citation map)
+# Format: "MODULE:COQ_THEOREM_REF"
+declare -A COQ_CITATIONS
+COQ_CITATIONS["gf16_mul"]="t27/trios-coq/IGLA/gf16_precision.v::lucas_values_gf16_exact_n1"
+COQ_CITATIONS["gf16_add"]="t27/trios-coq/IGLA/lucas_closure_gf16.v::lucas_closure_phi_sq"
+COQ_CITATIONS["gf16_dot4"]="t27/trios-coq/IGLA/gf16_precision.v::lucas_4_eq_7"
+COQ_CITATIONS["trinity_gf16_tile"]="t27/trios-coq/IGLA/IGLA_ASHA_Bound.v::champion_survives_pruning"
+
+# ---------------------------------------------------------------------------
+# Utilities
+# ---------------------------------------------------------------------------
+log()  { echo "[eqy_check] $*"; }
+warn() { echo "[eqy_check] WARNING: $*" >&2; }
+fail() { echo "[eqy_check] ERROR: $*" >&2; exit 1; }
+
+sha256_of() {
+    if [[ -f "$1" ]]; then
+        sha256sum "$1" | awk '{print $1}'
+    else
+        echo "MISSING"
+    fi
+}
+
+timestamp_utc() {
+    date -u +"%Y-%m-%dT%H:%M:%SZ"
+}
+
+get_git_sha() {
+    git -C "${REPO_ROOT}" rev-parse --short HEAD 2>/dev/null || echo "unknown"
+}
+
+write_evidence_json() {
+    local module="$1" src_sha="$2" t27c_sha="$3" eqy_ver="$4" yosys_ver="$5"
+    local verdict="$6" ts="$7" evidence_path="$8"
+
+    mkdir -p "${EVIDENCE_DIR}"
+    python3 -c "
+import json, sys
+d = {
+    'module':        '${module}',
+    'src_sha':       '${src_sha}',
+    't27c_sha':      '${t27c_sha}',
+    'eqy_version':   '${eqy_ver}',
+    'yosys_version': '${yosys_ver}',
+    'verdict':       '${verdict}',
+    'timestamp_utc': '${ts}',
+    'evidence_path': '${evidence_path}',
+    'anchor':        'phi^2 + phi^-2 = 3 · Wave-24 RVR-017 · DOI 10.5281/zenodo.19227877',
+    't27c_commit':   '${T27C_COMMIT}',
+    'coq_citation':  '${COQ_CITATIONS[${module}]:-UNKNOWN}',
+    'r5_note':       'PENDING = t27c gen-verilog output not yet committed to build/t27c/'
+}
+print(json.dumps(d, indent=2))
+" > "${evidence_path}"
+}
+
+# ---------------------------------------------------------------------------
+# Toolchain version probing
+# ---------------------------------------------------------------------------
+probe_toolchain() {
+    local yosys_ver eqy_ver
+    yosys_ver="$(yosys --version 2>/dev/null | head -1 || echo "NOT_INSTALLED")"
+    eqy_ver="$(eqy --version 2>/dev/null | head -1 || echo "NOT_INSTALLED")"
+    echo "${yosys_ver}|${eqy_ver}"
+}
+
+# ---------------------------------------------------------------------------
+# EQY config generator
+# ---------------------------------------------------------------------------
+write_eqy_config() {
+    local module="$1" gold_v="$2" gate_v="$3" work_dir="$4"
+
+    cat > "${work_dir}/${module}.eqy" <<EOF
+[options]
+depth 20
+
+[gold]
+read_verilog ${gold_v}
+prep -top ${module}
+
+[gate]
+read_verilog ${gate_v}
+prep -top ${module}
+
+[script]
+connect -set gclk \$gold.clk \$gate.clk
+# Equivalence check on all outputs
+EOF
+}
+
+# ---------------------------------------------------------------------------
+# Run EQY for one module
+# ---------------------------------------------------------------------------
+run_eqy_module() {
+    local module="$1"
+    local src_file="${SRC_DIR}/${module}.v"
+    local t27c_file="${BUILD_T27C_DIR}/${module}.v"
+    local git_sha
+    git_sha="$(get_git_sha)"
+    local evidence_path="${EVIDENCE_DIR}/eqy_${git_sha}_${module}.json"
+    local ts
+    ts="$(timestamp_utc)"
+    local toolchain_raw
+    toolchain_raw="$(probe_toolchain)"
+    local yosys_ver="${toolchain_raw%%|*}"
+    local eqy_ver="${toolchain_raw##*|}"
+
+    local src_sha
+    src_sha="$(sha256_of "${src_file}")"
+    local t27c_sha
+    t27c_sha="$(sha256_of "${t27c_file}")"
+
+    log "--------------------------------------------------------------"
+    log "Module: ${module}"
+    log "  src:   ${src_file}  (sha256: ${src_sha:0:16}...)"
+    log "  t27c:  ${t27c_file} (sha256: ${t27c_sha:0:16}...)"
+    log "  EQY:   ${eqy_ver}"
+    log "  Yosys: ${yosys_ver}"
+
+    # --- PENDING path: t27c file missing -----------------------------------
+    if [[ "${t27c_sha}" == "MISSING" ]]; then
+        warn "t27c-output-pending for ${module}: ${t27c_file} not found."
+        warn "  Action: run 't27c gen-verilog' from gHashTag/t27 @ ${T27C_COMMIT}"
+        warn "  and commit output to build/t27c/${module}.v"
+        write_evidence_json "${module}" "${src_sha}" "MISSING" \
+            "${eqy_ver}" "${yosys_ver}" "PENDING" "${ts}" "${evidence_path}"
+        log "  Verdict: PENDING (t27c output not yet generated)"
+        return 0
+    fi
+
+    # --- PENDING path: src file missing ------------------------------------
+    if [[ "${src_sha}" == "MISSING" ]]; then
+        warn "src file missing for ${module}: ${src_file}"
+        write_evidence_json "${module}" "MISSING" "${t27c_sha}" \
+            "${eqy_ver}" "${yosys_ver}" "PENDING" "${ts}" "${evidence_path}"
+        log "  Verdict: PENDING (src file missing)"
+        return 0
+    fi
+
+    # --- PENDING path: EQY not installed -----------------------------------
+    if [[ "${eqy_ver}" == "NOT_INSTALLED" ]]; then
+        warn "eqy binary not found. Install: pip install yosys-eqy"
+        write_evidence_json "${module}" "${src_sha}" "${t27c_sha}" \
+            "NOT_INSTALLED" "${yosys_ver}" "PENDING" "${ts}" "${evidence_path}"
+        log "  Verdict: PENDING (eqy not installed in this environment)"
+        return 0
+    fi
+
+    # --- Active EQY run ----------------------------------------------------
+    local work_dir
+    work_dir="$(mktemp -d /tmp/eqy_${module}_XXXXXX)"
+    write_eqy_config "${module}" "${t27c_file}" "${src_file}" "${work_dir}"
+
+    local verdict="FAIL"
+    local eqy_exit=0
+    eqy "${work_dir}/${module}.eqy" -d "${work_dir}/eqy_out" 2>&1 | \
+        tee "${work_dir}/eqy_${module}.log" || eqy_exit=$?
+
+    if [[ ${eqy_exit} -eq 0 ]]; then
+        verdict="PASS"
+        log "  Verdict: PASS (EQY exit 0)"
+    else
+        verdict="FAIL"
+        warn "EQY reported non-equivalence for ${module} (exit ${eqy_exit})"
+        log "  Verdict: FAIL"
+    fi
+
+    write_evidence_json "${module}" "${src_sha}" "${t27c_sha}" \
+        "${eqy_ver}" "${yosys_ver}" "${verdict}" "${ts}" "${evidence_path}"
+
+    rm -rf "${work_dir}"
+
+    if [[ "${verdict}" == "FAIL" ]]; then
+        return 1
+    fi
+    return 0
+}
+
+# ---------------------------------------------------------------------------
+# Main
+# ---------------------------------------------------------------------------
+main() {
+    log "=============================================================="
+    log "Yosys EQY t27c↔src equivalence check · Wave-24 RVR-017"
+    log "Repo root: ${REPO_ROOT}"
+    log "T27C_COMMIT: ${T27C_COMMIT}"
+    log "=============================================================="
+
+    mkdir -p "${EVIDENCE_DIR}"
+
+    local any_fail=0
+    local any_pending=0
+    local results=()
+
+    for module in "${MODULES[@]}"; do
+        if run_eqy_module "${module}"; then
+            # Check written evidence for PENDING
+            local git_sha
+            git_sha="$(get_git_sha)"
+            local ev="${EVIDENCE_DIR}/eqy_${git_sha}_${module}.json"
+            if [[ -f "${ev}" ]]; then
+                local v
+                v="$(python3 -c "import json; print(json.load(open('${ev}'))['verdict'])" 2>/dev/null || echo "UNKNOWN")"
+                results+=("${module}:${v}")
+                if [[ "${v}" == "PENDING" ]]; then
+                    any_pending=1
+                fi
+            fi
+        else
+            results+=("${module}:FAIL")
+            any_fail=1
+        fi
+    done
+
+    log "=============================================================="
+    log "SUMMARY"
+    for r in "${results[@]}"; do
+        log "  ${r%%:*}  →  ${r##*:}"
+    done
+    log "=============================================================="
+
+    if [[ ${any_fail} -eq 1 ]]; then
+        fail "One or more modules FAILED equivalence check. See evidence/ for details."
+    fi
+
+    if [[ ${any_pending} -eq 1 ]] && [[ "${EQY_STRICT}" == "1" ]]; then
+        fail "One or more modules are PENDING and EQY_STRICT=1 is set."
+    elif [[ ${any_pending} -eq 1 ]]; then
+        warn "One or more modules are PENDING (t27c output not yet generated)."
+        warn "This is expected pre-TTSKY26c. See docs/EQY_CHECK.md 'Current Status'."
+        warn "Set EQY_STRICT=1 to treat PENDING as failure."
+    fi
+
+    log "All checks complete. Evidence written to ${EVIDENCE_DIR}/"
+    exit 0
+}
+
+main "$@"