diff --git a/research/fstar-yu-oh-zero-digraph/PROOF.md b/research/fstar-yu-oh-zero-digraph/PROOF.md new file mode 100644 index 0000000000..0fc10a76f2 --- /dev/null +++ b/research/fstar-yu-oh-zero-digraph/PROOF.md @@ -0,0 +1,185 @@ +# The Yu–Oh rays as a rational zero-digraph fixture + +The thirteen rays below are the established Yu–Oh configuration, not a new +graph construction. This note admits them into the repository's rational +three-total model and proves three different values for the same instance: + +\[ +\operatorname{rank}M=3,\qquad +\chi(Z)=4,\qquad +\operatorname{MP}(M)=12<\operatorname{box}(M)=13. +\] + +Here `MP` is the matched-unit-pivot value, and `box` uses the complete directed +anchor-label definition. The distinction is essential: this coloring +obstruction does not obstruct a full thirteen-row box witness. + +## 1. Exact rational input and anchors + +Take the rows of both factors `P = Q` to be the following integer vectors: + +| Names | Vectors | +|---|---| +| `z1,z2,z3` | `(1,0,0),(0,1,0),(0,0,1)` | +| `y1+,y1−` | `(0,1,1),(0,1,−1)` | +| `y2+,y2−` | `(1,0,1),(1,0,−1)` | +| `y3+,y3−` | `(1,1,0),(1,−1,0)` | +| `h++,h+−,h−+,h−−` | `(1,1,1),(1,1,−1),(1,−1,1),(1,−1,−1)` | + +Set `M = P Qᵀ` over the rationals. Its diagonal entries are respectively +`1,2,3` on axes, faces and bodies; they are nonzero. Its axis principal +submatrix is `I3`, so its rank is exactly three. + +Every factor column contains a unit. Therefore the actual canonical +2-adic column minima are all zero, `γ = 0`, and both anchor supports `A_i,B_i` +are exactly the nonzero coordinates of row `i`. This uses the mathematical +valuation `ν₂(0)=∞`, with no finite sentinel approximation. No zero-product +column needs to be deleted. The common-anchor cardinalities are + +\[ +\tau_i=|A_i\cap B_i|= +\begin{cases}1&\text{on the three axes},\\ +2&\text{on the six faces},\\ +3&\text{on the four bodies}. +\end{cases} +\] + +In particular every tied set is nonempty. Reducing the exact integer +identity `M_ij=0` modulo two gives the source zero-arc implication +`A_i·B_j=0` over `F2`. + +The zero digraph has both arcs on each orthogonal pair, because `M` is +symmetric. Such a digraph is acyclic on a vertex subset precisely when that +subset contains no orthogonal pair: any pair already gives a directed +two-cycle. Thus its dichromatic number equals the ordinary chromatic number +of the orthogonality graph. The latter has exactly 24 edges: three among +the axes, six axis–face edges, three within face pairs, and twelve +face–body edges. Faces from different pairs are not orthogonal, and no +body is orthogonal to an axis or another body. + +## 2. An eight-case proof that `χ(Z) = 4` + +In any proper three-coloring the mutually adjacent axes have different +colors; rename them so `z1,z2,z3` have colors `0,1,2`. The two faces `yi±` +are adjacent to each other and to `zi`. Hence they receive the two colors +other than the color of `zi`, in either order. These are the only eight +remaining choices before coloring the bodies. + +Let bit `b_i` select the color of `yi+` from the increasing list of the +two available colors, and give `yi−` the other color. The body neighbors +among the faces are exactly + +\[ +\begin{array}{c|c} +h_{++}&y1^-,y2^-,y3^-\\ +h_{+-}&y1^+,y2^+,y3^-\\ +h_{-+}&y1^+,y2^-,y3^+\\ +h_{--}&y1^-,y2^+,y3^+ +\end{array} +\] + +The following table identifies a body whose neighbors receive all three +colors; substitution in the preceding four rows checks every case. + +| `(b1,b2,b3)` | Body blocked from all three colors | +|---|---| +| `000` | `h−+` | +| `001` | `h−−` | +| `010` | `h++` | +| `011` | `h+−` | +| `100` | `h+−` | +| `101` | `h++` | +| `110` | `h−−` | +| `111` | `h−+` | + +Consequently three colors do not suffice. Conversely, use any of the eight +colorings on the axes and faces and give all four bodies a fourth color. +There are no body–body edges, so this is a proper four-coloring. Therefore +`χ(Z)=4`, including its directed, dichromatic meaning. + +## 3. The matched-unit-pivot value is exactly twelve + +A matched canonical unit pivot chooses a coordinate `c_i ∈ A_i∩B_i` and +uses `a_i=b_i=e_(c_i)` on each retained line. Since every zero edge here is +bidirected, a retained pivot class must be independent, regardless of its +order. If all thirteen rows could be retained, the three coordinates would +therefore give a proper three-coloring, contradicting Section 2. Thus +`MP(M)≤12`. + +For the reverse inequality, take orientation `000`, omit `h−+`, and use +the following colors (coordinate number is color plus one): + +\[ +\begin{array}{c|c} +(z1,z2,z3)&(0,1,2)\\ +(y1^+,y1^-,y2^+,y2^-,y3^+,y3^-)&(1,2,0,2,0,1)\\ +(h_{++},h_{+-},h_{--})&(0,2,1). +\end{array} +\] + +Each color is in its row's tied support, and each color class is +independent. This supplies twelve valid unit labels, proving `MP(M)=12`. +An exhaustive pivot census can independently check this value, but is not +needed for the upper or lower bound. + +## 4. All thirteen rows satisfy the full directed box constraints + +Recall the constraints: for a retained ordered subset choose binary labels +`a_i ⊆ A_i`, `b_i ⊆ B_i` with `a_i·b_i=1`; whenever `i` precedes `j` and +`M_ij=0`, require `a_i·b_j=0`. Only this forward ordered constraint is +imposed, not its reverse with the labels exchanged. + +Order all rows in three consecutive blocks: + +\[ +F=(y1^+,y2^+,y3^+),\qquad +O=(z1,z2,z3,h_{++},h_{+-},h_{-+},h_{--}),\qquad +L=(y1^-,y2^-,y3^-). +\] + +For a face in either outer block choose any coordinate `c_i` in its +two-element support, and assign + +\[ +(a_i,b_i)= +\begin{cases} +(A_i,e_{c_i})&i\in F,\\ +(A_i,B_i)&i\in O,\\ +(e_{c_i},B_i)&i\in L. +\end{cases} +\] + +These labels lie in the anchors. The outer-block diagonal products are +one, and the middle-block products are one because every middle row has +odd `τ`. Within either outer block there are no actual zero arcs: two +different face planes have dot product `±1`. Within the middle block, +and from any earlier block to any later block, the two labels involved +in a forward constraint are the full anchors `A_i,B_j`. Every such zero +arc is therefore satisfied by the modulo-two implication in Section 1. +This verifies every directed constraint and keeps all thirteen rows. +As no box can retain more rows than the input has, `box(M)=13`. + +## Attribution and scope + +The ray configuration is from Sixia Yu and C. H. Oh, +[*State-independent proof of Kochen–Specker theorem with 13 rays*, +arXiv:1109.4396v1](https://arxiv.org/pdf/1109.4396v1), visible equation (1) +on PDF page 2; its journal version is +[*Physical Review Letters* 108, 030402 (2012)](https://doi.org/10.1103/PhysRevLett.108.030402). +Their ray `h1=(-1,1,1)` is represented here by its negative `(1,-1,-1)`; +this does not change any orthogonality relation. The other representatives +are the same up to naming and order. No quantum-contextuality claim is +needed for the arguments above. + +The repository question and distinction between dichromatic number and +`D(t)`-compatible matched pivots come from Aaron Wang (navinor), +[PR 2890](https://github.com/CrocSwap/integer-mult-bounds/pull/2890), +head `08a44355403604c346f8d907811edce992382cc4`, +`research/fstar-chi4-zero-digraph-seed73765f29/README.md`. This package +supplies a concrete admitted fixture for its open `χ(Z)≥4` question and +separates its pivot value from the complete directed anchor box. It claims +neither a smallest fixture, a new graph, a general coloring bound, nor a +general F-star theorem or counterexample. + +Copyright 2026 Sagar Thakrar. Written with substantial OpenAI Codex +assistance. Licensed under the Apache License, Version 2.0. diff --git a/research/fstar-yu-oh-zero-digraph/README.md b/research/fstar-yu-oh-zero-digraph/README.md new file mode 100644 index 0000000000..95dbd0fff2 --- /dev/null +++ b/research/fstar-yu-oh-zero-digraph/README.md @@ -0,0 +1,112 @@ + + +# A known four-chromatic zero graph with a full thirteen-line box + +The Yu–Oh thirteen-ray configuration supplies an admitted rational example +for the unrestricted `chi(Z)>=4` branch requested in PR #2890. Its three +relevant quantities are different: + +| Quantity | Exact value | +| --- | ---: | +| Ordinary chromatic number of the mutual-zero graph | 4 | +| Dichromatic number of the zero digraph | 4 | +| Best canonical matched-unit-pivot value | 12 | +| General directed sub-anchor box | 13 | + +Thus the coloring and unit-pivot obstructions coexist with a full general +box. This is not an F-star counterexample or a new graph construction. + +The rays are due to **Sixia Yu and C. H. Oh**, [arXiv:1109.4396v1](https://arxiv.org/abs/1109.4396v1), +visible Eq. (1) on page 2 and Figure 2. The contribution is their exact +instantiation in the repository's rational, canonical-anchor and directed +label contracts, with separate proofs and executable witnesses. No novelty +is claimed for the thirteen rays or their known chromatic property. + +## First working example + +Take `P=Q`, with one row for every nonzero direction in `{-1,0,1}³`, using +the representative whose first nonzero coordinate is positive. The rows are +the three axes, the six face directions + +```text +(0,1,±1), (1,0,±1), (1,±1,0), +``` + +and the four body directions `(1,±1,±1)`. The verifier uses lexicographic +order. The paper's `h1=(-1,1,1)` becomes its negative `(1,-1,-1)`; changing +a ray representative's sign preserves its zero relations. + +The product has rank three, nonzero diagonal and 24 unordered zero edges. +Every zero edge occurs in both directions, so an acyclic color class is +exactly an independent set. Ordinary and dichromatic coloring coincide +for this example. Actual canonical gamma is zero and `A_i=B_i` is the +coordinate-support mask. Tied cardinalities are one on the three axes, +two on the six faces, and three on the four bodies; none is empty. + +## Why the three values differ + +The axes force three distinct colors in any proposed three-coloring. +Each orthogonal face pair must use the other two colors, leaving eight +orientations. In every orientation one body direction sees all three +colors, so a three-coloring is impossible. An explicit four-coloring +proves equality. [PROOF.md](PROOF.md) records the finite eight-case argument. + +A matched unit-pivot solution retaining all thirteen rows would be a +proper three-coloring, so its value is at most twelve. An explicit +tie-compatible twelve-row coloring attains twelve. The verifier separately +cross-checks all `2^6 * 3^4 = 5,184` canonical pivot maps; this finite +enumeration is additional evidence, not the sole upper-bound proof. + +The general directed box retains all thirteen. Put the three positive +face directions first, all seven odd-tie rows in the middle, and the three +negative face directions last. The first faces use full source anchors +and tied unit target anchors; the middle uses full anchors on both sides; +the last faces use tied unit source anchors and full target anchors. +The outer blocks have no internal forward zeros. Every remaining required +zero follows from the original binary support implication SG. The literal +definition and a source-authenticated independent oracle both check the +explicit witness. Thirteen is maximal because there are thirteen rows. + +## Reproduction and attribution + +From the repository root, using CPython 3.12: + +```sh +python3 -B scripts/research_package.py --package research/fstar-yu-oh-zero-digraph --check-only +python3.12 -B scripts/research_package.py --package research/fstar-yu-oh-zero-digraph +python3 -B scripts/check_research_commit.py --package research/fstar-yu-oh-zero-digraph --check-source-history +``` + +`VERIFY.json` registers normal and isolated/optimized/warnings-as-errors +replays. Exact finite checks cover the matrix, canonical anchors, coloring, +pivot values, general box and semantic/source failure controls. No numerical +tolerance, quantum-mechanical premise or predecessor search replay is used. + +`SOURCES.json` identifies the literature source, its inspected version and +PDF digest, the sign mapping, the frozen PR #2890 question, and the unchanged +corrected PR #3393 oracle. The paper is cited rather than redistributed; +the replay uses the explicit integer coordinates. Aaron Wang/navinor's +zero-digraph, matched-pivot and directed-box lineage and DreamingOfClouds's +F-star definitions retain attribution. The labeling mechanisms also retain +predecessor credit. New repository instantiation and controls are Apache-2.0, +by Sagar Thakrar with substantial OpenAI Codex assistance. + +Separate same-session agents contributed proof, exact controls and review; +these are not independent human acceptance or formal kernel checking. +The declared PR #2890 searches are not contradicted: this is a known +literature configuration outside those retained search results. + +## Open next questions and limits + +The fixture does not settle a general anchor-box theorem, the all-even +twelve-line floor, or supplier admission. Its full witness uses seven +odd-tie middle rows, which the unresolved all-even case lacks. No selected +frontier or κ changes. + +For another rational orthogonality configuration, check its actual canonical +anchors and explicit directed labels before treating a coloring obstruction +as a useful F-star obstruction. Keep unrestricted coloring, canonical unit +pivots and general sub-anchor witnesses as separate quantities. + +Coordination: [canonical claim and handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19009748), +following [PR #2890's released investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18966804). diff --git a/research/fstar-yu-oh-zero-digraph/RESULT.json b/research/fstar-yu-oh-zero-digraph/RESULT.json new file mode 100644 index 0000000000..06c0ec9d26 --- /dev/null +++ b/research/fstar-yu-oh-zero-digraph/RESULT.json @@ -0,0 +1,904 @@ +{ + "M": [ + [ + 1, + -1, + 0, + 1, + -1, + 0, + 1, + -1, + 0, + 1, + -1, + 0, + 1 + ], + [ + -1, + 2, + 1, + 0, + 0, + -1, + -2, + 1, + 0, + -1, + 2, + 1, + 0 + ], + [ + 0, + 1, + 1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 1, + 1, + 1 + ], + [ + 1, + 0, + 1, + 2, + -2, + -1, + 0, + -1, + 0, + 1, + 0, + 1, + 2 + ], + [ + -1, + 0, + -1, + -2, + 3, + 2, + 1, + 2, + 1, + 0, + 1, + 0, + -1 + ], + [ + 0, + -1, + -1, + -1, + 2, + 2, + 2, + 1, + 1, + 1, + 0, + 0, + 0 + ], + [ + 1, + -2, + -1, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + -1, + 0, + 1 + ], + [ + -1, + 1, + 0, + -1, + 2, + 1, + 0, + 2, + 1, + 0, + 2, + 1, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + -1, + 0, + 1, + 0, + 1, + 2, + 0, + 1, + 2, + 0, + 1, + 2 + ], + [ + -1, + 2, + 1, + 0, + 1, + 0, + -1, + 2, + 1, + 0, + 3, + 2, + 1 + ], + [ + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 2, + 2, + 2 + ], + [ + 1, + 0, + 1, + 2, + -1, + 0, + 1, + 0, + 1, + 2, + 1, + 2, + 3 + ] + ], + "P_equals_Q": true, + "a0": [ + 4, + 6, + 2, + 6, + 7, + 3, + 7, + 5, + 1, + 5, + 7, + 3, + 7 + ], + "b0": [ + 4, + 6, + 2, + 6, + 7, + 3, + 7, + 5, + 1, + 5, + 7, + 3, + 7 + ], + "chromatic_number": 4, + "controls": { + "semantic_mutants_rejected": [ + "matched_units_on_all_thirteen", + "full_even_anchor_diagonals", + "reversed_general_witness", + "out_of_box_unit" + ], + "small_coloring_comparisons": 24, + "source_corruption_rejected_before_execution": [ + "inputs/pr3393-independent_box.py", + "inputs/pr2890-README.md" + ] + }, + "dichromatic_number": 4, + "dichromatic_reason": "Every zero edge occurs in both directions, so an acyclic induced class is exactly an independent set.", + "directed_arc_count": 48, + "four_color_nodes": 14, + "four_coloring": [ + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 2, + 2, + 0, + 2, + 2, + 3 + ], + "gamma": 0, + "general_box": { + "first": [ + 3, + 9, + 11 + ], + "last": [ + 1, + 7, + 5 + ], + "maximum": 13, + "middle": [ + 0, + 2, + 4, + 6, + 8, + 10, + 12 + ], + "upper_bound": "There are only thirteen lines.", + "witness": { + "a": [ + 4, + 2, + 2, + 6, + 7, + 1, + 7, + 1, + 1, + 5, + 7, + 3, + 7 + ], + "b": [ + 4, + 6, + 2, + 2, + 7, + 3, + 7, + 5, + 1, + 1, + 7, + 1, + 7 + ], + "kept": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12 + ], + "order": [ + 3, + 9, + 11, + 0, + 2, + 4, + 6, + 8, + 10, + 12, + 1, + 7, + 5 + ] + } + }, + "inputs_sha256": { + "inputs/pr2890-README.md": "87e1de6007d5f4770048153f188561bb2f68720fddaf45938da134f02654e931", + "inputs/pr3393-independent_box.py": "6792f0c92943e418d93ae6bc8b616447efc2a505612c87c011a36025d98f814d" + }, + "matched_unit_pivots": { + "best": { + "kept": [ + 0, + 1, + 2, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12 + ], + "pivot_coordinates": [ + 2, + 1, + 1, + 1, + 0, + 0, + 2, + 0, + 0, + 2, + 1, + 1, + 2 + ], + "value": 12 + }, + "histogram": { + "10": 2046, + "11": 588, + "12": 48, + "7": 6, + "8": 378, + "9": 2118 + }, + "maps": 5184, + "maximum": 12, + "upper_bound": "A matched-unit witness keeping all13 would be a proper three-coloring of the bidirected zero graph.", + "witness": { + "a": [ + 4, + 2, + 2, + 2, + 1, + 1, + 4, + 1, + 1, + 4, + 2, + 2, + 4 + ], + "b": [ + 4, + 2, + 2, + 2, + 1, + 1, + 4, + 1, + 1, + 4, + 2, + 2, + 4 + ], + "kept": [ + 0, + 1, + 2, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12 + ], + "order": [ + 0, + 1, + 2, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12 + ] + } + }, + "rank": 3, + "rays": [ + [ + 0, + 0, + 1 + ], + [ + 0, + 1, + -1 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 1, + 1 + ], + [ + 1, + -1, + -1 + ], + [ + 1, + -1, + 0 + ], + [ + 1, + -1, + 1 + ], + [ + 1, + 0, + -1 + ], + [ + 1, + 0, + 0 + ], + [ + 1, + 0, + 1 + ], + [ + 1, + 1, + -1 + ], + [ + 1, + 1, + 0 + ], + [ + 1, + 1, + 1 + ] + ], + "schema_version": 1, + "scope": "Known Yu-Oh graph, instantiated as a rational three-total decoder: chi(Z)=4, matched-unit value12, general box13. No new graph, global floor or kappa claim.", + "source_question": { + "lines_241_through_252_sha256": "60eb1d9c6e42841ba29282c4e5cd19ebd177c8d562f0f6c48199747faf9e2685", + "path": "inputs/pr2890-README.md", + "predecessor_search_executed": false, + "question_lines": [ + 241, + 248 + ] + }, + "status": "PASS_FSTAR_YU_OH_ZERO_DIGRAPH", + "tau": [ + 1, + 2, + 1, + 2, + 3, + 2, + 3, + 2, + 1, + 2, + 3, + 2, + 3 + ], + "tau_histogram": { + "1": 3, + "2": 6, + "3": 4 + }, + "three_color_nodes": 25, + "three_color_obstruction": { + "axes": [ + 8, + 2, + 0 + ], + "bodies": [ + 12, + 10, + 6, + 4 + ], + "coverage": "After normalizing the three axis colors, each orthogonal face pair has exactly two choices.", + "face_pairs": [ + [ + 3, + 1 + ], + [ + 9, + 7 + ], + [ + 11, + 5 + ] + ], + "orientations": [ + { + "blocked_body": 6, + "face_colors": [ + [ + 1, + 2 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "neighbor_colors": [ + 0, + 1, + 2 + ], + "orientation": [ + 0, + 0, + 0 + ] + }, + { + "blocked_body": 4, + "face_colors": [ + [ + 1, + 2 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ], + "neighbor_colors": [ + 0, + 1, + 2 + ], + "orientation": [ + 0, + 0, + 1 + ] + }, + { + "blocked_body": 12, + "face_colors": [ + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ], + "neighbor_colors": [ + 0, + 1, + 2 + ], + "orientation": [ + 0, + 1, + 0 + ] + }, + { + "blocked_body": 10, + "face_colors": [ + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ] + ], + "neighbor_colors": [ + 0, + 1, + 2 + ], + "orientation": [ + 0, + 1, + 1 + ] + }, + { + "blocked_body": 10, + "face_colors": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 0, + 1 + ] + ], + "neighbor_colors": [ + 0, + 1, + 2 + ], + "orientation": [ + 1, + 0, + 0 + ] + }, + { + "blocked_body": 12, + "face_colors": [ + [ + 2, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ], + "neighbor_colors": [ + 0, + 1, + 2 + ], + "orientation": [ + 1, + 0, + 1 + ] + }, + { + "blocked_body": 4, + "face_colors": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 1 + ] + ], + "neighbor_colors": [ + 0, + 1, + 2 + ], + "orientation": [ + 1, + 1, + 0 + ] + }, + { + "blocked_body": 6, + "face_colors": [ + [ + 2, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ] + ], + "neighbor_colors": [ + 0, + 1, + 2 + ], + "orientation": [ + 1, + 1, + 1 + ] + } + ] + }, + "undirected_edge_count": 24, + "zero_edges": [ + [ + 0, + 2 + ], + [ + 0, + 5 + ], + [ + 0, + 8 + ], + [ + 0, + 11 + ], + [ + 1, + 3 + ], + [ + 1, + 4 + ], + [ + 1, + 8 + ], + [ + 1, + 12 + ], + [ + 2, + 7 + ], + [ + 2, + 8 + ], + [ + 2, + 9 + ], + [ + 3, + 6 + ], + [ + 3, + 8 + ], + [ + 3, + 10 + ], + [ + 4, + 9 + ], + [ + 4, + 11 + ], + [ + 5, + 10 + ], + [ + 5, + 11 + ], + [ + 5, + 12 + ], + [ + 6, + 7 + ], + [ + 6, + 11 + ], + [ + 7, + 9 + ], + [ + 7, + 12 + ], + [ + 9, + 10 + ] + ] +} diff --git a/research/fstar-yu-oh-zero-digraph/SOURCES.json b/research/fstar-yu-oh-zero-digraph/SOURCES.json new file mode 100644 index 0000000000..e4581ebfef --- /dev/null +++ b/research/fstar-yu-oh-zero-digraph/SOURCES.json @@ -0,0 +1,59 @@ +{ + "schema_version": 1, + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ], + "frozen_sources": [ + { + "path": "inputs/pr3393-independent_box.py", + "origin_commit": "8e1e574fa68465dc0ec69d07852266b9597f9597", + "origin_path": "research/fstar-six-line-floor/independent_box.py", + "git_blob": "d15e05f45e2bf66195f25bb2bb7820e5db4ee9cc", + "sha256": "6792f0c92943e418d93ae6bc8b616447efc2a505612c87c011a36025d98f814d" + }, + { + "path": "inputs/pr2890-README.md", + "origin_commit": "08a44355403604c346f8d907811edce992382cc4", + "origin_path": "research/fstar-chi4-zero-digraph-seed73765f29/README.md", + "git_blob": "acbea2b0ffc66a87573bcd53bfcd24d3e5a17956", + "sha256": "87e1de6007d5f4770048153f188561bb2f68720fddaf45938da134f02654e931" + } + ], + "attribution": { + "known_construction": "Sixia Yu and C. H. Oh, arXiv:1109.4396v1 (2011), visible Eq.(1) on page2 and Figure2: the thirteen rays and their orthogonality graph. No novelty is claimed for this construction or its known chromatic property; the package independently rechecks it and instantiates repository contracts.", + "repository_question": "Aaron Wang/navinor, PR2890 at 08a44355403604c346f8d907811edce992382cc4, retained open request for an actual unrestricted chi(Z)>=4 instance; its declared bounded searches are not refuted or rerun by this literature fixture.", + "definitions": "DreamingOfClouds, PR1590/2111 F-star/certificate definitions; Aaron Wang/navinor, PR2717/2747/2774 matched-pivot and zero-digraph distinction, and PR2914/3031 directed sub-anchor/SG lineage. The asymmetric and odd-middle labeling mechanisms retain predecessor credit.", + "frozen_oracle": "Sagar Thakrar with substantial OpenAI Codex assistance, corrected PR3393, Apache-2.0; original commit/blob/SHA above, exported unchanged through PR3445 at 322a7c89f683a50e154a843150923087ff119973. Target-first oracle is used to check the explicit directed witness, not as a coloring proof.", + "frozen_question": "The PR2890 README is unchanged, exported through PR3452 at dc49c7d7c2fca45e18a9a3da7c9f40aca97d1701. Its original source attribution and pinned bytes remain intact; the C5 correction is a separate contribution.", + "this_package": "Sagar Thakrar with substantial OpenAI Codex assistance, including separate proof, exact-control and review agents. Exact repository instantiation, canonical pivot/general-box separation, executable certificates and semantic controls. Same-session reviews are not independent human acceptance or formal proof." + }, + "literature": [ + { + "authors": [ + "Sixia Yu", + "C. H. Oh" + ], + "title": "State-independent proof of Kochen-Specker theorem with 13 rays", + "arxiv": "1109.4396v1", + "url": "https://arxiv.org/abs/1109.4396v1", + "pdf_url": "https://arxiv.org/pdf/1109.4396v1", + "location": "Visible equation (1), page 2; Figure 2 gives the orthogonality graph.", + "pdf_sha256": "6a7a914beb7f8f9f1d2d25a72ac2ef325aad012aba5c352ddd900fd2d1d46a91", + "pdf_bytes": 214784, + "inspection": "The versioned PDF was visually rendered and checked. Its hidden parsed text also contains an older equation number; visible Eq.(1) is used. The paper is a provenance source, not an executed or redistributed replay input.", + "mapping": "All nonzero vectors in {-1,0,1}^3 modulo sign, represented by first nonzero coordinate +1 and sorted lexicographically. Paper h1=(-1,1,1) is represented by its negative (1,-1,-1); other listed rays already have the chosen sign. All scalar products and zero relations are checked from these integer representatives." + } + ] +} diff --git a/research/fstar-yu-oh-zero-digraph/TASK.json b/research/fstar-yu-oh-zero-digraph/TASK.json new file mode 100644 index 0000000000..9e2642cc05 --- /dev/null +++ b/research/fstar-yu-oh-zero-digraph/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "changed", + "actual_scope": "Instantiate the retained unrestricted chi(Z)>=4 example request with the known Yu-Oh thirteen-ray rational configuration; prove its chromatic/dichromatic number four, canonical matched-unit-pivot value twelve and full directed sub-anchor box thirteen.", + "scope_change_reason": "Handoff-first literature instantiation following PR2890 and the source-bound C5 repair PR3452. Complete fresh overlap searches found no matching repository application. The construction is credited to Yu and Oh; this contribution is exact admission, separation of repository quantities and reproducible witnesses, not discovery of the graph.", + "bottleneck_link": "Shows that the unrestricted four-chromatic zero-digraph branch is nonempty while preserving a full general anchor box, so a unit-pivot deficit or coloring obstruction alone is not a failure of the F-star box route.", + "budget_minutes": 60, + "stop_rule": "Structural checkpoint after approximately 20 minutes; finish with a scoped proof, counterexample or reusable obstruction within approximately 60 minutes. Stop unpromising search branches early; no unstructured directed-zero census.", + "outcome": "completed", + "evidence": "PROOF.md gives the exact canonical anchors, an eight-orientation exclusion of three colors, a four-color witness, a supported twelve-row unit-pivot witness and a thirteen-row general directed witness. The verifier independently checks coloring, all 5,184 canonical pivot maps, exact witnesses, and source/control failures. The known graph is attributed to Yu and Oh.", + "author": "Sagar Thakrar, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance, including separate proof, exact-control and independent-review agents. Same-session AI reviews are not independent human acceptance or formal proof.", + "open_questions": [ + { + "question": "Which other rational orthogonality configurations separate global zero-digraph coloring from canonical anchor-box admission?", + "why_it_matters": "The present four-chromatic configuration has a full box, so coloring failure alone cannot identify a useful F-star obstruction.", + "first_step": "Keep the three quantities separate and inspect actual canonical anchors before launching another graph census; retain an explicit literature source for any imported construction.", + "blocked_by": "One fixed thirteen-ray instance does not classify all rational rank-three zero digraphs or anchor boxes." + }, + { + "question": "Can the completed thirteen-line label witness help resolve the remaining all-even twelve-line box-eight case?", + "why_it_matters": "The thirteen-ray witness uses seven odd-tie middle rows, whereas the unresolved twelve-line case has no such row.", + "first_step": "Use PR3445's obstruction reduction and nonempty canonical ties. Do not transfer a mixed-tie fixture's full-box conclusion to the all-even domain.", + "blocked_by": "The odd-middle construction does not settle general all-even instances." + } + ] +} diff --git a/research/fstar-yu-oh-zero-digraph/VERIFY.json b/research/fstar-yu-oh-zero-digraph/VERIFY.json new file mode 100644 index 0000000000..3de141f2e4 --- /dev/null +++ b/research/fstar-yu-oh-zero-digraph/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate the retained question and independent box oracle; verify the known thirteen-ray graph, coloring, canonical pivots, full directed box and semantic controls using exact arithmetic." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-Werror", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat exact fixture and source controls under isolation, optimization and warnings-as-errors; no global F-star or new graph construction claim." + } + ] +} diff --git a/research/fstar-yu-oh-zero-digraph/inputs/pr2890-README.md b/research/fstar-yu-oh-zero-digraph/inputs/pr2890-README.md new file mode 100644 index 0000000000..acbea2b0ff --- /dev/null +++ b/research/fstar-yu-oh-zero-digraph/inputs/pr2890-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-yu-oh-zero-digraph/inputs/pr3393-independent_box.py b/research/fstar-yu-oh-zero-digraph/inputs/pr3393-independent_box.py new file mode 100644 index 0000000000..d15e05f45e --- /dev/null +++ b/research/fstar-yu-oh-zero-digraph/inputs/pr3393-independent_box.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""Definition-level box oracle, independently written by Sagar Thakrar/Codex. + +SPDX-License-Identifier: Apache-2.0 + +Fix the target labels first. For a proposed next source in the order, solve +its restricted three-variable affine system against all later targets. +No predecessor executable or enumeration routine is imported. +""" + +from fractions import Fraction +from functools import lru_cache +from itertools import combinations, product +import json + + +def dot(left, right): + return (left & right).bit_count() & 1 + + +def linear_solution(allowed, equations): + """Solve dot(x, coefficients)=rhs with x a submask of allowed.""" + rows = [(coefficients & allowed) | (rhs << 3) + for coefficients, rhs in equations] + pivots = [] + cursor = 0 + for column in range(3): + pivot = next((i for i in range(cursor, len(rows)) + if rows[i] & (1 << column)), None) + if pivot is None: + continue + rows[cursor], rows[pivot] = rows[pivot], rows[cursor] + for i in range(len(rows)): + if i != cursor and rows[i] & (1 << column): + rows[i] ^= rows[cursor] + pivots.append((column, cursor)) + cursor += 1 + if any(row == 8 for row in rows): + return None + return sum(1 << column for column, row in pivots if rows[row] & 8) + + +def _inputs(a0, b0, arcs): + a0, b0 = tuple(a0), tuple(b0) + if len(a0) != len(b0): + raise ValueError("anchor lengths differ") + if any(type(mask) is not int or not 0 <= mask < 8 for mask in a0 + b0): + raise ValueError("anchors must be three-bit masks") + arcs = frozenset(tuple(arc) for arc in arcs) + if any(len(arc) != 2 or any(type(i) is not int or not 0 <= i < len(a0) + for i in arc) or arc[0] == arc[1] for arc in arcs): + raise ValueError("zero arcs must be distinct valid line pairs") + return a0, b0, arcs + + +def _target_completion(a0, targets, arcs, kept): + """Every fixed-target source system is independent of earlier sources.""" + @lru_cache(None) + def order_sources(remaining): + if not remaining: + return () + for source in remaining: + later = tuple(i for i in remaining if i != source) + equations = [(targets[source], 1)] + equations.extend((targets[target], 0) for target in later + if (source, target) in arcs) + label = linear_solution(a0[source], equations) + if label is None: + continue + suffix = order_sources(later) + if suffix is not None: + return ((source, label),) + suffix + return None + + chosen = order_sources(tuple(kept)) + if chosen is None: + return None + sources = [0] * len(a0) + for line, label in chosen: + sources[line] = label + return {"a": sources, "b": list(targets), "kept": list(kept), + "order": [line for line, _label in chosen]} + + +def kept_witness(a0, b0, arcs, kept=None): + """Return a witness keeping every specified line, or None exactly.""" + a0, b0, arcs = _inputs(a0, b0, arcs) + kept = tuple(range(len(a0))) if kept is None else tuple(kept) + if len(set(kept)) != len(kept) or any(type(i) is not int or + not 0 <= i < len(a0) for i in kept): + raise ValueError("invalid kept lines") + choices = [tuple(b for b in range(1, 8) if not b & ~b0[i] and b & a0[i]) + for i in kept] + for labels in product(*choices): + targets = [0] * len(a0) + for line, label in zip(kept, labels): + targets[line] = label + witness = _target_completion(a0, targets, arcs, kept) + if witness is not None: + if not check_witness(a0, b0, arcs, witness): + raise ValueError("constructed witness failed its definition") + return witness + return None + + +def find_kept(a0, b0, arcs, count=4): + """Find any kept set of the requested cardinality, or None exactly.""" + a0, b0, arcs = _inputs(a0, b0, arcs) + if type(count) is not int or not 0 <= count <= len(a0): + raise ValueError("invalid kept count") + for kept in combinations(range(len(a0)), count): + witness = kept_witness(a0, b0, arcs, kept) + if witness is not None: + return witness + return None + + +def maximum_box(a0, b0, arcs): + a0, b0, arcs = _inputs(a0, b0, arcs) + for count in range(len(a0), -1, -1): + witness = find_kept(a0, b0, arcs, count) + if witness is not None: + return count, witness + raise ValueError("empty kept set should always exist") + + +def check_witness(a0, b0, arcs, witness): + """Literal forward-arc definition; nonkept labels do not matter.""" + a0, b0, arcs = _inputs(a0, b0, arcs) + a, b = witness["a"], witness["b"] + order, kept = witness["order"], witness["kept"] + if len(a) != len(a0) or len(b) != len(b0) or len(set(kept)) != len(kept): + return False + if sorted(order) != sorted(kept) or any(not 0 <= i < len(a0) for i in kept): + return False + if any(type(a[i]) is not int or type(b[i]) is not int or + not 0 <= a[i] < 8 or not 0 <= b[i] < 8 or + a[i] & ~a0[i] or b[i] & ~b0[i] or dot(a[i], b[i]) != 1 for i in kept): + return False + return all((source, target) not in arcs or dot(a[source], b[target]) == 0 + for k, source in enumerate(order) for target in order[k + 1:]) + + +def valuation(value): + value = Fraction(value) + if not value: + raise ValueError("valuation of zero") + numerator, denominator = abs(value.numerator), value.denominator + return ((numerator & -numerator).bit_length() - + (denominator & -denominator).bit_length()) + + +def rational_rank(matrix): + rows = [[Fraction(x) for x in row] for row in matrix] + rank = 0 + for column in range(len(rows[0]) if rows else 0): + pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + divisor = rows[rank][column] + rows[rank] = [x / divisor for x in rows[rank]] + for i in range(len(rows)): + if i != rank: + multiplier = rows[i][column] + rows[i] = [x - multiplier * y for x, y in zip(rows[i], rows[rank])] + rank += 1 + return rank + + +def rational_data(P, Q): + P, Q = [list(map(Fraction, row)) for row in P], [list(map(Fraction, row)) for row in Q] + if not P or len(P) != len(Q) or any(len(row) != 3 for row in P + Q): + raise ValueError("expected two equally sized nonempty three-column arrays") + matrix = [[sum(x * y for x, y in zip(p, q)) for q in Q] for p in P] + if any(not matrix[i][i] for i in range(len(P))): + raise ValueError("zero diagonal") + minima = [] + for column in range(3): + left = [valuation(row[column]) for row in P if row[column]] + right = [valuation(row[column]) for row in Q if row[column]] + minima.append((min(left), min(right)) if left and right else None) + gamma = min(left + right for pair in minima if pair for left, right in [pair]) + a0 = [sum(1 << j for j, pair in enumerate(minima) if pair and row[j] + and valuation(row[j]) == pair[0]) for row in P] + b0 = [sum(1 << j for j, pair in enumerate(minima) if pair and row[j] + and valuation(row[j]) == gamma - pair[0]) for row in Q] + arcs = [(i, j) for i in range(len(P)) for j in range(len(P)) + if i != j and not matrix[i][j]] + if any(dot(a0[i], b0[j]) != bool(matrix[i][j] and valuation(matrix[i][j]) == gamma) + for i in range(len(P)) for j in range(len(P))): + raise ValueError("rational normalization violated the scope identity") + return {"M": matrix, "rank": rational_rank(matrix), "gamma": gamma, + "a0": a0, "b0": b0, "tau": [(a & b).bit_count() for a, b in zip(a0, b0)], + "arcs": arcs} + + +def core_fixture(): + P = [(-1, -3, 0), (1, -1, -2), (3, 3, 3)] + Q = [(1, -3, 2), (3, -1, -2), (3, -1, 2)] + return ([row for row in P for _ in range(2)], + [row for row in Q for _ in range(2)]) + + +def fixture_certificate(): + data = rational_data(*core_fixture()) + value, witness = maximum_box(data["a0"], data["b0"], data["arcs"]) + expected = [[(8 if i < 4 else 12) if i // 2 == j // 2 else 0 + for j in range(6)] for i in range(6)] + if data["M"] != expected or data["rank"] != 3 or data["tau"] != [2] * 6 or value != 4: + raise ValueError("sharp fixture failed") + # Every five-set meets all three blocks; representatives have only zero + # off-diagonal entries. Their forward constraints force triangular rank3. + # Every target label is in the same two-dimensional space, a contradiction. + upper_bound = all(len({i // 2 for i in subset}) == 3 + for subset in combinations(range(6), 5)) + if not upper_bound or any(mask & ~3 for mask in data["b0"]): + raise ValueError("analytic upper-bound preconditions failed") + data["M"] = [[int(value) for value in row] for row in data["M"]] + return {**data, "box": value, "witness": witness, + "upper_bound": "every five-set contains a rank3 triangular minor; target span has rank2"} + + +if __name__ == "__main__": + print(json.dumps(fixture_certificate(), sort_keys=True)) diff --git a/research/fstar-yu-oh-zero-digraph/verify.py b/research/fstar-yu-oh-zero-digraph/verify.py new file mode 100644 index 0000000000..02f19318cf --- /dev/null +++ b/research/fstar-yu-oh-zero-digraph/verify.py @@ -0,0 +1,279 @@ +#!/usr/bin/env python3 +"""Exact coloring, matched-unit and general-box certificates for Yu--Oh rays. + +SPDX-License-Identifier: Apache-2.0 +Sagar Thakrar (thakrarsagar), with substantial OpenAI Codex assistance. +The thirteen-ray construction is due to Yu and Oh (arXiv:1109.4396v1). +The released question is Aaron Wang/navinor's PR2890; the definition-level +oracle is the author's unchanged PR3393 file, authenticated before execution. +""" + +from collections import Counter +import hashlib +from itertools import combinations, permutations, product +import json +from pathlib import Path +import sys +import types +from unittest.mock import patch + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ORACLE = "inputs/pr3393-independent_box.py" +PREDECESSOR = "inputs/pr2890-README.md" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(root=ROOT): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + rows = [(root, row) for row in manifest["files"] if row["usage"] == "input"] + rows += [(HERE, row) for row in manifest["frozen_sources"]] + result = {} + for base, row in rows: + raw = (base / row["path"]).read_bytes() + require(hashlib.sha256(raw).hexdigest() == row["sha256"], "Input changed: " + row["path"]) + result[row["path"]] = raw + return result + + +def load_oracle(): + raw = authenticate()[ORACLE] + module = types.ModuleType("frozen_box") + exec(compile(raw, str(HERE / ORACLE), "exec"), module.__dict__) + return module + + +def source_question(): + lines = authenticate()[PREDECESSOR].decode().splitlines() + require("Is `chi(Z) <= 3` forced at rank 3?" in lines[240], "released question moved") + require("Would `chi(Z) >= 4` even falsify F-star?" in lines[247], "released box question moved") + excerpt = "\n".join(lines[240:252]) + "\n" + return {"path": PREDECESSOR, "question_lines": [241, 248], + "lines_241_through_252_sha256": hashlib.sha256(excerpt.encode()).hexdigest(), + "predecessor_search_executed": False} + + +def rays(): + return [vector for vector in product((-1, 0, 1), repeat=3) + if any(vector) and next(value for value in vector if value) == 1] + + +def coloring(adjacent, count): + """Exact backtracking; only global renaming of unused colors is removed.""" + colors = [-1] * len(adjacent) + nodes = 0 + + def visit(): + nonlocal nodes + nodes += 1 + remaining = [i for i, color in enumerate(colors) if color < 0] + if not remaining: + return colors[:] + vertex = max(remaining, key=lambda i: ( + len({colors[j] for j in adjacent[i] if colors[j] >= 0}), len(adjacent[i]), -i)) + forbidden = {colors[j] for j in adjacent[vertex]} + for color in range(min(count, 2 + max(colors))): + if color not in forbidden: + colors[vertex] = color + answer = visit() + if answer is not None: + return answer + colors[vertex] = -1 + return None + + answer = visit() + return answer, nodes + + +def face_obstruction(vectors, adjacent): + axes = [vectors.index(tuple(int(i == j) for j in range(3))) for i in range(3)] + pairs = [[vectors.index(positive), vectors.index(negative)] for positive, negative in + [((0, 1, 1), (0, 1, -1)), ((1, 0, 1), (1, 0, -1)), ((1, 1, 0), (1, -1, 0))]] + bodies = [vectors.index(row) for row in ((1, 1, 1), (1, 1, -1), (1, -1, 1), (1, -1, -1))] + require(all(j in adjacent[i] for i, j in combinations(axes, 2)), "axes do not force three colors") + require(all(pair[1] in adjacent[pair[0]] and all(face in adjacent[axes[i]] for face in pair) + for i, pair in enumerate(pairs)), "face orientation premise failed") + records = [] + for bits in product((0, 1), repeat=3): + colors = [-1] * 13 + for i, axis in enumerate(axes): + colors[axis] = i + for i, pair in enumerate(pairs): + available = [color for color in range(3) if color != i] + colors[pair[0]], colors[pair[1]] = available[bits[i]], available[1 - bits[i]] + blocked = [body for body in bodies if {colors[j] for j in adjacent[body]} == {0, 1, 2}] + require(len(blocked) == 1, "three-color obstruction failed") + records.append({"orientation": bits, "face_colors": [[colors[j] for j in pair] for pair in pairs], + "blocked_body": blocked[0], "neighbor_colors": sorted(colors[j] for j in adjacent[blocked[0]])}) + require([vectors[record["blocked_body"]] for record in records] == + [(1, -1, 1), (1, -1, -1), (1, 1, 1), (1, 1, -1), + (1, 1, -1), (1, 1, 1), (1, -1, -1), (1, -1, 1)], "orientation table changed") + return {"axes": axes, "face_pairs": pairs, "bodies": bodies, "orientations": records, + "coverage": "After normalizing the three axis colors, each orthogonal face pair has exactly two choices."} + + +def unit_pivots(supports, adjacent): + size = len(supports) + adjacency = [sum(1 << j for j in row) for row in adjacent] + alpha = [0] * (1 << size) + independent = [0] * (1 << size) + for mask in range(1, 1 << size): + bit = mask & -mask + vertex = bit.bit_length() - 1 + omit = mask ^ bit + include = omit & ~adjacency[vertex] + if 1 + alpha[include] > alpha[omit]: + alpha[mask], independent[mask] = 1 + alpha[include], bit | independent[include] + else: + alpha[mask], independent[mask] = alpha[omit], independent[omit] + require(all(alpha[(1 << i) | (1 << j)] == 1 for i in range(size) for j in adjacent[i]), + "bidirectional edge was not excluded from an acyclic class") + histogram, best = Counter(), None + choices = [[j for j in range(3) if support & (1 << j)] for support in supports] + for pivot in product(*choices): + classes = [sum(1 << i for i, color in enumerate(pivot) if color == j) for j in range(3)] + value = sum(alpha[group] for group in classes) + histogram[value] += 1 + if best is None or value > best["value"]: + kept = independent[classes[0]] | independent[classes[1]] | independent[classes[2]] + best = {"value": value, "pivot_coordinates": pivot, + "kept": [i for i in range(size) if kept & (1 << i)]} + require(sum(histogram.values()) == 5184 and best["value"] == 12, "matched-unit census changed") + require(dict(histogram) == {7: 6, 8: 378, 9: 2118, 10: 2046, 11: 588, 12: 48}, "pivot histogram changed") + labels = [1 << color for color in best["pivot_coordinates"]] + witness = {"a": labels, "b": labels, "kept": best["kept"], "order": best["kept"]} + return {"maps": 5184, "histogram": dict(sorted(histogram.items())), "maximum": 12, + "best": best, "witness": witness, + "upper_bound": "A matched-unit witness keeping all13 would be a proper three-coloring of the bidirected zero graph."} + + +def literal_check(values, supports, witness): + a, b, kept, order = (witness[key] for key in ("a", "b", "kept", "order")) + if len(a) != len(values) or len(b) != len(values) or sorted(order) != sorted(kept): + return False + if len(set(kept)) != len(kept) or any(not 0 <= i < len(values) for i in kept): + return False + if any(type(a[i]) is not int or type(b[i]) is not int or not 0 <= a[i] < 8 or + not 0 <= b[i] < 8 or a[i] & ~supports[i] or b[i] & ~supports[i] or + (a[i] & b[i]).bit_count() % 2 != 1 for i in kept): + return False + return all(values[i][j] or (a[i] & b[j]).bit_count() % 2 == 0 + for k, i in enumerate(order) for j in order[k + 1:]) + + +def full_witness(vectors, values, supports): + first = [vectors.index(row) for row in ((0, 1, 1), (1, 0, 1), (1, 1, 0))] + last = [vectors.index(row) for row in ((0, 1, -1), (1, 0, -1), (1, -1, 0))] + middle = [i for i in range(13) if i not in first + last] + require(all(values[i][j] for block in (first, last) for i, j in permutations(block, 2)), + "face block has a zero entry") + require(all(supports[i].bit_count() % 2 == 1 for i in middle), "middle contains an even diagonal label") + a, b = supports[:], supports[:] + for i in first: + b[i] &= -b[i] + for i in last: + a[i] &= -a[i] + witness = {"a": a, "b": b, "order": first + middle + last, "kept": list(range(13))} + require(literal_check(values, supports, witness), "full-box literal witness failed") + return {"maximum": 13, "first": first, "middle": middle, "last": last, "witness": witness, + "upper_bound": "There are only thirteen lines."} + + +def rejects(action, message): + try: + action() + except ValueError as error: + require(message in str(error), "unexpected failure: " + str(error)) + return + raise ValueError("failure control accepted: " + message) + + +def controls(oracle, values, supports, arcs, full, unit): + all_indices = list(range(13)) + unit_labels = [support & -support for support in supports] + mutants = { + "matched_units_on_all_thirteen": {"a": unit_labels, "b": unit_labels, "kept": all_indices, "order": all_indices}, + "full_even_anchor_diagonals": {"a": supports, "b": supports, "kept": all_indices, "order": all_indices}, + "reversed_general_witness": {**full, "order": list(reversed(full["order"]))}, + "out_of_box_unit": {**unit, "a": unit["a"][:]}, + } + mutants["out_of_box_unit"]["a"][unit["kept"][0]] = 8 + for name, witness in mutants.items(): + require(not literal_check(values, supports, witness) and + not oracle.check_witness(supports, supports, arcs, witness), "semantic mutant accepted: " + name) + # Each simple graph on three vertices is independently compared with literal color assignments. + pairs = list(combinations(range(3), 2)) + for mask in range(8): + adjacent = [set() for _ in range(3)] + for bit, (i, j) in enumerate(pairs): + if mask & (1 << bit): + adjacent[i].add(j) + adjacent[j].add(i) + for colors in (1, 2, 3): + direct = any(all(assignment[i] != assignment[j] for i in range(3) for j in adjacent[i]) + for assignment in product(range(colors), repeat=3)) + require((coloring(adjacent, colors)[0] is not None) == direct, "coloring control disagrees") + old_read = Path.read_bytes + for target, action in ((ORACLE, load_oracle), (PREDECESSOR, source_question)): + def counterfeit(path): + return b'raise RuntimeError("counterfeit executed")\n' if path == HERE / target else old_read(path) + with patch.object(Path, "read_bytes", counterfeit): + rejects(action, "Input changed: " + target) + return {"semantic_mutants_rejected": list(mutants), "small_coloring_comparisons": 24, + "source_corruption_rejected_before_execution": [ORACLE, PREDECESSOR]} + + +def build(): + authenticated = authenticate() + oracle = load_oracle() + vectors = rays() + values = [[sum(x * y for x, y in zip(left, right)) for right in vectors] for left in vectors] + supports = [sum(1 << j for j, value in enumerate(row) if value) for row in vectors] + adjacent = [{j for j in range(13) if i != j and not values[i][j]} for i in range(13)] + edges = [(i, j) for i, j in combinations(range(13), 2) if j in adjacent[i]] + require(len(vectors) == 13 and len(edges) == 24 and all(values[i][i] for i in range(13)), "ray graph changed") + require(all(values[i][j] == values[j][i] for i in range(13) for j in range(13)), "zero graph symmetry failed") + require(all(tuple(int(i == j) for j in range(3)) in vectors for i in range(3)), "rank-three basis missing") + normalized = oracle.rational_data(vectors, vectors) + require(normalized["rank"] == 3 and normalized["gamma"] == 0 and + normalized["a0"] == normalized["b0"] == supports, "canonical data changed") + require(Counter(normalized["tau"]) == {1: 3, 2: 6, 3: 4}, "tie histogram changed") + three, three_nodes = coloring(adjacent, 3) + four, four_nodes = coloring(adjacent, 4) + require(three is None and four is not None and all(four[i] != four[j] for i, j in edges), "chromatic result failed") + unit = unit_pivots(supports, adjacent) + full = full_witness(vectors, values, supports) + for witness in (unit["witness"], full["witness"]): + require(literal_check(values, supports, witness) and oracle.check_witness( + supports, supports, normalized["arcs"], witness), "frozen definition rejects retained witness") + result = {"schema_version": 1, "status": "PASS_FSTAR_YU_OH_ZERO_DIGRAPH", + "scope": "Known Yu-Oh graph, instantiated as a rational three-total decoder: chi(Z)=4, matched-unit value12, general box13. No new graph, global floor or kappa claim.", + "inputs_sha256": {path: hashlib.sha256(raw).hexdigest() for path, raw in authenticated.items()}, + "source_question": source_question(), "rays": vectors, "P_equals_Q": True, "M": values, + "rank": 3, "gamma": 0, "a0": supports, "b0": supports, "tau": normalized["tau"], + "tau_histogram": {1: 3, 2: 6, 3: 4}, "zero_edges": edges, "undirected_edge_count": 24, + "directed_arc_count": 48, "chromatic_number": 4, "dichromatic_number": 4, + "dichromatic_reason": "Every zero edge occurs in both directions, so an acyclic induced class is exactly an independent set.", + "three_color_nodes": three_nodes, "four_color_nodes": four_nodes, "four_coloring": four, + "three_color_obstruction": face_obstruction(vectors, adjacent), "matched_unit_pivots": unit, + "general_box": full, "controls": controls(oracle, values, supports, normalized["arcs"], full["witness"], unit["witness"])} + return json.loads(json.dumps(result)) + + +def main(): + require(sys.argv[1:] in ([], ["--emit"]), "usage: verify.py [--emit]") + result = build() + if sys.argv[1:] == ["--emit"]: + print(json.dumps(result, sort_keys=True, indent=2)) + else: + require(result == json.loads((HERE / "RESULT.json").read_text()), "RESULT.json mismatch") + print("PASS_FSTAR_YU_OH_ZERO_DIGRAPH: chi4, matched-unit12, general-box13; exact retained witnesses") + + +if __name__ == "__main__": + main()