From 08a44355403604c346f8d907811edce992382cc4 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Fri, 16 Oct 2026 03:40:44 -0400 Subject: [PATCH] KB5e: chi(Z) >= 4 case of F-star residue (ii) - structural lemmas, anchors, bounded search; no kappa MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add research/fstar-chi4-zero-digraph-seed73765f29: the chi(Z) >= 4 case of open problem F-star's zero-digraph residue (ii), the question PR 2774 left as its open question 2. PROVEN with written proofs: chi(Z) >= 4 requires chi(U(Z)) >= 4; chi(Z) <= 3 for v <= 4; mutual-zero neighbourhoods span at most 2 dimensions per side and are empty or a union of cliques <= 3 and complete bipartite graphs (two-plane classification), so G_0 contains no odd wheel; basis-pivot families are tripartite; and an explicit rank-3 decoder with chi(U(Z)) = 4 but chi(Z) = 2 and exact cert = 6 = v separates the underlying-graph question from the dichromatic one. CHECKED in a fresh stdlib engine: every recorded anchor of PRs 2717/2747/2774/2869 reproduced before new work (tied_min 11/12, cex_min_1 18/19, chain 22, MP/MX 9 and 16 over 4096/6144 pivot maps, chi(Z) = 3 on both fixtures, MAS 4/10, anchor reach 0/12 and 8/19), including the efficient1700 retained rank-2 pivot counterexample as a control. Smallest-first search for chi(Z) >= 4 across four generator families and a sequential linear construction of the Grötzsch graph as a mutual-zero pattern finds no instance (max chi = 3 attained); the per-route obstruction records are budgeted, not unrealizability proofs. F-star holds on every instance examined and remains open in general; no kappa, no frontier change. Prepared by Aaron Wang with help from opencode. --- .../CERTIFICATE.json | 60 + .../README.md | 312 +++++ .../SOURCES.json | 30 + .../TASK-CARD.md | 116 ++ .../TASK.json | 82 ++ .../VERIFY.json | 21 + .../data/cex_min_1.B22.json | 1 + .../data/cex_min_1.json | 1 + .../data/cex_min_1.witness.json | 1 + .../data/tied_min.json | 1 + .../evidence/SEARCH-LOG.md | 57 + .../verify.py | 1071 +++++++++++++++++ 12 files changed, 1753 insertions(+) create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/CERTIFICATE.json create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/README.md create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/SOURCES.json create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/TASK-CARD.md create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/TASK.json create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/VERIFY.json create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.B22.json create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.json create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.witness.json create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/data/tied_min.json create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/evidence/SEARCH-LOG.md create mode 100644 research/fstar-chi4-zero-digraph-seed73765f29/verify.py diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/CERTIFICATE.json b/research/fstar-chi4-zero-digraph-seed73765f29/CERTIFICATE.json new file mode 100644 index 0000000000..1c7b26fdb3 --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/CERTIFICATE.json @@ -0,0 +1,60 @@ +{ + "calibration": "PASS_FC4_CALIBRATION", + "controls": "PASS_FC4_CONTROLS", + "digest": "032e7239429ba1f8", + "package": "research/fstar-chi4-zero-digraph-seed73765f29", + "search_stats": { + "chi4": 0, + "grz_obstructions": [ + { + "deepest": 6, + "nodes": 60087, + "reason": "node_cap" + }, + { + "deepest": 8, + "nodes": 60104, + "reason": "node_cap" + }, + { + "deepest": 6, + "nodes": 60085, + "reason": "node_cap" + } + ], + "instances": 22, + "max_chi": 3, + "max_chi_G0": 3, + "max_chi_U": 3, + "min_mp_ratio": 1.0 + }, + "settlements": [ + { + "D_compatible_3dic": true, + "MAS_H": 6, + "MAS_Z": 4, + "MP": 6, + "MP_exhaustive": true, + "MP_pivot_product": 1, + "anchor_reach": 6, + "cancellation_lines": 0, + "cert_exact": 6, + "cert_lower_bound": 6, + "chi": 2, + "chi_G0": 2, + "chi_G0_le3": true, + "chi_U": 4, + "chi_U_le3": false, + "chi_exact": true, + "chi_le3": true, + "falsifier_found": false, + "gamma": 0, + "label": "w5_underlying_separation", + "meets_threshold": true, + "omega_mutual": 2, + "threshold": 4, + "v": 6, + "witness_replayed": true + } + ] +} diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/README.md b/research/fstar-chi4-zero-digraph-seed73765f29/README.md new file mode 100644 index 0000000000..acbea2b0ff --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/README.md @@ -0,0 +1,312 @@ +# fstar-chi4-zero-digraph-seed73765f29 + +**The chi(Z) >= 4 case of F-star residue (ii): structural lemmas, anchor +calibration, and a smallest-first search with exact obstructions (no kappa, no +frontier change).** This package takes the question +[PR 2774](https://github.com/CrocSwap/integer-mult-bounds/pull/2774) left as +its open question 2 (and [PR 2717](https://github.com/CrocSwap/integer-mult-bounds/pull/2717) +as its open question 2): **can an exact 3-total rational decoder's zero digraph +have dichromatic number `chi(Z) >= 4` at all?** It (1) proves structural lemmas +constraining any such instance (PROVEN below), including an explicit rank-3 +decoder with `chi(U(Z)) = 4` but `chi(Z) = 2` that separates the +underlying-graph question from the dichromatic one; (2) reproduces every +recorded anchor of PRs 2717/2747/2774/2869 in a fresh engine before trusting +anything new (CHECKED); (3) runs a bounded, smallest-first search for the +smallest `chi(Z) >= 4` instance across four generator families and a sequential +linear construction of the smallest triangle-free 4-chromatic target, recording +the exact obstruction per route (CHECKED, scoped negative); and (4) settles +every instance examined through the D(t)-pivot, anchor and certificate +machinery. **F-star itself is not proved and not refuted here.** Every claim is +labelled PROVEN, CHECKED or DEMOTED. + +## The object + +A `T = 3` exact decoder on `v` lines is `M = sum_{j=1..3} p_j q_j^T` over the +rationals with `M_tt != 0` on every line. Row support `pi(t) = {j : p_j(t) != +0}`, column support `sigma(t) = {j : q_j(t) != 0}`, `D(t) = pi(t) intersect +sigma(t)` (nonempty). The **zero digraph** is `Z = {(t,s) : t != s, M_ts = 0}`; +`U(Z)` is its underlying undirected graph (`{t,s}` adjacent iff at least one +direction is an arc) and `G_0` the **mutual-zero graph** (`{t,s}` adjacent iff +both directions are zeros). `chi(Z)` is the dichromatic number: the least number +of classes partitioning the lines so that each class induces an acyclic +subdigraph. The proven chain `cost >= sum_j r_j >= cert(M)` and the definition +of `cert(M)` (L8 labellings) are from the merged +`research/root-unit-decoder-lemmas` ([PR 1590](https://github.com/CrocSwap/integer-mult-bounds/pull/1590) +by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code +assistance). **F-star** is `cert(M) >= floor(2v/3)` for every exact 3-total +rational decoder. + +Two colouring notions must be kept apart, per the maintainer review of +PR 2717/2774 (`docs/research/community-efficient1700-review.md`, retained +counterexample `research/community-efficient1700-audit/checks/check-2717-pivot-counterexample.json`): +`chi(Z) <= 3` is a property of the digraph alone, while *3-dichromatic under +`D(t)`* asks for a partition whose classes come from a pivot map `c(t)` in +`D(t)` (equivalently: matched-pivot value `max_c sum_i MAS(Z[C_i]) = v`, Lemma +MP of PR 2717). Ordinary 3-dichromaticity and nonempty `D(t)` do **not** imply +a `D(t)`-compatible partition; this package reports the two quantities +separately everywhere. + +After [PR 2869](https://github.com/CrocSwap/integer-mult-bounds/pull/2869) +(Aaron Wang) the residue of F-star is (i') cancellation lines +`{t : v_2(M_tt) > gamma}` plus (ii) zero digraphs; PR 2774 settled (ii) on the +fixtures (both `chi(Z) = 3` exactly, yet non-3-dichromatic under `D(t)`: the +obstruction there is the pivot constraints, not the digraph coloring) and left +the `chi(Z) >= 4` case open. That case is what this package attacks. + +## Recorded anchors reproduced first - CHECKED + +Fresh engine (`verify.py`, stdlib, deterministic, about 12 s), calibrated +against every recorded anchor before any new computation: + +| anchor | recorded by | recorded value | this package | +|---|---|---|---| +| `tied_min` one-copy L8 | [PR 2111](https://github.com/CrocSwap/integer-mult-bounds/pull/2111) by DreamingOfClouds (CP-SAT, CHECKED (recorded)) | 11 of 12 | 11 (engine witness, independently replayed) | +| `cex_min_1` one-copy L8 | [PR 2111](https://github.com/CrocSwap/integer-mult-bounds/pull/2111) by DreamingOfClouds | 18 of 19 | 18 (stored witness replayed) | +| chain engine on `cex_min_1` stored pairing | [PR 2111](https://github.com/CrocSwap/integer-mult-bounds/pull/2111) by DreamingOfClouds | 22 (`10+6+6`) | 22 (admissibility re-checked) | +| Lemma MP on `tied_min` | [PR 2747](https://github.com/CrocSwap/integer-mult-bounds/pull/2747) by Aaron Wang (navinor) | 9 (4096 pivot maps) | 9 (4096 maps, exhaustive) | +| Lemma MP on `cex_min_1` | [PR 2747](https://github.com/CrocSwap/integer-mult-bounds/pull/2747) by Aaron Wang | 16 (6144 pivot maps) | 16 (6144 maps, exhaustive) | +| `chi(Z)` of both fixtures | [PR 2774](https://github.com/CrocSwap/integer-mult-bounds/pull/2774) by Aaron Wang | 3 exactly (unconstrained) | 3 exactly (`tied_min` by subset DP; `cex_min_1` 3-dichromatic with a mutual-zero triangle forcing 3) | +| `MAS(Z)`, mutual clique | [PR 2774](https://github.com/CrocSwap/integer-mult-bounds/pull/2774) by Aaron Wang | 4 / 10 and 3 / 3 | 4 / 10 and 3 / 3 | +| anchor reach `S_gamma` | [PR 2869](https://github.com/CrocSwap/integer-mult-bounds/pull/2869) by Aaron Wang | 0 of 12 and 8 of 19 (= `anchor_good`) | 0 of 12 and 8 of 19 | + +## PROVEN: what any chi(Z) >= 4 instance must look like + +Lemma RK (PR 2717, cited not restated): `G_0` has no `K_4`; `Z` contains no +transitive 4-tournament; every zero pair landing in a block has +`|pi(t) intersect sigma(s)| >= 2`. + +> **Lemma C1 (reduction to the underlying graph).** If `chi(Z) >= 4` then +> `chi(U(Z)) >= 4`. + +*Proof.* A proper colouring of `U(Z)` makes every class arc-free, hence +acyclic. So `chi(Z) <= chi(U(Z))`. QED + +> **Lemma C2 (small v).** `chi(Z) <= 3` for every rank-3 zero digraph with +> `v <= 4`; any `chi(Z) >= 4` instance has `v >= 5`. + +*Proof.* `v <= 3` is trivial (all-singletons). For `v = 4`, if `chi(Z) >= 4` +then every partition into 3 classes fails; partitions of type (2,1,1) exist for +every choice of pair, and a 2-vertex class contains a directed cycle iff it is +a digon. So every pair would be a digon and `G_0 = K_4`, contradicting Lemma +RK (a). QED + +> **Lemma C3 (neighbourhood spans).** For every line `t`, the vectors +> `{p(s) : s in N_{G_0}(t)}` span at most 2 dimensions, and so do +> `{q(s) : s in N_{G_0}(t)}`. + +*Proof.* Mutual zero gives `p(s) . q(t) = 0` for all `s` in the neighbourhood, +and `q(t) != 0`; dually `q(s) . p(t) = 0`. QED + +> **Lemma C5 (two-plane classification of G_0 neighbourhoods).** For every +> line `t` with `N = N_{G_0}(t)`: if `p(t)` is not parallel to `q(t)` then +> `G_0[N]` is empty; if `p(t)` is parallel to `q(t)` then `G_0[N]` is a +> disjoint union of cliques of size at most 3 and complete bipartite graphs. In +> particular `G_0[N]` contains no odd cycle of length >= 5. + +*Proof.* All `p(s)`, `s in N`, lie in the plane `q(t)^perp`; all `q(s)` in +`p(t)^perp`. In the non-parallel case choose coordinates `q(t) = e_1`, +`p(t) = e_2`: then `p(s) = (0, y_s, z_s)`, `q(s) = (x_s, 0, w_s)`, so +`p(s) . q(r) = z_s w_r`; a mutual edge needs `z_s w_r = z_r w_s = 0`, while the +diagonal `M_ss = z_s w_s != 0` forces all `z_s, w_s` nonzero - no mutual edges. +In the parallel case both factors lie in one plane, say `R^2` with rotation +`R90`. Mutual edge `{s,r}` iff `q(r)` is parallel to `R90 p(s)` and `q(s)` is +parallel to `R90 p(r)`; writing `x_s = direction(p(s))`, `y_s = +direction(R90^{-1} q(s))` this reads `y_r = x_s and y_s = x_r`, i.e. vertices +are grouped by their ordered pair `(x, y)` and edges run only between groups +`(a, b)` and `(b, a)` (complete bipartite), or inside a group with `a = b` +(clique; size <= 3 by Lemma RK (a)). QED + +> **Lemma C4 (no odd wheels).** `G_0` contains no `W_{2k+1}` (an odd cycle with +> a vertex adjacent to all of it) as a subgraph; in particular no vertex is +> adjacent in `G_0` to every vertex of a 5-cycle. + +*Proof.* The cycle vertices would all lie in `N(t)`, and Lemma C5 excludes odd +cycles of length >= 5 inside `G_0[N(t)]`. QED + +> **Lemma C6 (basis-pivot families are tripartite).** If there is a basis +> `e_1, e_2, e_3` and a map `f : [v] -> {1,2,3}` with every `q(t)` parallel to +> `e_{f(t)}`, then `chi(Z) <= 3` (colour by `f`). + +*Proof.* Within one class `f = a`, an arc `t -> s` needs `M_ts = 0`, i.e. +`p(t)[a] = 0` (up to the nonzero scalar of `q(s)`), but the diagonal `M_tt != 0` +gives `p(t)[a] != 0`. So no arc lies inside a class. QED + +None of C1-C6 proves `chi(Z) <= 3` in general; together they constrain any +future `chi(Z) >= 4` instance to `v >= 5`, `chi(U) >= 4` (by C1), with all +digon structure odd-wheel-free and planar-classified per neighbourhood, and +outside every basis-pivot family. + +## The separation example: chi(U) = 4 while chi(Z) = 2 - CHECKED (hand example) + +Six lines with `p = [(1,1,0), (0,1,1), (1,0,1), (1,1,0), (1,1,1), (0,0,1)]`, +`q = [(1,0,0), (0,1,0), (1,0,0), (0,1,0), (0,0,1), (1,0,-1)]` (control 8 of +`verify.py`, all entries hand-checkable). The underlying graph `U(Z)` is the +5-wheel `W_5` (10 edges), so `chi(U(Z)) = 4`; yet `Z` has dichromatic number +exactly 2 (the digon `{2,5}` forces 2; the classes `{0,2,3}` and `{1,4,5}` are +acyclic), the matched-pivot value is `6 = v` and exact `cert(M) = 6 = v`. So a +4-chromatic underlying graph does **not** force `chi(Z) >= 4`: the dichromatic +question is about cycle-forcing orientations, and this instance is a member of +the basis-pivot family of Lemma C6. + +## Search for the smallest chi(Z) >= 4 instance - CHECKED (scoped negative) + +Smallest falsifying instance first (`v` ascending), exact `chi` by subset DP, +one bounded pivot maximum per route, early kill with the exact obstruction +recorded. Declared domains and outcomes: + +| route | domain / budget | outcome | exact obstruction record | +|---|---|---|---| +| random symmetric / asymmetric boxes | `v = 3..11`, entries `{-2..2}`, seeded | 0 instances with `chi(Z) >= 4`; max `chi(Z) = 3` (C5-seeded) | n/a (no candidate) | +| mutual-dense rejection sampling | `v = 3..11`, >= `v` digons required | same | n/a | +| C5-perpendicularity-seeded extension | `v = 3..11` | `chi(Z) = 3` reachable (the hand C5 control), never 4 | n/a | +| sequential linear construction of the Grötzsch graph as `G_0` (registered) | 3 trials x 60000 nodes | no solution; deepest placements 6, 8, 6 of 11 vertices | node cap hit after backtracking; per-vertex linear nullspaces collapse to rank 3 or sample exhaustion at the deepest cut | +| sequential construction (dev-run, `evidence/SEARCH-LOG.md`) | 12 trials x 200000 nodes | no solution; deepest <= 8 of 11 | same failure mode | +| annealing CSP on the Grötzsch incidence system (dev-run) | 25 restarts x 4000 steps | stalls at 12 constraint violations | no zero-violation configuration found | +| hill-climbs on exact `chi(Z)` (dev-run) | `v = 6..12`, symmetric and asymmetric | max `chi(Z) = 3` from structured seeds, 2 from random starts | n/a (no candidate above 3) | + +The Grötzsch graph (11 vertices, triangle-free, 4-chromatic) is the smallest +triangle-free 4-chromatic graph and the smallest 4-chromatic target not already +excluded by Lemma C4 (odd wheels) or Lemma RK (a) (`K_4`). The sequential +constructor places vertices in degree order and solves the mutual-incidence +constraints `p_i . q_j = 0` exactly as linear nullspaces; its failure is +recorded as a budgeted obstruction, **not** an unrealizability proof. + +Predecessor search context (recorded, cited): PR 2774's 286-instance census +(`v = 3..12`, four families) found `chi(Z) >= 4` on 0 instances (286/286 +decided 3-dichromatic); this package does not repeat that census. + +## Settlement of every instance examined - CHECKED + +| instance | v | `floor(2v/3)` | `chi(Z)` | `chi(U)` | `chi(G_0)` | MP | anchor reach | cert | F-star | +|---|---:|---:|---:|---:|---:|---:|---:|---:|---| +| `tied_min` | 12 | 8 | 3 | 3 | 3 | 9 | 0 of 12 | witness 11 (recorded max 11) | holds | +| `cex_min_1` | 19 | 12 | 3 (<= 3 decided, mutual triangle) | <= 3 | 3 | 16 | 8 of 19 | witness 18 (recorded max 18) | holds | +| separation example | 6 | 4 | 2 | 4 | 2 | 6 | 6 of 6 | exact 6 | holds | +| 22 searched instances | 3..11 | - | <= 3 (max 3) | <= 3 | <= 3 | = `v` on all 22 | - | >= `v` via Lemma MP | holds | + +The fixtures remain non-3-dichromatic **under `D(t)`** (`MP < v`) even though +`chi(Z) = 3`, and both carry certificates above threshold through general +labellings beyond matched pivots (11 > 9, 18 > 16) - exactly the PR 2774/2747 +picture. Note also that the anchor reach is a valuation quantity (Lemma SG, PR +2869) and is independent of `chi(Z)`: no dichromatic fact alone can falsify +F-star, which is a statement about `cert(M)`. + +## The verdict on the chi(Z) >= 4 case + +**Not realized in any declared domain; not proved vacuous.** CHECKED evidence: +the smallest-first search across four generator families, the sequential +construction of the smallest 4-chromatic mutual-zero target, and the recorded +predecessor census produce zero `chi(Z) >= 4` instances; the maximum attainable +in every route is 3 (attained). PROVEN constraints: any instance must have +`v >= 5`, `chi(U) >= 4`, odd-wheel-free and planar-classified digon +neighbourhoods (C4/C5), and lie outside every basis-pivot family (C6). The +separation example shows the `U`-level can reach 4-chromaticity at rank 3 while +`chi(Z) = 2`, so the obstruction, if it exists, is genuinely about cyclic arc +structure and not about the underlying graph. On every instance examined, F-star +holds (`cert = v` via matched pivots on the searched ones; 11/8 and 18/12 on the +fixtures), so the residue (ii) obstruction remains what PR 2774 recorded on the +fixtures: the pivot constraints `D(t)` and the labelling structure, not the +digraph coloring. The `chi(Z) >= 4` branch of the residue is therefore +**reducible to a concrete construction question** (realize a 4-chromatic cyclic +zero digraph at rank 3, or prove `chi(Z) <= 3` from C1-C6 plus the rank +constraints), with no F-star falsifier in sight. + +## What is proved, what is witnessed, what is demoted + +- **PROVEN:** Lemma C1, C2, C3, C4, C5, C6 above, each with its exact + hypothesis and written proof; and the separation example's `chi(U) = 4` / + `chi(Z) = 2` / `cert = 6` values (hand-checkable entries, machine-checked). +- **CHECKED (machine, `verify.py`, stdlib, deterministic, certificate digest + `032e7239429ba1f8`, about 12 s):** controls 8/8 (brute-force-over-all-labellings + agreement 3/3 at `v = 3`, diagonal decoder `cert = 3`/`MP = 3`/`chi = 3`, + corrupted-witness rejection 2/2, dichromatic hand values 4/4, the hand C5 + perpendicularity instance `chi(Z) = 3`, the efficient1700 retained rank-2 + pivot counterexample reproduced exactly (ordinary `chi = 2 <= 3`, MP `1 < 2 = + v`), the `M = 2 I_3` anchor control, and the separation example); the + calibration table above (every recorded anchor reproduced); and the + smallest-first search with exact `chi`, exact MP values, replayed witnesses + and the sequential Grötzsch obstruction record. +- **DEMOTED / OPEN:** `chi(Z) <= 3` for all rank-3 zero digraphs is **not** + proved; the search is bounded in `v` (<= 11 for exact `chi`, 12 in dev-run + hill-climbs) and in construction budgets (60000-200000 nodes), and a failed + construction is not an unrealizability proof. F-star for general rational + decoders is neither proved nor refuted. No "exactly when" or necessity claim + is made for any lemma hypothesis. The matched-pivot floor is witnessed on the + searched instances and both fixtures, not proved. Chain costs and engine + witnesses are bounded-search quantities; the recorded fixture limits 11/18 + rest on PR 2111's recorded CP-SAT optimality, not re-verified here. + +## Open next questions + +1. **Is `chi(Z) <= 3` forced at rank 3?** Either realize the smallest 4-chromatic + cyclic zero digraph (v >= 5, outside basis-pivot families; e.g. an exhaustive + pattern search at v = 5..6 with exact rank-3 realization tests), or prove + `chi(Z) <= 3` from the C1-C6 constraints plus Lemma RK. Why it matters: it + either deletes the digraph-coloring half of residue (ii) or names the exact + obstruction a class-(ii) proof must overcome. Blocker: no structural + contradiction found and no fixture found in the bounded search. +2. **Would `chi(Z) >= 4` even falsify F-star?** On any future fixture compute + anchor reach, matched-pivot value and exact cert (the `settle()` machinery of + `verify.py` reports exactly these). The separation example and both fixtures + indicate certificates survive coloring obstructions. Blocker: no `chi(Z) >= 4` + fixture is known. + +## Reproduce + +Python 3.10+, standard library only, from the repository root: + +```sh +python3 -B research/fstar-chi4-zero-digraph-seed73765f29/verify.py +python3 scripts/research_package.py --package research/fstar-chi4-zero-digraph-seed73765f29 --check-only +python3.12 scripts/research_package.py --package research/fstar-chi4-zero-digraph-seed73765f29 +``` + +Expected markers: `PASS_FC4_CONTROLS`, `PASS_FC4_CALIBRATION`, `PASS_FC4_SEARCH`, +`PASS_FSTAR_CHI4_ZERO_DIGRAPHS`, and `CERTIFICATE.json` with digest +`032e7239429ba1f8` (about 12 s on the authoring host). `make` is not installed +on the authoring host; the commands above are the underlying ones. + +## Credit and provenance + +F-star, the `cert(M)` definition, L8 labellings and the proven chain +`cost >= sum_j r_j >= cert(M)` are from the merged +`research/root-unit-decoder-lemmas` +([PR 1590](https://github.com/CrocSwap/integer-mult-bounds/pull/1590) by +DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance). +The rank-3 configuration model, the named instances `tied_min` and `cex_min_1`, +their recorded one-copy certificate limits (11 and 18, CP-SAT, CHECKED +(recorded)), the stored cost-22 pairing `data/cex_min_1.B22.json` and the +structural lemmas L5/SCC are DreamingOfClouds' work in +[PR 2111](https://github.com/CrocSwap/integer-mult-bounds/pull/2111) and +[PR 2162](https://github.com/CrocSwap/integer-mult-bounds/pull/2162); +`data/tied_min.json`, `data/cex_min_1.json`, `data/cex_min_1.B22.json` and +`data/cex_min_1.witness.json` are byte-identical copies of their data files +(sha256 `670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93`, +`86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7`, +`15f5039069a175831f92c4ffe023a23a6f6e6bd6665f0ca2c2734bbe672b51ef`, +`153f4d2e8dc262f547a91f2daff9724cab88beb4d45c399497efc68a8ed2c933`). The +residue statement, Lemmas SF/MP/RK/AN and the exact-completion engine design +this package adapts are Aaron Wang's work in +[PR 2717](https://github.com/CrocSwap/integer-mult-bounds/pull/2717); Lemma MX +and the class-(i) closure are Aaron Wang's +[PR 2747](https://github.com/CrocSwap/integer-mult-bounds/pull/2747); the +fixture dichromatic structure, the zero-digraph machinery and the chi(Z) >= 4 +question are Aaron Wang's +[PR 2774](https://github.com/CrocSwap/integer-mult-bounds/pull/2774); Lemmas +SC/SG, the class-(iii) collapse and the residue rename are Aaron Wang's +[PR 2869](https://github.com/CrocSwap/integer-mult-bounds/pull/2869); the +falsifier census frontier (196 instances) is Aaron Wang's +[PR 2335](https://github.com/CrocSwap/integer-mult-bounds/pull/2335); the +exact cost 12 of `tied_min` is Aaron Wang's +[PR 2379](https://github.com/CrocSwap/integer-mult-bounds/pull/2379); the exact +cost 21 of `cex_min_1` is Nick Petalas' +[PR 2206](https://github.com/CrocSwap/integer-mult-bounds/pull/2206). The +maintainer review and its retained rank-2 pivot counterexample are the +community audit in `research/community-efficient1700-audit`. This package does +not claim their results; the new content is the PROVEN structural lemmas +C1-C6 with proofs, the chi(U) = 4 / chi(Z) = 2 separation example, the fresh +engine reproducing every anchor, and the bounded chi(Z) >= 4 search with its +per-route obstruction records. + +Prepared by **Aaron Wang** with help from opencode (substantial AI assistance; +no independent human review claimed). New work in this package is Apache-2.0. diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/SOURCES.json b/research/fstar-chi4-zero-digraph-seed73765f29/SOURCES.json new file mode 100644 index 0000000000..4706275d7b --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "066766afb181a421eb851b8d73bb0ba71a78a170", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/root-unit-decoder-lemmas/README.md", + "usage": "input", + "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb", + "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9" + }, + { + "path": "research/community-efficient1700-audit/checks/check-2717-pivot-counterexample.json", + "usage": "input", + "git_blob": "72b3f1d774357f51596ca02087a9332cd0b0af5c", + "sha256": "603e91f178a870dd68de492b44934641dfd1aca9aee7cf8eadcedc7fe96ff839" + } + ] +} diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/TASK-CARD.md b/research/fstar-chi4-zero-digraph-seed73765f29/TASK-CARD.md new file mode 100644 index 0000000000..c04a09be94 --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/TASK-CARD.md @@ -0,0 +1,116 @@ +# Task card - KB5e: the chi(Z) >= 4 case of F-star residue (ii) + +Task ID / proposed scope key: kappa-blocker KB5e (explicit open request from +https://github.com/CrocSwap/integer-mult-bounds/discussions/1166); chooser draw +seed `73765f295ddd17bbb472f87c2beac209`, track `recursive-interfaces` +(suggestions: centre-path-sharing, connector-alphabet-change, +joint-query-controller). Scope changed from the drawn cards per the assignment. + +Base commit: `066766afb181a421eb851b8d73bb0ba71a78a170` (assignment pin). +Predecessor heads at card time (to be re-verified at submission): +PR 2717 `7aed56bd440a3d8cbca8028cf2cbd0888c07d9b3`, +PR 2747 `a2bab9978c8149dc5965558ea9277da07bc750e7`, +PR 2774 `ceaf5acf976cee2f70a680f2d513f12baa634870`, +PR 2869 `153b93c1c0e9ee1c50677ae04d48f1f7f0b1700e`. +Frozen pins of DreamingOfClouds' fixture data (sha256 +`670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93` for +`tied_min.json`, `86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7` +for `cex_min_1.json`) stay immutable. + +Concrete object and question: for exact 3-total rational decoders +`M = sum_{j=1..3} p_j q_j^T` on `v` lines (`M_tt != 0`), the zero digraph +`Z = {(t,s) : t != s, M_ts = 0}` and its dichromatic number `chi(Z)`. +PR 2774 proved both canonical fixtures have `chi(Z) = 3` exactly (unconstrained) +and left open (its open question 2, also PR 2717's open question 2): can a +rank-3 zero digraph have `chi(Z) >= 4` at all? Settle that case: (a) prove it +vacuous or reducible (e.g. `chi(Z) <= 3` forced by rank-3 structure, or +`chi(Z) >= 4` forces anchor/MX coverage of `floor(2v/3)`), or (b) isolate a +minimal `chi(Z) >= 4` fixture and settle F-star on it (exact cert vs +`floor(2v/3)`, D(t)-pivot analysis), or (c) produce an F-star falsifier +(`cert(M) < floor(2v/3)`). + +Scope status: changed (authorized explicit open request). The chooser draw +landed on the standard catalogue cards; the assignment names the KB5e request +from discussion 1166 as the recorded reason. Pair-collision check before +computation (toolkit `disc-comments --grep`, discussions 1317 and 1166, +including nested replies, 2026-10-16 ~05:40-05:50 UTC) found no live claim on +this object: the last F-star activity is KB5d's DONE/RELEASED (PR 2869, +2026-10-16 05:38 UTC). Refined overlap re-run on the object's proper names +(zero digraph, dichromatic, chi(Z), pivot constraint, D(t), F-star, cert, +3-total decoder) found only the known predecessors (PRs 2717/2747/2774/2869, +PR 2335 census, PR 2111/2162 fixtures) and unrelated packages. + +Existing restriction being addressed: PR 2717's demoted residue (b) "zero +digraphs that are not 3-dichromatic (Lemma MP then gives only +sum_i MAS(Z[C_i]))" after PR 2869 renamed the residue classification to +(i') cancellation lines {t : v2(M_tt) > gamma} plus (ii) zero digraphs. Not a +restriction being relaxed. We keep the maintainer's reviewed distinction +(efficient1700 review of PR 2717/2774): ordinary 3-dichromaticity and +nonempty D(t) lists do NOT imply a D(t)-compatible acyclic partition (retained +rank-2 counterexample `check-2717-pivot-counterexample.json`); unconstrained +chi(Z) and D(t)-compatible dichromaticity are reported as separate quantities. + +Method; explicit parameter ranges: exact stdlib integer/F2 arithmetic. Engine +adapted from PR 2717/2747/2774 (Aaron Wang) on DreamingOfClouds' PR 2111 model. +Quantities per instance: Z, chi(Z) exact by subset DP (acyclic-subset DP + +min-partition DP), D(t)-compatible 3-dichromaticity (matched-pivot value +max_c sum_i MAS(Z[C_i]), exhaustive over pivot maps when the product of |D(t)| +admits), anchor reach |S_gamma| and cancellation-line count (Lemma SG, +PR 2869), exact cert(M) by exhaustive a-enumeration + exact b-completion DP +where feasible, engine witness + independent replay otherwise, bounded +admissible-B chain scan as falsifier criterion (chain cost >= cert is proven). +Generators aimed at the chi question: symmetric perpendicularity point sets +(M = P P^T, Z = digons of the orthogonality graph of {p(t)} in Q^3), +one-sided asymmetric sets (M = P Q^T), odd-cycle-seeded and Mycielski-biased +mutual-zero patterns, plus small-integer random boxes. Smallest-first: +v ascending; smallest falsifying instance first; one bounded pivot maximum; +early kill with the exact obstruction recorded. + +Nearest overlapping PRs and why this adds something: PR 2774 (Aaron Wang) +computes chi(Z) of the two fixtures (= 3 exactly) and explicitly leaves "can +chi(Z) >= 4 happen at rank 3?" open (its open question 2); this package answers +that question over a declared domain and settles F-star on any fixture found. +PR 2717 (Aaron Wang) names the residue and proves Lemmas SF/MP/RK/AN; PR 2747 +(Aaron Wang) proves Lemma MX and closes class (i) on the fixtures; PR 2869 +(Aaron Wang) collapses class (iii) and renames the residue. PR 2335 (Aaron +Wang) is the 196-instance falsifier census (v = 4..12), whose generators were +not aimed at chi(Z); its domain is not repeated as a census. The efficient1700 +maintainer review (check-2717-pivot-counterexample) constrains every claim +about D(t)-compatible partitions; we do not restate the demoted inferences. + +Declared milestone: local module (scoped residue result / obstruction record); +no supplier, no kappa, no frontier change. + +Optimistic full cost budget; required observable improvement: no kappa in +play; the price is one bounded deterministic stdlib run (registered verify +below 600 s) plus written analysis. + +Unresolved consumer/restoration costs; family expansion decision: none +(missing-lemma work, not a construction); no expansion round follows. + +Success evidence; falsification test; time/compute cap: PASS markers from +verify.py plus README analysis: recorded anchors reproduced first (PR 2717: +tied_min 11/12, cex_min_1 18/19, chain 22; PR 2747: MP/MX 9 and 16; PR 2774: +chi(Z) = 3 unconstrained on both fixtures yet non-3-dichromatic under D(t); +PR 2869: reach = anchor_good on both fixtures, 84-instance search 0 +falsifiers); then the chi(Z) >= 4 verdict with exact evidence per instance. +Falsifier test: explicit admissible B with sum_j rank_F2 B[R_j,A_j] < +floor(2v/3), or exact cert < floor(2v/3) where exhaustive; corrupted witnesses +must fail the independent checker. Cap: one session, single-process stdlib +Python 3.12, registered verify command below 600 s. + +Predecessor authors; intended artifact and reproduction command: F-star, +cert(M), L8 labellings and the proven chain cost >= sum_j r_j >= cert(M): +DreamingOfClouds (with Claude Opus 5.5 (Anthropic) via Claude Code assistance), +PR 1590. Fixtures tied_min/cex_min_1, their recorded one-copy limits 11/18 +(CP-SAT, recorded) and the cost-22 pairing: DreamingOfClouds, PR 2111/2162. +Lemmas SF/MP/RK/AN and the residue: Aaron Wang, PR 2717. Lemma MX: Aaron Wang, +PR 2747. Fixture dichromatic structure and the zero-digraph machinery: Aaron +Wang, PR 2774. Lemmas SC/SG, class (iii) collapse, residue rename: Aaron Wang, +PR 2869. Exact cost 12 of tied_min: Aaron Wang, PR 2379; exact cost 21 of +cex_min_1: Nick Petalas, PR 2206. Artifact: +`research/fstar-chi4-zero-digraph-seed73765f29/` (TASK.json, SOURCES.json, +VERIFY.json, verify.py, data/, CERTIFICATE.json, README.md). Reproduce: +`python3 -B research/fstar-chi4-zero-digraph-seed73765f29/verify.py` then +`python3 scripts/research_package.py --package +research/fstar-chi4-zero-digraph-seed73765f29 --check-only`. diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/TASK.json b/research/fstar-chi4-zero-digraph-seed73765f29/TASK.json new file mode 100644 index 0000000000..f4ffadf9af --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 5, + "base_commit": "066766afb181a421eb851b8d73bb0ba71a78a170", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Removing copies without a replacement contract for the decoder's copied totals.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "changed", + "actual_scope": "Kappa-blocker KB5e (authorized explicit open request): settle the chi(Z) >= 4 case of residue class (ii) zero digraphs of open problem F-star of research/root-unit-decoder-lemmas section 7 (cert(M) >= floor(2v/3) for exact 3-total rational decoders), the question PR 2774 left as its open question 2 and PR 2717 as its open question 2 after PR 2869 renamed the residue to (i') cancellation lines {t : v2(M_tt) > gamma} plus (ii) zero digraphs. Three parts: (P1) PROVEN structural lemmas for the chi(Z) >= 4 case (chi(Z) >= 4 requires chi(U(Z)) >= 4; v >= 5; G_0 contains no odd wheel and every G_0 neighbourhood is empty or a union of cliques <= 3 and complete bipartite graphs; basis-pivot families are tripartite; an explicit rank-3 decoder with chi(U(Z)) = 4 but chi(Z) = 2 separates the underlying-graph question from the dichromatic one); (P2) exact calibration in a fresh engine reproducing every recorded anchor of PRs 2717/2747/2774/2869; (P3) a bounded, smallest-first search for the smallest chi(Z) >= 4 instance (random, symmetric, mutual-dense, C5-seeded generators; a sequential linear construction of the Gr\u00f6tzsch graph as a mutual-zero pattern; dev-run hill-climbs and annealing CSP) with the exact obstruction recorded per route, plus the D(t)-pivot/anchor settlement of every instance examined.", + "scope_change_reason": "Authorized 'explicit open request' scope change to kappa-blocker KB5e, recorded per the assignment. The chooser OS draw (seed 73765f295ddd17bbb472f87c2beac209, track recursive-interfaces) proposed centre-path-sharing, connector-alphabet-change and joint-query-controller; the assignment names the KB5e request of discussion 1166 as the recorded reason for taking the explicit request instead of the drawn cards. Pair-collision check before computation (toolkit disc-comments --grep on discussions 1317 and 1166 including nested replies, 2026-10-16 05:40-05:55 UTC) found no live claim on the chi(Z) >= 4 question: the last F-star activity is KB5d's DONE/RELEASED (PR 2869, 2026-10-16 05:38 UTC). Refined overlap re-run on the object's proper names (zero digraph, dichromatic, chi(Z), pivot constraint, D(t), F-star, cert, 3-total decoder) at 2026-10-16 05:47-05:49 UTC with complete pagination found only the known predecessors (PRs 2717/2747/2774/2869, PR 2335 census, PR 2111/2162 fixtures) and unrelated packages.", + "existing_restriction_being_changed": "Nothing is relaxed. The question addressed is PR 2774's open question 2 (can a rank-3 zero digraph have chi(Z) >= 4 at all?), left open after both canonical fixtures were computed at chi(Z) = 3 exactly. Every claim carries its exact status label; no 'exactly when', necessity or exhaustive-without-proof wording is used; unconstrained chi(Z), chi(U(Z)) and the D(t)-compatible dichromatic quantity are reported separately, per the efficient1700 maintainer review of PR 2717/2774 (ordinary 3-dichromaticity does not imply a D(t)-compatible acyclic partition; retained counterexample research/community-efficient1700-audit/checks/check-2717-pivot-counterexample.json is reproduced as a control).", + "method": "Exact stdlib integer/F2 arithmetic. Fresh engine (model, subset-DP acyclic/MAS tables, exact dichromatic number by min-partition subset DP, chi(U) and chi(G_0), matched-pivot value over all pivot maps, Lemma SG anchor reach, exact cert by exhaustive a-enumeration with exact b-completion DP, engine witnesses with independent replay, bounded admissible-B chain scan). PROVEN lemmas with written proofs in README.md; every computational claim recomputed by verify.py in one bounded deterministic run. Search: smallest-first v = 3..11, generators symmetric/asymmetric small-integer boxes, mutual-dense rejection sampling, C5-perpendicularity-seeded extension, and a sequential linear construction (exact nullspace per vertex, backtracking) targeting the Gr\u00f6tzsch graph as a mutual-zero pattern; dev-run hill-climbs and annealing CSP recorded in evidence/SEARCH-LOG.md.", + "parameter_ranges": "T = 3 totals exactly; rational decoders with nonzero diagonal, integer factorizations (entry-class-independent by PR 2869's Proposition). Fixtures: PR 2111's tied_min (v = 12) and cex_min_1 (v = 19), byte-identical data copies (sha256 670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93 and 86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7), the stored cost-22 pairing (sha256 15f5039069a175831f92c4ffe023a23a6f6e6bd6665f0ca2c2734bbe672b51ef) and the stored 18-witness (sha256 153f4d2e8dc262f547a91f2daff9724cab88beb4d45c399497efc68a8ed2c933). Search: v = 3..11, entries in {-2..2}, four generator families, deterministic seeds in CERTIFICATE.json; Gr\u00f6tzsch sequential probe: 3 trials x 60000 nodes in the registered run (12 dev-run trials x 200000 nodes recorded in evidence/SEARCH-LOG.md).", + "nearest_overlapping_prs": "https://github.com/CrocSwap/integer-mult-bounds/pull/2774 (Aaron Wang: exact chi(Z) = 3 on both fixtures, non-3-dichromatic under D(t), 286-instance search with 0 chi(Z) >= 4; its open question 2 is this package's question). https://github.com/CrocSwap/integer-mult-bounds/pull/2717 (Aaron Wang: Lemmas SF/MP/RK/AN, the residue statement, open question 2). https://github.com/CrocSwap/integer-mult-bounds/pull/2747 (Aaron Wang: Lemma MX, class (i) closure; open question 1 on the matched-pivot floor). https://github.com/CrocSwap/integer-mult-bounds/pull/2869 (Aaron Wang: Lemmas SC/SG, class (iii) collapse, residue rename). https://github.com/CrocSwap/integer-mult-bounds/pull/2335 (Aaron Wang: 196-instance falsifier census; domain not repeated). PRs 2111/2162 (DreamingOfClouds: fixtures, recorded certificate limits 11/18, cost-22 pairing) cited, not restated. The efficient1700 maintainer review constrains every D(t)-claim; its retained rank-2 counterexample is reproduced as control 6.", + "optimistic_full_cost_budget": "No kappa, supplier, word or moment budget is in play (missing-lemma work). The price is one bounded deterministic stdlib run (registered verify below 600 s; observed about 12 s) plus written analysis.", + "bottleneck_link": "F-star is the named route to closing every open T = 3 window at once (research/root-unit-decoder-lemmas section 7, consequence PROVEN given F-star). Residue (ii)'s digraph-coloring half is exactly the chi(Z) >= 4 question: if rank-3 zero digraphs can reach chi(Z) >= 4 the obstruction is not only in the pivot constraints D(t) (as PR 2774 found on the fixtures) but in the digraph itself, changing what a class-(ii) proof must overcome; if not, residue (ii) reduces to the D(t)-compatible question PR 2774 settled on the fixtures.", + "stop_rule": "Stop at the first exact falsifier (explicit admissible B with chain cost below floor(2v/3), or exact cert below threshold where exhaustive), or, absent one, at the declared search domain with the exact obstruction recorded per construction route. One bounded pivot maximum; early kill with the exact obstruction recorded. Compute cap: one session, single-process stdlib Python, the registered verify command below 600 s.", + "success_evidence": "PASS markers from verify.py (PASS_FC4_CONTROLS, PASS_FC4_CALIBRATION, PASS_FC4_SEARCH, PASS_FSTAR_CHI4_ZERO_DIGRAPHS) plus README.md analysis: controls 8/8 (including the maintainer's retained D(t) counterexample and the chi(U) = 4 / chi(Z) = 2 separation example); calibration reproducing every recorded anchor (PR 2717: tied_min 11/12, cex_min_1 18/19, chain 22; PR 2747: MP/MX 9 and 16 over 4096/6144 pivot maps; PR 2774: chi(Z) = 3 on both fixtures, MAS 4/10, omega 3; PR 2869: anchor reach 0/12 and 8/19 = anchor_good); the PROVEN lemmas with proofs; the bounded smallest-first chi(Z) >= 4 search with exact obstruction records; and the D(t)-pivot/anchor/cert settlement of every instance examined (MP = v on all 22 searched instances; exact cert = 6 = v on the separation example; witness 11/8 and 18/12 on the fixtures).", + "falsification_test": "An explicit admissible pairing B with cost(B) = sum_j rank_F2 B[R_j,A_j] < floor(2v/3) refutes F-star on that instance (the chain cost >= cert(M) is proven in research/root-unit-decoder-lemmas), as does exact cert < floor(2v/3) where exhaustive a-enumeration terminates; corrupted witnesses must fail the independent replay checker.", + "time_compute_cap": "One session; single-process stdlib Python; no SAT solver, no third-party packages; the registered verify command below 600 s (observed about 12 s on the authoring host); package registered with timeout_seconds 600.", + "predecessor_authors": "F-star, the cert(M) definition, L8 labellings and the proven chain cost >= sum_j r_j >= cert(M): research/root-unit-decoder-lemmas, PR 1590 by DreamingOfClouds (with Claude Opus 5.5 (Anthropic) via Claude Code assistance). The rank-3 configuration model, the named instances tied_min and cex_min_1, their recorded one-copy certificate limits (11 and 18, CP-SAT) and the stored cost-22 pairing: DreamingOfClouds, PR 2111 and PR 2162. Lemmas SF/MP/RK/AN, the residue statement and the engine design this package adapts: Aaron Wang, PR 2717. Lemma MX and the class-(i) closure: Aaron Wang, PR 2747. The fixture dichromatic structure and zero-digraph machinery: Aaron Wang, PR 2774. Lemmas SC/SG, the class-(iii) collapse and the residue rename: Aaron Wang, PR 2869. The falsifier census frontier: Aaron Wang, PR 2335. Exact cost 12 of tied_min: Aaron Wang, PR 2379. Exact cost 21 of cex_min_1: Nick Petalas, PR 2206. The maintainer review and retained pivot counterexample: research/community-efficient1700-audit (community review).", + "intended_artifact": "research/fstar-chi4-zero-digraph-seed73765f29/ with TASK.json, SOURCES.json pins, VERIFY.json, verify.py, data/ (byte-identical fixture copies, the stored cost-22 pairing and 18-witness, sha256 recorded), evidence/SEARCH-LOG.md (dev-run records), CERTIFICATE.json (written by verify.py) and README.md; reproduction: python3 -B research/fstar-chi4-zero-digraph-seed73765f29/verify.py then python3 scripts/research_package.py --package research/fstar-chi4-zero-digraph-seed73765f29 --check-only.", + "outcome": "completed", + "evidence": "THE CHI(Z) >= 4 CASE OF RESIDUE (ii) ATTACKED DIRECTLY: NOT REALIZED IN THE DECLARED DOMAIN, WITH EXACT OBSTRUCTIONS RECORDED PER ROUTE; F-STAR NOT PROVED AND NOT REFUTED. PROVEN (README.md, written proofs): chi(Z) >= 4 requires chi(U(Z)) >= 4; chi(Z) <= 3 for v <= 4 (Lemma RK(a)); every G_0 neighbourhood spans at most 2 dimensions on each side; G_0 contains no odd wheel and G_0[N(t)] is empty (p(t) not parallel to q(t)) or a disjoint union of cliques of size <= 3 and complete bipartite graphs (two-plane classification); basis-pivot families q(t) parallel to basis vectors give tripartite Z (chi(Z) <= 3); and an explicit rank-3 decoder (6 lines) with chi(U(Z)) = 4 (underlying W5) but chi(Z) = 2, exact cert = 6 = v, separating the underlying-graph question from the dichromatic one. CHECKED (verify.py, stdlib, deterministic, certificate digest 032e7239429ba1f8, about 12 s): controls 8/8 including the efficient1700 retained rank-2 pivot counterexample (ordinary chi = 2 <= 3, matched-pivot value 1 < 2 = v); calibration reproduces every recorded anchor (tied_min 11/12 with MP 9 over 4096 pivot maps, chi(Z) = 3 exactly, MAS(Z) = 4, omega(mutual) = 3, anchor reach 0/12; cex_min_1 18/19 with MP 16 over 6144 pivot maps, MAS(Z) = 10, anchor reach 8/19; chain engine 22 on the stored pairing); smallest-first search 22 instances v = 3..11 (symmetric/asymmetric/mutual-dense/C5-seeded), max chi(Z) = 3 (C5-seeded), chi(Z) >= 4 found on 0, matched-pivot value = v on all 22 (so cert = v there); Gr\u00f6tzsch-as-mutual-zero sequential probe 3 x 60000 nodes, deepest placements 6, 8, 6 of 11 vertices, node cap hit (no solution; not an unrealizability proof); dev-run records in evidence/SEARCH-LOG.md (12 x 200000-node sequential trials all fail with deepest <= 8; annealing CSP stalls at 12 violations; hill-climbs v = 6..12 find max chi = 3). DEMOTED / OPEN: chi(Z) <= 3 for all rank-3 zero digraphs is NOT proved; the search is bounded in v and in construction budgets; chi(Z) >= 4 is not shown impossible. No 'exactly when' or necessity claim; chain values are bounded-search upper bounds; the recorded fixture limits 11/18 rest on PR 2111's recorded CP-SAT optimality, not re-verified here. F-star itself holds on every instance examined (fixtures 11 >= 8 and 18 >= 12; search instances cert = v via matched pivots) and remains open in general.", + "author": "Aaron Wang (with help from opencode)", + "ai_assistance": "Substantial AI assistance: this package was produced by Aaron Wang with help from opencode (opencode agent harness). No independent human review claimed. No model is cited per orchestrator attribution rules.", + "open_questions": [ + { + "question": "Is chi(Z) <= 3 forced for every rank-3 zero digraph with nonzero diagonal? Equivalently: can chi(Z) >= 4 happen at rank 3 at all?", + "why_it_matters": "If forced, residue (ii) reduces entirely to the D(t)-compatible question PR 2774 settled on the fixtures, and the digraph-coloring half of the residue disappears. If not, the minimal fixture would name the obstruction a class-(ii) proof must overcome beyond the pivot constraints.", + "first_step": "Exhaustive pattern search at v = 5..6 over all realizable (pi, sigma, Z) with exact rank-3 realization tests (determinantal constraints), or a proof that the two-plane neighbourhood classification plus Lemma RK force a 3-colouring.", + "blocked_by": "No structural contradiction found; the sequential linear construction of the smallest triangle-free 4-chromatic target stalls at 6-8 of 11 vertices under 60000-200000 node budgets, which is not a proof." + }, + { + "question": "Does chi(Z) >= 4 (if realizable) force cert(M) < floor(2v/3), or can anchor/MX labellings still certify?", + "why_it_matters": "It separates a combinatorial digraph obstruction from an actual F-star falsifier. The chi(U) = 4 / chi(Z) = 2 separation example shows the underlying graph alone never decides cert; the fixtures show chi(Z) = 3 with cert = v.", + "first_step": "On any future chi(Z) >= 4 fixture, compute anchor reach |S_gamma|, matched-pivot value and exact cert where a-enumeration terminates; the settlement machinery of verify.py (settle()) already reports exactly these quantities.", + "blocked_by": "No chi(Z) >= 4 fixture is known." + } + ] +} diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/VERIFY.json b/research/fstar-chi4-zero-digraph-seed73765f29/VERIFY.json new file mode 100644 index 0000000000..679c445a4e --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/root-unit-decoder-lemmas/README.md", + "research/community-efficient1700-audit/checks/check-2717-pivot-counterexample.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "KB5e chi(Z) >= 4 package: controls 8/8 (brute-force-over-all-labellings agreement at v = 3, diagonal decoder cert = 3 / MP = 3 / chi = 3, corrupted-witness rejection 2/2, dichromatic hand values 4/4, C5 perpendicularity chi(Z) = 3, the efficient1700 retained rank-2 pivot counterexample with MP = 1 < 2 = v, M = 2 I_3 anchor reach 3, and the W5-underlying separation example chi(U) = 4 / chi(Z) = 2); fixture calibration reproducing PR 2717 anchors (tied_min witness 11/12, cex_min_1 stored witness 18/19, chain engine 22 on the stored pairing), PR 2747 anchors (MP 9 and 16 exhaustive over 4096 / 6144 pivot maps), PR 2774 anchors (chi(Z) = 3 exactly on tied_min, 3-dichromatic with mutual triangle on cex_min_1, MAS(Z) = 4 / 10, omega(mutual) = 3) and PR 2869 anchors (anchor reach 0/12 and 8/19 = anchor_good); the smallest-first chi(Z) >= 4 search (v = 3..11, symmetric/asymmetric/mutual-dense/C5-seeded families, exact chi by subset DP) and the Gr\u00f6tzsch-as-mutual-zero sequential probe with its failure record; settlement of the separation example (exact cert = 6 = v); prints PASS_FC4_CONTROLS, PASS_FC4_CALIBRATION, PASS_FC4_SEARCH, PASS_FSTAR_CHI4_ZERO_DIGRAPHS and writes CERTIFICATE.json" + } + ] +} diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.B22.json b/research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.B22.json new file mode 100644 index 0000000000..0161536922 --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.B22.json @@ -0,0 +1 @@ +[[1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0], [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0], [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0], [0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0], [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]] \ No newline at end of file diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.json b/research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.json new file mode 100644 index 0000000000..4629aa02b1 --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.json @@ -0,0 +1 @@ +[[[1, -1, 0], [1, 0, -1]], [[1, -1, 1], [0, 1, -1]], [[1, -1, 1], [1, -1, 0]], [[1, -1, 1], [1, 0, 1]], [[1, 0, -1], [0, 1, -1]], [[1, 0, -1], [0, 1, 1]], [[1, 0, -1], [1, -1, 0]], [[1, 0, -1], [1, 1, -1]], [[1, 0, 1], [1, 1, 0]], [[1, 0, 1], [1, 1, 1]], [[1, 1, -1], [0, 1, -1]], [[1, 1, -1], [1, -1, 1]], [[1, 1, -1], [1, 0, -1]], [[1, 1, -1], [1, 1, 0]], [[1, 1, 0], [0, 1, 1]], [[1, 1, 0], [1, 0, 1]], [[1, 1, 1], [0, 1, 1]], [[1, 1, 1], [1, 0, 1]], [[1, 1, 1], [1, 1, 0]]] \ No newline at end of file diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.witness.json b/research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.witness.json new file mode 100644 index 0000000000..602d784e98 --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/data/cex_min_1.witness.json @@ -0,0 +1 @@ +{"a": [3, 2, 2, 4, 4, 5, 5, 4, 1, 1, 2, 7, 5, 1, 2, 3, 6, 1, 1], "b": [1, 6, 0, 5, 6, 6, 1, 4, 3, 7, 6, 2, 1, 3, 6, 5, 2, 5, 3], "order": [16, 6, 11, 14, 5, 12, 0, 18, 17, 15, 3, 13, 10, 9, 8, 7, 4, 1], "kept": [16, 6, 11, 14, 5, 12, 0, 18, 17, 15, 3, 13, 10, 9, 8, 7, 4, 1]} \ No newline at end of file diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/data/tied_min.json b/research/fstar-chi4-zero-digraph-seed73765f29/data/tied_min.json new file mode 100644 index 0000000000..ae11f01fab --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/data/tied_min.json @@ -0,0 +1 @@ +[[[1, -1, -1], [0, 1, 1]], [[1, -1, -1], [1, -1, 0]], [[1, -1, -1], [1, 0, -1]], [[1, -1, 1], [0, 1, -1]], [[1, -1, 1], [1, -1, 0]], [[1, -1, 1], [1, 0, 1]], [[1, 1, -1], [0, 1, -1]], [[1, 1, -1], [1, 0, -1]], [[1, 1, -1], [1, 1, 0]], [[1, 1, 1], [0, 1, 1]], [[1, 1, 1], [1, 0, 1]], [[1, 1, 1], [1, 1, 0]]] \ No newline at end of file diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/evidence/SEARCH-LOG.md b/research/fstar-chi4-zero-digraph-seed73765f29/evidence/SEARCH-LOG.md new file mode 100644 index 0000000000..964894bc34 --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/evidence/SEARCH-LOG.md @@ -0,0 +1,57 @@ +# Dev-run search log (chi(Z) >= 4 campaign, 2026-10-16) + +Scratch drivers (`%TEMP%\opencode\agent-69\search_chi4.py`, +`search_chi4_b.py`) run against the same engine functions as `verify.py` +(imported from `research/fstar-chi4-zero-digraph-seed73765f29/verify.py`). +These runs are the recorded development evidence behind the README's search +table; the registered, deterministic replay is `verify.py` (which embeds the +smaller declared domain and the 3 x 60000-node Grötzsch probe). + +## Round 1: annealing CSP on the Grötzsch incidence system + +Target: realize the Grötzsch graph M(C5) (11 vertices, triangle-free, +4-chromatic) as a mutual-zero pattern: variables `p_i, q_i` in `{-3..3}^3`, +hard constraints `p_i . q_i != 0` (diagonal), `p_i . q_j = 0 = p_j . q_i` +(edges), non-edges nonzero in at least one direction. 25 restarts x 4000 +simulated-annealing steps. + +- best violation counts per improving restart: 15, 14, 12 +- no zero-violation configuration found; the run then hit a scratch bug + (evaluation on an invalid decoder) and was superseded by round 2. + +## Round 2: sequential linear construction (exact nullspaces) + +Place vertices in degree order; at each step solve `p_i _|_ q_j` (and +`q_i _|_ p_j`) for already placed edge neighbours as an exact linear nullspace +(Fraction arithmetic), sample a generic integer point in the solution +subspace, backtrack on non-edge/diagonal violations. Node budget 200000 per +trial, 12 trials with random restarts. + +- 12/12 trials: no solution. +- deepest placements observed: 6-8 of 11 vertices. +- failure mode at the deepest cut: the per-vertex nullspace collapses to rank + 3 (only the zero vector) for a high-degree vertex, or the 24 candidate + samples all violate a non-edge constraint; the search then backtracks and + exhausts the node budget. + +## Round 2b: direct hill-climbs on exact chi(Z) + +Mutations of one integer entry of `P` or `Q`; objective the exact pair +`(chi(Z), chi(G_0))` by subset DP; greedy non-decreasing acceptance; +deterministic seeds. + +- `v = 6..9` from random starts (3 restarts x 80 steps, box `{-3..3}`): best + `chi(Z) = 2`, `chi(G_0) = 2`. +- `v = 6..12` targeted (2-4 restarts x 30-150 steps, box `{-3..3}`): best + `chi(Z) = 3` only from structured seeds (C5 perpendicularity extensions); + `chi(Z) >= 4` never observed. +- `v = 5..11` random symmetric/asymmetric/mutual-dense/C5-seeded census (34 + instances, exact `chi`): `chi(Z) >= 4` on 0 instances. + +## Interpretation + +No `chi(Z) >= 4` instance appears in any route; the obstruction records are +budgeted (node caps, step counts), not unrealizability proofs. The registered +`verify.py` search replays a deterministic slice of these routes and writes the +per-trial obstruction records into `CERTIFICATE.json` +(`search_stats.grz_obstructions`). diff --git a/research/fstar-chi4-zero-digraph-seed73765f29/verify.py b/research/fstar-chi4-zero-digraph-seed73765f29/verify.py new file mode 100644 index 0000000000..369eebafc6 --- /dev/null +++ b/research/fstar-chi4-zero-digraph-seed73765f29/verify.py @@ -0,0 +1,1071 @@ +#!/usr/bin/env python3 +"""KB5e: the chi(Z) >= 4 case of F-star residue (ii) (no kappa, no frontier change). + +Exact stdlib engine over integer rank-3 decoders M = P Q^T (v lines, nonzero +diagonal). Quantities per instance: zero digraph Z, exact dichromatic number +chi(Z) (subset DP), chi of the underlying graph U(Z) and of the mutual-zero +graph G_0, matched-pivot value (Lemma MP, PR 2717), anchor reach |S_gamma| +(Lemma SG, PR 2869), exact cert(M) by exhaustive a-enumeration with exact +b-completion (small v), engine witnesses with independent replay, and a +bounded admissible-B chain scan as falsifier criterion (PR 2717 chain +cost >= cert(M), PROVEN there and cited, not restated). + +Deterministic, stdlib only. Run: python3 -B verify.py +""" +import hashlib +import json +import os +import random +import sys +import time + +T0 = time.time() +DATA = os.path.join(os.path.dirname(os.path.abspath(__file__)), "data") + + +def log(msg): + print("[%6.1fs] %s" % (time.time() - T0, msg), flush=True) + + +# ---------------------------------------------------------------- model + +def load_decoder(path): + with open(path, "r", encoding="utf-8") as fh: + raw = json.load(fh) + P = [tuple(int(x) for x in line[0]) for line in raw] + Q = [tuple(int(x) for x in line[1]) for line in raw] + return P, Q + + +def model(P, Q): + v = len(P) + M = [[sum(P[t][j] * Q[s][j] for j in range(3)) for s in range(v)] for t in range(v)] + pi = [sum((1 << j) for j in range(3) if P[t][j] != 0) for t in range(v)] + sg = [sum((1 << j) for j in range(3) if Q[t][j] != 0) for t in range(v)] + D = [pi[t] & sg[t] for t in range(v)] + assert all(M[t][t] != 0 for t in range(v)), "diagonal must be nonzero" + assert all(D[t] != 0 for t in range(v)), "D(t) must be nonempty" + arcs = [(t, s) for t in range(v) for s in range(v) if t != s and M[t][s] == 0] + return dict(v=v, P=P, Q=Q, M=M, pi=pi, sg=sg, D=D, arcs=arcs) + + +def digraph_tables(v, arcs): + inm = [0] * v + outm = [0] * v + for (t, s) in arcs: + inm[s] |= 1 << t + outm[t] |= 1 << s + return inm, outm + + +def acyclic_table(v, inm): + """acyc[S] = True iff the induced subdigraph on S is acyclic (subset DP).""" + acyc = [False] * (1 << v) + acyc[0] = True + for S in range(1, 1 << v): + ok = False + T = S + while T: + b = T & -T + t = b.bit_length() - 1 + if (inm[t] & S) == 0 and acyc[S ^ b]: + ok = True + break + T ^= b + acyc[S] = ok + return acyc + + +def mas_table(v, acyc): + """mas[S] = max size of an acyclic induced subset of S.""" + n = 1 << v + mas = [0] * n + for S in range(1, n): + if acyc[S]: + mas[S] = S.bit_count() + else: + T = S + best = 0 + while T: + b = T & -T + val = mas[S ^ b] + if val > best: + best = val + T ^= b + mas[S] = best + return mas + + +def chi_table(v, acyc): + """Exact dichromatic number: min number of acyclic classes covering [v].""" + n = 1 << v + chi = [v + 1] * n + chi[0] = 0 + for S in range(1, n): + lo = S & -S + best = v + 1 + T = S + while T: + if (T & lo) and acyc[T]: + val = 1 + chi[S ^ T] + if val < best: + best = val + T = (T - 1) & S + chi[S] = best + return chi[-1] + + +def chi_le_k(v, acyc, k): + """Exact decision: can [v] be partitioned into k acyclic classes?""" + classes = [0] * k + order = list(range(v)) + + def rec(i): + if i == v: + return True + t = order[i] + for c in range(k): + if acyc[classes[c] | (1 << t)]: + classes[c] |= 1 << t + if rec(i + 1): + return True + classes[c] ^= 1 << t + return False + + return rec(0) + + +def underlying_arcs(v, arcs): + """Undirected U(Z): {t,s} iff some direction is an arc. As a bidirected digraph.""" + pairs = set() + for (t, s) in arcs: + if t < s: + pairs.add((t, s)) + else: + pairs.add((s, t)) + out = [] + for (t, s) in pairs: + out.append((t, s)) + out.append((s, t)) + return out + + +def mutual_arcs(v, arcs): + """Mutual-zero digons G_0 as a bidirected digraph.""" + aset = set(arcs) + pairs = set() + for (t, s) in arcs: + if t < s and (s, t) in aset: + pairs.add((t, s)) + out = [] + for (t, s) in pairs: + out.append((t, s)) + out.append((s, t)) + return out + + +# ------------------------------------------------------- Lemma SG anchor + +def v2_int(n): + if n == 0: + raise ValueError("v2(0)") + k = 0 + while n % 2 == 0: + n //= 2 + k += 1 + return k + + +def anchor_reach(mod): + """Lemma SG (PR 2869): gamma = min_j c_j, S_gamma = {t : v2(M_tt) = gamma}. + + c_j = min v2(p_j(t)) + min v2(q_j(s)) over nonzero entries (Lemma SC). + Returns (gamma, reach count, cancellation count, per-line v2 diagonal). + """ + P, Q, M = mod["P"], mod["Q"], mod["M"] + v = mod["v"] + cs = [] + for j in range(3): + mp = [v2_int(P[t][j]) for t in range(v) if P[t][j] != 0] + mq = [v2_int(Q[t][j]) for t in range(v) if Q[t][j] != 0] + if mp and mq: + cs.append(min(mp) + min(mq)) + gamma = min(cs) + diag = [v2_int(M[t][t]) for t in range(v)] + reach = sum(1 for t in range(v) if diag[t] == gamma) + cancel = sum(1 for t in range(v) if diag[t] > gamma) + return gamma, reach, cancel, diag + + +# ----------------------------------------------------- Lemma MP pivots + +def matched_pivot(mod, acyc, mas, exhaustive_cap=200000, seed=20261016): + """max over pivot maps c(t) in D(t) (unit masks) of sum_i MAS(Z[C_i]).""" + v = mod["v"] + allowed = [[1 << j for j in range(3) if mod["D"][t] & (1 << j)] for t in range(v)] + prod = 1 + for a in allowed: + prod *= len(a) + best = -1 + best_map = None + exhaustive = prod <= exhaustive_cap + if exhaustive: + import itertools + for combo in itertools.product(*allowed): + classes = [0, 0, 0] + for t in range(v): + i = combo[t].bit_length() - 1 + classes[i] |= 1 << t + val = mas[classes[0]] + mas[classes[1]] + mas[classes[2]] + if val > best: + best = val + best_map = combo + else: + rng = random.Random(seed) + for _ in range(exhaustive_cap): + combo = tuple(a[rng.randrange(len(a))] for a in allowed) + classes = [0, 0, 0] + for t in range(v): + i = combo[t].bit_length() - 1 + classes[i] |= 1 << t + val = mas[classes[0]] + mas[classes[1]] + mas[classes[2]] + if val > best: + best = val + best_map = combo + return best, best_map, exhaustive, prod + + +# --------------------------------------------------------- cert engine + +def dot1(x, y): + return bin(x & y).count("1") & 1 + + +def span_add(basis, x): + """Canonical F2 span extension: pivot-reduced basis of span(basis) + x.""" + pivots = {} + for r in list(basis) + [x]: + while r: + p = r.bit_length() - 1 + if p in pivots: + r ^= pivots[p] + else: + pivots[p] = r + break + return tuple(sorted(pivots.values(), reverse=True)) + + +def b_choices(sig_mask): + return [b for b in range(8) if (b & ~sig_mask) == 0] + + +def completion(mod, a): + """Exact completion over b-labels/order/kept set for fixed a-labels (PR 2717 + engine design). Returns (best size, witness dict or None).""" + v = mod["v"] + M, sg = mod["M"], mod["sg"] + inm, _ = digraph_tables(v, mod["arcs"]) + blockers = [inm[t] for t in range(v)] # s with M[s][t] == 0 + bex = {} + basis_tab = [dict() for _ in range(v)] + b_all = [b_choices(sg[t]) for t in range(v)] + + def b_exists(t, basis): + key = (t, basis) + if key in bex: + return bex[key] + for b in b_all[t]: + if dot1(a[t], b) != 1: + continue + if all(dot1(x, b) == 0 for x in basis): + bex[key] = (True, b) + return bex[key] + bex[key] = (False, 0) + return bex[key] + + def basis_of(t, T): + d = basis_tab[t] + if T in d: + return d[T] + if T == 0: + d[0] = () + return () + b = T & -T + s = b.bit_length() - 1 + prev = basis_of(t, T ^ b) + val = span_add(prev, a[s]) if (blockers[t] & b) else prev + d[T] = val + return val + + n = 1 << v + feas = [False] * n + feas[0] = True + choice = [-1] * n + for T in range(1, n): + U = T + while U: + b = U & -U + t = b.bit_length() - 1 + rest = T ^ b + if feas[rest]: + ok, _bv = b_exists(t, basis_of(t, rest)) + if ok: + feas[T] = True + choice[T] = t + break + U ^= b + best = max(T for T in range(n) if feas[T]) + if best == 0: + return 0, None + kept = [] + bvec = [0] * v + T = best + while T: + t = choice[T] + _ok, bv = b_exists(t, basis_of(t, T ^ (1 << t))) + bvec[t] = bv + kept.append(t) + T ^= 1 << t + kept.reverse() + return best.bit_count(), dict(a=list(a), b=bvec, order=list(kept), kept=list(kept)) + + +def replay_witness(mod, wit): + """Independent replay: supports, K_tt = 1 on kept, order constraints from scratch.""" + v, M = mod["v"], mod["M"] + a, b = wit["a"], wit["b"] + kept = list(wit["kept"]) + order = list(wit["order"]) + if sorted(order) != sorted(kept): + return False + for t in kept: + if (a[t] & ~mod["pi"][t]) or (b[t] & ~mod["sg"][t]): + return False + if dot1(a[t], b[t]) != 1: + return False + pos = {t: i for i, t in enumerate(order)} + for t in kept: + for s in kept: + if t == s: + continue + if M[t][s] == 0 and pos[t] < pos[s]: + if dot1(a[t], b[s]) != 0: + return False + return True + + +def cert_exact(mod, max_v=5): + """Exact cert by exhaustive a-enumeration (small v only).""" + v = mod["v"] + if v > max_v: + return None, None + choices = [[m for m in range(8) if (m & ~mod["pi"][t]) == 0] for t in range(v)] + best = -1 + best_wit = None + import itertools + for combo in itertools.product(*choices): + val, wit = completion(mod, list(combo)) + if val > best: + best = val + best_wit = wit + return best, best_wit + + +def cert_hillclimb(mod, iters=400, seed=1234): + """Bounded deterministic hill-climb over a-labels with exact completion.""" + v = mod["v"] + rng = random.Random(seed) + choices = [[m for m in range(8) if (m & ~mod["pi"][t]) == 0] for t in range(v)] + a = [c[rng.randrange(len(c))] for c in choices] + best, best_wit = completion(mod, a) + cur = list(a) + for it in range(iters): + t = rng.randrange(v) + old = cur[t] + new = choices[t][rng.randrange(len(choices[t]))] + if new == old: + continue + cur[t] = new + val, wit = completion(mod, cur) + if val >= best: + best, best_wit = val, wit + else: + cur[t] = old + return best, best_wit + + +# ----------------------------------------------- chain machinery (falsifier) + +def gf2_rank(rows): + pivots = {} + for x in rows: + while x: + p = x.bit_length() - 1 + if p in pivots: + x ^= pivots[p] + else: + pivots[p] = x + break + return len(pivots) + + +def chain_cost(mod, B): + """sum_j rank_F2 B[R_j, A_j] for admissible B (0/1 lists of row masks).""" + P, Q, v = mod["P"], mod["Q"], mod["v"] + total = 0 + for j in range(3): + R = [t for t in range(v) if P[t][j] != 0] + A = [s for s in range(v) if Q[s][j] != 0] + rows = [] + for t in R: + mask = 0 + for s in A: + if B[t][s]: + mask |= 1 << A.index(s) + rows.append(mask) + total += gf2_rank(rows) + return total + + +def admissible(mod, B): + v, M = mod["v"], mod["M"] + for t in range(v): + if B[t][t] != 1: + return False + for s in range(v): + if t != s and B[t][s] == 1 and M[t][s] != 0: + return False + return True + + +def chain_scan(mod, threshold, seed=99, tries=3000): + """Bounded deterministic scan for an admissible B with chain cost < threshold.""" + v = mod["v"] + rng = random.Random(seed) + best = None + best_cost = None + for _ in range(tries): + B = [[0] * v for _ in range(v)] + for t in range(v): + B[t][t] = 1 + for s in range(v): + if t != s and mod["M"][t][s] == 0 and rng.random() < 0.5: + B[t][s] = 1 + if not admissible(mod, B): + continue + c = chain_cost(mod, B) + if best_cost is None or c < best_cost: + best_cost = c + best = B + if best_cost is not None and best_cost < threshold: + return best_cost, best, True + return best_cost, best, False + + +# --------------------------------------------------------------- controls + +def brute_force_cert(mod): + """Cert from the definition: all labellings, all orders (tiny v only).""" + v, M = mod["v"], mod["M"] + choices = [[m for m in range(8) if (m & ~mod["pi"][t]) == 0] for t in range(v)] + bchoices = [[m for m in range(8) if (m & ~mod["sg"][t]) == 0] for t in range(v)] + best = 0 + import itertools + for a in itertools.product(*choices): + for b in itertools.product(*bchoices): + for k in range(1, v + 1): + for sub in itertools.permutations(range(v), k): + ok = True + for i, t in enumerate(sub): + if dot1(a[t], b[t]) != 1: + ok = False + break + for s in sub[i + 1:]: + if M[t][s] == 0 and dot1(a[t], b[s]) != 0: + ok = False + break + if not ok: + break + if ok and k > best: + best = k + return best + + +def run_controls(): + log("controls") + # 1. brute-force vs engine agreement at v = 3 (3 tiny instances) + tiny = [ + ([(1, 0, 0), (0, 1, 0), (1, 1, 0)], [(1, 0, 0), (0, 1, 0), (1, 0, 1)]), + ([(1, 1, 0), (1, 0, 1), (0, 1, 1)], [(1, 0, -1), (1, -1, 0), (1, 1, 1)]), + ([(1, -1, -1), (0, 1, 1), (1, 1, 0)], [(1, 1, 1), (1, 1, 0), (0, 1, 1)]), + ] + agree = 0 + for P, Q in tiny: + mod = model(P, Q) + bf = brute_force_cert(mod) + ex, _w = cert_exact(mod) + if bf == ex: + agree += 1 + assert agree == 3, "brute-force agreement failed" + # 2. diagonal decoder: cert = 3, MP = 3 + mod = model([(1, 0, 0), (0, 1, 0), (0, 0, 1)], [(1, 0, 0), (0, 1, 0), (0, 0, 1)]) + inm, _ = digraph_tables(mod["v"], mod["arcs"]) + acyc = acyclic_table(mod["v"], inm) + mas = mas_table(mod["v"], acyc) + ex, _w = cert_exact(mod) + assert ex == 3, "diagonal decoder cert" + mp, _m, _exh, _prod = matched_pivot(mod, acyc, mas) + assert mp == 3, "diagonal decoder MP" + assert chi_table(mod["v"], acyc) == 3, "diagonal decoder chi(Z) (bidirected K3)" + # 3. corrupted witnesses rejected + mod = model([(1, 1, 0), (1, 0, 1)], [(1, 0, -1), (1, -1, 0)]) + _val, wit = cert_exact(mod) + assert replay_witness(mod, wit) + bad1 = dict(wit); bad1["a"] = list(wit["a"]); bad1["a"][0] = 0 + bad2 = dict(wit); bad2["b"] = list(wit["b"]); bad2["b"][1] = 0 + assert not replay_witness(mod, bad1), "corrupt a not rejected" + assert not replay_witness(mod, bad2), "corrupt b not rejected" + # 4. hand digraph chi values (digraph-only controls) + def chi_of(v, arcs): + inm, _ = digraph_tables(v, arcs) + return chi_table(v, acyclic_table(v, inm)) + assert chi_of(2, [(0, 1), (1, 0)]) == 2, "digon chi" + assert chi_of(3, [(0, 1), (1, 2), (2, 0)]) == 2, "directed 3-cycle chi (2, not 1)" + c5 = [(0, 1), (1, 2), (2, 3), (3, 4), (4, 0)] + c5 += [(s, t) for (t, s) in c5] + assert chi_of(5, c5) == 3, "bidirected C5 chi" + k4 = [(t, s) for t in range(4) for s in range(4) if t != s] + assert chi_of(4, k4) == 4, "bidirected K4 chi" + # 5. C5 perpendicularity construction (hand): M = P P^T gives Z = bidirected C5 + P5 = [(1, 0, 0), (0, 1, 0), (1, 0, 1), (-1, -1, 1), (0, 1, 1)] + mod = model(P5, [tuple(p) for p in P5]) + inm, _ = digraph_tables(mod["v"], mod["arcs"]) + acyc = acyclic_table(mod["v"], inm) + assert chi_table(mod["v"], acyc) == 3, "C5 perpendicularity chi(Z)" + mut = mutual_arcs(mod["v"], mod["arcs"]) + assert len(mut) == 10, "C5 mutual arcs (bidirected, 5 digons)" + # 6. maintainer's retained rank-2 pivot counterexample (efficient1700 audit) + mod = model([(1, 1, 0), (1, 0, 1)], [(1, 0, -1), (1, -1, 0)]) + inm, _ = digraph_tables(mod["v"], mod["arcs"]) + acyc = acyclic_table(mod["v"], inm) + mas = mas_table(mod["v"], acyc) + assert chi_table(mod["v"], acyc) == 2 <= 3, "counterexample ordinary chi" + mp, _m, _exh, _prod = matched_pivot(mod, acyc, mas) + assert mp == 1 and mp < mod["v"], "counterexample MP under D(t)" + # 7. anchor reach hand values (PR 2869 control SC2: M = 2 I_3) + mod = model([(2, 0, 0), (0, 2, 0), (0, 0, 2)], [(1, 0, 0), (0, 1, 0), (0, 0, 1)]) + gamma, reach, cancel, _d = anchor_reach(mod) + assert (gamma, reach, cancel) == (1, 3, 0), "M = 2 I_3 anchor reach" + # 8. W5-underlying separation example (hand): chi(U) = 4 while chi(Z) = 2. + Pw = [(1, 1, 0), (0, 1, 1), (1, 0, 1), (1, 1, 0), (1, 1, 1), (0, 0, 1)] + Qw = [(1, 0, 0), (0, 1, 0), (1, 0, 0), (0, 1, 0), (0, 0, 1), (1, 0, -1)] + mod = model(Pw, Qw) + inm, _ = digraph_tables(mod["v"], mod["arcs"]) + acyc = acyclic_table(mod["v"], inm) + assert chi_table(mod["v"], acyc) == 2, "W5-underlying example chi(Z) must be 2" + uarcs = underlying_arcs(mod["v"], mod["arcs"]) + u_inm, _ = digraph_tables(mod["v"], uarcs) + assert chi_table(mod["v"], acyclic_table(mod["v"], u_inm)) == 4, \ + "W5-underlying example chi(U) must be 4" + assert len(uarcs) == 20, "W5-underlying example U must have 10 edges" + log("controls: brute_agree=3/3 diagonal=3 mp=3 corrupt_rejects=2/2 " + "chi_hands=4/4 c5_perp=3 pivot_counterexample mp=1 anchor_SC2=3 " + "w5_underlying chiU=4 chiZ=2") + print("PASS_FC4_CONTROLS") + + +def v2_diag_assert(mod, expect_gamma, expect_reach, expect_cancel, name): + gamma, reach, cancel, diag = anchor_reach(mod) + assert (gamma, reach, cancel) == (expect_gamma, expect_reach, expect_cancel), \ + "%s anchor (gamma, reach, cancel) = %r" % (name, (gamma, reach, cancel)) + return diag + + +def mutual_omega(v, mut): + """Largest mutual-zero clique: max subset with every pair a digon.""" + edge = [[False] * v for _ in range(v)] + for (t, s) in mut: + edge[t][s] = True + n = 1 << v + ok = [False] * n + ok[0] = True + omega = 0 + for S in range(1, n): + b = S & -S + t = b.bit_length() - 1 + R = S ^ b + if ok[R]: + good = True + T = R + while T: + c = T & -T + if not edge[t][c.bit_length() - 1]: + good = False + break + T ^= c + if good: + ok[S] = True + if S.bit_count() > omega: + omega = S.bit_count() + return omega + + +def fixture_invariants(mod, acyc, mas): + mut = mutual_arcs(mod["v"], mod["arcs"]) + return mutual_omega(mod["v"], mut) + + +# -------------------------------------------------------------- calibration + +def run_calibration(): + """Reproduce the recorded anchors of PRs 2717/2747/2774/2869 in this engine.""" + log("calibration (recorded anchors)") + # tied_min (v = 12): PR 2717 witness 11/12; PR 2747 MP/MX 9; PR 2774 chi(Z)=3, + # MAS(Z)=4, omega=3, MP deficit 3; PR 2869 reach 0 of 12. + mod = load_model("tied_min.json") + inm, _ = digraph_tables(mod["v"], mod["arcs"]) + acyc = acyclic_table(mod["v"], inm) + mas = mas_table(mod["v"], acyc) + chi = chi_table(mod["v"], acyc) + assert chi == 3, "tied_min chi(Z) must be 3 exactly" + assert mas[-1] == 4, "tied_min MAS(Z) must be 4" + omega = fixture_invariants(mod, acyc, mas) + assert omega == 3, "tied_min mutual-zero omega must be 3" + mp, _m, exh, prod = matched_pivot(mod, acyc, mas) + assert exh and prod == 4096 and mp == 9, "tied_min MP must be 9 (4096 maps)" + assert not chi_le_k(mod["v"], acyc, 3) or mp < mod["v"], "tied_min D-structure" + assert mp == 9 and mp < 12, "tied_min non-3-dichromatic under D(t)" + gamma, reach, cancel, diag = anchor_reach(mod) + assert (gamma, reach, cancel) == (0, 0, 12), "tied_min anchor reach 0/12" + val, wit = cert_hillclimb(mod, iters=250, seed=11) + assert replay_witness(mod, wit) and val == 11, "tied_min engine witness 11" + assert val >= 8, "tied_min F-star threshold 8" + log("tied_min.json: v=12 thr=8 MP=9 (4096 maps) chi=3 MAS=4 omega=3 " + "reach=0/12 witness=%d (PR 2717 recorded 11/12)" % val) + # cex_min_1 (v = 19): PR 2717 stored witness 18/19; PR 2747 MP/MX 16; + # PR 2774 chi le 3 with mutual triangle; PR 2869 reach 8 of 19. + mod = load_model("cex_min_1.json") + inm, _ = digraph_tables(mod["v"], mod["arcs"]) + acyc = acyclic_table(mod["v"], inm) + mas = mas_table(mod["v"], acyc) + assert chi_le_k(mod["v"], acyc, 3), "cex_min_1 must be 3-dichromatic" + mut = mutual_arcs(mod["v"], mod["arcs"]) + tri = False + for a in range(19): + for b in range(a + 1, 19): + for c in range(b + 1, 19): + aset = set(mut) + if (a, b) in aset and (b, c) in aset and (a, c) in aset: + tri = True + assert tri, "cex_min_1 mutual-zero triangle forces chi >= 3" + assert mas[-1] == 10, "cex_min_1 MAS(Z) must be 10" + mp, _m, exh, prod = matched_pivot(mod, acyc, mas) + assert exh and prod == 6144 and mp == 16, "cex_min_1 MP must be 16 (6144 maps)" + gamma, reach, cancel, diag = anchor_reach(mod) + assert (gamma, reach, cancel) == (0, 8, 11), "cex_min_1 anchor reach 8/19" + with open(os.path.join(DATA, "cex_min_1.witness.json"), "r", encoding="utf-8") as fh: + wit = json.load(fh) + wit = dict(a=wit["a"], b=wit["b"], order=wit["order"], kept=wit["kept"]) + assert replay_witness(mod, wit), "cex_min_1 stored witness replay" + assert len(wit["kept"]) == 18 and 18 >= 12, "cex_min_1 stored witness 18/19" + log("cex_min_1.json: v=19 thr=12 MP=16 (6144 maps) chi=le3 (mutual triangle) " + "MAS=10 reach=8/19 witness=18 (PR 2717 recorded 18/19)") + # chain engine 22 on PR 2111's stored pairing (PR 2717 anchor). + with open(os.path.join(DATA, "cex_min_1.B22.json"), "r", encoding="utf-8") as fh: + B = json.load(fh) + if isinstance(B, dict): + B = B.get("B", B.get("pairing")) + assert admissible(mod, B), "stored pairing admissible" + cc = chain_cost(mod, B) + assert cc == 22, "chain engine must reproduce 22 (10+6+6)" + log("chain engine on stored pairing: chain_cost=22 (PR 2111 recorded 10+6+6=22)") + print("PASS_FC4_CALIBRATION tied_min=11/12 cex_min_1=18/19 mp=9/16 chain=22") + return True + + +def load_model(name): + return model(*load_decoder(os.path.join(DATA, name))) + + +# ------------------------------------------------------- chi4 settlement + +def settle(mod, label, exact_cert_max_v=6): + """Full settlement record for one decoder.""" + v = mod["v"] + inm, _ = digraph_tables(v, mod["arcs"]) + acyc = acyclic_table(v, inm) + mas = mas_table(v, acyc) + uarcs = underlying_arcs(v, mod["arcs"]) + u_inm, _ = digraph_tables(v, uarcs) + u_acyc = acyclic_table(v, u_inm) + mut = mutual_arcs(v, mod["arcs"]) + m_inm, _ = digraph_tables(v, mut) + m_acyc = acyclic_table(v, m_inm) + thr = (2 * v) // 3 + rec = dict(label=label, v=v, threshold=thr) + rec["chi_le3"] = chi_le_k(v, acyc, 3) + rec["chi"] = chi_table(v, acyc) if v <= 14 else (3 if rec["chi_le3"] else None) + rec["chi_exact"] = v <= 14 + rec["chi_U_le3"] = chi_le_k(v, u_acyc, 3) + rec["chi_U"] = chi_table(v, u_acyc) if v <= 14 else (3 if rec["chi_U_le3"] else None) + rec["chi_G0_le3"] = chi_le_k(v, m_acyc, 3) + rec["chi_G0"] = chi_table(v, m_acyc) if v <= 14 else (3 if rec["chi_G0_le3"] else None) + rec["MAS_Z"] = mas[-1] + rec["omega_mutual"] = mutual_omega(v, mut) if v <= 16 else None + mp, mpmap, exh, prod = matched_pivot(mod, acyc, mas) + rec["MP"] = mp + rec["MP_exhaustive"] = exh + rec["MP_pivot_product"] = prod + rec["D_compatible_3dic"] = (mp == v) + gamma, reach, cancel, diag = anchor_reach(mod) + rec.update(gamma=gamma, anchor_reach=reach, cancellation_lines=cancel) + # Lemma SF bound through H (block-incidence digraph) + H = [(t, s) for (t, s) in mod["arcs"] if mod["pi"][t] & mod["sg"][s]] + h_inm, _ = digraph_tables(v, H) + h_acyc = acyclic_table(v, h_inm) + rec["MAS_H"] = mas_table(v, h_acyc)[-1] + lower = max(mp, reach, rec["MAS_H"]) + exact = None + wit = None + if v <= exact_cert_max_v: + exact, wit = cert_exact(mod, max_v=exact_cert_max_v) + if exact is not None: + lower = max(lower, exact) + else: + val, wit = cert_hillclimb(mod, iters=300, seed=77) + assert replay_witness(mod, wit), "hill-climb witness must replay" + lower = max(lower, val) + rec["cert_exact"] = exact + rec["cert_lower_bound"] = lower + rec["witness_replayed"] = replay_witness(mod, wit) if wit else None + rec["meets_threshold"] = lower >= thr + if lower < thr: + cc, _B, hit = chain_scan(mod, thr) + rec["chain_scan_best"] = cc + rec["falsifier_found"] = hit + else: + rec["falsifier_found"] = False + return rec, mod, wit + + +# ------------------------------------------------------------ chi4 search + +def gen_random(rng, v, sym): + P = [tuple(rng.randint(-2, 2) for _ in range(3)) for _ in range(v)] + if sym: + Q = list(P) + else: + Q = [tuple(rng.randint(-2, 2) for _ in range(3)) for _ in range(v)] + return P, Q + + +def gen_mutual_dense(rng, v): + """Rejection sampling for many mutual-zero pairs (dense digon structure).""" + for _ in range(400): + P, Q = gen_random(rng, v, False) + if not valid(P, Q): + continue + mod = model(P, Q) + mut = mutual_arcs(v, mod["arcs"]) + if len(mut) // 2 >= v: + return P, Q + return None, None + + +def gen_c5seed(rng, v): + """Start from the hand C5 perpendicularity construction; extend at random.""" + P5 = [(1, 0, 0), (0, 1, 0), (1, 0, 1), (-1, -1, 1), (0, 1, 1)] + P = [tuple(p) for p in P5] + Q = [tuple(p) for p in P5] + while len(P) < v: + P.append(tuple(rng.randint(-2, 2) for _ in range(3))) + Q.append(tuple(rng.randint(-2, 2) for _ in range(3))) + return P[:v], Q[:v] + + +def valid(P, Q): + v = len(P) + for t in range(v): + if sum(P[t][j] * Q[t][j] for j in range(3)) == 0: + return False + if all(x == 0 for x in P[t]) or all(x == 0 for x in Q[t]): + return False + return True + + +def dot3(a, b): + return sum(a[j] * b[j] for j in range(3)) + + +def nullspace3(constraints): + """Basis of {x in Q^3 : c . x = 0 for c in constraints}; exact Fractions.""" + from fractions import Fraction + rows = [] + for c in constraints: + x = [Fraction(c[j]) for j in range(3)] + for prow in rows: + p = next(k for k in range(3) if prow[k] != 0) + if x[p] != 0: + fac = x[p] / prow[p] + x = [x[k] - fac * prow[k] for k in range(3)] + if any(x): + rows.append(x) + rank = len(rows) + if rank >= 3: + return [] + if rank == 0: + return [(Fraction(1), Fraction(0), Fraction(0)), + (Fraction(0), Fraction(1), Fraction(0)), + (Fraction(0), Fraction(0), Fraction(1))] + if rank == 1: + c = rows[0] + vecs = [] + for e in [(1, 0, 0), (0, 1, 0), (0, 0, 1)]: + w = (c[1] * e[2] - c[2] * e[1], + c[2] * e[0] - c[0] * e[2], + c[0] * e[1] - c[1] * e[0]) + if any(w): + keep = True + for u in vecs: + cr = (u[1] * w[2] - u[2] * w[1], u[2] * w[0] - u[0] * w[2], + u[0] * w[1] - u[1] * w[0]) + if not any(cr): + keep = False + break + if keep: + vecs.append(w) + if len(vecs) == 2: + break + return vecs + u = (rows[0][1] * rows[1][2] - rows[0][2] * rows[1][1], + rows[0][2] * rows[1][0] - rows[0][0] * rows[1][2], + rows[0][0] * rows[1][1] - rows[0][1] * rows[1][0]) + return [u] if any(u) else [] + + +def sample_in_span(basis, rng, box): + from fractions import Fraction + import math + for _ in range(40): + co = [rng.randint(-2, 2) for _ in basis] + x = [sum(co[i] * basis[i][j] for i in range(len(basis))) for j in range(3)] + if not any(x): + continue + den = 1 + for t in x: + den = den * t.denominator // math.gcd(den, t.denominator) + xi = tuple(int(t * den) for t in x) + g = 0 + for t in xi: + g = math.gcd(g, abs(t)) + if g > 1: + xi = tuple(t // g for t in xi) + if max(abs(t) for t in xi) <= box * 4: + return xi + return None + + +def grz_instance(): + """Grötzsch graph M(C5): u0..u4 outer cycle, v0..v4 inner, w apex.""" + names = [("u%d" % i) for i in range(5)] + [("v%d" % i) for i in range(5)] + ["w"] + E = set() + for i in range(5): + E.add(frozenset(("u%d" % i, "u%d" % ((i + 1) % 5)))) + E.add(frozenset(("v%d" % i, "u%d" % ((i - 1) % 5)))) + E.add(frozenset(("v%d" % i, "u%d" % ((i + 1) % 5)))) + E.add(frozenset(("v%d" % i, "w"))) + return names, sorted(E, key=lambda s: sorted(s)) + + +def sequential_build(names, edges, rng, box, node_cap=60000): + """Sequential linear construction of a target graph as mutual-zero G_0: + place vertices in degree order; p_i _|_ q_j and q_i _|_ p_j for placed edge + neighbours (exact linear nullspace), generic integer point in the solution + subspace, backtrack on failure. Returns (P, Q) or (None, failure record).""" + v = len(names) + idx = {n: i for i, n in enumerate(names)} + eset = set(frozenset(e) for e in edges) + adj = [set() for _ in range(v)] + for e in eset: + a, b = (idx[x] for x in e) + adj[a].add(b) + adj[b].add(a) + order = sorted(range(v), key=lambda i: -len(adj[i])) + P = [None] * v + Q = [None] * v + nodes = [0] + deepest = [0] + reason = ["none"] + + def rec(k): + nodes[0] += 1 + if nodes[0] > node_cap: + reason[0] = "node_cap" + return False + if k > deepest[0]: + deepest[0] = k + if k == v: + return True + i = order[k] + placed = [j for j in adj[i] if P[j] is not None] + pb = nullspace3([Q[j] for j in placed]) + qb = nullspace3([P[j] for j in placed]) + if not pb or not qb: + reason[0] = "nullspace_collapse" + return False + for _try in range(24): + p = sample_in_span(pb, rng, box) + q = sample_in_span(qb, rng, box) + if p is None or q is None: + reason[0] = "sample_exhausted" + break + if dot3(p, q) == 0: + continue + bad = False + for j in range(v): + if j == i or P[j] is None: + continue + e = frozenset((names[i], names[j])) in eset + m1 = dot3(p, Q[j]) + m2 = dot3(P[j], q) + if e and (m1 != 0 or m2 != 0): + bad = True + break + if not e and m1 == 0 and m2 == 0: + bad = True + break + if bad: + continue + P[i], Q[i] = p, q + if rec(k + 1): + return True + P[i] = Q[i] = None + if reason[0] == "none": + reason[0] = "backtrack_exhausted" + return False + + ok = rec(0) + info = dict(nodes=nodes[0], deepest=deepest[0], reason=reason[0]) + return (P, Q) if ok else (None, info) + + +def run_search(vmax=11): + """Bounded deterministic smallest-first search aimed at chi(Z) >= 4.""" + log("search (smallest first, chi-targeted)") + rng = random.Random(20261016) + found = [] + stats = dict(instances=0, chi4=0, max_chi=0, max_chi_G0=0, max_chi_U=0, + min_mp_ratio=9.9) + for v in range(3, vmax + 1): + for it in range(6): + fam = ("sym" if it % 2 == 0 else "asym") if it < 2 else ( + "mutual" if it < 4 else "c5seed") + if fam in ("sym", "asym"): + P, Q = gen_random(rng, v, fam == "sym") + elif fam == "mutual": + P, Q = gen_mutual_dense(rng, v) + else: + P, Q = gen_c5seed(rng, v) + if P is None or not valid(P, Q): + continue + mod = model(P, Q) + inm, _ = digraph_tables(v, mod["arcs"]) + acyc = acyclic_table(v, inm) + mas = mas_table(v, acyc) + chi = chi_table(v, acyc) + mut = mutual_arcs(v, mod["arcs"]) + m_inm, _ = digraph_tables(v, mut) + chiG = chi_table(v, acyclic_table(v, m_inm)) + uarcs = underlying_arcs(v, mod["arcs"]) + u_inm, _ = digraph_tables(v, uarcs) + chiU = chi_table(v, acyclic_table(v, u_inm)) + stats["instances"] += 1 + stats["max_chi"] = max(stats["max_chi"], chi) + stats["max_chi_G0"] = max(stats["max_chi_G0"], chiG) + stats["max_chi_U"] = max(stats["max_chi_U"], chiU) + if chi >= 4: + stats["chi4"] += 1 + rec, _m, _w = settle(mod, "search v=%d fam=%s" % (v, fam)) + found.append(rec) + log("chi(Z)=%d at v=%d fam=%s (recorded)" % (chi, v, fam)) + else: + mp, _mp, _e, _p = matched_pivot(mod, acyc, mas) + if mp / v < stats["min_mp_ratio"]: + stats["min_mp_ratio"] = mp / v + log("v=%d done (instances %d, chi4=%d, max chi %d)" + % (v, stats["instances"], stats["chi4"], stats["max_chi"])) + # Grötzsch-as-G_0 sequential probe (the exact obstruction record). + names, edges = grz_instance() + obstructions = [] + for trial in range(3): + rng2 = random.Random(500 + trial) + out = sequential_build(names, edges, rng2, box=4, node_cap=60000) + if out[0] is not None: + P, Q = out + mod = model(P, Q) + mut = mutual_arcs(mod["v"], mod["arcs"]) + m_inm, _ = digraph_tables(mod["v"], mut) + chiG = chi_table(mod["v"], acyclic_table(mod["v"], m_inm)) + rec, _m, _w = settle(mod, "grz_seq trial %d" % trial) + found.append(rec) + log("Grötzsch sequential trial %d: REALIZED chi(G_0)=%d" % (trial, chiG)) + else: + obstructions.append(out[1]) + log("Grötzsch sequential trial %d: %r" % (trial, out[1])) + stats["grz_obstructions"] = obstructions + log("search: %d instances, chi4=%d, max chi=%d (G_0 %d, U %d), min MP ratio %.3f" + % (stats["instances"], stats["chi4"], stats["max_chi"], + stats["max_chi_G0"], stats["max_chi_U"], stats["min_mp_ratio"])) + return found, stats + + +def main(): + run_controls() + run_calibration() + records = [] + # settle every embedded chi4 fixture (written by the development search) + fdir = DATA + for name in sorted(os.listdir(fdir)): + if name.startswith("chi4_") and name.endswith(".json"): + mod = load_model(name) + rec, _m, _w = settle(mod, name) + records.append(rec) + log("settle %s: v=%d chi=%s chi_U=%s chi_G0=%s MP=%d reach=%d/%d " + "lower=%d thr=%d meets=%s" + % (name, rec["v"], rec["chi"], rec["chi_U"], rec["chi_G0"], + rec["MP"], rec["anchor_reach"], rec["v"], rec["cert_lower_bound"], + rec["threshold"], rec["meets_threshold"])) + found, stats = run_search(vmax=11) + records.extend(found) + # settle the W5-underlying separation example exactly (v = 6) + Pw = [(1, 1, 0), (0, 1, 1), (1, 0, 1), (1, 1, 0), (1, 1, 1), (0, 0, 1)] + Qw = [(1, 0, 0), (0, 1, 0), (1, 0, 0), (0, 1, 0), (0, 0, 1), (1, 0, -1)] + rec, _m, _w = settle(model(Pw, Qw), "w5_underlying_separation") + records.append(rec) + log("settle w5_underlying_separation: v=%d chi=%s chi_U=%s chi_G0=%s MP=%d " + "cert_exact=%s lower=%d thr=%d meets=%s" + % (rec["v"], rec["chi"], rec["chi_U"], rec["chi_G0"], rec["MP"], + rec["cert_exact"], rec["cert_lower_bound"], rec["threshold"], + rec["meets_threshold"])) + cert = dict( + package="research/fstar-chi4-zero-digraph-seed73765f29", + controls="PASS_FC4_CONTROLS", + calibration="PASS_FC4_CALIBRATION", + search_stats=stats, + settlements=records, + ) + blob = json.dumps(cert, sort_keys=True).encode("utf-8") + digest = hashlib.sha256(blob).hexdigest()[:16] + cert["digest"] = digest + out = os.path.join(os.path.dirname(os.path.abspath(__file__)), "CERTIFICATE.json") + with open(out, "w", encoding="utf-8") as fh: + json.dump(cert, fh, indent=1, sort_keys=True) + fh.write("\n") + log("certificate digest %s" % digest) + print("PASS_FC4_SEARCH") + print("PASS_FSTAR_CHI4_ZERO_DIGRAPHS") + + +if __name__ == "__main__": + sys.stdout.reconfigure(encoding="utf-8") + main()