Wave Loop 408 — real P12 CCLK attempt + SPI transaction model in Lean 4 - #1322

…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>