Wave Loop 411 — measured-to-lean auto-proof + PVT margin

[gHashTag]

Closes #1329

• Adds tri fpga measured-to-lean subcommand that turns a --json measurement into a type-correct Lean theorem.
• Adds PVT-margin predicate with conservative 2× derated SCK low/high constants and proves it implies the flash transaction spec.
• W411 report, evidence, and W412 cooperation variants.

Verification:

• lake build Trinity.TernaryFPGABoot green
• cargo test -p tri fpga::tests 14/14
• ./scripts/tri test parse/typecheck/gen/seal-verify green

🤖 Generated with Claude Code

[github-actions]

📓 NotebookLM Notebook linked to this PR

• Notebook ID: b83263109fb055dc
• URL: https://notebooklm.google.com/notebook/b83263109fb055dc

This notebook contains session context, decisions, and artifacts for this work.

[github-actions]

PR Dashboard

Generated at: 2026-07-04 13:06:35 UTC

• Wave Loop 411 — measured-to-lean auto-proof + PVT margin #1331 Wave Loop 411 — measured-to-lean auto-proof + PVT margin | Created: 2026-07-04 | Updated: 2026-07-04 | 13 failing / 17 total
• feat(igla): Wave Loop 410 - measured-duty formal link and Rust JSON export #1330 feat(igla): Wave Loop 410 - measured-duty formal link and Rust JSON export | Created: 2026-07-04 | Updated: 2026-07-04 | 0 failing / 3 total
• takum32/64: promote structural -> curated_named bitexact (SW 70->72) #1328 takum32/64: promote structural -> curated_named bitexact (SW 70->72) | Created: 2026-07-04 | Updated: 2026-07-04 | 0 failing / 19 total
• Wave Loop 409 — per-OSCFSEL SPI transaction lookup + tighter duty bound #1324 Wave Loop 409 — per-OSCFSEL SPI transaction lookup + tighter duty bound | Created: 2026-07-04 | Updated: 2026-07-04 | 0 failing / 4 total
• Wave Loop 408 — real P12 CCLK attempt + SPI transaction model in Lean 4 #1322 Wave Loop 408 — real P12 CCLK attempt + SPI transaction model in Lean 4 | Created: 2026-07-04 | Updated: 2026-07-04 | 0 failing / 4 total
• feat(igla): Wave Loop 407 — deeper N25Q128 SPI timing in Lean 4 + synthetic CCLK fixture #1317 feat(igla): Wave Loop 407 — deeper N25Q128 SPI timing in Lean 4 + synthetic CCLK fixture | Created: 2026-07-04 | Updated: 2026-07-04 | 5 failing / 26 total
• feat(igla): Wave Loop 406 — live CCLK capture + OSCFSEL/CCLK flash-spec safety in Lean 4 #1315 feat(igla): Wave Loop 406 — live CCLK capture + OSCFSEL/CCLK flash-spec safety in Lean 4 | Created: 2026-07-04 | Updated: 2026-07-04 | 5 failing / 25 total
• chore(ci)(deps): bump actions/download-artifact from 4 to 8 #1238 chore(ci)(deps): bump actions/download-artifact from 4 to 8 | Created: 2026-07-01 | Updated: 2026-07-01 | 3 failing / 26 total
• chore(ci)(deps): bump docker/build-push-action from 6 to 7 #1237 chore(ci)(deps): bump docker/build-push-action from 6 to 7 | Created: 2026-07-01 | Updated: 2026-07-01 | 0 failing / 17 total
• chore(ci)(deps): bump actions/upload-artifact from 4 to 7 #1236 chore(ci)(deps): bump actions/upload-artifact from 4 to 7 | Created: 2026-07-01 | Updated: 2026-07-01 | 4 failing / 29 total
• chore(deps)(deps): bump uuid from 1.23.2 to 1.23.4 #1227 chore(deps)(deps): bump uuid from 1.23.2 to 1.23.4 | Created: 2026-06-29 | Updated: 2026-06-29 | 3 failing / 25 total
• chore(deps)(deps): bump candle-nn from 0.10.2 to 0.11.0 #1226 chore(deps)(deps): bump candle-nn from 0.10.2 to 0.11.0 | Created: 2026-06-29 | Updated: 2026-06-29 | 3 failing / 25 total
• docs(metrics): сводка ключевых метрик 83 числовых форматов (SSOT-derived) #1225 docs(metrics): сводка ключевых метрик 83 числовых форматов (SSOT-derived) | Created: 2026-06-28 | Updated: 2026-06-28 | 3 failing / 17 total
• chore(deps)(deps): bump tower-http from 0.6.8 to 0.7.0 #1220 chore(deps)(deps): bump tower-http from 0.6.8 to 0.7.0 | Created: 2026-06-22 | Updated: 2026-06-22 | 3 failing / 25 total
• conformance: promote gf10/gf256 to bitexact_selfconsistent (WP-34) #1216 conformance: promote gf10/gf256 to bitexact_selfconsistent (WP-34) | Created: 2026-06-19 | Updated: 2026-06-19 | 0 failing / 19 total
• chore(deps)(deps): bump ignore from 0.4.25 to 0.4.26 #1145 chore(deps)(deps): bump ignore from 0.4.25 to 0.4.26 | Created: 2026-06-15 | Updated: 2026-06-15 | 1 failing / 25 total
• chore(deps)(deps): bump regex from 1.12.3 to 1.12.4 #1143 chore(deps)(deps): bump regex from 1.12.3 to 1.12.4 | Created: 2026-06-15 | Updated: 2026-06-15 | 1 failing / 25 total
• conformance(gf14): add 14 bit-exact GF14 vectors (52 -> 53) #1142 conformance(gf14): add 14 bit-exact GF14 vectors (52 -> 53) | Created: 2026-06-15 | Updated: 2026-06-15 | 0 failing / 19 total
• ci(trust): OpenSSF Scorecard + SBOM + Sigstore signed releases #1141 ci(trust): OpenSSF Scorecard + SBOM + Sigstore signed releases | Created: 2026-06-15 | Updated: 2026-06-15 | 3 failing / 17 total
• fix(gen): untrack stale gen/numeric catalog artifacts (committed gen drifts 77 vs SSOT 83) -- Closes #1120 #1128 fix(gen): untrack stale gen/numeric catalog artifacts (committed gen drifts 77 vs SSOT 83) -- Closes #1120 | Created: 2026-06-14 | Updated: 2026-06-14 | 0 failing / 21 total

Summary

Status	Count
Total Open PRs	20
PRs with Failing Checks	11
PRs with All Checks Green	9
READY	8
FAILING	11
PENDING	0

Seal Status

• ⚠️ STALE -- sha256(compiler.rs)=b12011de7c23 != manifest seal=49e55df6d444.
  The committed NMSE numbers were certified against an older compiler.rs.
  Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).