From 0833fff0bdc9acdd3b174c7677ab1b46873b22d3 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Sun, 18 Oct 2026 07:10:08 +0530 Subject: [PATCH] Research: prove the eleven-line anchor-box floor seven --- research/fstar-eleven-line-floor/PROOF.md | 230 +++++++ research/fstar-eleven-line-floor/README.md | 120 ++++ research/fstar-eleven-line-floor/RESULT.json | 616 ++++++++++++++++++ research/fstar-eleven-line-floor/SOURCES.json | 34 + research/fstar-eleven-line-floor/TASK.json | 66 ++ research/fstar-eleven-line-floor/VERIFY.json | 19 + .../inputs/pr3393-independent_box.py | 225 +++++++ research/fstar-eleven-line-floor/verify.py | 385 +++++++++++ 8 files changed, 1695 insertions(+) create mode 100644 research/fstar-eleven-line-floor/PROOF.md create mode 100644 research/fstar-eleven-line-floor/README.md create mode 100644 research/fstar-eleven-line-floor/RESULT.json create mode 100644 research/fstar-eleven-line-floor/SOURCES.json create mode 100644 research/fstar-eleven-line-floor/TASK.json create mode 100644 research/fstar-eleven-line-floor/VERIFY.json create mode 100644 research/fstar-eleven-line-floor/inputs/pr3393-independent_box.py create mode 100644 research/fstar-eleven-line-floor/verify.py diff --git a/research/fstar-eleven-line-floor/PROOF.md b/research/fstar-eleven-line-floor/PROOF.md new file mode 100644 index 0000000000..8d5ba85a4c --- /dev/null +++ b/research/fstar-eleven-line-floor/PROOF.md @@ -0,0 +1,230 @@ + + +# Eleven rational three-total lines have a seven-line box witness + +## Statements + +An ordered nonzero block of a matrix M is a sequence of distinct indices +such that M_ij is nonzero whenever i precedes j in the sequence. A block +of size three is called a transitive nonzero triple. + +We prove over an arbitrary field K: + +> Every eleven-by-eleven matrix of rank at most three with nonzero +> diagonal contains an ordered nonzero block of size four. + +Its seven-row complement contains a transitive nonzero triple by the +preceding seven-row matrix lemma. Thus there are disjoint ordered blocks +of sizes four and three. + +Consequently, if rational P,Q have eleven rows and three columns, +M=P Q^T has nonzero diagonal, and every canonical tied set is nonempty, +then the directed sub-anchor box satisfies **box(M)>=7**. This proof does +not claim sharpness of the seven-line floor. + +## Two preliminary matrix lemmas + +**Rank-two half-size lemma.** A matrix of rank at most two with nonzero +diagonal has an ordered nonzero block of size at least ceil(n/2). + +Write M_ij=p_i^T q_j with nonzero vectors p_i,q_i in K^2, and partition +the q_j into projective directions, meaning nonzero proportionality +classes. The zeros in row i consist of at most one complete class: +the kernel of the nonzero functional p_i^T has only one projective +direction. This forbidden class, if present, differs from i's own +class because M_ii is nonzero. + +Choose a uniformly random order of the finitely many classes. Retain +row i when its forbidden class is earlier than its own class, retaining +every row without a forbidden class. Order retained indices by their +classes, with arbitrary order inside each class. Every zero from a +retained row points to an earlier class; all entries within a class +are nonzero by the diagonal condition. The retained order is therefore +an ordered nonzero block. Each row is retained with probability at least +one half, so some order retains at least ceil(n/2) rows. + +**Seven-row triple lemma.** A seven-by-seven matrix of rank at most three +with nonzero diagonal has a transitive nonzero triple. This is the +arbitrary-field lemma proved in PR3420; we recall its argument here. + +Suppose no triple exists. Let G join distinct indices when at least one +of the two corresponding matrix entries is nonzero. If G has an +independent triple I, its principal matrix D is diagonal and invertible. +Rank reconstruction gives, for all u,v, + + M_uv = M[u,I] D^(-1) M[I,v]. (1) + +A nonzero entry M_uv with distinct u,v outside I has a nonzero summand +through some i in I, giving the transitive order (u,i,v). Hence the four +outside vertices are independent, contradicting rank at most three. + +Otherwise G has no independent triple. The elementary Ramsey fact +R(3,3)=6 gives a triangle. To recall that fact, among the other five +vertices of a six-vertex graph some vertex has either three neighbors +or three nonneighbors; inspecting edges among those three produces a +triangle or an independent triple. A triangle with no transitive +nonzero triple has exactly the arcs of a directed three-cycle. Its +principal matrix can be written + + A = [[a,x,0], [0,b,y], [z,0,c]], + +with all six displayed entries nonzero. Every outside vertex has at +most one outgoing and at most one incoming neighbor in this triangle; +two such neighbors would give a transitive triple. + +If A is invertible, every entry of its inverse is nonzero: its adjugate +is [[bc,-xc,xy], [yz,ac,-ay], [-bz,xz,ab]]. Rank reconstruction through A +and the nonzero outside diagonals force each outside row and column +against A to have exactly one nonzero entry. Every entry between outside +vertices is then nonzero, supplying a transitive triple. + +If A is singular, its rank is two. Factor the whole matrix as +M_ij=p_i^T q_j in K^3. At least one of the three-by-three cycle factors +P_A,Q_A has rank two. Suppose it is P_A. Its row dependence spans the +left kernel of A, whose nonzero vectors have all three coordinates +nonzero, as follows directly from the cycle equations. Every outside +column into A has at most one nonzero entry and satisfies that dependence, +so the entire column is zero. All outside q-vectors lie in the same +one-dimensional annihilator of the rows of P_A. They are nonzero by +the diagonal condition, hence are nonzero scalar multiples of each +other. Every entry between outside vertices is therefore nonzero, +again giving a triple. If Q_A has rank two, transpose the argument. +This proves the seven-row lemma without an order or positivity +assumption on the field. + +## Repeated factor directions are impossible in an obstruction + +Suppose, for contradiction, that an eleven-row matrix as in the theorem +has no ordered four-block. The half-size lemma rules out rank at most +two. Fix a rank-three factorization M_ij=p_i^T q_j with vectors in K^3. + +We first exclude three proportional p-rows. Such rows form a fully +nonzero three-block, since each diagonal is nonzero. Any outside column +is either zero on all three rows or nonzero on all three. The latter +would extend their block to four. Thus all eight outside q-vectors lie +in the common two-dimensional annihilator of that p-direction. Their +principal matrix has rank at most two, so the half-size lemma gives a +four-block. This is impossible. Transposition excludes three +proportional q-rows as well. + +Suppose now that two p-rows a,b are proportional. They form a fully +nonzero pair. Among the other nine indices let S be those whose +q-vectors are not annihilated by that common p-direction, and Z the +rest. Any nonzero edge within S, preceded by (a,b), would make a +four-block. Thus S is independent and |S|<=3. The q-vectors on Z lie +in a plane, so M[Z,Z] has rank at most two and the half-size lemma +implies |Z|<=6. Equality is forced in both bounds: + + |S|=3, |Z|=6. + +Use the independent S triple as a rank basis. An invertible change of +factor coordinates and individual nonzero row and column scalings +preserve all zero patterns and allow the normalization + + p_s=q_s=e_s for s=1,2,3 in S, + p_a=p_b=(1,1,1). + +For clarity, first change factor coordinates so that P_S is the identity; +then Q_S is diagonal, and column scalings make Q_S the identity too. +Every coordinate of the common p-direction is nonzero since 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. + +Every q_z is a nonzero vector in the plane + + H = { (x_1,x_2,x_3) : x_1+x_2+x_3=0 }. + +Each s in S has at most four outgoing neighbors in Z: five such +neighbors have a rank-at-most-two principal matrix, hence an ordered +triple by the half-size lemma, which s could precede. Each coordinate +therefore vanishes on at least two of the six q_z. A nonzero vector in +H has at most one zero coordinate. Counting forces exactly two q_z +in each of the three distinct projective 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. All rows outside U with +nonzero entries into U must be independent: otherwise their nonzero +edge followed by (u,v) gives a four-block. Those rows include s_j,s_k. +If any z in Z outside U had a nonzero entry into U, independence would +force M[z,s_j]=M[z,s_k]=0. Since q_s=e_s, its p_z would then be supported +only on coordinate i. This would give p_z^T q_u=0, a contradiction. + +Thus every row in Z outside U has zero entries into U. Applying this +to all three q-pairs makes M[Z,Z] block diagonal with three two-by-two +blocks. Each block has proportional columns and nonzero diagonal, hence +rank exactly one. The resulting rank three contradicts rank(M[Z,Z])<=2. +This excludes any repeated p-direction. By transposition, the q-directions +are also all distinct. + +## The projective incidence contradiction + +For each vertex v, its nonzero out-neighborhood has no transitive triple, +since prefixing v would give a four-block. The seven-row lemma therefore +bounds this neighborhood by six. Of the ten off-diagonal entries in +row v, at least four are zero. + +The eleven distinct q-directions are eleven projective points. The +eleven distinct p-directions define eleven distinct zero lines, where +the line for p_i consists of the directions annihilated by p_i. Each +such line contains at least four of the eleven points. Two distinct +lines cannot contain the same pair of distinct points: two distinct +q-directions span a plane whose annihilator has only one projective +direction. Counting unordered point pairs on the lines gives + + 66 = 11 * binom(4,2) + <= sum_i binom(number of points on line i,2) + <= binom(11,2) = 55. + +This contradiction proves the ordered-four-block theorem over K. + +## Transfer to the directed rational box + +Take an ordered four-block F from the theorem. Its seven-row complement +has an ordered triple L by the seven-row lemma. We use the asymmetric +two-block transfer retained from PR3409 and PR3420. + +The binary anchor hypotheses are nonempty ties A_i intersect B_i and + + M_ij=0 implies A_i dot B_j=0 over F_2. (SG) + +Choose c_i in A_i intersect B_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, keeping their internal orders. All labels are sub-anchors +and every diagonal dot is one. Inside each block there is no forward +zero entry. Across the blocks the forward dot is exactly A_i dot B_j, +so SG enforces every required zero. This is a seven-line witness under +the directed contract, which imposes constraints only when i precedes j +and the actual matrix entry M_ij is zero. + +For canonical rational anchors, SG follows from actual 2-adic +normalization. Delete product columns for which an entire factor column +is zero, and set + + 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 entries have odd +denominator and p q^T=2^(-gamma)M. Their reductions modulo two define +A_i,B_i, so an actual zero entry gives SG. Nonempty ties remain an +explicit hypothesis. This uses actual rational valuations, not a finite +valuation sentinel in an archived implementation. + +## Scope and attribution + +The matrix theorem is analytic over arbitrary fields. The canonical +box corollary is for rational three-total factorizations with the stated +nonzero-diagonal and nonempty-tie hypotheses. No eleven-line example +attaining exactly seven is claimed: the README's (4,4,3) duplicate-core +control has box eight. The next unresolved floor threshold is twelve +lines and box at least eight. This is not a complete multiplication +theorem, a new selected frontier, or a physical supplier/controller invoice. + +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 head +e2d39da9c7109f361d6cff677cf9f8eba51f3dd6; the asymmetric two-block +transfer is retained from PR3409 and PR3420. diff --git a/research/fstar-eleven-line-floor/README.md b/research/fstar-eleven-line-floor/README.md new file mode 100644 index 0000000000..8c90160359 --- /dev/null +++ b/research/fstar-eleven-line-floor/README.md @@ -0,0 +1,120 @@ + + +# Eleven rational three-total lines admit a box of seven + +For rational `M=P Q^T` with eleven rows, three factor columns, nonzero +diagonal, and nonempty canonical tied sets on every row, this package +proves **box(M)>=7**. It does not claim sharpness: the included rational +example has box exactly eight. + +The new matrix theorem is stronger and works over **any field**: every +eleven-by-eleven matrix of rank at most three with nonzero diagonal has an +ordered nonzero four-block. An ordered block requires every forward entry +to be nonzero; an undirected clique is insufficient. The remaining seven +rows have an ordered triple by [PR3420](https://github.com/CrocSwap/integer-mult-bounds/pull/3420). +The retained asymmetric two-block labels then produce the seven-row box. + +## Why the matrix theorem holds + +[PROOF.md](PROOF.md) gives a self-contained analytic argument, including +the retained seven-row lemma. Its new steps are: + +1. A rank-at-most-two matrix with nonzero diagonal has an ordered block of + at least half its rows. Order the projective column classes randomly; + retain a row after its unique forbidden class. Every row is retained + with probability at least one half. +2. An eleven-row counterexample cannot have repeated projective factor + directions. The two-copy boundary forces an independent triple and + six columns in a plane. Coordinate-zero counting divides those six + columns into three proportional pairs. The supposed obstruction then + forces their rank-at-most-two principal matrix to have three nonzero + rank-one diagonal blocks, a contradiction. +3. With both sets of factor directions distinct, zero rows are distinct + projective lines on eleven distinct points. A nonzero out-neighborhood + has at most six vertices, or its ordered triple could be prefixed to + form four. Each zero line therefore contains at least four points. + Eleven lines would account for at least `11*choose(4,2)=66` point pairs, + whereas only `choose(11,2)=55` exist. Distinct lines cannot count the + same point pair. + +There is no positivity, characteristic-zero or finite-census premise. +The rational box transfer separately uses actual 2-adic normalization to +prove that scalar zeros imply binary anchor orthogonality, plus the +explicit nonempty-tie hypothesis. + +## Exact control fixture + +Duplicate Aaron Wang/navinor's PR2978 paired core rows `(4,4,3)` times: + +```text +P = [(-1,-3,0), (1,-1,-2), (3,3,3)] +Q = [( 1,-3,2), (3,-1,-2), (3,-1,2)] +``` + +The eleven-row product is `diag(8 J4,8 J4,12 J3)`, with rank three, +`gamma=0`, two ties on every row, source anchors `011` in the first two +groups and `111` in the third, and target anchors all `011`. The constructor +returns a literal seven-row witness; the first two complete groups give +eight. + +No witness can meet all three groups. Three retained representatives in +their actual order would have a lower-triangular binary label-dot matrix +with diagonal ones and rank three, but every target label lies in the +same two-dimensional space. Thus box is exactly eight. This verifies a +positive case and **does not establish sharpness of seven**. + +## Reproduce + +From the repository root with Python 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/fstar-eleven-line-floor +python3 -B scripts/research_package.py --package research/fstar-eleven-line-floor --check-only +python3 -B scripts/check_research_commit.py --package research/fstar-eleven-line-floor --check-source-history +``` + +The last command applies to the committed publication. `VERIFY.json` +registers normal and isolated/optimized replay with warnings treated as +errors. No third-party dependencies are needed; the author used CPython +3.12.15. The executable construction and finite semantic controls are +recorded in `RESULT.json`. They do not replace the analytic proof or +constitute formal verification of it. + +The independent oracle is copied unchanged from corrected PR3393 at +`8e1e574fa68465dc0ec69d07852266b9597f9597`, exported through PR3420 at +`e2d39da9c7109f361d6cff677cf9f8eba51f3dd6`. `SOURCES.json` pins its original +Git blob and SHA256. It is reused checking code, not a newly independent +implementation. The theorem does not invoke that oracle. Bounded search +was discovery work only and is not a premise or published census. + +## Coordination, attribution and limits + +Canonical main and fork base: `6f100d4bb5083f8c35d96fd95a539811c62f245c`, +priority revision 6. The card baseline passed. `TASK.json` records this +handoff-first scope change, with status in the [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19009289). +The complete overlap snapshot covered 336 open PRs, 2,761 closed/merged PRs, +and 2,262 Discussion records, fetched 2026-10-18 01:18:23–01:19:20 UTC. +Coverage was titles, bodies and local package prose, not every PR code diff. +Earlier eleven-row results concerned named fixtures; absence of a matching +claim is not proof of novelty. + +Prepared by Sagar Thakrar with substantial OpenAI Codex assistance, including +separate proof, control and review agents. Same-session agent review is not +human acceptance. New work is Apache-2.0. DreamingOfClouds retains the +PR1590/2111 F-star/certificate attribution; Aaron Wang/navinor retains the +PR2914/2978/3031 directed-box, SG and core attribution. Arham Tahir's PR3105 +joint-triple classification is related work, not a premise. The seven-row +lemma is retained from PR3420, and the two-block transfer from PR3409/3420. + +This result does not handle zero-tie rows, settle general F-star, admit a +physical supplier, change the selected frontier, or improve κ. No formal +proof, independent human acceptance, or literature-priority claim is made. + +## Open next questions + +Do twelve admitted rational lines always have box at least eight? Start +with the `(4,4,4)` core duplication, whose box is exactly eight. Seek +disjoint ordered blocks with total size eight, allowing `4+4` or `5+3`. +The present theorem supplies one four-block; its eight-row complement is +guaranteed only a triple. A failure of this sufficient matrix condition +would not itself be a box counterexample. diff --git a/research/fstar-eleven-line-floor/RESULT.json b/research/fstar-eleven-line-floor/RESULT.json new file mode 100644 index 0000000000..85b97b7292 --- /dev/null +++ b/research/fstar-eleven-line-floor/RESULT.json @@ -0,0 +1,616 @@ +{ + "controls": { + "boundaries": [ + "zero_diagonal", + "empty_ties", + "SG", + "rank_four_no_ordered_four", + "submask", + "exact_rational_rescaling", + "source_corruption_before_execution" + ], + "orientation": { + "all_directed_four_patterns": 4096, + "forward_definition_and_reverse_mutant": true, + "rank_two_directed_triangle_has_no_ordered_triple": true, + "seven_row_rank_three_has_three_but_not_four": true + }, + "rank_two_class_order": { + "average_retained": "11/2", + "class_orders": 24, + "largest_retained": 9, + "no_forbidden_class_total_retained": 144, + "projective_classes": 4, + "rank": 2, + "reverse_order_failure_observed": true, + "rows": 11, + "three_copy_small_size_allowed": true, + "total_retained": 132 + }, + "repeated_direction": { + "P": [ + [ + 1, + 0, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 0, + 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 + ], + [ + 0, + 1, + -1 + ], + [ + 0, + 1, + -1 + ], + [ + 1, + 0, + -1 + ], + [ + 1, + 0, + -1 + ], + [ + 1, + -1, + 0 + ], + [ + 1, + -1, + 0 + ] + ], + "S": [ + 0, + 1, + 2 + ], + "Z": [ + 5, + 6, + 7, + 8, + 9, + 10 + ], + "Z_rank": 2, + "coordinate_pair_directions": [ + [ + 0, + 1, + -1 + ], + [ + 1, + 0, + -1 + ], + [ + 1, + -1, + 0 + ] + ], + "coordinate_zero_counts": [ + 2, + 2, + 2 + ], + "hypothetical_three_block_rank": 3, + "inconsistent_pair_isolation_systems": 3, + "ordered_four": [ + 1, + 5, + 9, + 10 + ], + "rank": 3, + "repeated_P_pair": [ + 3, + 4 + ], + "signed_rational_direction_rescaling": true + }, + "zero_line_incidence": { + "abstract_four_point_neighborhood_collision_rejected": true, + "available_point_pairs": 55, + "distinct_line_and_point_mutants_rejected": true, + "realizable_conic_points": 11, + "realizable_distinct_lines": 11, + "realizable_pair_uses": 11, + "required_pairs_at_four_zeros": 66 + } + }, + "inputs_sha256": { + "inputs/pr3393-independent_box.py": "6792f0c92943e418d93ae6bc8b616447efc2a505612c87c011a36025d98f814d" + }, + "schema_version": 1, + "scope": "finite exact controls for the analytic theorem; no exhaustive matrix search or formal kernel claim", + "status": "PASS_FSTAR_ELEVEN_LINE_FLOOR", + "working_fixture": { + "M": [ + [ + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 8, + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 8, + 8, + 8, + 8, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 8, + 8, + 8, + 8, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 8, + 8, + 8, + 8, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 8, + 8, + 8, + 8, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 12, + 12, + 12 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 12, + 12, + 12 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 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 + ] + ], + "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 + ] + ], + "a0": [ + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 7, + 7, + 7 + ], + "b0": [ + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3 + ], + "eight_witness": { + "a": [ + 3, + 3, + 3, + 3, + 1, + 1, + 1, + 1, + 0, + 0, + 0 + ], + "b": [ + 1, + 1, + 1, + 1, + 3, + 3, + 3, + 3, + 0, + 0, + 0 + ], + "kept": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "order": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ] + }, + "exact_box": 8, + "gamma": 0, + "rank": 3, + "sharpness_at_seven": false, + "sizes": [ + 4, + 4, + 3 + ], + "tau": [ + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2 + ], + "theorem_witness": { + "a": [ + 3, + 3, + 3, + 3, + 1, + 1, + 1, + 0, + 0, + 0, + 0 + ], + "b": [ + 1, + 1, + 1, + 1, + 3, + 3, + 3, + 0, + 0, + 0, + 0 + ], + "kept": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "order": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ] + }, + "upper_bound": "any nine-set meets three zero-separated groups, forcing a triangular rank3 label minor; all target labels lie in a rank2 space" + } +} diff --git a/research/fstar-eleven-line-floor/SOURCES.json b/research/fstar-eleven-line-floor/SOURCES.json new file mode 100644 index 0000000000..1de9661f55 --- /dev/null +++ b/research/fstar-eleven-line-floor/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 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": "Arham Tahir/Arham-Tahir64, PR3105 joint triple classification; Sagar Thakrar with OpenAI Codex assistance, PR3332/3393 finite floors, PR3409 asymmetric two-block transfer, and PR3420 six/seven/nine-row lemmas. The retained six/seven-row argument is reproduced with attribution in PROOF.md; the eleven-row proof does not use the joint census or the earlier real trace argument.", + "this_package": "Sagar Thakrar with substantial OpenAI Codex assistance; rank-two half-size lemma, repeated-direction exclusion, arbitrary-field eleven-row incidence proof, rational box transfer and exact controls. Same-session agent reviews are not independent human acceptance or formal proof." + } +} diff --git a/research/fstar-eleven-line-floor/TASK.json b/research/fstar-eleven-line-floor/TASK.json new file mode 100644 index 0000000000..75972daf3f --- /dev/null +++ b/research/fstar-eleven-line-floor/TASK.json @@ -0,0 +1,66 @@ +{ + "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": "Prove that every eleven-by-eleven matrix of rank at most three with nonzero diagonal over any field has an ordered nonzero four-block, and derive the rational three-total anchor-box floor seven under canonical tau>=1.", + "scope_change_reason": "Handoff-first continuation of PR3420 after refreshing canonical main and revision6, replaying the original baseline, and checking complete current/historical PR and Discussion snapshots. The sufficient ordered-four matrix condition is proved; finite search is discovery evidence only.", + "bottleneck_link": "Closes the eleven-line floor(2v/3) threshold in the nonempty-tie anchor-box route. It does not admit the full F-star supplier or change the selected kappa.", + "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 rank-two averaging, exclusion of repeated factor directions, the retained seven-row triple lemma, and a projective incidence contradiction (66 required point pairs versus 55 available). verify.py and RESULT.json supply exact finite controls and source-authenticated oracle agreement, not a formal or exhaustive proof.", + "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": "Do twelve rational three-total lines with nonzero diagonal and nonempty canonical tied sets always have box>=8?", + "why_it_matters": "This is the next floor(2v/3) threshold. The present ordered four-block leaves eight rows; the seven-row lemma guarantees only another triple.", + "first_step": "Begin with the (4,4,4) duplication of the PR2978 core, whose box is exactly eight. Seek disjoint ordered blocks with total size eight, allowing 4+4 or 5+3 rather than insisting on one split.", + "blocked_by": "The eleven-row theorem guarantees one ordered four-block, not two disjoint four-blocks or a larger alternative. A failure of that sufficient matrix condition need not be a box counterexample." + } + ] +} diff --git a/research/fstar-eleven-line-floor/VERIFY.json b/research/fstar-eleven-line-floor/VERIFY.json new file mode 100644 index 0000000000..c929aec438 --- /dev/null +++ b/research/fstar-eleven-line-floor/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Exact ordered-four-plus-three construction, rational fixture, source-authenticated independent oracle, and finite rank-two/repeated-direction/incidence controls. The general result is the analytic proof, not a finite census or formal kernel check." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "-Werror", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Repeat all exact controls under isolation, optimization and warnings-as-errors; explicit rejection checks remain active without assertions." + } + ] +} diff --git a/research/fstar-eleven-line-floor/inputs/pr3393-independent_box.py b/research/fstar-eleven-line-floor/inputs/pr3393-independent_box.py new file mode 100644 index 0000000000..d15e05f45e --- /dev/null +++ b/research/fstar-eleven-line-floor/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-eleven-line-floor/verify.py b/research/fstar-eleven-line-floor/verify.py new file mode 100644 index 0000000000..64d0fa2a7d --- /dev/null +++ b/research/fstar-eleven-line-floor/verify.py @@ -0,0 +1,385 @@ +#!/usr/bin/env python3 +"""Exact controls for the analytic eleven-row matrix and directed-box proof. + +SPDX-License-Identifier: Apache-2.0 +Sagar Thakrar (thakrarsagar), with substantial OpenAI Codex assistance. +Shared small checker patterns follow the author's PR3420 verifier. The frozen +PR3393 oracle is unchanged and authenticated before any execution. +""" + +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 product(p, q): + return [[sum(x*y for x, y in zip(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 parity(left, right): + return (left & right).bit_count() & 1 + + +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 admit(matrix, a0, b0): + require(len(matrix) == 11 and all(len(row) == 11 for row in matrix), "expected eleven square rows") + require(len(a0) == len(b0) == 11, "anchor length mismatch") + require(all(type(mask) is int and 0 <= mask < 8 for mask in a0 + b0), "invalid anchor mask") + require(all(matrix[i][i] for i in range(11)), "zero diagonal") + require(rank(matrix) <= 3, "matrix 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(11) for j in range(11)), "SG failed") + + +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(a0) 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 position, i in enumerate(order) for j in order[position + 1:]) + + +def labelled_blocks(matrix, a0, b0, first, second): + require(set(first).isdisjoint(second) and ordered(matrix, first) and ordered(matrix, second), + "blocks are not disjoint ordered nonzero subsets") + 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), "two-block labels violate the directed box") + return witness + + +def construct(matrix, a0, b0): + admit(matrix, a0, b0) + first = find_ordered(matrix, 4) + require(first is not None, "ordered-four theorem failed on admitted matrix") + second = find_ordered(matrix, 3, [i for i in range(11) if i not in first]) + require(second is not None, "seven-row complement theorem failed") + return labelled_blocks(matrix, a0, b0, first, second) + + +def core_fixture(oracle): + sizes = (4, 4, 3) + p0 = [(-1, -3, 0), (1, -1, -2), (3, 3, 3)] + q0 = [(1, -3, 2), (3, -1, -2), (3, -1, 2)] + p = [row for row, count in zip(p0, sizes) for _ in range(count)] + q = [row for row, count in zip(q0, sizes) for _ in range(count)] + data = oracle.rational_data(p, q) + matrix = product(p, q) + groups = [g for g, count in enumerate(sizes) for _ in range(count)] + expected = [[(8 if g < 2 else 12) if g == h else 0 for h in groups] for g in groups] + require(matrix == expected == data["M"] and rank(matrix) == 3, "core matrix changed") + require(data["gamma"] == 0 and data["tau"] == [2] * 11 and + data["a0"] == [3] * 8 + [7] * 3 and data["b0"] == [3] * 11, "core normalization changed") + witness = construct(matrix, data["a0"], data["b0"]) + sharp = labelled_blocks(matrix, data["a0"], data["b0"], list(range(4)), list(range(4, 8))) + require(len(witness["kept"]) == 7 and len(sharp["kept"]) == 8, "core witness sizes failed") + require(all(oracle.check_witness(data["a0"], data["b0"], data["arcs"], value) + for value in (witness, sharp)), "frozen definition disagrees") + require(all(len({groups[i] for i in subset}) == 3 for subset in combinations(range(11), 9)), + "nine-set rank obstruction premise failed") + record = {"P": list(map(list, p)), "Q": list(map(list, q)), "sizes": list(sizes), "M": matrix, "rank": 3, "gamma": 0, + "a0": data["a0"], "b0": data["b0"], "tau": data["tau"], + "theorem_witness": witness, "exact_box": 8, "eight_witness": sharp, + "upper_bound": "any nine-set meets three zero-separated groups, forcing a triangular rank3 label minor; all target labels lie in a rank2 space", + "sharpness_at_seven": False} + return record, data, p, q + + +def rejects(action, message): + try: + action() + except ValueError as error: + require(message in str(error), "unexpected failure control: " + str(error)) + return + raise ValueError("failure control accepted: " + message) + + +def boundary_controls(oracle, data, p, q): + matrix, a0, b0 = data["M"], data["a0"], data["b0"] + zero_diag = [row[:] for row in matrix] + zero_diag[0][0] = 0 + rejects(lambda: construct(zero_diag, a0, b0), "zero diagonal") + empty_tie = a0[:] + empty_tie[0] = 0 + rejects(lambda: construct(matrix, empty_tie, b0), "empty tied set") + rejects(lambda: construct(matrix, [1] * 11, [1] * 11), "SG failed") + groups = [0]*3 + [1]*3 + [2]*3 + [3]*2 + rank_four = [[int(i == j) for j in groups] for i in groups] + require(rank(rank_four) == 4 and find_ordered(rank_four, 4) is None, "rank boundary failed") + rejects(lambda: construct(rank_four, [3]*11, [3]*11), "rank exceeds three") + witness = construct(matrix, a0, b0) + witness["a"][witness["kept"][0]] = 8 + require(not literal_check(matrix, a0, b0, witness) and not oracle.check_witness( + a0, b0, data["arcs"], witness), "submask corruption accepted") + scales = [Fraction(-3, 2), Fraction(5, 4), Fraction(7)] + scaled = oracle.rational_data([[x*s for x, s in zip(row, scales)] for row in p], + [[x/s for x, s in zip(row, scales)] for row in q]) + require(all(scaled[key] == data[key] for key in ("M", "a0", "b0", "tau")), "rational scaling changed canonical data") + 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_no_ordered_four", "submask", + "exact_rational_rescaling", "source_corruption_before_execution"] + + +def class_orders(p, q): + """Literal finite class-order construction used only by the rank-two control.""" + require(all(len(row) == 2 for row in p + q), "expected two-coordinate factors") + matrix = product(p, q) + require(all(matrix[i][i] for i in range(len(matrix))) and rank(matrix) <= 2, "rank-two premise failed") + 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 premise failed") + result = [] + for order in permutations(range(len(classes))): + position = {value: i for i, value in enumerate(order)} + kept = [i for value in order for i in range(len(p)) if owner[i] == value and + (not forbidden[i] or position[next(iter(forbidden[i]))] < position[value])] + require(ordered(matrix, kept), "class-order construction failed") + result.append(kept) + return matrix, result + + +def rank_two_controls(): + qtypes = [(1, 0), (0, 1), (1, 1), (1, -1)] + ptypes = [(1, 0), (1, -1), (1, 1), (0, 1)] + sizes = (3, 3, 3, 2) + p = [row for row, count in zip(ptypes, sizes) for _ in range(count)] + q = [tuple(Fraction((-2 if k % 2 else 3), 5) * x for x in row) + for row, count in zip(qtypes, sizes) for k in range(count)] + matrix, orders = class_orders(p, q) + require(len(orders) == 24 and sum(map(len, orders)) == 132, "half-size mass changed") + require(max(map(len, orders)) >= 6 and any(not ordered(matrix, tuple(reversed(order))) + for order in orders), "orientation control did not fail") + no_forbidden = p[:] + no_forbidden[0] = (1, 2) + _matrix, augmented = class_orders(no_forbidden, q) + require(all(0 in order for order in augmented) and sum(map(len, augmented)) == 144, + "a row without a forbidden class was not always retained") + # A three-copy direction is legal at small sizes; no global multiplicity rule is used. + low = [[1]*3 for _ in range(3)] + require(rank(low) == 1 and ordered(low, (0, 1, 2)) and find_ordered(low, 4) is None, "low-size duplicate control failed") + return {"rows": 11, "rank": 2, "projective_classes": 4, "class_orders": 24, + "total_retained": 132, "average_retained": "11/2", "largest_retained": max(map(len, orders)), + "no_forbidden_class_total_retained": 144, + "reverse_order_failure_observed": True, "three_copy_small_size_allowed": True} + + +def repeated_pair_controls(): + basis = [[int(i == j) for j in range(3)] for i in range(3)] + p = basis + [[1, 1, 1]]*2 + [[0, 1, 0], [1, 2, 0], [1, 0, 0], [2, 1, 0], [1, 0, 1], [2, 0, 1]] + qdirections = [(0, 1, -1), (1, 0, -1), (1, -1, 0)] + q = basis + [[1, 1, 1], [1, 1, 0]] + [list(row) for row in qdirections for _ in range(2)] + matrix = product(p, q) + require(rank(matrix) == 3 and all(matrix[i][i] for i in range(11)), "repeated-pair fixture failed") + for factors in (p, q): + directions = [projective(row) for row in factors] + require(max(directions.count(value) for value in directions) == 2, "fixture uses a three-copy shortcut") + scaled = [row[:] for row in p] + scaled[3] = [Fraction(-2) * x for x in p[3]] + scaled[4] = [Fraction(3, 5) * x for x in p[4]] + require(projective(scaled[3]) == projective(scaled[4]) == (1, 1, 1) and + ordered(product(scaled, q), (1, 5, 9, 10)), "projective rescaling failed") + require(all(matrix[3][i] and matrix[4][i] for i in range(3)) and + all(not matrix[3][i] and not matrix[4][i] for i in range(5, 11)), "S/Z partition failed") + z = [row[5:] for row in matrix[5:]] + require(rank(z) == 2 and ordered(matrix, (1, 5, 9, 10)), "actual pair-branch four-block failed") + require(all(sum(row) == 0 and sum(value == 0 for value in row) == 1 for row in qdirections), "coordinate-plane premise failed") + require(rank(qdirections) == 2 and all(sum(q[i][j] == 0 for i in range(5, 11)) == 2 + for j in range(3)), "coordinate zero counts failed") + impossible = [[int(i//2 == j//2) for j in range(6)] for i in range(6)] + require(rank(impossible) == 3, "three rank-one blocks lost rank") + for target in range(3): + augmented = [list(row) + [int(i == target)] for i, row in enumerate(qdirections)] + require(rank(augmented) == 3, "impossible isolated pair constraints became solvable") + return {"P": p, "Q": q, "rank": 3, "S": [0, 1, 2], "repeated_P_pair": [3, 4], + "Z": list(range(5, 11)), "Z_rank": 2, "ordered_four": [1, 5, 9, 10], + "coordinate_pair_directions": [list(row) for row in qdirections], + "coordinate_zero_counts": [2, 2, 2], "hypothetical_three_block_rank": 3, + "inconsistent_pair_isolation_systems": 3, "signed_rational_direction_rescaling": True} + + +def cross(left, right): + a, b, c = left + d, e, f = right + return [b*f-c*e, c*d-a*f, a*e-b*d] + + +def unique_pairs(neighborhoods): + owners = {} + for line, points in enumerate(neighborhoods): + for pair in combinations(sorted(points), 2): + require(pair not in owners, "point pair lies on two lines") + owners[pair] = line + return len(owners) + + +def incidence(p, q): + require(len({projective(row) for row in p}) == len(p), "repeated line direction") + require(len({projective(row) for row in q}) == len(q), "repeated point direction") + matrix = product(p, q) + neighborhoods = [[j for j, value in enumerate(row) if not value] for row in matrix] + return neighborhoods, unique_pairs(neighborhoods) + + +def incidence_controls(): + q = [[1, i, i*i] for i in range(11)] + p = [cross(q[i], q[(i+1) % 11]) for i in range(11)] + neighborhoods, pairs = incidence(p, q) + require([len(points) for points in neighborhoods] == [2]*11 and pairs == 11, "conic incidence control failed") + rejects(lambda: incidence([p[0]] + p[:-1], q), "repeated line direction") + rejects(lambda: incidence(p, [q[0]] + q[:-1]), "repeated point direction") + abstract = [[(i+j) % 11 for j in range(4)] for i in range(11)] + required = sum(len(list(combinations(points, 2))) for points in abstract) + available = len(list(combinations(range(11), 2))) + require(required == 66 and available == 55 and required > available, "incidence contradiction arithmetic changed") + rejects(lambda: unique_pairs(abstract), "point pair lies on two lines") + return {"realizable_conic_points": 11, "realizable_distinct_lines": 11, + "realizable_pair_uses": 11, "required_pairs_at_four_zeros": 66, + "available_point_pairs": 55, "distinct_line_and_point_mutants_rejected": True, + "abstract_four_point_neighborhood_collision_rejected": True} + + +def orientation_controls(oracle): + arcs = [(i, j) for i in range(4) for j in range(4) if i != j] + for pattern in range(4096): + matrix = [[int(i == j) for j in range(4)] for i in range(4)] + for bit, (i, j) in enumerate(arcs): + matrix[i][j] = int(bool(pattern & (1 << bit))) + direct = any(matrix[a][b] and matrix[a][c] and matrix[a][d] and + matrix[b][c] and matrix[b][d] and matrix[c][d] + for a, b, c, d in permutations(range(4))) + require(bool(find_ordered(matrix, 4)) == direct, "directed-four predicate mismatch") + directed = [[int(i <= j) for j in range(3)] for i in range(3)] + zeros = [(i, j) for i in range(3) for j in range(3) if i != j and not directed[i][j]] + witness = {"a": [1]*3, "b": [1]*3, "kept": [0, 1, 2], "order": [0, 1, 2]} + require(literal_check(directed, [1]*3, [1]*3, witness) and + oracle.check_witness([1]*3, [1]*3, zeros, witness), "forward definition control 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, zeros, witness), "reversed definition control accepted") + cycle = [[-2, 0, 2], [-8, -2, 0], [0, 2, 8]] + require(rank(cycle) == 2 and find_ordered(cycle, 3) is None, "directed cycle mistaken for a triple") + groups = [0]*3 + [1]*2 + [2]*2 + seven = [[int(i == j) for j in groups] for i in groups] + require(rank(seven) == 3 and find_ordered(seven, 3) is not None and + find_ordered(seven, 4) is None, "rank-three seven-row boundary failed") + return {"all_directed_four_patterns": 4096, "forward_definition_and_reverse_mutant": True, + "rank_two_directed_triangle_has_no_ordered_triple": True, + "seven_row_rank_three_has_three_but_not_four": True} + + +def build(): + authenticated = authenticate() + oracle = load_oracle() + fixture, data, p, q = core_fixture(oracle) + return {"schema_version": 1, "status": "PASS_FSTAR_ELEVEN_LINE_FLOOR", + "scope": "finite exact controls for the analytic theorem; no exhaustive matrix search or formal kernel claim", + "inputs_sha256": {path: hashlib.sha256(raw).hexdigest() for path, raw in authenticated.items()}, + "working_fixture": fixture, + "controls": {"boundaries": boundary_controls(oracle, data, p, q), + "orientation": orientation_controls(oracle), "rank_two_class_order": rank_two_controls(), + "repeated_direction": repeated_pair_controls(), "zero_line_incidence": incidence_controls()}} + + +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_ELEVEN_LINE_FLOOR: exact construction, proof-branch controls and source binding") + + +if __name__ == "__main__": + main()