…c safety in Lean 4, close-out reports

- Add axiomatic Artix-7 OSCFSEL -> nominal CCLK lookup and N25Q128_3V
  standard-read spec (50 MHz) to TernaryFPGABoot.lean.
- Define BitstreamConfig.cclk_within_flash_spec and integrate it into
  cold_por_spi_flash_pred; prove canonical_oscfsel_within_flash_spec,
  canonical_implies_cclk_within_flash_spec, and
  cold_por_implies_cclk_within_flash_spec.
- Extend tri fpga measure-cclk with --live, --driver, --channel,
  --samplerate, --samples, and --validate to drive sigrok-cli, parse logic
  CSV, and validate against the flash spec.
- Add fpga/HARDWARE_SSOT.md §3.6 with CCLK table, live/CSV capture protocol,
  and validation rules.
- Write W406 report, evidence, and W407 cooperation variants; update
  docs/NOW.md and .trinity/experience.md.

Closes #1313

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

Closes nothing; opens the W407 loop on branch wave-loop-407.

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

…thetic CCLK fixture

- Add N25Q128_MIN_SCK_LOW_NS, N25Q128_MIN_SCK_HIGH_NS,
  N25Q128_WAKE_FROM_POWERDOWN_US, cclk_period_ns, sck_duty_ok, and
  flash_spi_timing_ok to TernaryFPGABoot.lean.
- Replace cclk_within_flash_spec with flash_spi_timing_ok in
  cold_por_spi_flash_pred; prove canonical_oscfsel_flash_spi_timing_ok,
  canonical_implies_flash_spi_timing_ok, cold_por_implies_flash_spi_timing_ok,
  and flash_spi_timing_ok_implies_cclk_within_flash_spec.
- Extend tri fpga measure-cclk with --synth to generate a board-less 2.5 MHz
  square-wave logic CSV; add duty-cycle (25%–75%) validation.
- Add Rust unit tests for is_logic_csv, parse_logic_csv, and
  generate_synth_cclk_csv.
- Update fpga/HARDWARE_SSOT.md §3.6 with deeper timing constraints, synthetic
  fixture instructions, real-capture wiring checklist, and updated validation
  rules.
- Write W407 report, evidence, and W408 cooperation variants; update
  docs/NOW.md and .trinity/experience.md.

Closes #1316

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

…tion model

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

Closes #1318

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

…odel in Lean 4

- Add `SPIReadTransaction`, `artix7_boot_transaction`, and
  `transaction_satisfies_flash_spec` to the Lean 4 FPGA boot model.
- Prove canonical `OSCFSEL=0` transaction satisfies the N25Q128_3V spec and link
  the cold-POR predicate to the transaction spec.
- Attempt real P12 CCLK capture; document the missing-wiring blocker in
  `fpga/HARDWARE_SSOT.md` and evidence file.
- Update `docs/NOW.md`, `.trinity/experience.md`, W408 plan, report, and W409
  cooperation variants.
- Reseal all `.t27` specs against the current `t27c` release binary.

Note: `./scripts/tri test` has 16 pre-existing gen-verilog-yosys-smoke failures
in scratch/IGLA specs from unmerged backend gaps tracked in
`docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`; all other phases (parse,
typecheck, gen, seal-verify) pass 576/576.

Closes #1318

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

Closes #1323 setup; branch wave-loop-409 created.

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

Closes #1323

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

Closes #1323

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

Closes #1323

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

…ter duty bound

- Add `artix7_boot_transaction_for_oscfsel` and prove every documented
  OSCFSEL ∈ {0..7} produces an N25Q128_3V-compliant transaction.
- Rewrite `artix7_boot_transaction` as a wrapper around the per-OSCFSEL lookup.
- Import `Mathlib.Tactic` so `interval_cases` can enumerate the lookup table.
- Replace the placeholder 25%–75% duty-cycle guard in `cli/tri/src/fpga.rs`
  with a frequency-derived bound from N25Q128 t_CL/t_CH limits, clamped to
  10%–90%.
- Re-attempt real P12 CCLK capture; wiring blocker persists and is documented.
- Update `fpga/HARDWARE_SSOT.md` §3.6.9 with the per-OSCFSEL transaction table.
- Add W409 plan, report, evidence, and W410 cooperation variants.

Note: `./scripts/tri test` passes parse/typecheck/gen/seal-verify (576/576).
The 16 pre-existing gen-verilog-yosys-smoke failures are tracked in
`docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`; W409 did not touch the Verilog
backend.

Closes #1323

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

Closes #1325 setup; branch wave-loop-410 created.

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

Closes #1325

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

Closes #1325

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

…xport

- Add measured_cclk_satisfies_flash_spec predicate and linking theorem in proofs/lean4/Trinity/TernaryFPGABoot.lean.

- Add MeasuredCclk Rust record and --json output in cli/tri/src/fpga.rs.

- Document the formal link in fpga/HARDWARE_SSOT.md §3.6.10 and note remaining P12/DLC10 blockers.

- W410 report, evidence, and W411 cooperation variants.

Closes #1325

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

Closes #1325

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

Closes #1325

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