From 322a7c89f683a50e154a843150923087ff119973 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Sun, 18 Oct 2026 07:34:07 +0530 Subject: [PATCH] Research: narrow twelve-line obstructions and settle the F2 case --- .../fstar-twelve-line-obstruction/PROOF.md | 275 +++ .../fstar-twelve-line-obstruction/README.md | 126 ++ .../fstar-twelve-line-obstruction/RESULT.json | 1885 +++++++++++++++++ .../SOURCES.json | 34 + .../fstar-twelve-line-obstruction/TASK.json | 72 + .../fstar-twelve-line-obstruction/VERIFY.json | 30 + .../inputs/pr3393-independent_box.py | 225 ++ .../fstar-twelve-line-obstruction/verify.py | 412 ++++ 8 files changed, 3059 insertions(+) create mode 100644 research/fstar-twelve-line-obstruction/PROOF.md create mode 100644 research/fstar-twelve-line-obstruction/README.md create mode 100644 research/fstar-twelve-line-obstruction/RESULT.json create mode 100644 research/fstar-twelve-line-obstruction/SOURCES.json create mode 100644 research/fstar-twelve-line-obstruction/TASK.json create mode 100644 research/fstar-twelve-line-obstruction/VERIFY.json create mode 100644 research/fstar-twelve-line-obstruction/inputs/pr3393-independent_box.py create mode 100644 research/fstar-twelve-line-obstruction/verify.py diff --git a/research/fstar-twelve-line-obstruction/PROOF.md b/research/fstar-twelve-line-obstruction/PROOF.md new file mode 100644 index 0000000000..3b029d2b97 --- /dev/null +++ b/research/fstar-twelve-line-obstruction/PROOF.md @@ -0,0 +1,275 @@ + + +# Necessary structure of a twelve-row obstruction + +## Statements and limits + +An ordered nonzero block is a sequence of distinct matrix indices whose +every forward off-diagonal entry is nonzero. We study the following +sufficient condition for a twelve-line box witness: + + Two disjoint ordered nonzero blocks retain at least eight indices. (T) + +The main theorem is a partial reduction, not a proof of (T) over the +rationals: + +> Let M be a twelve-by-twelve matrix over any field K, of rank at most +> three and with nonzero diagonal. If (T) fails, then rank(M)=3. In a +> rank-three factorization M_ij=p_i^T q_j, no projective p-direction or +> q-direction occurs more than twice, and every row and column has at +> most five zero entries. + +Here a projective direction means a nonzero proportionality class. +The diagonal condition ensures that all factor vectors are nonzero. +The conclusion holds for any rank-three factorization. + +These necessary conditions imply that (T) always holds over F_2. They +have not been shown contradictory over Q or R. A rational directed box +can also have a witness that does not arise from (T), so failure of (T) +is not itself a counterexample to the rational box bound. + +We use the seven-row matrix lemma from PR3420 at head +e2d39da9c7109f361d6cff677cf9f8eba51f3dd6: over any field, seven rows of +rank at most three with nonzero diagonal contain an ordered triple. +Its proof is analytic, not a finite-census premise. + +## Rank two partitions into two ordered blocks + +Let M have rank at most two and nonzero diagonal. Write +M_ij=p_i^T q_j with vectors in K^2, padding a smaller factorization if +necessary. Partition the nonzero q-vectors into projective classes. +The zeros in row i consist of at most one complete class: the kernel +of the nonzero functional p_i^T is one projective direction. Call this +its forbidden class, if that direction occurs among the q-vectors. +It is never i's own class because M_ii is nonzero. + +Choose any order of the classes. Put i in F if its forbidden class is +earlier than its own class, and in L if its forbidden class is later. +Rows with no forbidden class, called free rows, may be put in either +block. Order F by increasing class and L by decreasing class. Every +zero from a retained row points backwards. Within a class all entries +are nonzero, since q_j is a nonzero scalar multiple of q_i and M_ii is +nonzero. Thus F,L partition all indices into ordered nonzero blocks. + +Either block can be empty in this construction. If an application +requires two nonempty blocks and one block alone retains at least eight, +split its order into two nonempty blocks. In particular, rank at most +two already proves (T) at twelve rows. The partition also supplies an +ordered block of size at least ceil(n/2) on any n-row rank-two matrix. + +## One or two prescribed outside prefixes + +Let Z be a principal set whose q-vectors lie in a two-dimensional plane H. +Each row of its principal matrix has a nonzero restriction to H, by its +nonzero diagonal, so the preceding class construction applies on H. + +Suppose an outside row a has a nonzero restriction to H. Let A be its +kernel direction on H. Put the Q_Z class A first, if present, in the +class order. Assign free rows of A to L. No other row of A goes to F, +because its forbidden class is different from A and therefore later. +Thus F avoids A, and a can precede F. Together with L this retains all +of Z and a. An absent class A is treated as a formal first class. + +Suppose instead that two outside rows a,b have nonzero restrictions +with distinct kernel directions A,B. Put A first and B last. Assign +free rows of A to L and free rows of B to F, assigning other free rows +arbitrarily. Then F avoids A and L avoids B. Prefix a to F and b to L. +This gives two disjoint ordered blocks retaining |Z|+2 indices. Formal +endpoint classes also cover the case where A or B is absent. + +## Consequences of failure of (T) + +Assume now that (T) fails. Rank at most two has already been excluded. +An ordered five-block is also impossible: its seven-row complement +contains an ordered triple by PR3420, giving five plus three. Two +disjoint ordered four-blocks are impossible by definition. + +We first prove that every factor direction occurs at most twice. + +### Four proportional rows + +Four proportional p-rows form a fully nonzero four-block, since their +diagonals are nonzero. Any outside q-vector is either zero on all four +rows or nonzero on all four. The latter would extend their block to five. +Consequently all eight outside q-vectors lie in the common annihilator +plane. Their rank-two principal matrix partitions into two ordered blocks +retaining eight, a contradiction. This also excludes larger multiplicity. + +### Three proportional rows + +Suppose three proportional p-rows form C. They give a fully nonzero +three-block. Let S be the other indices whose q-vectors are nonzero +against that common p-direction, and let Z be the remaining indices. +A nonzero edge in S could follow C to give five. Therefore S is +independent: its principal matrix is diagonal with nonzero diagonal, +so |S|<=3. All q-vectors on Z lie in a plane. + +If |S|<=1, then |Z|>=8, and its rank-two partition settles (T). +If |S|=2, then |Z|=7. Its rank-two principal matrix has an ordered +four-block. The three-block C followed by either member of S is a +disjoint four-block, again settling (T). Only + + |C|=3, |S|=3, |Z|=6 + +can remain. + +Use the independent S triple as a rank basis. An invertible factor +coordinate change and nonzero individual row and column scalings, +which preserve rank and all zero patterns, permit the normalization + + p_s=q_s=e_s for s=1,2,3 in S, + p_c=(1,1,1) for c in C. + +Indeed, first make P_S the identity; then Q_S is diagonal, and column +scalings make it the identity. The common p-direction has three nonzero +coordinates because it is nonzero on every q_s. A diagonal coordinate +change makes that direction (1,1,1), and row and column scalings on S +restore p_s=q_s=e_s. Scaling the rows of C makes their p-vectors equal. + +Every q_z is nonzero and lies in H={x_1+x_2+x_3=0}. If some s in S has +five nonzero entries into Z, those five rank-two principal indices have +an ordered triple. Prefixing s gives four; C followed by a different +member of S gives a disjoint four. Thus each s has at most four nonzero +entries into Z. Each coordinate vanishes on at least two q_z, while a +nonzero vector in H has at most one zero coordinate. Counting forces +exactly two q_z on each of the three distinct directions + + H intersect {x_1=0}, H intersect {x_2=0}, H intersect {x_3=0}. + +Fix one of these proportional q-pairs U={u,v}, whose zero coordinate +is i, and let j,k be the other coordinates. Let W consist of rows +outside U with nonzero entries into U. They have nonzero entries into +both members. The set W excludes C and contains s_j,s_k. + +If W had a nonzero directed edge, that edge followed by (u,v) would +give four. It uses at most two members of S, leaving an unused member +that can follow C to give a disjoint four. Hence W is independent. +If z in Z outside U belonged to W, independence from s_j,s_k would +force p_z to have only coordinate i, contradicting its nonzero entry +into q_u, whose coordinate i is zero. + +Every row of Z outside U therefore has zero entries into U. Apply this +to all three pairs: M[Z,Z] becomes block diagonal with three two-by-two +blocks. Each has proportional columns and nonzero diagonal, so each +has rank one. This gives rank three, contradicting the rank-at-most-two +construction on Z. Three proportional p-rows are impossible. + +Transposition reverses the order of an ordered block and preserves (T). +The same proof therefore bounds every q-direction's multiplicity by two. + +## Six zero entries in a row already settle (T) + +We prove the remaining zero-degree condition under the multiplicity +bound just established. If a row has at least eight zero columns, choose +eight of them. Their q-vectors lie in a plane and the rank-two partition +settles (T). + +Suppose a row v has seven zero columns Z, and let H=ker(p_v). If an +outside row has nonzero restriction to H, the one-prefix construction +retains all seven indices and that row, settling (T). Otherwise the +five outside p-vectors all annihilate H, and therefore are proportional +to p_v, contradicting the multiplicity bound. + +It remains to consider six zero columns Z of row v. Let Y be the other +six indices, including v, and write U=span{p_y:y in Y}. If U has +dimension three, choose p_a,p_b among these rows so that p_v,p_a,p_b +are independent. Their restrictions to H=ker(p_v) are nonzero and +nonproportional; their kernel directions on H are distinct. The two-prefix +construction retains all six members of Z and a,b, settling (T). + +If U has dimension one, the six indices in Y are fully nonzero, giving +an ordered five-block, which has already been excluded. Suppose U has +dimension two. Let q_0 span its annihilator. Since p_v belongs to U, +q_0 lies in H. Remove from Y the class C of p_v, and from Z the class +D of q_0. Each class has at most two members; D can be empty. + +Every cross entry from Y\C to Z\D is nonzero. To see this, a p-vector +in U not proportional to p_v restricts to a nonzero functional on H. +Its kernel there is exactly q_0, because it annihilates q_0 and that +kernel is one-dimensional. A q-vector outside D does not lie in it. + +Both remaining principal sides have rank at most two: the P-vectors +on Y\C lie in U, and the Q-vectors on Z\D lie in H. Partition each +side into two ordered blocks. Append each Z-side block to the corresponding +Y-side block. The nonzero cross entries make both concatenations valid, +and their union has size + + 12-|C|-|D| >= 8. + +This contradiction excludes six zero entries in a row. Transposition +gives the same result for columns. Since diagonal entries are nonzero, +these zero counts are automatically off-diagonal. The obstruction theorem +is proved over arbitrary fields. + +## The finite-field corollary + +Over F_2 there are exactly seven projective directions in dimension three. +Twelve q-vectors with multiplicity at most two have one of two patterns: +six doubled directions and one absent direction; or five doubled directions +and two singleton directions. + +Each nonzero p-direction annihilates a three-point Fano line. A line +containing three doubled q-directions gives six zero entries and is +forbidden by the obstruction theorem. In the first pattern, every allowed +p-line must pass through the absent q-point. There are only three such +lines, allowing at most six p-rows under the multiplicity bound. In the +second pattern, every allowed line must pass through at least one of the +two singleton q-points. Their two pencils contain 3+3-1=5 distinct lines, +allowing at most ten p-rows. Both contradict twelve. + +Thus every twelve-by-twelve F_2 matrix of rank at most three with nonzero +diagonal satisfies (T). This conclusion is specific to its nonzero-diagonal +finite-field hypotheses. + +## What transfers to the rational directed box + +For binary anchors with nonempty ties, the required scalar implication is + + M_ij=0 implies A_i dot B_j=0 over F_2. (SG) + +Given two ordered blocks F,L, choose a tied coordinate c_i on every +retained line. On F use (a_i,b_i)=(A_i,e_(c_i)); on L use +(a_i,b_i)=(e_(c_i),B_i). Order F before L. Inside a block there are no +forward zero entries. Across the blocks the forward label dot is the +original A_i dot B_j, so SG enforces every required zero. Every diagonal +dot is one. Thus (T) is a sufficient condition for box at least eight, +using the retained asymmetric two-block transfer. + +Canonical rational normalization supplies SG using actual valuations. +Delete product columns for which one whole factor column is zero and put + + m_j=min_i nu_2(P_ij), n_j=min_i nu_2(Q_ij), + gamma=min_j(m_j+n_j), + p_ij=2^(-m_j)P_ij, q_ij=2^(m_j-gamma)Q_ij. + +Zero entries have valuation infinity. The normalized rational entries +have odd denominator, p q^T=2^(-gamma)M, and their reductions modulo two +define A_i,B_i. An actual zero gives SG. This statement concerns actual +rational valuations, not a finite sentinel in an archived implementation. + +There is also a completed rational subcase. If any tied set has odd size, +choose that row r. The other eleven rows have a four-block F and a disjoint +three-block L by PR3435 at head +0833fff0bdc9acdd3b174c7677ab1b46873b22d3. Use the preceding asymmetric +labels on F,L, and insert r between them with (a_r,b_r)=(A_r,B_r). +Its diagonal dot is one because its tie is odd. Dots from F to r, from r +to L, and from F to L are all original anchor dots, so SG supplies every +required zero. This retains eight lines. It uses the original global +anchors; no canonical normalization on a subset is asserted. + +With three total coordinates, the only remaining admitted rational case +has every tie of size two. Its normalized matrix modulo two has zero +diagonal. The F_2 corollary above therefore cannot be applied to that +reduction. The rational twelve-line floor remains open here. In +particular, box less than eight would force both failure of (T) and all +the obstruction conditions, but matrices satisfying those necessary +conditions have not been proved to exist or to have small box. + +## Attribution + +Prepared by Sagar Thakrar with substantial OpenAI Codex assistance. +New work is Apache-2.0. The directed box definition, canonical normalization, +and SG implication retain the Aaron Wang/navinor predecessor attribution. +The seven-row matrix lemma is retained from PR3420 at the head specified +above; the eleven-row four-plus-three conclusion is retained from PR3435. +The asymmetric two-block transfer is retained from PR3409 and PR3420. diff --git a/research/fstar-twelve-line-obstruction/README.md b/research/fstar-twelve-line-obstruction/README.md new file mode 100644 index 0000000000..7c89594b78 --- /dev/null +++ b/research/fstar-twelve-line-obstruction/README.md @@ -0,0 +1,126 @@ + + +# Twelve-line obstruction reduction: general structure and an F₂ theorem + +The rational twelve-line anchor-box floor eight remains **open**. This +package narrows failures of a sufficient matrix route and proves that the +route always succeeds over F₂. It also settles the rational case with an +odd canonical tied cardinality on at least one row. + +An ordered nonzero block is a sequence of distinct indices with a nonzero +matrix entry from every earlier index to every later index. Suppose a +twelve-by-twelve matrix over any field has rank at most three and nonzero +diagonal, but has no two disjoint ordered blocks retaining at least eight +indices in total. Then: + +- its rank is exactly three; +- every projective direction among either factor's rows occurs at most twice; +- each matrix row and column has at most five zero entries. + +These restrictions exclude the entire residual class over F₂. There are +only seven projective directions: twelve nonzero Q rows with multiplicity +at most two have either six doubled directions and one absent direction, +or five doubled directions and two singletons. The zero-degree restriction +then permits at most three or five P directions, respectively, and hence +at most six or ten P rows. Neither permits twelve. + +This is an analytic theorem, not a finite matrix census. [PROOF.md](PROOF.md) +gives the rank-two partition and prescribed-prefix constructions, the +repeated-direction reduction, the zero-degree reduction, and the F₂ count. +The retained seven-row ordered-triple lemma is attributed to [PR #3420 at +its exact head](https://github.com/CrocSwap/integer-mult-bounds/blob/e2d39da9c7109f361d6cff677cf9f8eba51f3dd6/research/fstar-nine-line-floor/PROOF.md). + +## What transfers to rational anchors + +For canonical rational three-total factorizations, actual zero entries +satisfy the binary support condition SG. Two ordered blocks therefore +give a directed sub-anchor witness by the retained asymmetric labeling. +Rank at most two admits a partition into two ordered blocks, so it gives +a full box of all rows under the nonempty-tie hypothesis. + +For twelve rows, one odd tied cardinality suffices: apply [PR #3435's +eleven-row four-plus-three matrix theorem](https://github.com/CrocSwap/integer-mult-bounds/blob/0833fff0bdc9acdd3b174c7677ab1b46873b22d3/research/fstar-eleven-line-floor/PROOF.md) +to the other eleven rows and place the odd row, with its full anchors, +between the two blocks. This keeps eight rows. The original global +anchors are retained; they are not recomputed on the eleven-row subset. + +The unresolved rational case thus has rank three and tied cardinality two +on every row. Its normalized matrix has **zero diagonal modulo two**. +Consequently the F₂ theorem's nonzero-diagonal assumption fails: reducing +the factors modulo two does not solve the rational problem. A failure of +the two-block route would also not itself be a box counterexample. + +## First working example + +Use Aaron Wang's PR #2978 rational core and repeat each paired row four times: + +```text +P = [(-1,-3,0), (1,-1,-2), (3,3,3)] +Q = [(1,-3,2), (3,-1,-2), (3,-1,2)] +``` + +The twelve-row product is `diag(8 J4, 8 J4, 12 J4)`, with rank three, +canonical gamma zero, and tied cardinality two everywhere. Two components +give an eight-row witness. The box is exactly eight: any larger witness +would meet all three components, whose three representatives have zero +off-diagonal pairings. Their ordered label matrix would have rank three, +whereas every B sub-anchor lies in the same two-dimensional binary +coordinate plane. This example is an upper bound for the sought floor, +not a proof that all rational instances attain it. + +## A rejected intermediate lemma + +The tempting statement “eight rows of rank three with no ordered +four-block must contain an independent triple” is false over Q. The +retained exact counterexample is: + +```text +P = [(1,0,0), (0,-1,1), (-1,1,0), (0,1,0), + (-1,1,-1), (1,0,0), (0,0,1), (0,0,1)] +Q = [(1,0,0), (0,0,1), (0,1,0), (1,1,0), + (1,0,0), (1,1,1), (0,1,1), (0,0,1)] +``` + +Its product has rank three and nonzero diagonal. All 1,680 ordered +four-tuples fail, and none of its 56 triples is independent in the graph +joining pairs with at least one nonzero directed entry. Its canonical +ties all have cardinality one, so full anchors retain all eight rows. +It refutes the intermediate matrix lemma, not an anchor-box bound. + +## Reproduction and evidence + +From the repository root, using CPython 3.12: + +```sh +python3 -B scripts/research_package.py --package research/fstar-twelve-line-obstruction --check-only +python3.12 -B scripts/research_package.py --package research/fstar-twelve-line-obstruction +python3 -B scripts/check_research_commit.py --package research/fstar-twelve-line-obstruction --check-source-history +``` + +`VERIFY.json` registers normal and isolated/optimized/warnings-as-errors +replays. `verify.py` and `RESULT.json` provide finite exact controls for +the constructions and proof branches, the F₂ multiplicity count, positive +anchor witnesses, and the rejected shortcut. The frozen independent box +oracle is authenticated before execution. These controls are not formal +proof checking or an exhaustive search of rational matrices. Bounded +discovery searches are not premises and are not publication artifacts. + +New work is Apache-2.0, by Sagar Thakrar with substantial OpenAI Codex +assistance. Separate same-session agents contributed proof, controls and +review; this is not independent human acceptance. `SOURCES.json` preserves +the exact oracle lineage and predecessor attribution, including +DreamingOfClouds's F-star definitions and Aaron Wang/navinor's directed +box, SG and rational-core work. The selected frontier and κ are unchanged. + +## Open next questions + +1. Exclude or realize the residual rational matrix class: rank three, + direction multiplicities at most two, and zero degrees at most five. + An exact counterexample must check all ordered-block alternatives, + not only the four-plus-four split. +2. If that sufficient route fails, inspect its actual canonical anchors. + The rational twelve-line target only remains open when all ties have + cardinality two; a zero-diagonal F₂ reduction cannot use this package's + finite-field theorem. + +Coordination: [canonical claim and handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19009506). diff --git a/research/fstar-twelve-line-obstruction/RESULT.json b/research/fstar-twelve-line-obstruction/RESULT.json new file mode 100644 index 0000000000..baa5869ddd --- /dev/null +++ b/research/fstar-twelve-line-obstruction/RESULT.json @@ -0,0 +1,1885 @@ +{ + "controls": { + "F2_residual_capacity": { + "absent_point_patterns": 7, + "capacity_histogram": { + "10": 21, + "6": 7 + }, + "count": 28, + "patterns": [ + { + "P_capacity": 6, + "Q_weights": [ + 0, + 2, + 2, + 2, + 2, + 2, + 2 + ], + "allowed_P": [ + 2, + 4, + 6 + ] + }, + { + "P_capacity": 6, + "Q_weights": [ + 2, + 0, + 2, + 2, + 2, + 2, + 2 + ], + "allowed_P": [ + 1, + 4, + 5 + ] + }, + { + "P_capacity": 6, + "Q_weights": [ + 2, + 2, + 0, + 2, + 2, + 2, + 2 + ], + "allowed_P": [ + 3, + 4, + 7 + ] + }, + { + "P_capacity": 6, + "Q_weights": [ + 2, + 2, + 2, + 0, + 2, + 2, + 2 + ], + "allowed_P": [ + 1, + 2, + 3 + ] + }, + { + "P_capacity": 6, + "Q_weights": [ + 2, + 2, + 2, + 2, + 0, + 2, + 2 + ], + "allowed_P": [ + 2, + 5, + 7 + ] + }, + { + "P_capacity": 6, + "Q_weights": [ + 2, + 2, + 2, + 2, + 2, + 0, + 2 + ], + "allowed_P": [ + 1, + 6, + 7 + ] + }, + { + "P_capacity": 6, + "Q_weights": [ + 2, + 2, + 2, + 2, + 2, + 2, + 0 + ], + "allowed_P": [ + 3, + 5, + 6 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 1, + 1, + 2, + 2, + 2, + 2, + 2 + ], + "allowed_P": [ + 1, + 2, + 4, + 5, + 6 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 1, + 2, + 1, + 2, + 2, + 2, + 2 + ], + "allowed_P": [ + 2, + 3, + 4, + 6, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 1, + 2, + 2, + 1, + 2, + 2, + 2 + ], + "allowed_P": [ + 1, + 2, + 3, + 4, + 6 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 1, + 2, + 2, + 2, + 1, + 2, + 2 + ], + "allowed_P": [ + 2, + 4, + 5, + 6, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 1, + 2, + 2, + 2, + 2, + 1, + 2 + ], + "allowed_P": [ + 1, + 2, + 4, + 6, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 1, + 2, + 2, + 2, + 2, + 2, + 1 + ], + "allowed_P": [ + 2, + 3, + 4, + 5, + 6 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 1, + 1, + 2, + 2, + 2, + 2 + ], + "allowed_P": [ + 1, + 3, + 4, + 5, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 1, + 2, + 1, + 2, + 2, + 2 + ], + "allowed_P": [ + 1, + 2, + 3, + 4, + 5 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 1, + 2, + 2, + 1, + 2, + 2 + ], + "allowed_P": [ + 1, + 2, + 4, + 5, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 1, + 2, + 2, + 2, + 1, + 2 + ], + "allowed_P": [ + 1, + 4, + 5, + 6, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 1, + 2, + 2, + 2, + 2, + 1 + ], + "allowed_P": [ + 1, + 3, + 4, + 5, + 6 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 2, + 1, + 1, + 2, + 2, + 2 + ], + "allowed_P": [ + 1, + 2, + 3, + 4, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 2, + 1, + 2, + 1, + 2, + 2 + ], + "allowed_P": [ + 2, + 3, + 4, + 5, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 2, + 1, + 2, + 2, + 1, + 2 + ], + "allowed_P": [ + 1, + 3, + 4, + 6, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 2, + 1, + 2, + 2, + 2, + 1 + ], + "allowed_P": [ + 3, + 4, + 5, + 6, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 2, + 2, + 1, + 1, + 2, + 2 + ], + "allowed_P": [ + 1, + 2, + 3, + 5, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 2, + 2, + 1, + 2, + 1, + 2 + ], + "allowed_P": [ + 1, + 2, + 3, + 6, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 2, + 2, + 1, + 2, + 2, + 1 + ], + "allowed_P": [ + 1, + 2, + 3, + 5, + 6 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 2, + 2, + 2, + 1, + 1, + 2 + ], + "allowed_P": [ + 1, + 2, + 5, + 6, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 2, + 2, + 2, + 1, + 2, + 1 + ], + "allowed_P": [ + 2, + 3, + 5, + 6, + 7 + ] + }, + { + "P_capacity": 10, + "Q_weights": [ + 2, + 2, + 2, + 2, + 2, + 1, + 1 + ], + "allowed_P": [ + 1, + 3, + 5, + 6, + 7 + ] + } + ], + "relaxing_zero_cap_to_six_loses_this_contradiction": true, + "two_singleton_patterns": 21 + }, + "boundaries": [ + "zero_diagonal", + "empty_ties", + "SG", + "rank_four", + "submask_corruption", + "directed_order_reversal", + "rank_two_directed_cycle", + "source_corruption_before_execution" + ], + "odd_global_anchors": { + "P": [ + [ + -1, + -2, + 0 + ], + [ + -1, + -3, + 0 + ], + [ + -1, + -3, + 0 + ], + [ + -1, + -3, + 0 + ], + [ + 1, + -1, + -2 + ], + [ + 1, + -1, + -2 + ], + [ + 1, + -1, + -2 + ], + [ + 1, + -1, + -2 + ], + [ + 3, + 3, + 3 + ], + [ + 3, + 3, + 3 + ], + [ + 3, + 3, + 3 + ], + [ + 3, + 3, + 3 + ] + ], + "Q": [ + [ + 1, + -3, + 2 + ], + [ + 1, + -3, + 2 + ], + [ + 1, + -3, + 2 + ], + [ + 1, + -3, + 2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + 2 + ], + [ + 3, + -1, + 2 + ], + [ + 3, + -1, + 2 + ], + [ + 3, + -1, + 2 + ] + ], + "anchors_recomputed_on_subset": false, + "first_block": [ + 4, + 5, + 6, + 7 + ], + "global_a0": [ + 1, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 7, + 7, + 7, + 7 + ], + "global_b0": [ + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3 + ], + "moving_odd_row_after_suffix_rejected": true, + "odd_row": 0, + "rank": 3, + "second_block": [ + 8, + 9, + 10 + ], + "tau": [ + 1, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2 + ], + "total_kept": 8, + "witness": { + "a": [ + 1, + 0, + 0, + 0, + 3, + 3, + 3, + 3, + 1, + 1, + 1, + 0 + ], + "b": [ + 3, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 3, + 3, + 3, + 0 + ], + "kept": [ + 4, + 5, + 6, + 7, + 0, + 8, + 9, + 10 + ], + "order": [ + 4, + 5, + 6, + 7, + 0, + 8, + 9, + 10 + ] + } + }, + "rank_two_partition": { + "P": [ + [ + 1, + 0 + ], + [ + 1, + -1 + ], + [ + 0, + 1 + ], + [ + 1, + -1 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "Q": [ + [ + 1, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 1 + ], + [ + 1, + 1 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ], + "absent_kernel_prefix_blocks": [ + [ + 7, + 0, + 6, + 4, + 5 + ], + [ + 1, + 2, + 3 + ] + ], + "class_orders_checked": 6, + "dependent_prefixes_rejected": true, + "empty_block_with_absent_kernel": [ + [ + 1, + 0 + ], + [] + ], + "free_endpoint_rows": [ + 6, + 7 + ], + "one_prefix_blocks": [ + [ + 2, + 7, + 4, + 5 + ], + [ + 3, + 0, + 1, + 6 + ] + ], + "one_prefix_total": 9, + "rank": 2, + "reverse_order_mutant_rejected": true, + "two_prefix_blocks": [ + [ + 4, + 2, + 3, + 7 + ], + [ + 5, + 0, + 1, + 6 + ] + ], + "two_prefix_total": 10, + "two_prefixes": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ] + }, + "repeated_direction": { + "C": [ + 3, + 4, + 5 + ], + "P": [ + [ + 1, + 0, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 0, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 0, + 1, + 0 + ], + [ + 1, + 2, + 0 + ], + [ + 1, + 0, + 0 + ], + [ + 2, + 1, + 0 + ], + [ + 1, + 0, + 1 + ], + [ + 2, + 0, + 1 + ] + ], + "Q": [ + [ + 1, + 0, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 0, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 0 + ], + [ + 1, + 0, + 0 + ], + [ + 0, + 1, + -1 + ], + [ + 0, + 1, + -1 + ], + [ + 1, + 0, + -1 + ], + [ + 1, + 0, + -1 + ], + [ + 1, + -1, + 0 + ], + [ + 1, + -1, + 0 + ] + ], + "S": [ + 0, + 1, + 2 + ], + "Z": [ + 6, + 7, + 8, + 9, + 10, + 11 + ], + "Z_rank": 2, + "hypothetical_three_pair_blocks_rank": 3, + "multiplicity_three_is_not_a_universal_admission_error": true, + "pair_isolation_inconsistent_systems": 3, + "rank": 3, + "two_four_blocks": [ + [ + 1, + 6, + 10, + 11 + ], + [ + 3, + 4, + 5, + 0 + ] + ] + }, + "zero_six_two_plane_combination": { + "P": [ + [ + 1, + 0, + 0 + ], + [ + 1, + 0, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + 1, + 1, + 0 + ], + [ + 1, + 1, + 0 + ], + [ + 0, + 1, + 1 + ], + [ + 0, + 1, + 2 + ], + [ + 0, + 1, + 3 + ], + [ + 0, + 1, + 4 + ], + [ + 1, + 0, + 1 + ], + [ + 1, + 0, + -1 + ] + ], + "Q": [ + [ + 1, + 0, + 0 + ], + [ + 1, + 0, + 1 + ], + [ + 1, + 1, + 0 + ], + [ + 1, + 2, + 0 + ], + [ + 1, + 3, + 0 + ], + [ + 1, + 4, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 1, + 1 + ], + [ + 0, + 1, + -1 + ], + [ + 0, + 1, + 2 + ], + [ + 0, + 0, + 1 + ], + [ + 0, + 0, + 1 + ] + ], + "Z": [ + 6, + 7, + 8, + 9, + 10, + 11 + ], + "blocks": [ + [ + 2, + 3, + 4, + 5, + 8, + 6, + 7, + 9 + ], + [] + ], + "cross_rectangle_nonzero": true, + "rank": 3, + "removed_C": [ + 0, + 1 + ], + "removed_D": [ + 10, + 11 + ], + "total_kept": 8, + "zero_row": 0 + } + }, + "inputs_sha256": { + "inputs/pr3393-independent_box.py": "6792f0c92943e418d93ae6bc8b616447efc2a505612c87c011a36025d98f814d" + }, + "rational_eight_counterexample": { + "M": [ + [ + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 0, + 1, + -1, + -1, + 0, + 0, + 0, + 1 + ], + [ + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0 + ], + [ + 0, + 0, + 1, + 1, + 0, + 1, + 1, + 0 + ], + [ + -1, + -1, + 1, + 0, + -1, + -1, + 0, + -1 + ], + [ + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 1, + 1, + 1 + ], + [ + 0, + 1, + 0, + 0, + 0, + 1, + 1, + 1 + ] + ], + "P": [ + [ + 1, + 0, + 0 + ], + [ + 0, + -1, + 1 + ], + [ + -1, + 1, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + -1, + 1, + -1 + ], + [ + 1, + 0, + 0 + ], + [ + 0, + 0, + 1 + ], + [ + 0, + 0, + 1 + ] + ], + "Q": [ + [ + 1, + 0, + 0 + ], + [ + 0, + 0, + 1 + ], + [ + 0, + 1, + 0 + ], + [ + 1, + 1, + 0 + ], + [ + 1, + 0, + 0 + ], + [ + 1, + 1, + 1 + ], + [ + 0, + 1, + 1 + ], + [ + 0, + 0, + 1 + ] + ], + "a0": [ + 1, + 6, + 3, + 2, + 7, + 1, + 4, + 4 + ], + "b0": [ + 1, + 4, + 2, + 3, + 1, + 7, + 6, + 4 + ], + "exact_box": 8, + "gamma": 0, + "has_independent_triple": false, + "has_ordered_four": false, + "independent_triples_checked": 56, + "ordered_four_orders_checked": 1680, + "rank": 3, + "scope": "Counterexample to the proposed eight-row intermediate lemma; not a box-floor counterexample.", + "tau": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "witness": { + "a": [ + 1, + 6, + 3, + 2, + 7, + 1, + 4, + 4 + ], + "b": [ + 1, + 4, + 2, + 3, + 1, + 7, + 6, + 4 + ], + "kept": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "order": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ] + } + }, + "schema_version": 1, + "scope": "Finite exact controls for analytic residual reductions and the F2 theorem; the rational twelve-line box>=8 target remains open.", + "status": "PASS_FSTAR_TWELVE_LINE_OBSTRUCTION", + "working_fixture": { + "M": [ + [ + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 12, + 12, + 12, + 12 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 12, + 12, + 12, + 12 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 12, + 12, + 12, + 12 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 12, + 12, + 12, + 12 + ] + ], + "P": [ + [ + -1, + -3, + 0 + ], + [ + -1, + -3, + 0 + ], + [ + -1, + -3, + 0 + ], + [ + -1, + -3, + 0 + ], + [ + 1, + -1, + -2 + ], + [ + 1, + -1, + -2 + ], + [ + 1, + -1, + -2 + ], + [ + 1, + -1, + -2 + ], + [ + 3, + 3, + 3 + ], + [ + 3, + 3, + 3 + ], + [ + 3, + 3, + 3 + ], + [ + 3, + 3, + 3 + ] + ], + "Q": [ + [ + 1, + -3, + 2 + ], + [ + 1, + -3, + 2 + ], + [ + 1, + -3, + 2 + ], + [ + 1, + -3, + 2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + 2 + ], + [ + 3, + -1, + 2 + ], + [ + 3, + -1, + 2 + ], + [ + 3, + -1, + 2 + ] + ], + "a0": [ + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 7, + 7, + 7, + 7 + ], + "b0": [ + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3 + ], + "exact_box": 8, + "gamma": 0, + "rank": 3, + "tau": [ + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2 + ], + "upper_bound": "Every nine-set meets three zero-separated groups: a triangular rank3 label minor contradicts the rank2 target-label space.", + "witness": { + "a": [ + 3, + 3, + 3, + 3, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0 + ], + "b": [ + 1, + 1, + 1, + 1, + 3, + 3, + 3, + 3, + 0, + 0, + 0, + 0 + ], + "kept": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "order": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ] + } + } +} diff --git a/research/fstar-twelve-line-obstruction/SOURCES.json b/research/fstar-twelve-line-obstruction/SOURCES.json new file mode 100644 index 0000000000..6f8956c911 --- /dev/null +++ b/research/fstar-twelve-line-obstruction/SOURCES.json @@ -0,0 +1,34 @@ +{ + "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" + } + ], + "attribution": { + "frozen_oracle": "Sagar Thakrar with substantial OpenAI Codex assistance, corrected PR3393; target-first Gaussian oracle, Apache-2.0. Exported unchanged through PR3435 at 0833fff0bdc9acdd3b174c7677ab1b46873b22d3 (whose own export was through PR3420 at e2d39da9c7109f361d6cff677cf9f8eba51f3dd6); original bytes and origin remain pinned above.", + "definition_and_sharp_core": "Aaron Wang/navinor: directed sub-anchor box and SG/valuation lineage through PR2914 and PR3031; PR2978 three-line rational core. PR3031's retained definition engine is Git blob 9d8285e4e379d883c3c5ee8d95b0e1777ed866d8, SHA256 4e5a25152de0d4462fe1c987d4f6ea70f9e267ce7307a71f1586c45b518268ea at commit e75906fc4e8b9f756a9877b2e467f4e564851c7d.", + "fstar_origin": "DreamingOfClouds, PR1590 and PR2111; F-star/certificate definitions and original fixtures, with source-specific assistance disclosures retained there.", + "related_predecessors": "Sagar Thakrar with OpenAI Codex assistance: PR3420 at e2d39da9c7109f361d6cff677cf9f8eba51f3dd6, research/fstar-nine-line-floor/PROOF.md, seven-row ordered-triple lemma; PR3435 at 0833fff0bdc9acdd3b174c7677ab1b46873b22d3, research/fstar-eleven-line-floor/PROOF.md, eleven-row four-plus-three theorem and rank-two half-size starting point; PR3409/3420 asymmetric two-block transfer. These are retained analytic premises, not newly proved or formally checked by this verifier.", + "this_package": "Sagar Thakrar with substantial OpenAI Codex assistance; rank-two full partition and prescribed-prefix extension, twelve-row obstruction reduction and F_2 exclusion, odd-tie rational corollary, exact rational counterexample to the speculative eight-row shortcut, and finite controls. Separate same-session proof, controls and review agents assisted. These reviews are not independent human acceptance or formal proof." + } +} diff --git a/research/fstar-twelve-line-obstruction/TASK.json b/research/fstar-twelve-line-obstruction/TASK.json new file mode 100644 index 0000000000..92929465a7 --- /dev/null +++ b/research/fstar-twelve-line-obstruction/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": "Characterize any twelve-row rank-at-most-three matrix obstruction to two ordered nonzero blocks of total size eight; exclude every such obstruction over F_2, and settle the rational anchor case with at least one odd tied cardinality. The general rational twelve-line box>=8 question remains open.", + "scope_change_reason": "Handoff-first continuation of PR3435 after refreshed canonical main/revision6 and complete open/closed PR and Discussion overlap checks. A full rational proof was not obtained; the useful independently reviewable result is an arbitrary-field structural reduction, its F_2 corollary, and an exact counterexample to a tempting intermediate lemma.", + "bottleneck_link": "Narrows the unresolved twelve-line F-star threshold to rank-three all-even-tie instances and restricts failures of the sufficient two-block route. It does not claim that the stronger matrix route is necessary for a box witness.", + "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": "partial", + "evidence": "PROOF.md proves rank-two partitions, prescribed prefix extensions, factor multiplicity and zero-degree bounds for a twelve-row obstruction, and the F_2 incidence contradiction. Exact controls include the rational eight-row no-four/no-independent-triple counterexample, positive anchor witnesses and source binding. Bounded discovery searches are not proof premises.", + "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": "Can a rational twelve-row rank-three matrix with nonzero diagonal fail to contain two ordered nonzero blocks of total size eight?", + "why_it_matters": "A negative answer would settle the twelve-line box floor by the retained asymmetric transfer.", + "first_step": "Study only factor multiplicities at most two and zero row/column degrees at most five; PROOF.md excludes every other case. The F_2 argument does not extend merely by reducing rational factors modulo two.", + "blocked_by": "The projective line count is specific to the seven directions over F_2; no general-field exclusion of the residual class is proved." + }, + { + "question": "If the stronger two-block condition fails, do all rational twelve-line canonical anchor instances still have box>=8?", + "why_it_matters": "Two-block witnesses are sufficient, not necessary. A matrix obstruction alone is not an F-star counterexample.", + "first_step": "Keep nonempty canonical ties, actual rational valuations and the directed order. The odd-tie case is settled here, leaving only tied cardinality two on every row.", + "blocked_by": "Canonical reductions of the remaining all-even case have zero diagonal over F_2, so the finite-field theorem's nonzero-diagonal hypothesis fails." + } + ] +} diff --git a/research/fstar-twelve-line-obstruction/VERIFY.json b/research/fstar-twelve-line-obstruction/VERIFY.json new file mode 100644 index 0000000000..927cca2213 --- /dev/null +++ b/research/fstar-twelve-line-obstruction/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": "Exact finite controls for the analytic obstruction reduction, all F_2 multiplicity patterns, positive box witnesses and the rational eight-row shortcut counterexample; authenticate the frozen oracle. The general rational twelve-line threshold is not claimed solved." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-Werror", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Replay the same semantic and source rejection controls under isolation, optimization and warnings-as-errors; no finite matrix census or formal proof claim." + } + ] +} diff --git a/research/fstar-twelve-line-obstruction/inputs/pr3393-independent_box.py b/research/fstar-twelve-line-obstruction/inputs/pr3393-independent_box.py new file mode 100644 index 0000000000..d15e05f45e --- /dev/null +++ b/research/fstar-twelve-line-obstruction/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-twelve-line-obstruction/verify.py b/research/fstar-twelve-line-obstruction/verify.py new file mode 100644 index 0000000000..80eb105190 --- /dev/null +++ b/research/fstar-twelve-line-obstruction/verify.py @@ -0,0 +1,412 @@ +#!/usr/bin/env python3 +"""Exact finite controls for the twelve-line obstruction reductions. + +SPDX-License-Identifier: Apache-2.0 +Sagar Thakrar (thakrarsagar), with substantial OpenAI Codex assistance. +Small exact helpers follow the author's PR3435 verifier; the PR3393 oracle +is retained unchanged. This is not a proof by exhaustive rational search. +""" + +from fractions import Fraction +import hashlib +from itertools import combinations, permutations +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" + + +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 rank(matrix): + rows = [[Fraction(value) for value in row] for row in matrix] + 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: + multiplier = row[column] + rows[i] = [x - multiplier * y for x, y in zip(row, rows[cursor])] + cursor += 1 + return cursor + + +def dot(left, right): + return sum(x * y for x, y in zip(left, right)) + + +def product(p, q): + return [[dot(left, right) for right in q] for left in p] + + +def projective(vector): + vector = tuple(map(Fraction, vector)) + first = next((value for value in vector if value), None) + require(first is not None, "zero projective vector") + return tuple(value / first for value in vector) + + +def ordered(matrix, indices): + return len(indices) == len(set(indices)) and all(matrix[i][j] + for position, i in enumerate(indices) for j in indices[position + 1:]) + + +def find_ordered(matrix, size, allowed=None): + allowed = range(len(matrix)) if allowed is None else allowed + for subset in combinations(allowed, size): + for order in permutations(subset): + if ordered(matrix, order): + return order + return None + + +def partition(p, q, prefixes=(), class_order=None): + """Exact rank-two class partition; up to two outside prefix rows.""" + matrix = product(p, q) + require(len(p) == len(q) and all(matrix[i][i] for i in range(len(p))), "zero diagonal") + require(rank(q) <= 2 and rank(matrix) <= 2, "rank-two plane required") + require(len(prefixes) <= 2, "at most two prefixes") + classes = sorted({projective(row) for row in q}) + owner = [classes.index(projective(row)) for row in q] + forbidden = [{owner[j] for j in range(len(q)) if not matrix[i][j]} + for i in range(len(p))] + require(all(len(values) <= 1 and owner[i] not in values + for i, values in enumerate(forbidden)), "forbidden class failed") + restrictions = [[dot(prefix, row) for row in q] for prefix in prefixes] + require(rank(restrictions) == len(prefixes), "prefix restrictions must be nonzero and independent") + endpoints = [{owner[j] for j, value in enumerate(row) if not value} for row in restrictions] + require(all(len(values) <= 1 for values in endpoints), "prefix kernel class failed") + first = next(iter(endpoints[0]), None) if endpoints else None + last = next(iter(endpoints[1]), None) if len(endpoints) == 2 else None + sequence = ([first] if first is not None else []) + sequence += [i for i in range(len(classes)) if i not in (first, last)] + sequence += [last] if last is not None else [] + if class_order is not None: + require(not prefixes and sorted(class_order) == list(range(len(classes))), "invalid class order") + sequence = list(class_order) + position = {value: i for i, value in enumerate(sequence)} + forward, backward = [], [] + for i, zero in enumerate(forbidden): + to_forward = position[next(iter(zero))] < position[owner[i]] if zero else owner[i] != first + (forward if to_forward else backward).append(i) + forward.sort(key=lambda i: (position[owner[i]], i)) + backward.sort(key=lambda i: (-position[owner[i]], i)) + require(ordered(matrix, forward) and ordered(matrix, backward), "rank-two order failed") + require(sorted(forward + backward) == list(range(len(p))), "partition lost an index") + for prefix, block in zip(prefixes, (forward, backward)): + require(all(dot(prefix, q[i]) for i in block), "prefix hits its forbidden class") + return forward, backward + + +def parity(left, right): + return (left & right).bit_count() & 1 + + +def literal_check(matrix, a0, b0, witness): + order, kept, a, b = (witness[key] for key in ("order", "kept", "a", "b")) + if len(a) != len(a0) or len(b) != len(b0) or sorted(order) != sorted(kept): + return False + if len(set(kept)) != len(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 + parity(a[i], b[i]) != 1 for i in kept): + return False + return all(matrix[i][j] or not parity(a[i], b[j]) + for k, i in enumerate(order) for j in order[k + 1:]) + + +def labelled_blocks(matrix, a0, b0, first, second): + require(all(matrix[i][i] for i in range(len(matrix))), "zero diagonal") + require(rank(matrix) <= 3, "rank exceeds three") + require(all(a & b for a, b in zip(a0, b0)), "empty tied set") + require(all(matrix[i][j] or not parity(a0[i], b0[j]) + for i in range(len(matrix)) for j in range(len(matrix))), "SG failed") + require(set(first).isdisjoint(second) and ordered(matrix, first) and ordered(matrix, second), + "blocks are not disjoint directed orders") + a, b = [0] * len(matrix), [0] * len(matrix) + for i in first: + tied = a0[i] & b0[i] + a[i], b[i] = a0[i], tied & -tied + for i in second: + tied = a0[i] & b0[i] + a[i], b[i] = tied & -tied, b0[i] + kept = list(first) + list(second) + witness = {"a": a, "b": b, "kept": kept, "order": kept} + require(literal_check(matrix, a0, b0, witness), "literal directed box failed") + return witness + + +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 rank_two_controls(): + p = [(1, 0), (1, -1), (0, 1), (1, -1), (0, 1), (1, 0), (1, 2), (2, 1)] + q = [(1, 0), (1, 0), (0, 1), (0, 1), (1, 1), (1, 1), (1, 0), (0, 1)] + matrix = product(p, q) + partitions = [partition(p, q, class_order=order) for order in permutations(range(3))] + require(len(partitions) == 6 and rank(matrix) == 2, "rank-two fixture failed") + a, b = (0, 1), (1, 0) + first, second = partition(p, q, (a, b)) + require(6 in second and 7 in first, "free endpoint rows assigned incorrectly") + require(not dot(a, q[6]) and not dot(b, q[7]), "endpoint mutation not observable") + one = partition(p, q, (a,)) + absent = partition(p, q, ((1, 3),)) + empty = partition([(1, 2), (2, 1)], [(1, 0), (0, 1)], ((1, 1),)) + require(sorted(empty[0]) == [0, 1] and not empty[1], "empty block or absent kernel mishandled") + rejects(lambda: partition(p, q, (a, (0, 2))), "independent") + rejects(lambda: partition(p, q, ((0, 0),)), "nonzero") + reversed_failure = any(not ordered(matrix, list(reversed(block))) + for blocks in partitions for block in blocks) + require(reversed_failure, "orientation mutation was invisible") + scaled = [tuple(Fraction(-2, 3) * x for x in row) for row in q] + require(partition(p, scaled, (a, b)) == (first, second), "projective scaling changed partition") + return {"P": p, "Q": q, "rank": 2, "class_orders_checked": 6, + "two_prefixes": [a, b], "two_prefix_blocks": [first, second], + "two_prefix_total": 10, "one_prefix_blocks": one, "one_prefix_total": 9, + "absent_kernel_prefix_blocks": absent, "free_endpoint_rows": [6, 7], + "empty_block_with_absent_kernel": empty, + "reverse_order_mutant_rejected": True, "dependent_prefixes_rejected": True} + + +def repeated_direction_controls(): + basis = [[int(i == j) for j in range(3)] for i in range(3)] + p = basis + [[1, 1, 1]] * 3 + [[0, 1, 0], [1, 2, 0], [1, 0, 0], + [2, 1, 0], [1, 0, 1], [2, 0, 1]] + directions = [(0, 1, -1), (1, 0, -1), (1, -1, 0)] + q = basis + [[1, 1, 1], [1, 1, 0], [1, 0, 0]] + [list(row) for row in directions for _ in range(2)] + matrix = product(p, q) + require(rank(matrix) == 3 and all(matrix[i][i] for i in range(12)), "repeated fixture failed") + require(all(not matrix[i][j] for i in (3, 4, 5) for j in range(6, 12)), "common annihilator failed") + require(all(matrix[i][j] for i in (3, 4, 5) for j in range(3)), "independent S failed") + first, second = [1, 6, 10, 11], [3, 4, 5, 0] + require(ordered(matrix, first) and ordered(matrix, second) and set(first).isdisjoint(second), "repeated branch witness failed") + require(rank([row[6:] for row in matrix[6:]]) == 2, "Z is not rank two") + require(all(sum(row) == 0 and sum(x == 0 for x in row) == 1 for row in directions), "coordinate-plane premise failed") + impossible = [[int(i // 2 == j // 2) for j in range(6)] for i in range(6)] + require(rank(impossible) == 3, "isolated pair blocks lost rank") + for target in range(3): + require(rank([list(row) + [int(i == target)] for i, row in enumerate(directions)]) == 3, + "isolating one coordinate-plane pair became solvable") + require(projective([-2, -2, -2]) == projective([Fraction(3, 5)] * 3), "projective equality failed") + require(ordered([[1] * 3 for _ in range(3)], [0, 1, 2]), "small multiplicity control failed") + return {"P": p, "Q": q, "rank": 3, "C": [3, 4, 5], "S": [0, 1, 2], + "Z": list(range(6, 12)), "two_four_blocks": [first, second], "Z_rank": 2, + "hypothetical_three_pair_blocks_rank": 3, "pair_isolation_inconsistent_systems": 3, + "multiplicity_three_is_not_a_universal_admission_error": True} + + +def two_plane_controls(): + p = [(1, 0, 0)] * 2 + [(0, 1, 0)] * 2 + [(1, 1, 0)] * 2 + p += [(0, 1, 1), (0, 1, 2), (0, 1, 3), (0, 1, 4), (1, 0, 1), (1, 0, -1)] + q = [(1, 0, 0), (1, 0, 1), (1, 1, 0), (1, 2, 0), (1, 3, 0), (1, 4, 0)] + q += [(0, 1, 0), (0, 1, 1), (0, 1, -1), (0, 1, 2), (0, 0, 1), (0, 0, 1)] + matrix = product(p, q) + require(rank(matrix) == 3 and all(matrix[i][i] for i in range(12)), "two-plane diagonal failed") + require([j for j, value in enumerate(matrix[0]) if not value] == list(range(6, 12)), "six-zero row failed") + for factors in (p, q): + directions = [projective(row) for row in factors] + require(max(directions.count(value) for value in directions) <= 2, "two-plane multiplicity failed") + y, z = list(range(2, 6)), list(range(6, 10)) + left = partition([p[i][:2] for i in y], [q[i][:2] for i in y]) + right = partition([p[i][1:] for i in z], [q[i][1:] for i in z]) + blocks = [[y[i] for i in a] + [z[i] for i in b] for a, b in zip(left, right)] + require(all(matrix[i][j] for i in y for j in z), "cross-plane complete rectangle failed") + require(all(ordered(matrix, block) for block in blocks) and sum(map(len, blocks)) == 8, + "two-plane concatenation failed") + return {"P": p, "Q": q, "rank": 3, "zero_row": 0, "Z": list(range(6, 12)), + "removed_C": [0, 1], "removed_D": [10, 11], "blocks": blocks, + "total_kept": 8, "cross_rectangle_nonzero": True} + + +def f2_controls(): + points = list(range(1, 8)) + lines = {p: [q for q in points if not parity(p, q)] for p in points} + require(all(len(line) == 3 for line in lines.values()), "Fano line size failed") + patterns = [tuple(0 if q == missing else 2 for q in points) for missing in points] + patterns += [tuple(1 if q in singles else 2 for q in points) for singles in combinations(points, 2)] + records = [] + for weights in patterns: + require(sum(weights) == 12 and max(weights) == 2, "F2 multiplicity pattern failed") + zeros = {p: sum(weights[q - 1] for q in line) for p, line in lines.items()} + allowed = [p for p in points if zeros[p] <= 5] + light = [q for q in points if weights[q - 1] < 2] + require(allowed == [p for p in points if any(q in lines[p] for q in light)], "pencil classification failed") + require(len(allowed) == (3 if 0 in weights else 5) and 2 * len(allowed) < 12, + "F2 residual capacity contradiction failed") + require(len([p for p in points if zeros[p] <= 6]) == 7, "zero-six relaxation not observable") + records.append({"Q_weights": weights, "allowed_P": allowed, "P_capacity": 2 * len(allowed)}) + return {"patterns": records, "count": 28, "absent_point_patterns": 7, + "two_singleton_patterns": 21, "capacity_histogram": {"6": 7, "10": 21}, + "relaxing_zero_cap_to_six_loses_this_contradiction": True} + + +def core_fixture(oracle): + p0 = [(-1, -3, 0), (1, -1, -2), (3, 3, 3)] + q0 = [(1, -3, 2), (3, -1, -2), (3, -1, 2)] + p, q = ([row for row in factors for _ in range(4)] for factors in (p0, q0)) + data = oracle.rational_data(p, q) + matrix = product(p, q) + require(matrix == data["M"] and rank(matrix) == 3 and data["tau"] == [2] * 12, "core normalization failed") + require(data["a0"] == [3] * 8 + [7] * 4 and data["b0"] == [3] * 12 and data["gamma"] == 0, + "core anchor values failed") + first = find_ordered(matrix, 4) + second = find_ordered(matrix, 4, [i for i in range(12) if i not in first]) + require(first is not None and second is not None, "working fixture two blocks missing") + witness = labelled_blocks(matrix, data["a0"], data["b0"], first, second) + require(oracle.check_witness(data["a0"], data["b0"], data["arcs"], witness), "frozen definition disagrees") + require(all(len({i // 4 for i in subset}) == 3 for subset in combinations(range(12), 9)), "nine-set upper bound failed") + record = {"P": p, "Q": q, "M": matrix, "rank": 3, "gamma": 0, "a0": data["a0"], + "b0": data["b0"], "tau": data["tau"], "exact_box": 8, "witness": witness, + "upper_bound": "Every nine-set meets three zero-separated groups: a triangular rank3 label minor contradicts the rank2 target-label space."} + return record, data + + +def rational_eight_control(oracle): + p = [[1, 0, 0], [0, -1, 1], [-1, 1, 0], [0, 1, 0], + [-1, 1, -1], [1, 0, 0], [0, 0, 1], [0, 0, 1]] + q = [[1, 0, 0], [0, 0, 1], [0, 1, 0], [1, 1, 0], + [1, 0, 0], [1, 1, 1], [0, 1, 1], [0, 0, 1]] + data = oracle.rational_data(p, q) + matrix = product(p, q) + require(rank(matrix) == 3 and all(matrix[i][i] for i in range(8)), "rational lift rank failed") + require(find_ordered(matrix, 4) is None, "rational lift contains an ordered four") + require(not any(all(not matrix[i][j] and not matrix[j][i] for i, j in combinations(triple, 2)) + for triple in combinations(range(8), 3)), "rational lift contains an independent triple") + require(data["gamma"] == 0 and data["tau"] == [1] * 8, "rational lift normalization failed") + witness = {"a": data["a0"], "b": data["b0"], "kept": list(range(8)), "order": list(range(8))} + require(literal_check(matrix, data["a0"], data["b0"], witness) and oracle.check_witness( + data["a0"], data["b0"], data["arcs"], witness), "full eight-row box witness failed") + return {"P": p, "Q": q, "M": matrix, "rank": 3, "ordered_four_orders_checked": 1680, + "independent_triples_checked": 56, "has_ordered_four": False, + "has_independent_triple": False, "gamma": 0, "tau": data["tau"], + "a0": data["a0"], "b0": data["b0"], "exact_box": 8, "witness": witness, + "scope": "Counterexample to the proposed eight-row intermediate lemma; not a box-floor counterexample."} + + +def odd_anchor_control(oracle): + p0 = [(-1, -3, 0), (1, -1, -2), (3, 3, 3)] + q0 = [(1, -3, 2), (3, -1, -2), (3, -1, 2)] + p, q = ([row for row in factors for _ in range(4)] for factors in (p0, q0)) + p[0] = (-1, -2, 0) + data = oracle.rational_data(p, q) + require(data["rank"] == 3 and data["gamma"] == 0 and data["tau"] == [1] + [2] * 11, + "one-odd fixture normalization failed") + first, second = list(range(4, 8)), list(range(8, 11)) + witness = labelled_blocks(data["M"], data["a0"], data["b0"], first, second) + # Keep the original twelve-row global anchors throughout the restriction. + witness["a"][0], witness["b"][0] = data["a0"][0], data["b0"][0] + witness["kept"] = witness["order"] = first + [0] + second + require(literal_check(data["M"], data["a0"], data["b0"], witness) and oracle.check_witness( + data["a0"], data["b0"], data["arcs"], witness), "full-anchor middle insertion failed") + require(data["M"][0][0] == 5 and data["a0"][0] == 1 and data["b0"][0] == 3, + "special odd row changed") + misplaced = {**witness, "order": first + second + [0]} + require(not literal_check(data["M"], data["a0"], data["b0"], misplaced) and not oracle.check_witness( + data["a0"], data["b0"], data["arcs"], misplaced), "odd row after suffix was accepted") + return {"P": p, "Q": q, "rank": 3, "tau": data["tau"], "global_a0": data["a0"], + "global_b0": data["b0"], "odd_row": 0, "first_block": first, "second_block": second, + "total_kept": 8, "witness": witness, "anchors_recomputed_on_subset": False, + "moving_odd_row_after_suffix_rejected": True} + + +def boundary_controls(oracle, data): + matrix, a0, b0 = data["M"], data["a0"], data["b0"] + first, second = list(range(4)), list(range(4, 8)) + zero = [row[:] for row in matrix] + zero[0][0] = 0 + rejects(lambda: labelled_blocks(zero, a0, b0, first, second), "zero diagonal") + empty = a0[:] + empty[0] = 0 + rejects(lambda: labelled_blocks(matrix, empty, b0, first, second), "empty tied set") + rejects(lambda: labelled_blocks(matrix, [1] * 12, [1] * 12, first, second), "SG failed") + rank_four = [[int(i // 3 == j // 3) for j in range(12)] for i in range(12)] + rejects(lambda: labelled_blocks(rank_four, [3] * 12, [3] * 12, [0], [3]), "rank exceeds three") + invalid = labelled_blocks(matrix, a0, b0, first, second) + invalid["a"][0] = 8 + require(not literal_check(matrix, a0, b0, invalid) and not oracle.check_witness( + a0, b0, data["arcs"], invalid), "submask corruption accepted") + directed = [[int(i <= j) for j in range(3)] for i in range(3)] + witness = {"a": [1] * 3, "b": [1] * 3, "kept": [0, 1, 2], "order": [0, 1, 2]} + arcs = [(i, j) for i in range(3) for j in range(3) if i != j and not directed[i][j]] + require(literal_check(directed, [1] * 3, [1] * 3, witness), "forward witness failed") + witness["order"] = [2, 1, 0] + require(not literal_check(directed, [1] * 3, [1] * 3, witness) and + not oracle.check_witness([1] * 3, [1] * 3, arcs, witness), "reversed witness accepted") + cycle = [[1, 1, 0], [0, 1, 1], [-1, 0, 1]] + require(rank(cycle) == 2 and find_ordered(cycle, 3) is None, "cycle mistaken for a directed order") + old_read = Path.read_bytes + def counterfeit(path): + return b'raise RuntimeError("counterfeit executed")\n' if path == HERE / ORACLE else old_read(path) + with patch.object(Path, "read_bytes", counterfeit): + rejects(load_oracle, "Input changed: " + ORACLE) + return ["zero_diagonal", "empty_ties", "SG", "rank_four", "submask_corruption", "directed_order_reversal", + "rank_two_directed_cycle", "source_corruption_before_execution"] + + +def build(): + authenticated = authenticate() + oracle = load_oracle() + fixture, data = core_fixture(oracle) + result = {"schema_version": 1, "status": "PASS_FSTAR_TWELVE_LINE_OBSTRUCTION", + "scope": "Finite exact controls for analytic residual reductions and the F2 theorem; the rational twelve-line box>=8 target remains open.", + "inputs_sha256": {path: hashlib.sha256(raw).hexdigest() for path, raw in authenticated.items()}, + "working_fixture": fixture, "rational_eight_counterexample": rational_eight_control(oracle), + "controls": {"rank_two_partition": rank_two_controls(), "repeated_direction": repeated_direction_controls(), + "zero_six_two_plane_combination": two_plane_controls(), "F2_residual_capacity": f2_controls(), + "odd_global_anchors": odd_anchor_control(oracle), + "boundaries": boundary_controls(oracle, data)}} + 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_TWELVE_LINE_OBSTRUCTION: exact controls; rational twelve-line target open") + + +if __name__ == "__main__": + main()