merge(branch): claude/fix-prover-wiring-epyIR — corpus pipeline + verisim first-class modalities

Conflict resolutions:
- Justfile: kept HEAD (retrain: align-premises dep + retrain-skip-align escape hatch)
- provision_corpora.sh: kept HEAD (https:// vs http:// for nusmv URL)
- verisim_bridge.rs: took branch (OctadPayload + ProofOctadBuilder design —
  already the version agent/memory.rs and vcl_ut.rs depend on; HEAD had the
  older ProofOctad struct which nothing outside the file uses)

Branch commits incorporated:
- feat(ci,ml): Tier-3 live-prover provisioning + uncap Flux training
- feat(corpus): non-interactive upstream provisioning + extractor driver
- feat(just): corpus-refresh pipeline — provision → extract → merge → align → retrain
- feat(verisim): first-class Proof / TacticApplication / ProofVersion / ProofStateRecord
- feat(corpus): align premise proof_ids with UNIFIED after merge

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath