R6 — learned search behind the fixed acceptance boundary

R6 closes Proof Broker's first learned-search evaluation. An untrusted model proposed Farkas witnesses behind the broker's unchanged acceptance boundary: an independent checker, a pinned closer, and a kernel that validates the whole declaration with its axioms unchanged. The target was a frozen census of 15 omega obligations in VerInf's Bracket.lean.

Qualification: two post-collection amendments. The R6-014 evaluation is not an unchanged preregistered one. Each amendment changed only what the frozen live auditor (and, for the second, the block 2 runner) would accept. Neither changed the frozen analysis, a recorded outcome or a run.

• Amendment 1 covers the policy-directory check. It came after the first frozen audit rejected block 1 on the production directory layout.
• Amendment 2 covers live pre-send releases and retried slots. It came after block 2 paused on a pre-send connection failure.

Result

• Verified witnesses: all 80 certificate-feasible slots.
• Proof coverage: 6 of 15 primary obligations, in two declaration families. That is 48 of 88 slots: those six obligations at each of eight draws. Coverage was unchanged from draw 1 to draw 8.
• Gain over the deterministic arm: l096 and l099.
• The constraint: reconstruction, not proposal. The four obligations the pinned ℕ closer refused received verified witnesses at every draw.
• Negative control: 8 of 8 rejected, no false acceptance.

Harness

• Money: 9,011,200 µUSD net committed, which equals the authorization. That covers 89 reservations, one of them released.
• Usage: reported usage priced at 944,490 µUSD, an estimate and not a bill.
• Disclosure: operator scans with the real credential as the canary were clean, covering 132,450 files and binding all 89 runs.
• Audit: the frozen audit accepted 4,327 cases under live-evaluation-v3.

Publication. Sealed records are published unchanged. They include local paths as metadata. The credential value appears in none of them, within the scans' stated scope.

Start at experiments/r6/R6-SYNTHESIS.md. R6-015, an offline test of whether a suitable closer can consume the refused witnesses, is proposed and is not part of this release.