research: Yu–Oh χ=4 fixture with unit pivots 12 and full box 13

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.

research/fstar-yu-oh-zero-digraph/README.md

@@ -0,0 +1,112 @@
+<!-- SPDX-License-Identifier: Apache-2.0 -->
+
+# 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).