feat(probe): G7 ambiguity gate; refuse the G4 reshape with a measurement

.claude/board/AGENT_LOG.md

@@ -1,3 +1,13 @@
+## 2026-07-29 — PROBE-SUDOKU-TEACHER follow-ups (a)(b)(c): G7 shipped, G4 reshape refused with a number (main thread only, no subagents)
+
+- **Why no subagents.** All three follow-ups were design calls against a probe's existing invariants (which fixture can exhibit which property; whether a policy edit destroys a shipped measurement), i.e. accumulation, not grindwork. A worker briefed to "assert the bifurcate-vs-refuse contrast" would have hand-built a fixture until the assertion passed — the exact failure the two `build_ambiguity_fixture` write-order footnotes already record.
+- **(a) G7 ambiguity gate — SHIPPED, both halves.** Commit on a verified-unique puzzle (Hamming 0); `Underdetermined { cell: 0 }` with nothing written into any of 6 differing cells on a verified-ambiguous one. The reasoner refuses via its own fork (`try_bifurcate_or_flag`'s third arm: NEITHER branch contradicts); `count_completions` supplies the fixture's ground truth and is never called by the reasoner. Keeping them apart is the point — a verdict produced by the enumerator would assert only that a search solver can count solutions.
+- **Falsifier PROVEN, not assumed.** Flipped the refuse arm to "commit the first candidate" (literally a backtracking solver) → G7 fails both refuse assertions while `can_commit` stays true, so the gate discriminates the refusal specifically. Restored and re-verified green.
+- **(b) G4 reshape — REFUSED, and that is the deliverable.** Scan over k = 2..48 × 8 strides × 81 offsets: **26858 unique, 388 singles-stall, 0 fork-closable, best residual 16**. The contrast the follow-up asked me to assert does not exist on this family: `try_bifurcate` needs exactly-2-candidate cells while a singles-stalled board has mostly ≥3, and `has_contradiction` is one-shot so a contradiction two inferences deep is invisible. The identical censuses were the policies genuinely agreeing, not a missing assertion. Filed `TD-FORK-CANNOT-CLOSE-WHAT-SINGLES-CANNOT` with the numbers and the falsifiable close condition (`fork_closes > 0`).
+- **(c) hidden singles — granted in a different shape.** As literally worded it would have erased G5: hidden-single detection subsumes the exact 2-candidate separator G5's fixture uses, collapsing both graded policies onto one path. Landed as a third policy in the same loop (`ElectionsFirstWithHidden`); the two graded policies are byte-identical. G4 asserts both halves — Hamming 0 (catches a wrong write) and census ≥ baseline (catches "did nothing extra").
+- **Two of my own errors, caught by the scan rather than by review.** (i) The first ambiguous fixture put all four rectangle corners in ONE box, where a diagonal swap breaks the box constraint — it could never be ambiguous. (ii) Even corrected, no rectangle exists: `base_solution_boxmajor` is the cyclic grid `(f(r)+c) mod 9`, so a corner swap needs `2(c₁−c₂) ≡ 0 (mod 9)` and `gcd(2,9)=1` forces `c₁=c₂`. **The grid is provably rigid.** Both were found because the search REPORTS ITS COUNTS; an `expect()` would have said only "not found".
+- **Gates (central):** probe **ALL GATES GREEN (G1–G7)**; `cargo test -p lance-graph-planner` **322 + 4 passed, 0 failed**; `clippy -p lance-graph-planner --all-targets -- -D warnings` clean (two real fixes: a never-read counter, and an unused `rect` — resolved by USING it as a fixture sanity check that differing cells are all blanked, not by silencing it); `cargo fmt --check` clean. Scoped `-p` throughout.
+
 ## 2026-07-29 — #864 rebase onto merged main + reconciliation with a concurrent sibling session (main thread only, no subagents)
 
 - **The ask was "864 is dirty".** After #863 merged, `claude/happy-hamilton-0azlw4` no longer sat on `main`. Rebased it; ONE conflict, in `LATEST_STATE.md` only (`EPIPHANIES` + `AGENT_LOG` auto-merged) — both PRs had PREPENDED a top section. Resolved by keeping BOTH with #864's on top (it lands later); no prior entry edited, reordered, or dropped. Two branches obeying the same prepend convention always collide at line 1: an expected cost of the convention, not a fault on either side.

.claude/board/EPIPHANIES.md

@@ -1,3 +1,31 @@
+## 2026-07-29 — E-COMPUTED-PRINTED-NOT-ASSERTED-1 — I fixed that exact defect class in the morning and shipped two fresh instances of it in the afternoon; plus the gate's error turns out to be one-sided
+
+**Status:** IN PR (#865). **Confidence:** High — both defects confirmed by revert-test, the asymmetry by a test that failed against my own expectation.
+
+**The embarrassing shape of it.** `E-A-NULL-RESULT-IS-THE-DELIVERABLE-1` (same day, hours earlier) is *about* making a limitation gate-enforced instead of merely stated. The code I shipped alongside it then did the opposite twice: `find_fork_required_fixture`'s result was computed and **printed** while `g4_pass` ignored it, and `unique_count` was computed and **printed** under a comment claiming uniqueness was "VERIFIED" while `can_commit` never referenced it. Both found by CodeRabbit on #865, both real, both fixed with the predicate moved into the conjunction.
+
+**Why each mattered, concretely.** (1) Strengthen the fork later and G4 keeps passing while its own detail line still claims `0/388 closable` — a stale measurement frozen inside a PASS. It now asserts `fork_still_cannot_close`, so **a future improvement is SUPPOSED to fail this gate**, and the detail string is derived from the scan rather than hardcoded. (2) Fixture drift making the commit puzzle ambiguous would have left G7's commit half asserting the exact opposite of its documentation — that the reasoner confidently completed an underdetermined board, the precise failure the other half exists to catch. Both were revert-tested: forcing a fixture "found" fails G4 with the STALE NULL RESULT message; pointing the commit half at the ambiguous fixture drops `can_commit` to false with `unique completions=2`.
+
+**The generalization, stated so the third instance is the last.** *"Computed, printed, and described in a comment" is the most convincing possible disguise for an unasserted claim* — more convincing than silence, because the number is right there in the output and the prose says "verified". The reader's eye supplies the assertion that the code never makes. **Rule: if a value appears in a gate's printout and in its prose, it belongs in its predicate — or the prose must say it is diagnostic only.**
+
+**Separately, a real behavioural finding, from a test that failed against my expectation.** I wrote `fork_flag_reports_forced_when_one_branch_contradicts` expecting `Forced` at the target; it returned `Underdetermined(39)` — the parked companion, which precedes the target in scan order and whose two candidates both survive one-shot propagation. The behaviour is right and the expectation was wrong, so the test now pins what holds: **the verdict comes from the FIRST 2-candidate cell**, and because propagation is shallow, the gate **can refuse a puzzle that is actually determined**. It can never do the reverse — committing needs one branch to contradict, which is the `Forced` arm. **The error is one-sided, and it points the safe way**: a committed guess is an error; a declined deduction is merely incomplete. That asymmetry is now documented on the function and asserted by the renamed test.
+
+**Also taken from the review:** a candidate re-validation guard on both hidden-singles write loops (a snapshot entry can go stale when an earlier write in the same pass invalidates it). Applied, and **labelled as defensive rather than dressed up as a repair** — it is unreachable on a satisfiable grid (a completion places the digit once, so two forced positions for it in one unit contradict the completion's existence), and every fixture these loops run on is enumerator-verified satisfiable, so no test here can observe it. Declaring that is the same discipline as `E-A-FIX-CAN-BE-UNFALSIFIABLE-TOO-1`, applied to someone else's suggestion instead of my own fix.
+
+## 2026-07-29 — E-A-NULL-RESULT-IS-THE-DELIVERABLE-1 — G7 lands, the G4 reshape is refused with a number, and the canonical Sudoku grid turns out to be provably rigid
+
+**Status:** IN PR. **Confidence:** High — every claim below is either a printed measurement from `probe_sudoku_teacher` (ALL GATES GREEN, G1–G7) or a two-line proof.
+
+**G7, the gate a search solver structurally fails, is green — and its failure mode was verified, not assumed.** Both halves: on a verified-unique puzzle the reasoner commits (`Verdict::Committed`, Hamming 0); on a verified-ambiguous one (2 completions, 6 differing cells) it returns `Underdetermined { cell: 0 }` and **writes nothing into any cell the two completions disagree about**. The falsifier: change the `(false, false)` arm from "refuse" to "commit the first candidate" — which is exactly a backtracking solver's behaviour — and G7 fails on BOTH refuse assertions while `can_commit` stays true. The gate discriminates the refusal specifically, which is the whole claim.
+
+**The mechanism is deliberately split in two, and the split is load-bearing.** The reasoner detects ambiguity with its OWN fork machinery (`try_bifurcate_or_flag`: same operation as `try_bifurcate`, third arm made explicit — neither branch contradicting means *underdetermined*, not *pick one*). The fixture's ≥2-completion property is established by a separate `count_completions` enumerator that **the reasoner never calls**. If the verdict came from the enumerator, G7 would be asserting that a search solver can count solutions — trivially true, and proof of nothing. The reasoner's verdict is LOCAL (one-shot propagation); the enumerator's is global; the gate passes only when the local refusal agrees with the global truth.
+
+**The G4 reshape is REFUSED, with a number.** The follow-up asked to make bifurcate-vs-refuse an asserted contrast rather than a printed one. The scan says it cannot be: over k = 2..48 blanks × 8 strides × 81 offsets — **26858 unique puzzles, 388 where singles stall, 0 that the fork closes**, best residual 16. The identical censuses (staunen 63 / wisdom 18) were never an oversight in the gate; the two policies genuinely do the same thing on that family, because `try_bifurcate` needs exactly-2-candidate cells while a singles-stalled board is one whose cells mostly have ≥3, and `has_contradiction` is one-shot so a contradiction two inferences deep is invisible. **The null result is the deliverable** — G4 now states the non-contrast in its own detail line, and `TD-FORK-CANNOT-CLOSE-WHAT-SINGLES-CANNOT` carries the numbers and the falsifiable close condition (`fork_closes > 0`). Asserting the contrast would have required a hand-built fixture, and hand-built fixtures are precisely what this probe's two existing write-order footnotes warn about.
+
+**The canonical grid is provably rigid — a two-line proof that killed a whole fixture strategy.** The first ambiguous fixture tried the classic 4-corner unavoidable set and found none. Reason: `base_solution_boxmajor` is the cyclic grid `value(r,c) = (f(r) + c) mod 9`, so a valid corner swap needs `f(r₁)+c₁ ≡ f(r₂)+c₂` and `f(r₁)+c₂ ≡ f(r₂)+c₁`; subtracting gives `2(c₁−c₂) ≡ 0 (mod 9)`, and `gcd(2,9) = 1` forces `c₁ = c₂`. **No 2×2 in this grid is swappable.** (The first attempt also had an independent bug — all four corners inside ONE box, where a swap breaks the box constraint regardless — so it would have failed even on a grid that had them.) Ambiguity is now SEARCHED FOR and verified rather than constructed. Generalization worth keeping: **a fixture family can be structurally incapable of exhibiting the property you are about to test, and the cheapest way to find out is a search that reports its counts instead of an `expect()` that reports nothing.**
+
+**Hidden singles: the follow-up was granted, but not as asked.** "Thread hidden singles into `run_policy`" would have destroyed what G5 measures — hidden-single detection subsumes exactly the 2-candidate shape G5's fixture uses to separate elections-first from bifurcate-early, so both graded policies would have collapsed to the same path. Landed instead as a THIRD policy (`ElectionsFirstWithHidden`) inside the same loop: hidden singles are now exercised by the real policy machinery, `ElectionsFirst`/`BifurcateEarly` are byte-identical, and G4 asserts both halves that matter — the policy still solves correctly (Hamming 0, catching a wrong write) AND resolves no fewer cells (catching "did nothing extra"). **When a follow-up as literally worded would break a shipped measurement, the fix is a new variant beside it, not an edit through it.**
+
 ## 2026-07-29 — E-TRUNCATING-CONSTRUCTOR-IS-AN-ALIASING-HAZARD-1 — a silent `.min(CAP)` turns "malformed" into "a valid shorter thing", and a shared error that names one class misreports every other
 
 **Status:** IN PR (#864). **Confidence:** High — both findings are code-verified and each ships a falsifier that was PROVEN to fire (reverting the fix reproduces the exact defect signature).

.claude/board/LATEST_STATE.md

@@ -1,3 +1,11 @@
+## 2026-07-29 — branch `claude/x265-x266-plans-review-h9osnl` — PROBE-SUDOKU-TEACHER G7 + the fork-closure null result
+
+### Current Contract Inventory — probe surface only (no contract types added)
+- `lance_graph_planner::examples::probe_sudoku_teacher` — now **G1–G7, ALL GATES GREEN**. New: `count_completions` (bounded solution enumerator — the fixture VALIDATOR, never called by the reasoner), `try_bifurcate_or_flag` / `ForkOutcome` (the fork's explicit third arm: neither branch contradicting ⇒ `Underdetermined`), `Verdict` + `solve_with_ambiguity_gate`, `find_ambiguous_fixture` + `find_fork_required_fixture` (both DISCOVER-and-verify, never hand-derive), and `Policy::ElectionsFirstWithHidden`.
+- **G7 (new)** — the gate a search solver structurally fails: commit on a verified-unique puzzle, REFUSE on a verified-ambiguous one (2 completions, 6 differing cells, none written). Falsifier proven: flipping the refuse arm to "commit the first candidate" fails both refuse assertions with `can_commit` still true.
+- **G4 (amended)** — the bifurcate-vs-refuse contrast is explicitly **NOT asserted**, with the reason in the gate's own detail line: it does not exist on this puzzle family. Scan: 26858 unique / 388 singles-stall / **0 fork-closable** / best residual 16. Debt: `TD-FORK-CANNOT-CLOSE-WHAT-SINGLES-CANNOT` (close condition: `fork_closes > 0`). G4's third half instead asserts hidden-singles soundness (Hamming 0) and non-regression (census ≥ baseline).
+- **Finding worth carrying:** `base_solution_boxmajor` is the cyclic grid `(f(r)+c) mod 9` and is **provably free of 4-cell unavoidable sets** — a corner swap forces `2(c₁−c₂) ≡ 0 (mod 9)`, and `gcd(2,9)=1` ⟹ `c₁=c₂`. A fixture family can be structurally incapable of exhibiting the property under test. Detail: `EPIPHANIES` `E-A-NULL-RESULT-IS-THE-DELIVERABLE-1`; `AGENT_LOG` 2026-07-29.
+
 ## 2026-07-29 — branch `claude/happy-hamilton-0azlw4` — `invoke_recoder`: the SECOND keystone, proving `classid → ClassView → content` dispatch is class-AGNOSTIC (not fitted to one call shape)
 
 ### Current Contract Inventory — new entry

.claude/board/TECH_DEBT.md

@@ -1,5 +1,52 @@
 # Technical Debt Log — Open + Paid (double-entry, append-only)
 
+## TD-FORK-CANNOT-CLOSE-WHAT-SINGLES-CANNOT (2026-07-29)
+
+**Measured, not suspected.** `probe_sudoku_teacher`'s fixture scan over the
+stride family (k = 2..48 blanks × 8 strides × 81 offsets) reports:
+
+```text
+unique=26858   singles_stall=388   fork_closes=0   best_residual=16
+```
+
+26858 uniquely-solvable puzzles; 388 where naked singles genuinely stall; and
+**zero** that `try_bifurcate` then closes — the best fork-assisted run still
+leaves 16 cells wrong. So on this family the fork contributes NOTHING beyond
+what singles already had.
+
+**Two compounding causes, both structural:**
+
+1. `try_bifurcate` fires only on a cell with EXACTLY 2 candidates. A board on
+   which singles have stalled is precisely a board whose empty cells mostly
+   carry ≥3 — the two conditions are near-disjoint by construction.
+2. `has_contradiction` is ONE-SHOT propagation (an empty candidate set
+   somewhere). The wrong branch must therefore *immediately* empty some cell;
+   a contradiction two inferences deep is invisible, so `try_world` returns
+   "no contradiction" for branches that are in fact dead.
+
+**What this bounds.** The G4 follow-up asked to re-shape the gate so
+bifurcate-vs-refuse is the ASSERTED contrast rather than merely printed. It
+cannot be: the contrast does not exist to assert on this family. The two
+censuses were identical (staunen 63 / wisdom 18) not because the gate forgot
+to check, but because the two policies genuinely do the same thing there. G4
+now says so explicitly in its detail line instead of implying an untested
+contrast.
+
+**Cost of the naive fix.** Asserting `fork_beats_refuse` would have needed a
+hand-built fixture, and a hand-built fixture is exactly what the two
+`build_ambiguity_fixture` write-order footnotes already warn about — the
+earlier fixtures kept "working" for the wrong reason. The scan exists so the
+fixture's properties are VERIFIED (unique / stalls / closes) rather than
+argued.
+
+**To close this:** strengthen the fork, which is a mechanism change, not a
+gate reshape — either recursive propagation inside `try_world` (so deep
+contradictions are visible) or forking on ≥3 candidates (so the fork can
+reach the cells that actually block a stalled board). Either is a real design
+decision with a cost, and neither should be smuggled in under a gate edit.
+Re-run the scan afterwards: `fork_closes > 0` is the falsifiable success
+condition, and `best_residual` is the progress metric while it is still 0.
+
 ## TD-LENS-FACET-BY-VALUE-DECLINED (2026-07-29)
 
 **Codex P2 on #863** (`witness_fabric.rs:284`, "Keep lens facets borrowed