diff --git a/.claude/board/AGENT_LOG.md b/.claude/board/AGENT_LOG.md index 678a9b71..f8906243 100644 --- a/.claude/board/AGENT_LOG.md +++ b/.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. diff --git a/.claude/board/EPIPHANIES.md b/.claude/board/EPIPHANIES.md index bd6aec18..f043cfc4 100644 --- a/.claude/board/EPIPHANIES.md +++ b/.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). diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index 312b8fe9..4905b61a 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.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 diff --git a/.claude/board/TECH_DEBT.md b/.claude/board/TECH_DEBT.md index baee8ba7..469d1067 100644 --- a/.claude/board/TECH_DEBT.md +++ b/.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 diff --git a/.claude/plans/epistemic-quadrant-materialization-v1.md b/.claude/plans/epistemic-quadrant-materialization-v1.md index 2d6fae04..a7eed3d7 100644 --- a/.claude/plans/epistemic-quadrant-materialization-v1.md +++ b/.claude/plans/epistemic-quadrant-materialization-v1.md @@ -535,6 +535,49 @@ honest (that IS the metric) but thin; a wider-margin fixture would be sturdier. bifurcate-vs-refuse is the asserted contrast; (c) thread hidden singles into `run_policy` with a policy distinction that survives it. +> **⊘ ALL THREE RESOLVED 2026-07-29 — one shipped, one REFUSED with a number, +> one granted in a different shape** (`E-A-NULL-RESULT-IS-THE-DELIVERABLE-1`; +> probe re-run ALL GATES GREEN, now G1–G7). +> +> **(a) G7 — SHIPPED.** Both halves green: commit on a verified-unique puzzle +> (Hamming 0), `Underdetermined { cell: 0 }` + no digit written into any of +> the 6 differing cells on a verified-ambiguous one (2 completions). Two +> deliberately separate mechanisms: the reasoner refuses via its own +> `try_bifurcate_or_flag` (the fork's third arm — *neither* branch +> contradicting), while `count_completions` establishes the fixture's +> ground truth and **is never called by the reasoner**. Falsifier proven: +> flipping the refuse arm to "commit the first candidate" — a backtracking +> solver's behaviour — fails G7 on both refuse assertions with `can_commit` +> still true. +> +> **(b) G4 re-shape — REFUSED, and the refusal is the finding.** The contrast +> does not exist to assert on this puzzle family. Scan (k = 2..48 × 8 strides +> × 81 offsets): **26858 unique, 388 singles-stall, 0 fork-closable**, best +> residual 16. Cause is structural — `try_bifurcate` needs exactly-2-candidate +> cells, but a singles-stalled board has mostly ≥3; and `has_contradiction` is +> one-shot, so a contradiction two inferences deep is invisible. The identical +> censuses (staunen 63 / wisdom 18) were the two policies genuinely agreeing, +> not a missing assertion. G4 states the non-contrast in its detail line; +> `TD-FORK-CANNOT-CLOSE-WHAT-SINGLES-CANNOT` holds the numbers and the +> falsifiable close condition (`fork_closes > 0`). Closing it needs a stronger +> fork — a mechanism change, not a gate edit. +> +> **(c) hidden singles — GRANTED IN A DIFFERENT SHAPE.** Threading them into +> the existing policies would have erased what G5 measures (hidden-single +> detection subsumes G5's 2-candidate separator, collapsing both graded +> policies to one path). Landed as a third policy, `ElectionsFirstWithHidden`, +> inside the same `run_policy` loop; the two graded policies are byte-identical +> to before. G4 asserts both halves: still solves correctly (Hamming 0 — catches +> a wrong write) and resolves no fewer cells (catches "did nothing extra"). +> +> **Bonus finding, worth more than any of the three:** `base_solution_boxmajor` +> is the cyclic grid `value(r,c) = (f(r)+c) mod 9`, and a 4-corner swap needs +> `2(c₁−c₂) ≡ 0 (mod 9)` with `gcd(2,9)=1` ⟹ `c₁=c₂`. **No 2×2 in it is +> swappable**, so the classic unavoidable-set fixture cannot exist here at all — +> a fixture family can be structurally incapable of exhibiting the property +> about to be tested, and a search that reports its counts finds that out where +> an `expect()` reports nothing. + ## 4e. Comparison baseline: `zackthoutt/sudoku-ai` — search vs REASONING > Operator, 2026-07-29: *"for comparison — needs reimagining using logical diff --git a/crates/lance-graph-planner/examples/probe_sudoku_teacher.rs b/crates/lance-graph-planner/examples/probe_sudoku_teacher.rs index a0f37702..d02fe866 100644 --- a/crates/lance-graph-planner/examples/probe_sudoku_teacher.rs +++ b/crates/lance-graph-planner/examples/probe_sudoku_teacher.rs @@ -500,6 +500,18 @@ enum Policy { /// policy that demonstrates a bifurcation-required puzzle does not fully /// migrate. ForkRefusing, + /// Elections-first **including hidden singles** (follow-up (c)). + /// + /// Hidden singles are a SOUND inference the graded policies deliberately + /// omit — see the comment in [`run_policy`]. The follow-up asked to + /// "thread hidden singles into `run_policy`", and doing that to the + /// EXISTING policies would have destroyed the contrast G5 measures + /// (hidden-single detection subsumes the exact 2-candidate shape G5's + /// fixture uses to separate the two styles). Adding a THIRD policy gets + /// hidden singles exercised inside the real policy loop while leaving + /// `ElectionsFirst` / `BifurcateEarly` byte-identical, so G5 still + /// measures what it measured before. + ElectionsFirstWithHidden, } /// Run one policy to a fixed point (or `max_passes`), returning the full @@ -534,9 +546,41 @@ fn run_policy( let naked = apply_naked_singles(grid); made_any |= !naked.is_empty(); path.extend(naked); + // ...EXCEPT for the explicit hidden-singles policy, which opts in. + if matches!(policy, Policy::ElectionsFirstWithHidden) { + // `hidden_singles` is computed ONCE from the pre-write snapshot, so + // each write must be re-validated against the grid as it now + // stands: emptiness alone is not enough. Two entries from + // different units can name the same digit for two cells that share + // a THIRD unit; writing the first makes the second illegal, and a + // bare `is_none()` check would land it anyway (CodeRabbit, #865). + // + // Unreachable on a SATISFIABLE grid — if a completion exists, it + // places that digit somewhere, so two forced positions for it in + // one unit would contradict the completion's existence. So this + // guard only bites on an already-inconsistent grid (e.g. after a + // bad fork write), and **no test here can observe it**: every + // fixture this policy runs on is enumerator-verified satisfiable. + // Kept as defensive totality and labelled as such rather than + // dressed up as a proven repair (E-A-FIX-CAN-BE-UNFALSIFIABLE-TOO-1). + for (pos, digit) in hidden_singles(grid) { + if read_cell(&grid[pos]).is_none() + && candidates_from_full_sweep(grid, pos).contains(&digit) + { + write_cell(&mut grid[pos], digit, false); + path.push(Election { pos, digit }); + made_any = true; + } + } + } // Elections-first: bifurcation is the LAST resort, only when a pass // made zero progress via singles. Fork-refusing never bifurcates. - if !made_any && matches!(policy, Policy::ElectionsFirst) { + if !made_any + && matches!( + policy, + Policy::ElectionsFirst | Policy::ElectionsFirstWithHidden + ) + { if let Some(e) = try_bifurcate(grid) { path.push(e); made_any = true; @@ -654,7 +698,12 @@ fn atom_of(policy: Policy) -> u8 { match policy { Policy::ElectionsFirst => ATOM_A, Policy::BifurcateEarly => ATOM_B, - Policy::ForkRefusing => 0, + // Neither is a graded A/B style: both are diagnostic policies, so + // they carry the null atom (the zero-fallback ladder — 0 means "no + // designated style", never "style zero"). Left as explicit arms + // rather than a wildcard so the NEXT policy added has to make this + // choice deliberately instead of defaulting into null. + Policy::ForkRefusing | Policy::ElectionsFirstWithHidden => 0, } } @@ -686,6 +735,309 @@ fn set_frozen(row: &mut NodeRow, atom: u8) { row.set_style_lane(ValueTenant::FrozenStyle, lane); } +// ───────────────────────────────────────────────────────────────────────── +// G7 — the ambiguity gate. Two SEPARATE mechanisms, deliberately not shared. +// ───────────────────────────────────────────────────────────────────────── + +/// **The independent VALIDATOR — not part of the reasoner.** Enumerates +/// completions of `grid`, stopping once `cap` have been found, and returns +/// `(count, up to the first two completions)`. +/// +/// This is exactly the backtracking search §4e argues cannot teach a policy, +/// and it is included ONLY to establish a fixture's ground-truth property +/// (unique vs ≥2 completions) so the gate's anti-vacuity requirement can be +/// met. **The reasoner never calls it.** Keeping the two apart is the whole +/// point: if the ambiguity verdict were produced by the enumerator, G7 would +/// be asserting that a search solver can count solutions — which is trivially +/// true and proves nothing about the reasoner. +fn count_completions(grid: &[NodeRow; 81], cap: usize) -> (usize, Vec<[u8; 81]>) { + fn rec(g: &mut [NodeRow; 81], cap: usize, found: &mut usize, first: &mut Vec<[u8; 81]>) { + if *found >= cap { + return; + } + // Minimum-remaining-values, position-ascending tie-break — makes the + // enumeration order deterministic (D-QUANTGATE replay). + let mut best: Option<(usize, Vec)> = None; + for pos in 0..81 { + if read_cell(&g[pos]).is_some() { + continue; + } + let c = candidates_from_full_sweep(g, pos); + if c.is_empty() { + return; // dead end — this branch completes nothing + } + if best.as_ref().is_none_or(|(_, bc)| c.len() < bc.len()) { + best = Some((pos, c)); + } + } + let Some((pos, cands)) = best else { + *found += 1; + if first.len() < 2 { + let mut snap = [0u8; 81]; + for (p, slot) in snap.iter_mut().enumerate() { + *slot = read_cell(&g[p]).map_or(0, |(d, _)| d); + } + first.push(snap); + } + return; + }; + for d in cands { + write_cell(&mut g[pos], d, false); + rec(g, cap, found, first); + clear_cell(&mut g[pos]); + if *found >= cap { + return; + } + } + } + let mut g = *grid; + let (mut found, mut first) = (0usize, Vec::new()); + rec(&mut g, cap, &mut found, &mut first); + (found, first) +} + +/// What a fork attempt concluded — the fork-return rule with its THIRD arm +/// made explicit. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum ForkOutcome { + /// Exactly one branch contradicted, so the other is forced. The + /// elimination is the permanent gain (§4c); the losing world is discarded. + Forced(Election), + /// **NEITHER branch contradicted** — the cell is genuinely underdetermined + /// as far as propagation can see, so committing either digit would be a + /// guess dressed as a deduction. This is the arm a search solver does not + /// have: it would simply take the first branch and report success. + Underdetermined(usize), + /// No 2-candidate cell exists to fork on. + NoTwoCandidateCell, +} + +/// The reasoner's OWN ambiguity detection — same machinery as +/// [`try_bifurcate`], opposite ledger. `try_bifurcate` asks "did one branch +/// fail?" and commits the survivor; this asks the complete question and +/// distinguishes *forced* from *underdetermined*. +/// +/// The verdict is LOCAL: `has_contradiction` is one-shot propagation, not a +/// recursive search, so "neither branch contradicted" means "no contradiction +/// is visible from here", not "two global completions exist". That is why +/// G7's anti-vacuity half verifies the fixture's ≥2-completion property with +/// the independent [`count_completions`] enumerator instead of trusting this. +/// +/// # The error is one-sided, deliberately +/// +/// The scan returns on the FIRST 2-candidate cell, and locality means a cell +/// whose wrong branch only dies three inferences deep reads as +/// `Underdetermined`. So this **can refuse a puzzle that is actually +/// determined** — a false refusal. It cannot do the reverse: committing an +/// underdetermined cell would require one branch to contradict, which is +/// precisely the `Forced` arm. Under §4e's ledger that asymmetry points the +/// safe way — a committed guess is an error, a declined deduction is only +/// incomplete. Pinned by +/// `fork_flag_decides_on_the_first_two_candidate_cell_and_errs_toward_refusal`. +fn try_bifurcate_or_flag(grid: &mut [NodeRow; 81]) -> ForkOutcome { + for pos in 0..81 { + if read_cell(&grid[pos]).is_some() { + continue; + } + let cands = candidates_from_full_sweep(grid, pos); + if cands.len() == 2 { + let (a, b) = (cands[0], cands[1]); + let (a_bad, b_bad) = (try_world(grid, pos, a), try_world(grid, pos, b)); + match (a_bad, b_bad) { + (true, false) => { + write_cell(&mut grid[pos], b, false); + return ForkOutcome::Forced(Election { pos, digit: b }); + } + (false, true) => { + write_cell(&mut grid[pos], a, false); + return ForkOutcome::Forced(Election { pos, digit: a }); + } + (false, false) => return ForkOutcome::Underdetermined(pos), + // Both branches contradict ⇒ the grid is already inconsistent + // at this cell. Keep scanning; write nothing. + // + // **Unreachable on any SATISFIABLE grid**, which is why this + // arm cannot mask a G7 failure: if a completion exists, some + // candidate at `pos` belongs to it, and a world holding that + // candidate cannot have an empty candidate set anywhere — so + // at least one of `a_bad` / `b_bad` is false. Both being true + // therefore means the caller handed us an already-unsatisfiable + // board, which neither G7 fixture is (both are enumerator- + // verified: one completion, or two). The arm exists for + // totality, not for a live path. (Raised in #865 review; + // agreed non-blocking — recorded here so the reasoning is not + // re-derived next time someone reads a match arm with no test.) + (true, true) => {} + } + } + } + ForkOutcome::NoTwoCandidateCell +} + +/// The gate's verdict on a whole puzzle. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum Verdict { + /// Every cell resolved by forced steps only. + Committed, + /// Refused: an underdetermined cell was reached and NOT written. + Underdetermined { cell: usize }, + /// Ran out of forced moves without reaching an underdetermined 2-candidate + /// cell (e.g. every empty cell has ≥3 candidates). + Stalled, +} + +/// Solve under the ambiguity gate: singles (naked AND hidden) to exhaustion, +/// then a fork — but a fork that REFUSES when neither branch fails. +/// +/// This is where hidden singles belong in a policy loop. They are deliberately +/// NOT in [`run_policy`]'s graded policies (see the comment there): hidden- +/// single detection subsumes exactly the 2-candidate shape G5's fixture uses +/// to separate elections-first from bifurcate-early, so threading them into +/// the graded loop would erase the contrast G5 measures. Here there is no such +/// contrast to protect — the gate is being asked "can you finish honestly?", +/// so it should use every sound inference it has. +fn solve_with_ambiguity_gate(grid: &mut [NodeRow; 81], max_passes: usize) -> Verdict { + for _ in 0..max_passes { + let mut progress = !apply_naked_singles(grid).is_empty(); + for (pos, digit) in hidden_singles(grid) { + // Same re-validation as `run_policy`'s hidden-singles arm, for the + // same reason (snapshot staleness); see the comment there. + if read_cell(&grid[pos]).is_none() + && candidates_from_full_sweep(grid, pos).contains(&digit) + { + write_cell(&mut grid[pos], digit, false); + progress = true; + } + } + if progress { + continue; + } + match try_bifurcate_or_flag(grid) { + ForkOutcome::Forced(_) => {} + ForkOutcome::Underdetermined(cell) => return Verdict::Underdetermined { cell }, + ForkOutcome::NoTwoCandidateCell => break, + } + } + if (0..81).all(|p| read_cell(&grid[p]).is_some()) { + Verdict::Committed + } else { + Verdict::Stalled + } +} + +/// **DISCOVER** a genuinely ambiguous fixture — an *unavoidable set*: four +/// cells at the corners of a rectangle (2 rows × 2 columns) carrying the +/// pattern `a b / b a`. Blanking them leaves two completions, because the +/// diagonal swap preserves every row, column, and box multiset. +/// +/// Hand-picking the corners is how the first attempt failed: all four were +/// taken from ONE box, where a diagonal swap *does* break the box constraint, +/// so the fixture stayed unique and the gate's refuse-half asserted nothing. +/// The rectangle must straddle exactly two boxes. Rather than encode that +/// condition, every rectangle is tried and the ≥2-completion property is +/// VERIFIED by the enumerator — the same discipline the fork scan uses. +/// +/// **This base solution has NO 4-cell unavoidable set — provably.** +/// +/// `base_solution_boxmajor` is the canonical cyclic grid +/// `value(r,c) = (f(r) + c) mod 9` with `f(r) = 3r + r/3`. A 4-corner swap +/// needs both diagonals equal: +/// +/// ```text +/// f(r1) + c1 ≡ f(r2) + c2 and f(r1) + c2 ≡ f(r2) + c1 (mod 9) +/// ``` +/// +/// Subtracting gives `2(c1 − c2) ≡ 0 (mod 9)`, and `gcd(2, 9) = 1`, so +/// `c1 ≡ c2` — impossible for a genuine rectangle. Every 2×2 in this grid is +/// therefore rigid, which is why the first rectangle search returned nothing. +/// (The earlier failure had a second, independent bug — all four corners in +/// ONE box, where a swap breaks the box constraint regardless.) +/// +/// So ambiguity is SEARCHED FOR rather than constructed: blank progressively +/// larger deterministic stride-sets and return the first whose completion +/// count is ≥2. Verified by the enumerator, never assumed. +/// +/// Returns `(grid, the blanked cells)`. +fn find_ambiguous_fixture(sol: &[u8; 81]) -> Option<([NodeRow; 81], Vec)> { + for k in 4..=32usize { + for stride in [7usize, 11, 13, 17, 19, 23, 29, 31] { + for start in 0..81usize { + let grid = puzzle_from_stride(sol, start, stride, k); + if count_completions(&grid, 2).0 >= 2 { + let blanked = (0..81).filter(|&p| read_cell(&grid[p]).is_none()).collect(); + return Some((grid, blanked)); + } + } + } + } + None +} + +/// Blank `k` cells from `sol` on a deterministic stride and return the grid. +fn puzzle_from_stride(sol: &[u8; 81], start: usize, stride: usize, k: usize) -> [NodeRow; 81] { + let mut grid = grid_from_solution(sol); + let mut seen = Vec::new(); + for i in 0..k { + let p = (start + i * stride) % 81; + if !seen.contains(&p) { + seen.push(p); + } + } + blank_positions(&mut grid, &seen); + grid +} + +/// **DISCOVER** (never hand-derive) a fixture that singles alone cannot +/// finish but a fork can — the fixture G4's reshaped second half needs. +/// +/// Hand-constructing one is where the earlier fixtures kept going wrong (see +/// `build_ambiguity_fixture`'s two write-order footnotes). So this scans a +/// deterministic family of blank-sets and returns the first that PROVABLY has +/// all three properties, each verified rather than argued: +/// 1. exactly ONE completion (so "unresolved" means stalled, not ambiguous), +/// 2. a fork-refusing policy leaves ≥1 cell empty (singles genuinely stall), +/// 3. a fork-using policy reaches Hamming 0 (the fork is what closes it). +/// +/// Returns `(grid, solution)`. +fn find_fork_required_fixture(sol: &[u8; 81]) -> Option<([NodeRow; 81], [u8; 81])> { + let (mut n_unique, mut n_stalls) = (0usize, 0usize); + let mut best_residual = usize::MAX; + for k in 2..=48usize { + for stride in [7usize, 11, 13, 17, 19, 23, 29, 31] { + for start in 0..81usize { + let grid = puzzle_from_stride(sol, start, stride, k); + if count_completions(&grid, 2).0 != 1 { + continue; + } + n_unique += 1; + let mut refuse = grid; + let (_, _) = run_policy(&mut refuse, Policy::ForkRefusing, sol, 64); + if (0..81).all(|p| read_cell(&refuse[p]).is_some()) { + continue; // singles alone finished it — no fork required + } + n_stalls += 1; + let mut forked = grid; + let (_, _) = run_policy(&mut forked, Policy::ElectionsFirst, sol, 64); + let residual = hamming(&forked, sol); + best_residual = best_residual.min(residual); + if residual == 0 { + return Some((grid, *sol)); + } + } + } + } + // Report WHERE the scan died rather than just returning None — the counts + // separate "no unique puzzle in the family" from "singles never stall" + // from "the fork cannot close what singles leave", and those are three + // different findings. + // Reaching this line means the scan returned no fixture, so fork_closes + // is 0 by construction (the loop returns on the first success). + println!( + " [fixture scan] unique={n_unique} singles_stall={n_stalls} fork_closes=0 best_residual={best_residual}" + ); + None +} + fn main() { println!("════════ PROBE-SUDOKU-TEACHER ════════\n"); @@ -933,11 +1285,105 @@ fn main() { // solve PATH, not by final census (see below). let refuse_does_not_fully_migrate = refuse_census.wisdom < 81 && refuse_census.staunen + refuse_census.confusion > 0; - let g4_pass = easy_migrates && refuse_does_not_fully_migrate; + + // ── G4 second half, RESHAPED (follow-up (b)) ── + // + // As first written, the bifurcate-vs-refuse contrast was PRINTED but not + // ASSERTED, and on the sparse box3/box4 fixture the two censuses were in + // fact identical (staunen 63 / wisdom 18). The reason is mechanical: + // `try_bifurcate` only fires on cells with EXACTLY 2 candidates, and a + // ~15-given board leaves almost every empty cell with far more than two — + // so BifurcateEarly never found a fork and degenerated into ForkRefusing. + // The gate therefore asserted "easy differs from hard", which the easy + // half already covered, and the policy contrast rode along unasserted. + // + // The fix WOULD be a fixture where a fork is REQUIRED and REACHABLE. The + // scan below looks for one and **finds none** — and that null result is + // the actual deliverable of this follow-up, so it is reported rather than + // asserted away. Over the stride family (k = 2..48 blanks × 8 strides × + // 81 offsets): **26858 uniquely-solvable puzzles, 388 where naked singles + // genuinely stall, and 0 that the fork then closes** (best residual 16 + // cells). See `find_fork_required_fixture`, which prints the three counts. + // + // The cause is mechanical and worth stating precisely, because it bounds + // what G4's second half can ever assert: + // * `try_bifurcate` only fires on a cell with EXACTLY 2 candidates, and + // a board where singles have stalled is precisely a board whose empty + // cells mostly have ≥3; + // * `has_contradiction` is ONE-SHOT propagation, so the wrong branch + // has to empty some cell's candidate set immediately — a contradiction + // two inferences deep is invisible to it. + // So on this family the fork contributes nothing that singles did not + // already have, which is why the original censuses were identical + // (staunen 63 / wisdom 18) rather than merely unasserted. **The contrast + // was not un-asserted by oversight; it does not exist to assert.** + // Closing it needs a stronger fork (recursive propagation, or forking on + // ≥3 candidates), which is a mechanism change, not a gate reshape. + // Tracked as TD-FORK-CANNOT-CLOSE-WHAT-SINGLES-CANNOT. + // The null result is GATE-ENFORCED, not merely printed (CodeRabbit, #865). + // Printing it while `g4_pass` ignored it would let the gate stay green + // after its own stated limitation became false: strengthen the fork so a + // closable fixture exists, and G4 would keep passing while its detail line + // still claimed `0/388 closable` — a stale claim frozen inside a PASS. + // Asserting `is_none()` makes the limitation expire loudly. **A future + // fork improvement is SUPPOSED to fail this gate**; that failure is the + // reminder to re-shape G4 around the contrast that now exists (and to + // close TD-FORK-CANNOT-CLOSE-WHAT-SINGLES-CANNOT), which is exactly the + // inertness pairing the falsifiability rule asks for. + let fork_fixture = find_fork_required_fixture(&solved_variants[0]); + let fork_still_cannot_close = fork_fixture.is_none(); + println!( + " fork-required fixture found = {} → fork_still_cannot_close={fork_still_cannot_close}", + fork_fixture.is_some() + ); + if fork_fixture.is_some() { + println!( + " ⚠ the fork now CLOSES a singles-stalled puzzle — the G4 null result has expired.\n \ + Re-shape G4's second half to assert the bifurcate-vs-refuse contrast and close\n \ + TD-FORK-CANNOT-CLOSE-WHAT-SINGLES-CANNOT." + ); + } + + // Follow-up (c): the hidden-singles policy exercised in the REAL policy + // loop, on the easy fixture (a fresh copy — `g4_easy` above was consumed + // by its own run). Hidden singles are SOUND, so the policy must still + // land every digit correctly, and must resolve no fewer cells than the + // same policy without them. Both halves are asserted: Hamming alone would + // not catch "did nothing extra", and the census alone would not catch a + // wrong write. + let mut hidden_grid = grid_from_solution(&solved_variants[0]); + blank_positions(&mut hidden_grid, &easy_blanks); + write_box_witness(&mut hidden_grid); + let (_, _) = run_policy( + &mut hidden_grid, + Policy::ElectionsFirstWithHidden, + &solved_variants[0], + 40, + ); + let hidden_census = quadrant_census(&hidden_grid); + let hidden_is_sound = hamming(&hidden_grid, &solved_variants[0]) == 0; + let hidden_never_worse = hidden_census.wisdom >= easy_census.wisdom; + println!( + " hidden-singles census {hidden_census:?} sound={hidden_is_sound} never_worse={hidden_never_worse}" + ); + + let g4_pass = easy_migrates + && refuse_does_not_fully_migrate + && hidden_is_sound + && hidden_never_worse + && fork_still_cannot_close; + // The detail line is DERIVED from the scan, never hardcoded — a fixed + // string would keep asserting "0 closable" in prose after the code stopped + // making it true. + let fork_note = if fork_still_cannot_close { + "fork-vs-refuse contrast NOT asserted: no fork-required fixture exists in the scanned family (0 closable of 388 singles-stall) — TD-FORK-CANNOT-CLOSE-WHAT-SINGLES-CANNOT" + } else { + "STALE NULL RESULT: the scan FOUND a fork-closable fixture, so the documented limitation no longer holds — re-shape G4's second half to assert the contrast" + }; gates.push(( "G4", g4_pass, - format!("easy_migrates={easy_migrates} refuse_does_not_fully_migrate={refuse_does_not_fully_migrate} (bifurcate census printed above for comparison)"), + format!("easy_migrates={easy_migrates} refuse_does_not_fully_migrate={refuse_does_not_fully_migrate} hidden_sound={hidden_is_sound} hidden_never_worse={hidden_never_worse} fork_still_cannot_close={fork_still_cannot_close} | {fork_note}"), )); // ═══════════════════ G5 — triangle motion ═══════════════════ @@ -1090,6 +1536,91 @@ fn main() { ), )); + // ═══════════════════ G7 — the ambiguity gate ═══════════════════ + // + // The gate a search solver structurally fails. Both halves are required, + // and they are opposite behaviours on the SAME machinery: commit when the + // puzzle determines an answer, REFUSE when it does not. A backtracking + // solver returns a valid completion in both cases and is "successful" and + // precisely wrong in the second (§4e). + println!("\n── G7: ambiguity gate ──"); + + // Can-commit: a uniquely-determined puzzle. Uniqueness is VERIFIED by the + // independent enumerator rather than assumed from "we built it from a + // solution" — blanking cells out of a valid grid does not by itself keep + // the result unique, and an ambiguous "unique" fixture would make the + // commit half assert the opposite of what it claims. + let mut commit_grid = grid_from_solution(&solved_variants[0]); + blank_positions(&mut commit_grid, &easy_blanks); + write_box_witness(&mut commit_grid); + let (unique_count, _) = count_completions(&commit_grid, 2); + let commit_verdict = solve_with_ambiguity_gate(&mut commit_grid, 64); + let commit_hamming = hamming(&commit_grid, &solved_variants[0]); + // `unique_count == 1` is a CONJUNCT, not a printout (CodeRabbit, #865). + // The comment above says uniqueness is "VERIFIED by the enumerator" — but + // computing it and only printing it verifies nothing. Without this term, + // fixture drift that made the commit puzzle ambiguous would leave the + // can-commit half asserting the exact opposite of what it documents: that + // the reasoner CONFIDENTLY COMPLETED an underdetermined board, which is + // the failure G7's other half exists to catch. + let can_commit = + unique_count == 1 && commit_verdict == Verdict::Committed && commit_hamming == 0; + println!( + " unique puzzle completions={unique_count} verdict={commit_verdict:?} hamming={commit_hamming} → can_commit={can_commit}" + ); + + // Can-refuse: strip the fixture below the critical point so ≥2 valid + // completions exist. Blanking a whole box guarantees ambiguity is + // REACHABLE, but the property is not assumed — it is VERIFIED by the + // independent enumerator below (the anti-vacuity requirement: "reported + // ambiguity" must not be able to pass on a puzzle that was really unique). + let (ambiguous_grid, rect) = find_ambiguous_fixture(&solved_variants[0]) + .expect("an unavoidable set must exist in a full 9x9 solution"); + let (amb_count, amb_first_two) = count_completions(&ambiguous_grid, 2); + let genuinely_ambiguous = amb_count >= 2; + // Which cells actually differ between the two completions — the cells the + // reasoner must refuse to write. + let differing: Vec = if amb_first_two.len() == 2 { + (0..81) + .filter(|&p| amb_first_two[0][p] != amb_first_two[1][p]) + .collect() + } else { + Vec::new() + }; + let mut refuse_grid = ambiguous_grid; + let refuse_verdict = solve_with_ambiguity_gate(&mut refuse_grid, 64); + let reported_ambiguity = matches!(refuse_verdict, Verdict::Underdetermined { .. }); + // The load-bearing assertion: it did NOT write a digit into any cell that + // the two completions disagree about. + let wrote_nothing_undetermined = differing + .iter() + .all(|&p| read_cell(&refuse_grid[p]).is_none()); + // Sanity on the fixture itself: every cell the two completions disagree + // about must be one we actually blanked. If a GIVEN differed, the + // enumerator would be contradicting the fixture rather than exploring it, + // and the whole refuse-half would be measuring a bug. + let differing_are_blanked = differing.iter().all(|p| rect.contains(p)); + println!( + " ambiguous completions={amb_count} (≥2 verified) differing_cells={differing:?} verdict={refuse_verdict:?}" + ); + println!( + " → reported_ambiguity={reported_ambiguity} wrote_nothing_undetermined={wrote_nothing_undetermined}" + ); + + let g7_pass = can_commit + && genuinely_ambiguous + && differing_are_blanked + && reported_ambiguity + && wrote_nothing_undetermined; + gates.push(( + "G7", + g7_pass, + format!( + "can_commit={can_commit} (unique completions={unique_count}) | genuinely_ambiguous={genuinely_ambiguous} (completions={amb_count}, {} differing cells) reported_ambiguity={reported_ambiguity} wrote_nothing_undetermined={wrote_nothing_undetermined}", + differing.len() + ), + )); + // ═══════════════════ Report ═══════════════════ println!("\n════════ GATES ════════"); let mut all_pass = true; @@ -1178,6 +1709,108 @@ fn quadrant_census(grid: &[NodeRow; 81]) -> Census { /// zero-candidate cell during census, so the probe's printed output is /// byte-identical with and without the fix. Without this test the correction /// would be indistinguishable from a no-op. +/// The G7 helpers pinned directly, not only through the gate's print-out +/// (CodeRabbit, #865). Each asserts a DIFFERENT outcome of the same machinery, +/// so a change that collapsed the three verdicts into one would fail here even +/// if the gate's booleans still lined up. +#[test] +fn ambiguity_gate_helpers_separate_unique_from_underdetermined() { + let sol = permute_solution(&base_solution_boxmajor(), &PERM_A); + + // Unique puzzle: exactly one completion, and the gate COMMITS it. + let mut unique = grid_from_solution(&sol); + blank_positions( + &mut unique, + &(0..81).filter(|p| p % 5 == 0).collect::>(), + ); + assert_eq!( + count_completions(&unique, 2).0, + 1, + "the easy fixture must be uniquely determined, or the commit half is meaningless" + ); + let mut g = unique; + assert_eq!(solve_with_ambiguity_gate(&mut g, 64), Verdict::Committed); + assert_eq!(hamming(&g, &sol), 0, "committing must mean solving"); + + // Ambiguous puzzle: ≥2 completions, and the gate REFUSES rather than + // completing it — the discrimination a search solver cannot make. + let (amb, blanked) = find_ambiguous_fixture(&sol).expect("an ambiguous fixture must exist"); + let (n, first_two) = count_completions(&amb, 2); + assert_eq!(n, 2, "the refuse half needs a genuinely ambiguous fixture"); + let differing: Vec = (0..81) + .filter(|&p| first_two[0][p] != first_two[1][p]) + .collect(); + assert!( + !differing.is_empty(), + "two DISTINCT completions must disagree somewhere" + ); + assert!( + differing.iter().all(|p| blanked.contains(p)), + "only blanked cells may differ between completions" + ); + let mut g2 = amb; + let verdict = solve_with_ambiguity_gate(&mut g2, 64); + assert!( + matches!(verdict, Verdict::Underdetermined { .. }), + "an under-constrained puzzle must be refused, got {verdict:?}" + ); + for p in differing { + assert!( + read_cell(&g2[p]).is_none(), + "cell {p} is underdetermined and must NOT have been written" + ); + } +} + +/// **Scan order decides, and it errs toward refusal.** `try_bifurcate_or_flag` +/// returns on the FIRST 2-candidate cell it meets, so a grid holding both an +/// underdetermined cell and a forced one reports `Underdetermined` — it does +/// not go looking for a forced cell first. +/// +/// This test was written expecting `Forced` (the target at 43, which G3 proves +/// is forced) and **failed**, returning `Underdetermined(39)` — the parked +/// companion, which sits earlier in scan order and whose two candidates both +/// survive one-shot propagation. The behaviour is correct; the expectation was +/// wrong, so the test now pins what actually holds. +/// +/// The consequence is the important part: **the gate can refuse a puzzle that +/// is in fact determined** (a false refusal), because shallow propagation +/// cannot see a contradiction three inferences deep. It can never do the +/// opposite — commit an underdetermined cell — since that needs BOTH branches +/// to survive, which is exactly what triggers the refusal. The asymmetry +/// points the safe way for this doctrine: committing a guess is an error, +/// while declining to deduce is merely incomplete (§4e). +#[test] +fn fork_flag_decides_on_the_first_two_candidate_cell_and_errs_toward_refusal() { + let (mut grid, _z, target) = build_ambiguity_fixture((3, 3), (3, 0), &PERM_A); + write_box_witness(&mut grid); + assert_eq!( + candidates_from_full_sweep(&grid, target).len(), + 2, + "the fixture's target must be a genuine 2-candidate cell" + ); + let first_two_candidate = (0..81) + .find(|&p| read_cell(&grid[p]).is_none() && candidates_from_full_sweep(&grid, p).len() == 2) + .expect("the fixture has at least one 2-candidate cell"); + assert!( + first_two_candidate < target, + "this fixture's companion must precede the target, or the test proves nothing about order" + ); + match try_bifurcate_or_flag(&mut grid) { + ForkOutcome::Underdetermined(pos) => { + assert_eq!( + pos, first_two_candidate, + "the verdict must come from the FIRST 2-candidate cell in scan order" + ); + assert!( + read_cell(&grid[pos]).is_none(), + "a refusal must never write the cell it refused" + ); + } + other => panic!("expected Underdetermined at the first 2-candidate cell, got {other:?}"), + } +} + #[test] fn contradicted_cell_is_not_counted_as_wisdom() { // Box-major layout: box 0 owns positions 0..=8; `cell_in_box(8) == 8`, so