feat(igla): Wave Loop 420 — VCD exact-terminator + real-net auto-threshold, PVT process-corner monotonicity

Closes #1361

Variant C fallback (bench still blocked: P12 unwired, DLC10 cable missing,
no relay). Instrument-import depth and formal guarding only.

- cli/tri/src/fpga.rs:
  - exact-token VCD $date/$version/$comment terminator with regression test
    for embedded $end-like tokens (closes W419 report/actual gap)
  - real-valued VCD net auto-threshold from observed voltage swing
  - PVT half-period process-corner monotonicity regression test
- proofs/lean4/Trinity/TernaryFPGABoot.lean:
  - pvt_half_ns_monotone_in_process_corner (ff ≤ tt ≤ ss)
- fpga/HARDWARE_SSOT.md: §3.6.17 documenting W420 VCD/PVT improvements
- .trinity/experience.md: W420 learnings
- docs/reports: W420 report, evidence, and W421 cooperation variants

Verification:
- cargo test -p tri vcd: 13/13 PASS
- cargo test -p tri pvt: 10/10 PASS
- cargo test -p tri fpga::tests: 48/48 PASS
- lake build Trinity.TernaryFPGABoot: PASS (2967 jobs)
- ./scripts/tri test: 16 pre-existing yosys failures (#1245), no new ones

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: Dmitrii Vasilev

.claude/plans/wave-loop-420.md

@@ -0,0 +1,69 @@
+# Wave Loop 420 — Decomposed Plan
+
+**Issue:** #1361  
+**Branch:** `wave-loop-420`  
+**Default variant:** C (physical bench still blocked: DLC10 cable not found, P12 unwired, no relay)
+
+---
+
+## 1. Weak points identified
+
+1. **Missing VCD `$comment` exact-token terminator.** The W419 report claimed this
+   hardening landed, but the merged commit (`101fd0748`) did not touch the VCD
+   parser. The current code still uses `ends_with("$end")` / `contains(" $end")`
+   heuristics, so a `$comment` block containing the literal substring `$end`
+   terminates early and corrupts the signal dictionary.
+2. **Real-valued VCD nets require an explicit `--vcd-threshold-v`.** There is no
+   auto-threshold fallback for analog VCD exports; users must know the voltage
+   swing up-front.
+3. **PVT half-period bound lacks a process-corner monotonicity lemma.** We have
+   temperature monotonicity and VCCINT antitonicity from W419, but no formal
+   statement that `ff ≤ tt ≤ ss` is preserved by the half-period bound itself.
+
+---
+
+## 2. Competitor landscape (high-level)
+
+The closest formal-HDL competition is **Sparkle / Verilean** (Lean 4 native,
+binary RTL). Other credible players: **Clash** (Haskell, external formal),
+**Chisel/FIRRTL/CIRCT** (mainstream, SVA/model-checking oriented),
+**Bluespec** (rule-based, Coq bridge via Kami), **Coq Kami / Silver Oak**
+(dependent-type hardware), **ACL2** (specification/proof layer only).
+
+None combine Lean 4 native proof, a ternary compute stack, spec-first sealed
+`*.t27 → gen/` code generation, and physical boot-evidence instrumentation.
+That intersection is the gap t27 fills.
+
+---
+
+## 3. Implementation steps
+
+| Step | Files | Deliverable | Acceptance |
+|------|-------|-------------|------------|
+| 3.1 | `cli/tri/src/fpga.rs` | Replace VCD `$date`/`$version`/`$comment` terminator heuristics with exact-token check; clear state immediately on same-line termination. | `test_parse_vcd_comment_with_embedded_end_token` PASS |
+| 3.2 | `cli/tri/src/fpga.rs` | Add VCD auto-threshold for real-valued nets: compute `50% (vmin + vmax)` when `--vcd-threshold-v` is omitted; warn user. | `test_parse_vcd_real_auto_threshold` PASS |
+| 3.3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Add `pvt_half_ns_monotone_in_process_corner` lemma: `c1.worse_than c2 → bound c1 ≤ bound c2`. | `lake build` PASS |
+| 3.4 | `cli/tri/src/fpga.rs` | Add Rust test `test_pvt_half_ns_monotone_in_process_corner`. | `cargo test` PASS |
+| 3.5 | `fpga/HARDWARE_SSOT.md` | Document VCD `$comment` exact-terminator behavior and real-net auto-threshold. | docs render clean |
+| 3.6 | `.trinity/experience.md` | Capture W420 learnings. | committed |
+| 3.7 | `docs/reports/*` | W420 report, evidence, W421 cooperation variants. | committed |
+
+---
+
+## 4. Verification plan
+
+- `cargo test -p tri vcd` — expect 12 tests (was 11).
+- `cargo test -p tri pvt` — expect 10 tests (was 9).
+- `cargo test -p tri fpga::tests` — expect 47 tests (was 45).
+- `lake build Trinity.TernaryFPGABoot` — must PASS.
+- `./scripts/tri test` — must PASS except 16 pre-existing gen-verilog yosys failures.
+
+---
+
+## 5. Land
+
+- Commit with `Closes #1361`.
+- Open PR #? from `wave-loop-420` → `master`.
+- After merge, create issue #? and branch `wave-loop-421`.
+
+*φ² + φ⁻² = 3 | TRINITY*

.trinity/current-issue.md

@@ -1,16 +1,16 @@
-# Wave Loop 425 — FPGA board evidence / relay gate / PVT falsification
+# Wave Loop 420 — physical CCLK capture, real relay gate, or instrument-import depth
 
-**Issue:** #1374  
-**Branch:** `wave-loop-425`  
-**Milestone:** Continue the FPGA boot-evidence line from W424.
+**Issue:** #1361  
+**Branch:** `wave-loop-420`  
+**Milestone:** Continue the FPGA boot-evidence line from Wave Loop 419.
 
 ---
 
 ## Goal
 
-Wave 424 hardened the FPGA tooling around instrument import, PVT context, CSV
-voltage units, and non-blocking auto-continue. Wave 425 must produce real
-boot evidence by executing the first available variant:
+Wave 419 closed the Variant C fallback (instrument-import parity, PVT
+monotonicity, standalone lake workflow). Wave 420 re-evaluates the bench state
+and executes the first available variant.
 
 1. **Variant A (preferred when bench becomes available):**
    - Confirm P12 is wired to a logic-analyzer channel.
@@ -29,27 +29,33 @@ boot evidence by executing the first available variant:
    - Document the import recipe and PVT-context checklist in
      `fpga/HARDWARE_SSOT.md`.
 
-3. **Variant C (fallback if bench still fully blocked):**
-   - Implement or defer real XADC readout in `tri fpga boot-log` / `cclk-sweep`.
-   - Land the next safe gen-verilog #1245 sub-fix if one is narrow and
-     regression-free; otherwise explicitly defer.
-   - Harden boot-log / cold-por / cclk-sweep JSON schema and update the
-     competitor snapshot.
+2. **Variant B (if relay hardware is available, no CCLK probe):**
+   - Implement a real `--relay-port` backend for `tri fpga cold-por`
+     (e.g. serial or TCP relay controlling board power).
+   - Perform an automated cold-POR power-cycle and capture STAT without
+     operator intervention.
+   - Document relay wiring and port syntax in `fpga/HARDWARE_SSOT.md`.
+
+3. **Variant C (fallback if bench still blocked):**
+   - Extend instrument-import depth: VCD auto-threshold, CSV sample-rate
+     auto-detection, or additional vendor header aliases.
+   - Refine the PVT envelope if real N25Q128_3V timing curves become available,
+     otherwise add another shape-preservation lemma.
+   - Land one safe gen-verilog #1245 sub-fix that does not destabilize the
+     existing 16-failure yosys smoke baseline.
 
 ---
 
 ## Decomposed plan
 
-See `docs/reports/FPGA_LOOP_COOPERATION_W425_2026-07-05.md`.
-
 | Step | File(s) | Deliverable |
 |------|---------|-------------|
-| 1 | `cli/tri/src/fpga.rs` | Variant A capture import, B dry-run + PVT context, or C XADC/schema hardening |
-| 2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | New measured theorems or PVT helpers |
-| 3 | `fpga/HARDWARE_SSOT.md` | Updated capture / import / PVT protocol |
-| 4 | `docs/reports/*` | W425 report, evidence, W426 cooperation |
-| 5 | `.trinity/experience.md` | W425 learnings |
-| 6 | git/PR | squash-merge to `master`, close #1374, open next issue for W426 |
+| 1 | `cli/tri/src/fpga.rs` | Variant A import, B relay backend, or C instrument-import depth / gen-verilog sub-fix |
+| 2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | New measured theorems or PVT shape lemma |
+| 3 | `fpga/HARDWARE_SSOT.md` | Updated capture / relay / integration protocol |
+| 4 | `docs/reports/*` | W420 report, evidence, W421 cooperation |
+| 5 | `.trinity/experience.md` | W420 learnings |
+| 6 | git/PR | squash-merge to `master`, close #1361, open #? for W421 |
 
 ---
 
@@ -67,9 +73,9 @@ See `docs/reports/FPGA_LOOP_COOPERATION_W425_2026-07-05.md`.
 - [ ] AC-B3: `fpga/HARDWARE_SSOT.md` documents the import recipe and PVT-context checklist.
 
 ### Bundle C
-- [ ] AC-C1: Real XADC readout is implemented or a documented deferral explains why it remains placeholder.
-- [ ] AC-C2: `gen-verilog-yosys-smoke` failure count does not increase; any deferred #1245 sub-fix is explained.
-- [ ] AC-C3: Boot-log / cold-por / cclk-sweep JSON schema is measurably more robust or better documented.
+- [x] AC-C1: VCD instrument-import unit tests land: exact `$end` token terminator regression and real-valued net auto-threshold.
+- [x] AC-C2: New PVT envelope shape lemma/test lands: process-corner monotonicity (`ff ≤ tt ≤ ss`).
+- [ ] AC-C3: One safe gen-verilog #1245 sub-fix lands without increasing the 16-failure yosys smoke count. (Deferred; the remaining tracked gap is RAM style inference, which is not a safe narrow sub-fix for a Variant C wave.)
 
 ### Invariant checks
 - [ ] `./scripts/tri test` parse/typecheck/gen/seal-verify phases pass.
@@ -81,10 +87,11 @@ See `docs/reports/FPGA_LOOP_COOPERATION_W425_2026-07-05.md`.
 ## PR
 
 - Target: `master`
-- Body: `Closes #1374`
-- Report: `docs/reports/WAVE_LOOP_425_REPORT.md`
-- Evidence: `docs/reports/FPGA_LOOP_EVIDENCE_W425_2026-07-05.md`
-- Cooperation W426: `docs/reports/FPGA_LOOP_COOPERATION_W426_2026-07-05.md`
+- PR: to open after work
+- Body: `Closes #1361`
+- Report: `docs/reports/WAVE_LOOP_420_REPORT.md`
+- Evidence: `docs/reports/FPGA_LOOP_EVIDENCE_W420_2026-07-06.md`
+- Cooperation W421: `docs/reports/FPGA_LOOP_COOPERATION_W421_2026-07-06.md`
 
 ---
 

.trinity/current_task/activity.md

@@ -1464,7 +1464,15 @@
 - **Commit:** docs(w420): set W420 issue number to #1361 and record W419 PR #1360 (Closes #1357, Refs #1361)
 - **Files:** .trinity/current-issue.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W420_2026-07-05.md,docs/reports/FPGA_LOOP_EVIDENCE_W419_2026-07-05.md,docs/reports/WAVE_LOOP_419_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
 
-## 2026-07-05T07:14:41Z — wave-loop-425
-- **Commit:** chore(tri): update session log and commit count after W424 close-out
-- **Files:** .trinity/current-issue.md,docs/NOW.md
+## 2026-07-04T18:36:50Z — wave-loop-420
+- **Commit:** feat(igla): Wave Loop 419 — Variant C VCD/CSV hardening, PVT monotonicity, standalone lake workflow
+- **Files:** .trinity/current-issue.md
+
+## 2026-07-04T18:37:55Z — wave-loop-420
+- **Commit:** setup(igla): initialize Wave Loop 420 current issue (#1361)
+- **Files:** .trinity/current-issue.md,.trinity/current_task/activity.md,docs/NOW.md
+
+## 2026-07-04T19:27:38Z — wave-loop-420
+- **Commit:** setup(igla): initialize Wave Loop 420 current issue and NOW.md update
+- **Files:** .claude/plans/wave-loop-420.md,.trinity/current-issue.md,.trinity/current_task/activity.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W421_2026-07-06.md,docs/reports/FPGA_LOOP_EVIDENCE_W420_2026-07-06.md,docs/reports/WAVE_LOOP_420_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
 

.trinity/experience.md

@@ -1,5 +1,55 @@
 # t27 / Trinity Agent Experience Log
 
+## 2026-07-06 — Wave Loop 420 (Variant C fallback: VCD exact-terminator + auto-threshold, PVT corner monotonicity)
+
+### What worked
+- Re-reading the merged W419 code revealed that the reported VCD `$comment`
+  exact-token hardening had **not actually landed** in the committed diff. The
+  heuristic `ends_with("$end")` / `contains(" $end")` was still in place. Fixing it
+  for W420 and adding a regression test (`test_parse_vcd_comment_with_embedded_end_token`)
+  closed the gap. This shows that **report claims must be verified against the
+  actual tree**, not just the intended patch.
+- Adding **auto-threshold for real-valued VCD nets** removes a manual step for
+  oscilloscope imports: when `--vcd-threshold-v` is omitted, the parser computes
+  `50% (vmin + vmax)` from the observed swing. A regression test on a synthetic
+  0 V / 3.3 V 25 MHz square wave validates the recovery.
+- Completing the PVT envelope **process-corner monotonicity** lemma and Rust test
+  (ff ≤ tt ≤ ss) closes the last independent shape axis: temperature, voltage,
+  and process corner are now all formally guarded.
+
+### What changed behavior
+- `cli/tri/src/fpga.rs`: added `vcd_line_ends_with_token` helper; applied exact
+  `$end` token terminator to VCD `$date`/`$version`/`$comment` sections; added
+  real-valued VCD auto-threshold; added
+  `test_parse_vcd_comment_with_embedded_end_token` and
+  `test_parse_vcd_real_auto_threshold`.
+- `proofs/lean4/Trinity/TernaryFPGABoot.lean`: added
+  `pvt_half_ns_monotone_in_process_corner`.
+- `cli/tri/src/fpga.rs`: added `test_pvt_half_ns_monotone_in_process_corner`.
+- `fpga/HARDWARE_SSOT.md`: added §3.6.17 documenting W420 instrument-import and
+  PVT monotonicity work.
+- Close-out artifacts: `docs/reports/WAVE_LOOP_420_REPORT.md`,
+  `docs/reports/FPGA_LOOP_EVIDENCE_W420_2026-07-06.md`, and
+  `docs/reports/FPGA_LOOP_COOPERATION_W421_2026-07-06.md`.
+
+### Patterns to reuse
+- When a report claims a parser hardening landed, diff the relevant file and
+  run the claimed regression test before trusting the claim. Intention and
+  commit content can diverge, especially after rebases or clean-branch rebuilds.
+- For analog instrument imports, provide an **auto-threshold fallback** computed
+  from the observed swing, but keep the explicit override for noisy captures.
+- For placeholder models, prove **shape on every independent axis** (monotone in
+  temp, antitone in voltage, monotone in process corner). Each axis gets both a
+  symbolic Lean lemma and a numeric Rust sweep.
+
+### Anti-patterns to avoid
+- Do not assume a reported fix exists in the tree; verify with `git show` and
+  targeted tests.
+- Do not reject real-valued instrument imports when the threshold can be inferred
+  from the data itself.
+- Do not leave any PVT envelope axis without a shape lemma; even placeholder
+  coefficients must be formally well-behaved.
+
 ## 2026-07-05 — Wave Loop 419 (Variant C fallback: VCD/CSV hardening, PVT monotonicity, standalone lake workflow)
 
 ### What worked