anchor_rewrite_bound_roundfree_smt.py -- MEASURED 2026-10-07 (second form, after two adversarial reviews)
Windows 11, python 3.14.4, z3-solver 4.16.0. Commands: `python anchor_rewrite_bound_roundfree_smt.py`,
`python anchor_rewrite_bound_roundfree_smt.py --plant-bounds`, `python run_consensus_verification.py`.

=== the model alone: 28 checks, exit 0 ===
  PROVED    [LEMMA   ]  0.001s  L0a HASH CHAIN STEP (different parent hash -> different block hash)
  PROVED    [LEMMA   ]  0.000s  L0b R1 UNDER THE HASH (different certificate -> different anchor hash)
  CEX-FOUND [NEG-CTRL]  0.002s  P0c certificate outside the hashed pre-image            witness cert_alt=0 cert_hon=1
  PROVED    [PROOF   ]  0.005s  P1a REWRITE BOUND, baseline: at most 32 blocks (F above 20,746,736)
  PROVED    [PROOF   ]  0.006s  P1b PREFIX KEPT, baseline: the latest anchor's parent and below
  CEX-FOUND [CONFIG  ]  0.006s  C1a 32-block witness, forked AT the latest anchor      witness F=a_last=20746768 Hp=20746799 (32 blocks)
  CEX-FOUND [NEG-CTRL]  0.004s  N1  K_eff=0 -> 1000 blocks accepted                     witness F=20746737 Hp=20747736
  CEX-FOUND [NEG-CTRL]  0.006s  N2  adversary with every PQ key -> 1000 blocks          witness F=20746737 Hp=20747736
  PROVED    [PROOF   ]  0.007s  P2a REWRITE BOUND, corrected: at most 33 blocks
  PROVED    [PROOF   ]  0.008s  P2b PREFIX KEPT, corrected: the grandparent and below
  CEX-FOUND [CONFIG  ]  0.007s  C1b 33-block witness, fork at the latest anchor's parent  witness F=20966863 a_last=20966864 Hp=20966895 (33 blocks)
  PROVED    [PROOF   ]  0.008s  P2c fewer than K_eff=7 honest sibling seals -> 32 again
  CEX-FOUND [NEG-CTRL]  0.006s  N3  siblings over any parent (A3 dropped) -> 1000 blocks witness F=20746737 Hp=20747736
  PROVED    [PROOF   ]  0.007s  P4a PARTIAL COMPROMISE: K_eff=7, j=6 PQ keys -> still 33
  PROVED    [PROOF   ]  0.007s  P4b PARTIAL COMPROMISE: j=6, the extra block needs K_eff-j=1 honest sibling seal
  CEX-FOUND [NEG-CTRL]  0.006s  N4a j = K_eff = 7 PQ keys -> 1000 blocks accepted        witness F=20746737 Hp=20747736
  PROVED    [PROOF   ]  0.005s  P5a FOLLOWER K_eff=1, no PQ key: 32 holds
  PROVED    [PROOF   ]  0.007s  P5b FOLLOWER K_eff=1, siblings: 33 holds
  CEX-FOUND [CONFIG  ]  0.007s  C5c FOLLOWER: ONE honest sibling seal buys the 33rd block witness F=20966863 a_last=20966864 Hp=20966895
  CEX-FOUND [NEG-CTRL]  0.006s  N5d FOLLOWER K_eff=1 with ONE PQ key -> 1000 blocks      witness F=20746737 Hp=20747736
  PROVED    [PROOF   ]  0.005s  P6a DATED 128-INTERVAL WINDOW, baseline: at most 128 (any K_eff >= 1)
  PROVED    [PROOF   ]  0.007s  P6b DATED 128-INTERVAL WINDOW, corrected: at most 129
  CEX-FOUND [CONFIG  ]  0.006s  C6c 128-block witness in the window                      witness F=a_last=17226096 Hp=17226223
  PROVED    [PROOF   ]  0.352s  P3a REFERENCE: hash chain unrolled 1280 heights, no re-convergence at a_ref = F + d
  CEX-FOUND [NEG-CTRL]  0.350s  N3a hash not covering the parent -> re-convergence         witness F=13014001 d=1280
  PROVED    [PROOF   ]  0.009s  P3b REFERENCE + BOUND: everything through a_ref kept, at most 33 above the fork
  CEX-FOUND [NEG-CTRL]  0.010s  P3c no reference -> a short divergence below an anchor accepted  witness F=20746766 Hp=20746767 H=a_ref=20746768
  PROVED    [DEFN    ]  0.002s  D1  below stage 5 a header needs Q=7 classical keys (arithmetic restatement, not counted)
  checks by kind: PROOF 13, LEMMA 2, CONFIG 4, DEFN 1, NEG-CTRL 8 (all as expected; 0 FAILED)

=== control of the control: `--plant-bounds` (every claimed bound lowered by one), exit 1 ===
  FAILED (z3=sat): P1a, P2a, P2c, P4a, P4b, P5a, P5b, P6a, P6b, P3b   -- exactly the ten bound proofs; the bounds are tight.

=== whole suite the same day: `python run_consensus_verification.py`, exit 0 ===
  models run: 37   passed: 37   (16 consensus + 11 contract + 10 application)
  verdict lines: 301 PROVED   159 CEX-FOUND   0 FAILED
  wall time: 36.73 s (slowest: qbft_safety_smt.py 19.53 s; this model 4.38 s inside the suite)
  coverage: 37 of 37 *_smt.py files wired; RESULT: ALL MODELS PASS

=== what changed from the first form of the same day (reviewed adversarially the same day) ===
  - P3a was an arithmetic tautology (the conclusion added as a premise); it is now the unrolled hash chain with
    its own negative control N3a. C1c (now D1) is labelled DEFN and not counted as a proof; P0a/P0b are LEMMA.
  - K_eff and the adversary's post-quantum keys j are explicit: bounded iff j < K_eff (P4a / N4a); the
    published from-genesis follower runs at K_eff = 1 (SPEC 6.4): P5a/P5b/C5c/N5d.
  - the headline histories are confined to the regime in force today (fork above 20,746,736: interval 32,
    K = 7); the dated 128-interval window (2026-09-05 .. 2026-09-29) has its own proofs P6a/P6b (128 / 129).
  - the 33-block witness C1b forks at the latest anchor's parent (a_last = F + 1), as the text says.
  - the A1/A2 caps: seals over honest blocks are capped at N (made before any key leaked), honest seals over a
    sibling at N - j; the first draft of this form capped both at N - j and N2/N4a came out FAILED for that
    reason (contradictory axioms, not a property): corrected before anything was recorded.