diff --git a/research/fstar-mutual-zero-neighborhood/PROOF.md b/research/fstar-mutual-zero-neighborhood/PROOF.md new file mode 100644 index 0000000000..2242150e91 --- /dev/null +++ b/research/fstar-mutual-zero-neighborhood/PROOF.md @@ -0,0 +1,125 @@ + + +# Correct classification of mutual-zero neighborhoods + +Let M be a matrix over any field K with rank at most three and nonzero +diagonal. Define its mutual-zero graph G_0 on the matrix indices by + + {i,j} is an edge iff i!=j and M_ij=M_ji=0. + +For a vertex t, let N(t) be its open neighborhood in G_0. + +**Theorem.** Every induced graph G_0[N(t)] is a disjoint union of +complete bipartite components and isolated vertices. In particular, +every such neighborhood is bipartite and contains no odd cycle. + +There is no parallelism assumption on the factors of the center. + +## Rank-two classification + +First consider any matrix B of rank at most two with nonzero diagonal. +Factor B_ij=u_i^T v_j with u_i,v_i in K^2, padding a rank-one +factorization if needed. Every factor vector is nonzero by the +diagonal condition. Let alpha_i be the projective direction of v_i, +and let beta_i be the projective direction of the one-dimensional +kernel of the nonzero functional u_i^T. The diagonal condition says + + alpha_i != beta_i. + +A mutual-zero edge between i and j is equivalent to + + alpha_j=beta_i and alpha_i=beta_j. + +Group vertices by their ordered type (alpha,beta). A vertex of type +(a,b) can have neighbors only of type (b,a), and every vertex of the +first type is adjacent to every vertex of the reciprocal type. Since +a!=b, there are no edges inside either type. Distinct unordered pairs +{a,b} give disjoint components. If both reciprocal types occur, they +give one complete bipartite component; if only one occurs, all its +vertices are isolated. This proves the classification for B. + +The argument is valid in every characteristic. Rank one needs no +exception beyond the two-dimensional embedding; its mutual-zero graph +is edgeless. An empty index set is immediate. + +## Apply the classification to a neighborhood + +Choose a rank factorization M_ij=p_i^T q_j in K^3. The nonzero center +diagonal ensures p_t is nonzero. Every i in N(t) satisfies +p_t^T q_i=0, so all q_i on N(t) lie in the two-dimensional plane +ker(p_t^T). Hence the principal matrix M[N(t),N(t)] has rank at most +two and still has nonzero diagonal. Its mutual-zero graph is exactly +G_0[N(t)]. The preceding classification proves the theorem. + +An odd wheel would have its odd rim cycle entirely inside the open +neighborhood of its hub. A bipartite neighborhood cannot contain that +cycle, even as a non-induced subgraph. Thus the no-odd-wheel conclusion +of the predecessor's Lemma C4 remains valid, now for every odd rim length. + +## The error in the retained C5 case split + +The source being corrected is Aaron Wang/navinor's PR2890, head +`08a44355403604c346f8d907811edce992382cc4`, +`research/fstar-chi4-zero-digraph-seed73765f29/README.md`, Lemma C5 +(lines 100--118 in the retained bytes). The retained README has Git blob +`acbea2b0ffc66a87573bcd53bfcd24d3e5a17956` and SHA256 +`87e1de6007d5f4770048153f188561bb2f68720fddaf45938da134f02654e931`. + +Its nonparallel branch asserts that the neighborhood has no edges. +The proposed normalization q_t=e_1, p_t=e_2 would instead force +M_tt=p_t^T q_t=0, contrary to the standing diagonal hypothesis. +The parallel branch's same-type clique option also disappears when +the nonzero diagonal is enforced: the reciprocal type (a,a) is +forbidden. The uniform classification above avoids this case split. + +For clarity, the coordinate changes preserving a factorization are +dual changes. For any invertible S, + + q_i -> S q_i, p_i -> S^(-T) p_i + +leave every entry p_i^T q_j unchanged. Parallelism between p_t and q_t +is not invariant under these changes. In fact, since p_t^T q_t=d!=0, +choose a basis beginning with q_t and completed by a basis of ker(p_t^T). +The resulting dual coordinates give q_t=e_1 and p_t=d e_1. Every +admitted center permits this normalization, regardless of whether its +original factor vectors were parallel. + +## Minimal admitted rational counterexample + +Take the three-row rational factors + + P = [[1,1,0], [1,0,1], [0,1,1]], + Q = [[1,1,-1], [1,-1,1], [-1,1,1]]. + +Their product is M=P Q^T=2 I_3. The center 0 has nonparallel factors +p_0=(1,1,0), q_0=(1,1,-1). Its mutual-zero neighborhood consists of +vertices 1 and 2, which are adjacent. This contradicts the asserted +empty nonparallel neighborhood. Three vertices are minimal for an +edge inside an open neighborhood: one center and two distinct neighbors +are necessary. + +All three factor columns are active. Their 2-adic column minima and +the global normalization exponent gamma are zero. The canonical binary +anchor masks are A=(3,5,6), B=(7,7,7); every tie has size two. Thus the +counterexample also lies in the admitted all-even rational anchor domain. + +Four copies of each paired factor row give twelve rows and +M=2 diag(J_4,J_4,J_4). A center's neighborhood is K_(4,4). Giving the +three groups the respective unit-label masks 1,4,2 gives a full +twelve-line box witness: each unit belongs to its group's tie, and +different groups have zero binary dots. This is a counterexample to +the published C5 branch, not to the twelve-line box-eight target. + +## Scope and attribution + +The corrected classification and odd-wheel consequence are analytic +over arbitrary fields. The explicit counterexample and its canonical +anchor admission are over Q. No predecessor engine or census is needed +for this correction, and no changed census result is asserted. This +does not prove F-star, close the twelve-line bound, or change the selected +multiplication frontier. + +Prepared by Sagar Thakrar with substantial OpenAI Codex assistance. +New work is Apache-2.0. The predecessor C3/C4/C5 statements and F-star +context retain Aaron Wang/navinor's attribution. The exact retained +README is the source identified above. diff --git a/research/fstar-mutual-zero-neighborhood/README.md b/research/fstar-mutual-zero-neighborhood/README.md new file mode 100644 index 0000000000..0e24eccdba --- /dev/null +++ b/research/fstar-mutual-zero-neighborhood/README.md @@ -0,0 +1,99 @@ + + +# Repair the mutual-zero neighborhood classification + +PR #2890 Lemma C5's nonparallel-center branch is false as stated. A +three-row rational example with nonempty, even canonical tied sets +already contradicts it. The corrected theorem preserves the intended +no-odd-wheel conclusion: + +> For a matrix over any field with rank at most three and nonzero diagonal, +> every mutual-zero open neighborhood is a disjoint union of complete +> bipartite components and isolated vertices. + +Here a mutual-zero edge means **both** directed matrix entries are zero. +The theorem concerns the graph induced by a center's open neighborhood, +not the whole mutual-zero graph or the graph of one-way zeros. + +## First working example + +```text +P = [(1,1,0), (1,0,1), (0,1,1)] +Q = [(1,1,-1), (1,-1,1), (-1,1,1)] +P Q^T = 2 I3 +``` + +The center's factors `(1,1,0)` and `(1,1,-1)` are not parallel. Its two +mutual-zero neighbors are adjacent, contradicting C5's edgeless conclusion. +Three vertices are minimal for an edge inside an open neighborhood. +Every factor column is active, the actual valuation minima and gamma are +zero, and the canonical masks are `A=(3,5,6)`, `B=(7,7,7)`: all ties have +cardinality two. + +Repeating each paired row four times gives `2 diag(J4,J4,J4)`. The center's +neighborhood is `K4,4`. Unit labels `1,4,2` on the three respective groups +give a full twelve-line box. This refutes the source lemma, not the +twelve-line box-eight target or F-star. + +## What is corrected + +The pinned [PR #2890 source](https://github.com/CrocSwap/integer-mult-bounds/blob/08a44355403604c346f8d907811edce992382cc4/research/fstar-chi4-zero-digraph-seed73765f29/README.md) +uses `q_t=e1, p_t=e2` in the nonparallel case. That would make the center +diagonal zero. Coordinate changes preserving a factorization act dually +on P and Q; parallelism of their corresponding rows is not invariant. + +The replacement proof in [PROOF.md](PROOF.md) first classifies every +rank-two matrix with nonzero diagonal. A vertex has a projective column +direction and a different row-kernel direction. Mutual-zero edges connect +exactly reciprocal pairs of these types, giving complete bipartite +components. A rank-three center's mutual-zero neighbors have principal +rank at most two, so the classification applies uniformly. + +Thus every such neighborhood is bipartite. No odd wheel can occur, +including as a non-induced subgraph. The predecessor's Lemma C4 survives +with a valid stronger proof. The source's parallel branch is overbroad: +its same-type clique option is excluded by nonzero diagonal. + +## Verification and source boundary + +From the repository root, using CPython 3.12: + +```sh +python3 -B scripts/research_package.py --package research/fstar-mutual-zero-neighborhood --check-only +python3.12 -B scripts/research_package.py --package research/fstar-mutual-zero-neighborhood +python3 -B scripts/check_research_commit.py --package research/fstar-mutual-zero-neighborhood --check-source-history +``` + +`VERIFY.json` registers normal and isolated/optimized/warnings-as-errors +replays. The exact controls bind the predecessor statement, check the +canonical counterexamples, compare literal mutual-zero graphs with the +reciprocal-type classification, and exercise the nonzero-diagonal, +one-way-zero and dual-coordinate boundaries. They are finite controls for +an analytic proof, not a proof by exhaustive rational search. + +The predecessor README is frozen unchanged in `inputs/`; its original +commit, path, blob and SHA256 are in `SOURCES.json`. Read-only inspection +of the pinned predecessor verifier found no use of the false nonparallel +case as a search prune: its sequential construction uses actual nullspaces +and dot products. That engine was **not rerun**, and no changed census +result or comprehensive downstream audit is claimed. + +New work is Apache-2.0, by Sagar Thakrar with substantial OpenAI Codex +assistance. The original C3/C4/C5 statements, source package and F-star +context retain Aaron Wang/navinor's attribution. Separate same-session +agents contributed proof, controls and review; these are not independent +human acceptance or formal kernel checking. No supplier admission, +selected-frontier change or κ improvement is claimed. + +## Open next questions + +1. Which downstream arguments, if any, use the rejected nonparallel-empty + branch? Check the actual caller before changing it; a citation to the + predecessor engine is not evidence that its search used this lemma. +2. What additional information controls canonical anchor boxes when local + bipartite mutual-zero neighborhoods do not settle global coloring? + Keep ordinary directed coloring separate from tied-coordinate-compatible + labelings and actual rational realizability. + +Coordination: [canonical claim and handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19009680), +following the [released predecessor handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18966804). diff --git a/research/fstar-mutual-zero-neighborhood/RESULT.json b/research/fstar-mutual-zero-neighborhood/RESULT.json new file mode 100644 index 0000000000..e9a04d0422 --- /dev/null +++ b/research/fstar-mutual-zero-neighborhood/RESULT.json @@ -0,0 +1,1281 @@ +{ + "F2_controls": { + "admissible_types": [ + [ + [ + 1, + 0 + ], + [ + 1, + 0 + ] + ], + [ + [ + 1, + 0 + ], + [ + 1, + 1 + ] + ], + [ + [ + 0, + 1 + ], + [ + 0, + 1 + ] + ], + [ + [ + 0, + 1 + ], + [ + 1, + 1 + ] + ], + [ + [ + 1, + 1 + ], + [ + 1, + 0 + ] + ], + [ + [ + 1, + 1 + ], + [ + 0, + 1 + ] + ] + ], + "maximum_literal_edges": 12, + "multiplicity_domain": [ + 0, + 1, + 2 + ], + "nonempty_simple_subsets": 63, + "nonempty_weighted_configurations": 728, + "scope": "All six rank2 F2 factor types with multiplicities at most two; a control, not the proof over arbitrary fields." + }, + "boundaries": { + "dropped_neighbor_diagonal": { + "M": [ + [ + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0 + ] + ], + "induced_graph": "triangle" + }, + "invalid_coordinate_step_diagonal_after": 0, + "invalid_coordinate_step_diagonal_before": 2, + "one_way_zero_boundary": { + "P": [ + [ + 1, + 0, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 0, + 1 + ], + [ + 0, + -1, + 1 + ] + ], + "Q": [ + [ + 1, + 0, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 1, + 1 + ], + [ + 0, + 0, + 1 + ] + ], + "mutual_edges": [], + "neighbor_matrix": [ + [ + 1, + 1, + 0 + ], + [ + 0, + 1, + 1 + ], + [ + -1, + 0, + 1 + ] + ], + "one_way_graph": "triangle" + }, + "source_corruption_rejected_before_text_use": true, + "zero_diagonal_and_odd_cycle_rejected": true + }, + "counterexamples": { + "dual_change": { + "A": [ + [ + "1", + "-1", + "0" + ], + [ + "1", + "1", + "0" + ], + [ + "-1", + "0", + "1" + ] + ], + "center_parallel_after": true, + "matrix_preserved": true, + "transformed_P": [ + [ + "2", + "0", + "0" + ], + [ + "0", + "-1", + "1" + ], + [ + "0", + "1", + "1" + ] + ], + "transformed_Q": [ + [ + "1", + "0", + "0" + ], + [ + "0", + "-1", + "1" + ], + [ + "0", + "1", + "1" + ] + ] + }, + "minimal": { + "M": [ + [ + 2, + 0, + 0 + ], + [ + 0, + 2, + 0 + ], + [ + 0, + 0, + 2 + ] + ], + "P": [ + [ + 1, + 1, + 0 + ], + [ + 1, + 0, + 1 + ], + [ + 0, + 1, + 1 + ] + ], + "Q": [ + [ + 1, + 1, + -1 + ], + [ + 1, + -1, + 1 + ], + [ + -1, + 1, + 1 + ] + ], + "canonical": { + "a0": [ + 3, + 5, + 6 + ], + "b0": [ + 7, + 7, + 7 + ], + "column_minima_P": [ + 0, + 0, + 0 + ], + "column_minima_Q": [ + 0, + 0, + 0 + ], + "gamma": 0, + "tau": [ + 2, + 2, + 2 + ] + }, + "center_nonparallel": true, + "minimal_vertex_count": 3, + "neighborhood": { + "classification": { + "complete_bipartite_components": [ + [ + [ + 0 + ], + [ + 1 + ] + ] + ], + "edges": [ + [ + 0, + 1 + ] + ], + "isolates": [], + "type_classes": [ + { + "forbidden": [ + "1", + "1" + ], + "own": [ + "1", + "-1" + ], + "vertices": [ + 0 + ] + }, + { + "forbidden": [ + "1", + "-1" + ], + "own": [ + "1", + "1" + ], + "vertices": [ + 1 + ] + } + ] + }, + "global_edges": [ + [ + 1, + 2 + ] + ], + "vertices": [ + 1, + 2 + ] + }, + "reason_minimal": "An edge in an open neighborhood requires its center and two distinct neighbors." + }, + "twelve": { + "M": [ + [ + 2, + 2, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + 2, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + 2, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + 2, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 2 + ] + ], + "P": [ + [ + 1, + 1, + 0 + ], + [ + 1, + 1, + 0 + ], + [ + 1, + 1, + 0 + ], + [ + 1, + 1, + 0 + ], + [ + 1, + 0, + 1 + ], + [ + 1, + 0, + 1 + ], + [ + 1, + 0, + 1 + ], + [ + 1, + 0, + 1 + ], + [ + 0, + 1, + 1 + ], + [ + 0, + 1, + 1 + ], + [ + 0, + 1, + 1 + ], + [ + 0, + 1, + 1 + ] + ], + "Q": [ + [ + 1, + 1, + -1 + ], + [ + 1, + 1, + -1 + ], + [ + 1, + 1, + -1 + ], + [ + 1, + 1, + -1 + ], + [ + 1, + -1, + 1 + ], + [ + 1, + -1, + 1 + ], + [ + 1, + -1, + 1 + ], + [ + 1, + -1, + 1 + ], + [ + -1, + 1, + 1 + ], + [ + -1, + 1, + 1 + ], + [ + -1, + 1, + 1 + ], + [ + -1, + 1, + 1 + ] + ], + "canonical": { + "a0": [ + 3, + 3, + 3, + 3, + 5, + 5, + 5, + 5, + 6, + 6, + 6, + 6 + ], + "b0": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "column_minima_P": [ + 0, + 0, + 0 + ], + "column_minima_Q": [ + 0, + 0, + 0 + ], + "gamma": 0, + "tau": [ + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2 + ] + }, + "full_box": 12, + "labels_a": [ + 1, + 1, + 1, + 1, + 4, + 4, + 4, + 4, + 2, + 2, + 2, + 2 + ], + "labels_b": [ + 1, + 1, + 1, + 1, + 4, + 4, + 4, + 4, + 2, + 2, + 2, + 2 + ], + "neighborhood": { + "classification": { + "complete_bipartite_components": [ + [ + [ + 0, + 1, + 2, + 3 + ], + [ + 4, + 5, + 6, + 7 + ] + ] + ], + "edges": [ + [ + 0, + 4 + ], + [ + 0, + 5 + ], + [ + 0, + 6 + ], + [ + 0, + 7 + ], + [ + 1, + 4 + ], + [ + 1, + 5 + ], + [ + 1, + 6 + ], + [ + 1, + 7 + ], + [ + 2, + 4 + ], + [ + 2, + 5 + ], + [ + 2, + 6 + ], + [ + 2, + 7 + ], + [ + 3, + 4 + ], + [ + 3, + 5 + ], + [ + 3, + 6 + ], + [ + 3, + 7 + ] + ], + "isolates": [], + "type_classes": [ + { + "forbidden": [ + "1", + "1" + ], + "own": [ + "1", + "-1" + ], + "vertices": [ + 0, + 1, + 2, + 3 + ] + }, + { + "forbidden": [ + "1", + "-1" + ], + "own": [ + "1", + "1" + ], + "vertices": [ + 4, + 5, + 6, + 7 + ] + } + ] + }, + "global_edges": [ + [ + 4, + 8 + ], + [ + 4, + 9 + ], + [ + 4, + 10 + ], + [ + 4, + 11 + ], + [ + 5, + 8 + ], + [ + 5, + 9 + ], + [ + 5, + 10 + ], + [ + 5, + 11 + ], + [ + 6, + 8 + ], + [ + 6, + 9 + ], + [ + 6, + 10 + ], + [ + 6, + 11 + ], + [ + 7, + 8 + ], + [ + 7, + 9 + ], + [ + 7, + 10 + ], + [ + 7, + 11 + ] + ], + "vertices": [ + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11 + ] + }, + "order": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11 + ], + "rank": 3 + } + }, + "inputs_sha256": { + "inputs/pr2890-README.md": "87e1de6007d5f4770048153f188561bb2f68720fddaf45938da134f02654e931" + }, + "multiple_components": { + "P": [ + [ + 1, + 0, + 0 + ], + [ + 0, + 1, + -1 + ], + [ + 0, + 1, + -1 + ], + [ + 0, + 0, + -1 + ], + [ + 0, + 0, + -1 + ], + [ + 0, + 0, + -1 + ], + [ + 0, + 3, + -1 + ], + [ + 0, + 2, + -1 + ], + [ + 0, + 2, + -1 + ], + [ + 0, + 5, + -1 + ] + ], + "Q": [ + [ + 1, + 0, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 1, + 1 + ], + [ + 0, + 1, + 1 + ], + [ + 0, + 1, + 1 + ], + [ + 0, + 1, + 2 + ], + [ + 0, + 1, + 3 + ], + [ + 0, + 1, + 3 + ], + [ + 0, + 1, + 4 + ] + ], + "empty_neighborhood": { + "classification": { + "complete_bipartite_components": [], + "edges": [], + "isolates": [], + "type_classes": [] + }, + "global_edges": [], + "vertices": [] + }, + "neighborhood": { + "classification": { + "complete_bipartite_components": [ + [ + [ + 0, + 1 + ], + [ + 2, + 3, + 4 + ] + ], + [ + [ + 5 + ], + [ + 6, + 7 + ] + ] + ], + "edges": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 4 + ], + [ + 1, + 2 + ], + [ + 1, + 3 + ], + [ + 1, + 4 + ], + [ + 5, + 6 + ], + [ + 5, + 7 + ] + ], + "isolates": [ + 8 + ], + "type_classes": [ + { + "forbidden": [ + "1", + "1" + ], + "own": [ + "1", + "0" + ], + "vertices": [ + 0, + 1 + ] + }, + { + "forbidden": [ + "1", + "0" + ], + "own": [ + "1", + "1" + ], + "vertices": [ + 2, + 3, + 4 + ] + }, + { + "forbidden": [ + "1", + "3" + ], + "own": [ + "1", + "2" + ], + "vertices": [ + 5 + ] + }, + { + "forbidden": [ + "1", + "2" + ], + "own": [ + "1", + "3" + ], + "vertices": [ + 6, + 7 + ] + }, + { + "forbidden": [ + "1", + "5" + ], + "own": [ + "1", + "4" + ], + "vertices": [ + 8 + ] + } + ] + }, + "global_edges": [ + [ + 1, + 3 + ], + [ + 1, + 4 + ], + [ + 1, + 5 + ], + [ + 2, + 3 + ], + [ + 2, + 4 + ], + [ + 2, + 5 + ], + [ + 6, + 7 + ], + [ + 6, + 8 + ] + ], + "vertices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9 + ] + }, + "rank": 3, + "rank_one_isolates": [ + 0, + 1, + 2 + ] + }, + "schema_version": 1, + "scope": "Exact counterexamples and finite controls for the analytic corrected classification; no predecessor search replay or twelve-line floor claim.", + "source_claim": { + "C4_start_line": 119, + "C5_start_line": 100, + "lines_100_through_124_sha256": "3158a72906ea7e621787a97b337a484dac1982638ed71a3b87d6a470e6b78569", + "path": "inputs/pr2890-README.md", + "predecessor_executable_run": false + }, + "status": "PASS_FSTAR_MUTUAL_ZERO_NEIGHBORHOOD" +} diff --git a/research/fstar-mutual-zero-neighborhood/SOURCES.json b/research/fstar-mutual-zero-neighborhood/SOURCES.json new file mode 100644 index 0000000000..8fa56f4415 --- /dev/null +++ b/research/fstar-mutual-zero-neighborhood/SOURCES.json @@ -0,0 +1,42 @@ +{ + "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/pr2890-README.md", + "origin_commit": "08a44355403604c346f8d907811edce992382cc4", + "origin_path": "research/fstar-chi4-zero-digraph-seed73765f29/README.md", + "git_blob": "acbea2b0ffc66a87573bcd53bfcd24d3e5a17956", + "sha256": "87e1de6007d5f4770048153f188561bb2f68720fddaf45938da134f02654e931" + } + ], + "attribution": { + "predecessor": "Aaron Wang/navinor, PR2890 at 08a44355403604c346f8d907811edce992382cc4: original structural lemmas C3/C5/C4, rational search and calibration package. The pinned README is retained unchanged with its source attribution. This contribution corrects C5's nonparallel-empty branch and proves a stronger classification; it does not claim the predecessor census changed.", + "definitions": "DreamingOfClouds, PR1590/2111, F-star and certificate definitions; Aaron Wang/navinor's PR2717/2747/2774/2869/2890 directed-zero and canonical-anchor lineage. Ordinary zero-digraph coloring and tied-coordinate-compatible partitions remain distinct.", + "related_this_session": "Sagar Thakrar with OpenAI Codex assistance, PR3445 at 322a7c89f683a50e154a843150923087ff119973: source review during the twelve-line obstruction investigation exposed this separate C5 issue. No unresolved twelve-line result is imported as a premise.", + "this_package": "Sagar Thakrar with substantial OpenAI Codex assistance, including separate proof, exact-control and review agents. New rank-two reciprocal-class replacement proof, canonical all-even counterexamples and semantic controls. Same-session reviews are not independent human acceptance or formal proof." + }, + "inspected_not_executed": [ + { + "origin_commit": "08a44355403604c346f8d907811edce992382cc4", + "origin_path": "research/fstar-chi4-zero-digraph-seed73765f29/verify.py", + "git_blob": "369eebafc6b0425a1fd5dfeeb013966ae527dba3", + "sha256": "13f091538f38fad0334de432f19eb02670a40705cc771662108ebb70eb7f9a5e", + "scope": "Read-only inspection found no use of the false nonparallel classification as a prune; sequential_build uses actual nullspaces and dot products. No predecessor census or comprehensive downstream code audit was rerun." + } + ] +} diff --git a/research/fstar-mutual-zero-neighborhood/TASK.json b/research/fstar-mutual-zero-neighborhood/TASK.json new file mode 100644 index 0000000000..2985e7b104 --- /dev/null +++ b/research/fstar-mutual-zero-neighborhood/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": "Independently refute and repair PR2890 Lemma C5's nonparallel-center neighborhood branch, preserving the source and proving the correct reciprocal-class classification over any field.", + "scope_change_reason": "Source review during the preceding F-star handoff found a concrete false claimed implication. This round follows that independently checkable correction after refreshed canonical main and overlap checks, instead of the card's default PR2979 working example.", + "bottleneck_link": "Prevents an invalid neighborhood exclusion from entering later F-star arguments and supplies a valid stronger proof of the intended odd-wheel exclusion. It does not settle the zero-digraph coloring problem or admit a supplier.", + "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 an explicit canonical all-even rational counterexample to the pinned C5 branch and a rank-two reciprocal-class proof of the replacement. verify.py and RESULT.json bind the exact predecessor statement and check rational fixtures, literal graph identity, finite-field controls and the diagonal/one-way-zero/coordinate-change boundaries.", + "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": "What additional information controls canonical anchor boxes when the repaired local classification does not settle global coloring?", + "why_it_matters": "Local bipartite mutual-zero neighborhoods do not imply a global directed coloring or a tied-coordinate-compatible labeling.", + "first_step": "Use the repaired condition as a necessary condition only, retaining actual rational realizability and nonzero diagonal. Keep ordinary digraph coloring separate from canonical tied-coordinate constraints.", + "blocked_by": "This package proves a local mutual-zero statement, not a global directed coloring theorem." + }, + { + "question": "Does any downstream proof or pruning rule rely on the rejected nonparallel-empty branch?", + "why_it_matters": "Such uses would need the corrected premise even though the predecessor's intended no-odd-wheel conclusion remains valid.", + "first_step": "Inspect the exact caller before changing it; distinguish analytic citations from actual search pruning. The pinned predecessor verifier was inspected, not rerun.", + "blocked_by": "A comprehensive audit of all later source files and historical censuses is outside this focused correction." + } + ] +} diff --git a/research/fstar-mutual-zero-neighborhood/VERIFY.json b/research/fstar-mutual-zero-neighborhood/VERIFY.json new file mode 100644 index 0000000000..449c9f1ea8 --- /dev/null +++ b/research/fstar-mutual-zero-neighborhood/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 pinned C5 source statement; exact canonical counterexamples, literal mutual-zero graphs versus reciprocal classes, and semantic boundary controls. The general classification is proved analytically." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-Werror", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat exact source and graph controls under isolation, optimization and warnings-as-errors. No predecessor search replay or full F-star claim." + } + ] +} diff --git a/research/fstar-mutual-zero-neighborhood/inputs/pr2890-README.md b/research/fstar-mutual-zero-neighborhood/inputs/pr2890-README.md new file mode 100644 index 0000000000..acbea2b0ff --- /dev/null +++ b/research/fstar-mutual-zero-neighborhood/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-mutual-zero-neighborhood/verify.py b/research/fstar-mutual-zero-neighborhood/verify.py new file mode 100644 index 0000000000..0f9a9fc745 --- /dev/null +++ b/research/fstar-mutual-zero-neighborhood/verify.py @@ -0,0 +1,361 @@ +#!/usr/bin/env python3 +"""Exact controls for the corrected mutual-zero neighborhood classification. + +SPDX-License-Identifier: Apache-2.0 +Sagar Thakrar (thakrarsagar), with substantial OpenAI Codex assistance. +Aaron Wang/navinor's PR2890 README is retained unchanged and authenticated; +no predecessor executable or search engine is executed. +""" + +from fractions import Fraction +import hashlib +from itertools import combinations, product as cartesian_product +import json +from pathlib import Path +import sys +from unittest.mock import patch + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = "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 source_claim(): + raw = authenticate()[SOURCE] + lines = raw.decode().splitlines() + require("Lemma C5" in lines[99] and "G_0[N]` is empty" in lines[101], "retained C5 location changed") + require("`p(t) = e_2`" in lines[107] and "Lemma C4" in lines[118], "retained coordinate step changed") + excerpt = "\n".join(lines[99:124]) + "\n" + return {"path": SOURCE, "C5_start_line": 100, "C4_start_line": 119, + "lines_100_through_124_sha256": hashlib.sha256(excerpt.encode()).hexdigest(), + "predecessor_executable_run": False} + + +def dot(left, right, modulus=0): + value = sum(x * y for x, y in zip(left, right)) + return value % modulus if modulus else value + + +def matrix(p, q, modulus=0): + return [[dot(left, right, modulus) for right in q] for left in p] + + +def rank(values): + rows = [[Fraction(value) for value in row] for row in values] + cursor = 0 + for column in range(len(rows[0]) if rows else 0): + pivot = next((i for i in range(cursor, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[cursor], rows[pivot] = rows[pivot], rows[cursor] + scale = rows[cursor][column] + rows[cursor] = [value / scale for value in rows[cursor]] + for i, row in enumerate(rows): + if i != cursor: + scale = row[column] + rows[i] = [x - scale * y for x, y in zip(row, rows[cursor])] + cursor += 1 + return cursor + + +def inverse(values): + n = len(values) + rows = [[Fraction(value) for value in row] + [Fraction(i == j) for j in range(n)] + for i, row in enumerate(values)] + for column in range(n): + pivot = next((i for i in range(column, n) if rows[i][column]), None) + require(pivot is not None, "singular coordinate change") + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = rows[column][column] + rows[column] = [value / scale for value in rows[column]] + for i, row in enumerate(rows): + if i != column: + scale = row[column] + rows[i] = [x - scale * y for x, y in zip(row, rows[column])] + return [row[n:] for row in rows] + + +def projective(vector, modulus=0): + values = tuple(value % modulus for value in vector) if modulus else tuple(map(Fraction, vector)) + first = next((value for value in values if value), None) + require(first is not None, "zero projective vector") + if modulus: + return tuple(value * pow(first, -1, modulus) % modulus for value in values) + return tuple(value / first for value in values) + + +def mutual_edges(values, vertices=None): + vertices = range(len(values)) if vertices is None else vertices + return [(i, j) for i, j in combinations(vertices, 2) if not values[i][j] and not values[j][i]] + + +def component_check(size, edges): + """Independently color the literal graph and check each component is complete.""" + adjacent = [set() for _ in range(size)] + for i, j in edges: + adjacent[i].add(j) + adjacent[j].add(i) + remaining, components, isolates = set(range(size)), [], [] + while remaining: + start = min(remaining) + if not adjacent[start]: + isolates.append(start) + remaining.remove(start) + continue + color, queue = {start: 0}, [start] + for vertex in queue: + for neighbor in sorted(adjacent[vertex]): + if neighbor not in color: + color[neighbor] = 1 - color[vertex] + queue.append(neighbor) + require(color[neighbor] != color[vertex], "literal component is not bipartite") + sides = [[i for i in sorted(color) if color[i] == bit] for bit in (0, 1)] + require(all(adjacent[i] == set(sides[1 - bit]) for bit in (0, 1) for i in sides[bit]), + "literal bipartite component is not complete") + components.append(sides) + remaining.difference_update(color) + return components, isolates + + +def classify(p, q, modulus=0): + require(len(p) == len(q) and all(len(row) == 2 for row in p + q), "expected paired two-dimensional factors") + values = matrix(p, q, modulus) + require(all(values[i][i] for i in range(len(values))), "neighbor diagonal is zero") + types = [(projective(target, modulus), projective((source[1], -source[0]), modulus)) + for source, target in zip(p, q)] + require(all(alpha != beta for alpha, beta in types), "own and forbidden directions coincide") + expected = [(i, j) for i, j in combinations(range(len(p)), 2) + if types[i] == tuple(reversed(types[j]))] + actual = mutual_edges(values) + require(actual == expected, "reciprocal classes disagree with literal mutual zeros") + components, isolates = component_check(len(p), actual) + classes = {} + for i, kind in enumerate(types): + classes.setdefault(kind, []).append(i) + return {"edges": actual, "complete_bipartite_components": components, "isolates": isolates, + "type_classes": [{"own": list(map(str, alpha)), "forbidden": list(map(str, beta)), "vertices": members} + for (alpha, beta), members in sorted(classes.items())]} + + +def dual_coordinates(p, q, center): + """Use q_center and a basis of ker(p_center) as columns of A.""" + require(all(len(row) == 3 for row in p + q), "expected three-dimensional factors") + values = matrix(p, q) + require(values[center][center], "center diagonal is zero") + pivot = next(i for i, value in enumerate(p[center]) if value) + columns = [list(map(Fraction, q[center]))] + for free in range(3): + if free != pivot: + vector = [Fraction(0)] * 3 + vector[free] = 1 + vector[pivot] = -Fraction(p[center][free], p[center][pivot]) + columns.append(vector) + change = [list(row) for row in zip(*columns)] + inverse_change = inverse(change) + left = matrix(p, columns) + right = matrix(q, inverse_change) + require(matrix(left, right) == values, "dual change altered the matrix") + require(left[center] == [values[center][center], 0, 0] and right[center] == [1, 0, 0], + "center normalization failed") + return left, right, change + + +def neighborhood(p, q, center): + values = matrix(p, q) + require(all(values[i][i] for i in range(len(values))), "neighbor diagonal is zero") + vertices = [i for i in range(len(values)) if i != center and not values[center][i] and not values[i][center]] + left, right, change = dual_coordinates(p, q, center) + require(all(not left[i][0] and not right[i][0] for i in vertices), "mutual neighborhood did not enter two dimensions") + certificate = classify([left[i][1:] for i in vertices], [right[i][1:] for i in vertices]) + local = [(vertices[i], vertices[j]) for i, j in certificate["edges"]] + require(local == mutual_edges(values, vertices), "neighborhood indexing changed the graph") + require(rank([[values[i][j] for j in vertices] for i in vertices]) <= 2, "neighborhood rank exceeded two") + return {"vertices": vertices, "global_edges": local, "classification": certificate}, left, right, change + + +def masks(rows): + return [sum(1 << j for j, value in enumerate(row) if value) for row in rows] + + +def canonical_unit_data(p, q): + """Exact canonical normalization for these explicitly 0/+-1 fixtures.""" + require(all(value in (-1, 0, 1) for row in p + q for value in row), "unit-alphabet fixture required") + require(all(any(row[j] for row in factors) for factors in (p, q) for j in range(3)), "inactive factor column") + a0, b0 = masks(p), masks(q) + values = matrix(p, q) + require(all(values[i][i] for i in range(len(values))), "zero fixture diagonal") + require(all(((a0[i] & b0[j]).bit_count() & 1) == (values[i][j] % 2) + for i in range(len(p)) for j in range(len(q))), "scope identity failed") + return {"column_minima_P": [0, 0, 0], "column_minima_Q": [0, 0, 0], "gamma": 0, + "a0": a0, "b0": b0, "tau": [(a & b).bit_count() for a, b in zip(a0, b0)]} + + +def literal_box(values, a0, b0, a, b, order): + if sorted(order) != list(range(len(values))): + 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 + (a[i] & b[i]).bit_count() % 2 != 1 for i in order): + 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 counterexamples(): + p0 = [(1, 1, 0), (1, 0, 1), (0, 1, 1)] + q0 = [(1, 1, -1), (1, -1, 1), (-1, 1, 1)] + require(matrix(p0, q0) == [[2 * int(i == j) for j in range(3)] for i in range(3)], "2I3 fixture changed") + require(projective(p0[0]) != projective(q0[0]), "counterexample center became parallel") + small, left, right, change = neighborhood(p0, q0, 0) + require(small["vertices"] == [1, 2] and small["global_edges"] == [(1, 2)], "minimal counterexample failed") + normalized = canonical_unit_data(p0, q0) + require(normalized["a0"] == [3, 5, 6] and normalized["b0"] == [7] * 3 and normalized["tau"] == [2] * 3, + "minimal canonical anchors changed") + p, q = ([row for row in factors for _ in range(4)] for factors in (p0, q0)) + values = matrix(p, q) + expected = [[2 * int(i // 4 == j // 4) for j in range(12)] for i in range(12)] + require(values == expected and rank(values) == 3, "twelve-row matrix changed") + large, _left, _right, _change = neighborhood(p, q, 0) + require(large["vertices"] == list(range(4, 12)) and len(large["global_edges"]) == 16, "K4,4 neighborhood failed") + anchors = canonical_unit_data(p, q) + require(anchors["tau"] == [2] * 12, "twelve-row ties changed") + labels = [1] * 4 + [4] * 4 + [2] * 4 + require(literal_box(values, anchors["a0"], anchors["b0"], labels, labels, list(range(12))), "full-box twelve witness failed") + require(projective(left[0]) == projective(right[0]), "dual change did not change parallel status") + return {"minimal": {"P": p0, "Q": q0, "M": matrix(p0, q0), "canonical": normalized, + "neighborhood": small, "center_nonparallel": True, + "minimal_vertex_count": 3, "reason_minimal": "An edge in an open neighborhood requires its center and two distinct neighbors."}, + "twelve": {"P": p, "Q": q, "M": values, "rank": 3, "canonical": anchors, + "neighborhood": large, "full_box": 12, "labels_a": labels, "labels_b": labels, + "order": list(range(12))}, + "dual_change": {"A": [[str(x) for x in row] for row in change], + "transformed_P": [[str(x) for x in row] for row in left], + "transformed_Q": [[str(x) for x in row] for row in right], + "matrix_preserved": True, "center_parallel_after": True}} + + +def multiple_components(): + directions = [(1, i) for i in range(6)] + kinds = [(0, 1)] * 2 + [(1, 0)] * 3 + [(2, 3)] + [(3, 2)] * 2 + [(4, 5)] + p = [(directions[forbidden][1], -1) for own, forbidden in kinds] + q = [directions[own] for own, forbidden in kinds] + direct = classify(p, q) + require([list(map(len, sides)) for sides in direct["complete_bipartite_components"]] == [[2, 3], [1, 2]] + and direct["isolates"] == [8], "multiple reciprocal components failed") + outer_p = [(1, 0, 0)] + [(0, *row) for row in p] + outer_q = [(1, 0, 0)] + [(0, *row) for row in q] + embedded, _p, _q, _change = neighborhood(outer_p, outer_q, 0) + require(embedded["classification"]["edges"] == direct["edges"] and rank(matrix(outer_p, outer_q)) == 3, + "rank-three embedding disagrees") + rank_one = classify([(1, 0), (2, 0), (-3, 0)], [(1, 0), (2, 1), (3, 2)]) + require(not rank_one["edges"] and rank_one["isolates"] == [0, 1, 2], "rank-one boundary failed") + empty = neighborhood([(1, 0, 0)], [(1, 0, 0)], 0)[0] + require(not empty["vertices"] and not empty["classification"]["edges"] and + not empty["classification"]["isolates"], "empty neighborhood boundary failed") + return {"P": outer_p, "Q": outer_q, "rank": 3, "neighborhood": embedded, + "rank_one_isolates": rank_one["isolates"], "empty_neighborhood": empty} + + +def f2_controls(): + vectors = [(1, 0), (0, 1), (1, 1)] + kinds = [(p, q) for p in vectors for q in vectors if dot(p, q, 2)] + require(len(kinds) == 6, "F2 admissible type count changed") + configurations = subsets = max_edges = 0 + for weights in cartesian_product(range(3), repeat=6): + if not any(weights): + continue + p = [kind[0] for kind, count in zip(kinds, weights) for _ in range(count)] + q = [kind[1] for kind, count in zip(kinds, weights) for _ in range(count)] + certificate = classify(p, q, 2) + configurations += 1 + subsets += max(weights) == 1 + max_edges = max(max_edges, len(certificate["edges"])) + require(configurations == 728 and subsets == 63, "finite F2 coverage changed") + return {"admissible_types": [[list(p), list(q)] for p, q in kinds], + "multiplicity_domain": [0, 1, 2], "nonempty_weighted_configurations": configurations, + "nonempty_simple_subsets": subsets, "maximum_literal_edges": max_edges, + "scope": "All six rank2 F2 factor types with multiplicities at most two; a control, not the proof over arbitrary fields."} + + +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 boundary_controls(): + zero = [[int(i == j == 0) for j in range(4)] for i in range(4)] + require(mutual_edges(zero, [1, 2, 3]) == [(1, 2), (1, 3), (2, 3)] and rank(zero) == 1, + "zero-diagonal triangle boundary failed") + rejects(lambda: classify([(0, 0)] * 3, [(0, 0)] * 3), "neighbor diagonal") + rejects(lambda: component_check(3, [(0, 1), (0, 2), (1, 2)]), "not bipartite") + cycle_p = [(1, 0), (0, 1), (-1, 1)] + cycle_q = [(1, 0), (1, 1), (0, 1)] + cycle = matrix(cycle_p, cycle_q) + require(cycle == [[1, 1, 0], [0, 1, 1], [-1, 0, 1]] and rank(cycle) == 2, + "one-way zero cycle changed") + one_way = [(i, j) for i, j in combinations(range(3), 2) if not cycle[i][j] or not cycle[j][i]] + require(one_way == [(0, 1), (0, 2), (1, 2)] and not mutual_edges(cycle), "one-way and mutual zeros conflated") + embedded_p = [(1, 0, 0)] + [(0, *row) for row in cycle_p] + embedded_q = [(1, 0, 0)] + [(0, *row) for row in cycle_q] + require(rank(matrix(embedded_p, embedded_q)) == 3 and + neighborhood(embedded_p, embedded_q, 0)[0]["classification"]["isolates"] == [0, 1, 2], + "one-way triangle embedding failed") + require(dot((1, 1, 0), (1, 1, -1)) == 2 and dot((0, 1, 0), (1, 0, 0)) == 0, + "invalid nonparallel coordinate step no longer changes the diagonal") + old_read = Path.read_bytes + def counterfeit(path): + return b"Counterfeit C5 text\n" if path == HERE / SOURCE else old_read(path) + with patch.object(Path, "read_bytes", counterfeit): + rejects(source_claim, "Input changed: " + SOURCE) + return {"dropped_neighbor_diagonal": {"M": zero, "induced_graph": "triangle"}, + "one_way_zero_boundary": {"P": embedded_p, "Q": embedded_q, + "neighbor_matrix": cycle, "one_way_graph": "triangle", "mutual_edges": []}, + "invalid_coordinate_step_diagonal_before": 2, "invalid_coordinate_step_diagonal_after": 0, + "zero_diagonal_and_odd_cycle_rejected": True, "source_corruption_rejected_before_text_use": True} + + +def build(): + authenticated = authenticate() + result = {"schema_version": 1, "status": "PASS_FSTAR_MUTUAL_ZERO_NEIGHBORHOOD", + "scope": "Exact counterexamples and finite controls for the analytic corrected classification; no predecessor search replay or twelve-line floor claim.", + "inputs_sha256": {path: hashlib.sha256(raw).hexdigest() for path, raw in authenticated.items()}, + "source_claim": source_claim(), "counterexamples": counterexamples(), + "multiple_components": multiple_components(), "F2_controls": f2_controls(), + "boundaries": boundary_controls()} + 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_MUTUAL_ZERO_NEIGHBORHOOD: source-bound counterexamples and corrected-classification controls") + + +if __name__ == "__main__": + main()