From 8758f9b5eb04f2914e874a39fc55770bcdab2dfa Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Sun, 18 Oct 2026 06:25:09 +0530 Subject: [PATCH] Prove an eight-line rank-three anchor-box floor of five --- research/fstar-eight-line-floor/PROOF.md | 155 +++++++++ research/fstar-eight-line-floor/README.md | 104 ++++++ research/fstar-eight-line-floor/RESULT.json | 329 ++++++++++++++++++ research/fstar-eight-line-floor/SOURCES.json | 34 ++ research/fstar-eight-line-floor/TASK.json | 66 ++++ research/fstar-eight-line-floor/VERIFY.json | 30 ++ .../inputs/pr3393-independent_box.py | 225 ++++++++++++ research/fstar-eight-line-floor/verify.py | 283 +++++++++++++++ 8 files changed, 1226 insertions(+) create mode 100644 research/fstar-eight-line-floor/PROOF.md create mode 100644 research/fstar-eight-line-floor/README.md create mode 100644 research/fstar-eight-line-floor/RESULT.json create mode 100644 research/fstar-eight-line-floor/SOURCES.json create mode 100644 research/fstar-eight-line-floor/TASK.json create mode 100644 research/fstar-eight-line-floor/VERIFY.json create mode 100644 research/fstar-eight-line-floor/inputs/pr3393-independent_box.py create mode 100644 research/fstar-eight-line-floor/verify.py diff --git a/research/fstar-eight-line-floor/PROOF.md b/research/fstar-eight-line-floor/PROOF.md new file mode 100644 index 0000000000..f2bdd2ddc5 --- /dev/null +++ b/research/fstar-eight-line-floor/PROOF.md @@ -0,0 +1,155 @@ + + +# Eight rational three-total lines have a five-line box witness + +## Statement and the directed box contract + +Let `P,Q` be rational matrices with eight rows and three columns, let +`M=P Q^T`, and assume `M_ii != 0` on every line. Let `A_i,B_i` be the +canonical binary anchors and suppose every tied set `A_i intersect B_i` +is nonempty. Then **box(M)>=5** for the directed sub-anchor definition. +No sharpness claim is made. + +The proof uses only the following abstract hypotheses: `M` is a real +eight-by-eight matrix of rank at most three with nonzero diagonal; +`A_i,B_i` are binary support sets with nonempty intersection; and + + M_ij=0 implies A_i dot B_j=0 over F_2. (SG) + +A witness keeps some lines in an order and assigns labels +`a_i subset A_i`, `b_i subset B_i`, with `a_i dot b_i=1`. Its off-diagonal +requirements are only + + i precedes j and M_ij=0 implies a_i dot b_j=0. + +Thus the abstract statement is stronger than the rational canonical case, +but it does not replace the directed constraint by an unordered condition. + +For completeness, canonical normalization supplies SG as follows. Remove +degenerate product columns, which do not affect M, 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 entries are rational +numbers with odd denominator, and `p q^T=2^(-gamma)M`. Their reductions +modulo two have supports `A_i,B_i`, so every actual zero reduces to the +zero binary dot product in SG. Nonempty ties are the stated hypothesis. +This is an algebraic normalization using actual rational valuations, not a +claim about unbounded inputs to a predecessor's finite valuation sentinel. + +## Two ordered blocks give a box witness + +Suppose disjoint sets F and L each have an ordering in which every forward +off-diagonal entry of M is nonzero. Choose a tied coordinate c_i for every +line in their union. On F use + + a_i=A_i, b_i=e_(c_i), + +and on L use + + a_i=e_(c_i), b_i=B_i. + +Order all of F first, then all of L, respecting the two given orders. +Every diagonal dot is one and every label is a sub-anchor. Within each +block there are no forward zero entries to constrain. Between the blocks, +the forward dot is the original `A_i dot B_j`, so SG supplies every required +zero. This is a witness on all of F union L. + +We shall find a three-line F and a disjoint two-line L. In particular the +argument permits asymmetric labels: it does not restrict both sides to +the same tied unit vector. + +## Rank three forces a transitive nonzero triple + +Call distinct indices `(i,j,k)` a transitive nonzero triple if + + M_ij != 0, M_ik != 0, M_jk != 0. + +We prove that such a triple exists. Suppose otherwise. Let G be the simple +undirected graph whose edge `{i,j}` means at least one of `M_ij,M_ji` is +nonzero. An independent set has a diagonal principal matrix with nonzero +diagonal; hence G has no independent set of size four. + +First suppose G has an independent triple I. Its principal matrix +`D=M[I,I]` is diagonal and invertible. Since `rank(M)<=3`, its Schur +complement is zero. For any two indices u,v outside I, + + M_uv = sum_(i in I) M_ui M_ii^(-1) M_iv. + +If `u!=v` and `M_uv!=0`, some summand is nonzero. The indices `(u,i,v)` +then form a transitive nonzero triple, a contradiction. Therefore the +principal matrix on the five vertices outside I is diagonal with nonzero +diagonal. Its rank is five, again a contradiction. + +It remains that G has no independent triple. For a vertex v, its +out-neighbors in the directed nonzero graph form an independent set in G: +an edge between two out-neighbors would give a transitive triple starting +at v. Its in-neighbors are independent for the same reason. Each set +therefore has size at most two, and the undirected degree of v is at most +four. + +The nonneighbors of v form a clique in G, since two nonadjacent ones +together with v would form an independent triple. G has no clique of size +four: choose one nonzero direction of each edge in such a clique, obtaining +a tournament on four vertices; some vertex has two in-neighbors or two +out-neighbors, and the edge between those two completes a transitive +triple. Thus v has at most three nonneighbors. On eight vertices its +undirected degree is at least `8-1-3=4`. + +The degree bounds are equalities. The in-neighbor and out-neighbor sets +must each have size two and be disjoint, or their union would have size +less than four. Consequently + + M_ij M_ji=0 whenever i!=j. (1) + +Choose a real rank factorization `M_ij=u_i^T v_j` with vectors in R^3, +padding unused dimensions by zero if needed, and form the three-by-three +matrices `T_i=v_i u_i^T`. The trace identity and (1) give + + tr(T_i T_j)=M_ij M_ji=0 for i!=j, + tr(T_i^2)=M_ii^2>0. + +The symmetric three-by-three real matrices have dimension six. Therefore +the eight symmetric parts `(T_i+T_i^T)/2` have a nontrivial real linear +dependence. For its coefficients c_i, not all zero, the matrix +`T=sum_i c_i T_i` is skew-symmetric, yet + + tr(T^2)=sum_i c_i^2 M_ii^2>0. + +A real skew-symmetric matrix instead satisfies + + tr(T^2)=-sum_(a,b) T_ab^2<=0. + +This contradiction finishes the proof that a transitive nonzero triple +exists. Positivity over the reals is used explicitly; the argument does +not assert the same matrix lemma over an arbitrary field. + +## Completion of the five-line witness + +Use a transitive nonzero triple as F in its defining order. Among the +remaining five vertices there is an edge of G, since otherwise their +principal matrix would be diagonal of rank five. Orient that edge in a +nonzero direction and use its two vertices as L. The two-block construction +keeps `3+2=5` lines and proves the theorem. + +## The six-line consequence of the same construction + +With six lines, the nonzero graph G has two disjoint edges. Otherwise its +edges pairwise intersect, so it is a star, a triangle with isolated vertices, +or empty; each possibility has an independent set of four and therefore a +diagonal rank-four principal matrix. Orient the two disjoint edges in nonzero +directions and use them as the two blocks. The same construction gives +`box(M)>=4`. Thus the transfer argument also gives a short proof of PR3393's +six-line result, without its anchor-type case analysis. + +## Scope + +The proof is analytic and has no finite-census premise. It proves the scoped +box bound, not a complete multiplication theorem, a new selected frontier, +or a physical supplier/controller invoice. It does not prove `box>=6` at nine lines or an upper bound of five at eight lines. + +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. diff --git a/research/fstar-eight-line-floor/README.md b/research/fstar-eight-line-floor/README.md new file mode 100644 index 0000000000..23fe2403ac --- /dev/null +++ b/research/fstar-eight-line-floor/README.md @@ -0,0 +1,104 @@ +# Eight-line anchor-box floor + +For rational `P,Q` with eight rows and three columns, `M=P Q^T`, nonzero +diagonal, and canonical `tau_i>=1`, **`box(M)>=5`**. This answers the next +threshold question in +[PR3393](https://github.com/CrocSwap/integer-mult-bounds/pull/3393). +Sharpness at five is not established. + +[PROOF.md](PROOF.md) proves a stronger matrix statement: every real +eight-by-eight matrix of rank at most three with nonzero diagonal has distinct +indices `(i,j,k)` with all three forward entries `M_ij,M_ik,M_jk` nonzero. +An independent triple would give a rank-basis identity forcing the other five +vertices to be independent, a contradiction. Otherwise neighborhood counts +eliminate bidirectional nonzero pairs. Eight associated rank-one matrices +would then span a positive eight-dimensional space for the trace form on +three-by-three real matrices, whose positive index is six. + +An ordered triple and a disjoint nonzero pair become a five-line box witness: +use full source anchors and tied unit target labels in the first block, then +tied unit source labels and full target anchors in the second. The directed +zero constraints between the blocks are precisely the original SG implication. +This permits asymmetric labels and needs no anchor-type census. A short +corollary also gives the six-line floor four from two disjoint nonzero edges. + +## Exact evidence + +The working rational fixture duplicates Aaron Wang's PR2978 core with block +sizes `3,3,2`: + +``` +P0 = [(-1,-3,0), (1,-1,-2), (3,3,3)] +Q0 = [(1,-3,2), (3,-1,-2), (3,-1,2)] +M = diag(8 J3, 8 J3, 12 J2). +``` + +It has rank three, `gamma=0`, and every tied count is two. Its box is **six**: +two size-three blocks give six kept lines, while every seven-set meets all +three blocks and forces a triangular rank-three label minor inside a common +two-dimensional target space. This is a positive control, not a sharpness +example for the lower bound five. + +`verify.py` constructs the ordered blocks using exact arithmetic and checks +their labels both literally and with the unchanged target-first Gaussian +oracle exported from corrected PR3393 head +`8e1e574fa68465dc0ec69d07852266b9597f9597`. The export is authenticated before +execution. Controls exercise the directed-cycle boundary, rank-four exclusion, +SG/nonempty-tie/diagonal admission, the rank-basis identity, and the distinction +between symmetric and skew trace directions. [RESULT.json](RESULT.json) +records finite checks; the general theorem rests on the written proof. + +From the repository root, with Python 3.12 (tested with 3.12.15): + +```sh +python3 -B scripts/research_package.py --package research/fstar-eight-line-floor --check-only +python3.12 -B scripts/research_package.py --package research/fstar-eight-line-floor +``` + +Normal and isolated optimized replays are registered. There are no third-party +Python dependencies. Exact source history and hashes are in +[SOURCES.json](SOURCES.json); the selected record and task catalogue are +historical provenance. Development searches are not proof premises or claims +of an exhaustive rational census. + +## Scope + +The abstract result needs real rank at most three, nonzero diagonal, nonempty +tied sets and SG. Canonical rational three-total factors satisfy SG through +their actual 2-adic normalization. The trace argument uses real positivity; +no arbitrary-field extension is asserted. The proof is analytic, not formally +machine verified or independently reviewed by a human. + +This is a scoped box theorem. The full F-star conjecture, complete multiplication +theorem, physical controller/supplier admission and selected kappa are unchanged. +The explicitly changed `independent-moment` scope, baseline, stop rule and next +question are recorded in [TASK.json](TASK.json). The canonical investigation is +[Discussion1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19008770). + +## Open next questions + +Does `v=9` force six kept lines? A sufficient next target is two disjoint +transitive nonzero triples. Start from the `3,3,3` three-block duplication, +which has box six. One arbitrarily chosen triple can leave a six-line matrix +with no transitive triple, so the current argument does not answer this +question. Choosing a better triple or using further anchor information needs +a new argument; the matrix condition is sufficient, not necessary. + +## Attribution + +New work by **Sagar Thakrar with substantial OpenAI Codex assistance**, including +separate proof, exact-control and review agents. Separate AI runs are not +independent human review. New work is Apache-2.0. + +Aaron Wang/navinor supplied the directed sub-anchor box, SG and valuation +lineage through [PR2914](https://github.com/CrocSwap/integer-mult-bounds/pull/2914) +and [PR3031](https://github.com/CrocSwap/integer-mult-bounds/pull/3031), and the +three-line core in [PR2978](https://github.com/CrocSwap/integer-mult-bounds/pull/2978). +DreamingOfClouds supplied the F-star/certificate origins and earlier fixtures in +[PR1590](https://github.com/CrocSwap/integer-mult-bounds/pull/1590) and +[PR2111](https://github.com/CrocSwap/integer-mult-bounds/pull/2111). +Arham Tahir's [PR3105](https://github.com/CrocSwap/integer-mult-bounds/pull/3105) +gave the earlier joint triple classification. Those contributors retain their +source-specific assistance disclosures. The frozen independent oracle and the +six-line predecessor are Sagar Thakrar's +[PR3393](https://github.com/CrocSwap/integer-mult-bounds/pull/3393). diff --git a/research/fstar-eight-line-floor/RESULT.json b/research/fstar-eight-line-floor/RESULT.json new file mode 100644 index 0000000000..0a1956085b --- /dev/null +++ b/research/fstar-eight-line-floor/RESULT.json @@ -0,0 +1,329 @@ +{ + "admission_controls": { + "empty_ties_rejected": true, + "rank4_admission_rejected": true, + "rank4_has_no_ordered_triple": true, + "sg_failing_anchors_box": 3, + "zero_diagonal_rejected": true + }, + "algebra_controls": { + "factor_trace_pairs_checked": 64, + "schur_altered_entry_rejected": true, + "schur_entries_checked": 64, + "skew_trace_square": -28, + "symmetric_trace_square": 32 + }, + "directed_controls": { + "circulant_has_no_ordered_triple_or_independent_triple": true, + "circulant_rank": 8, + "rank2_directed_cycle": [ + [ + -2, + 0, + 2 + ], + [ + -8, + -2, + 0 + ], + [ + 0, + 2, + 8 + ] + ], + "unordered_triangle_is_insufficient": true + }, + "exhaustive_matrix_census_claimed": false, + "fixture": { + "A": [ + 3, + 3, + 3, + 3, + 3, + 3, + 7, + 7 + ], + "B": [ + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3 + ], + "M": [ + [ + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0 + ], + [ + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0 + ], + [ + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 8, + 8, + 8, + 0, + 0 + ], + [ + 0, + 0, + 0, + 8, + 8, + 8, + 0, + 0 + ], + [ + 0, + 0, + 0, + 8, + 8, + 8, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 12, + 12 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 12, + 12 + ] + ], + "P": [ + [ + -1, + -3, + 0 + ], + [ + -1, + -3, + 0 + ], + [ + -1, + -3, + 0 + ], + [ + 1, + -1, + -2 + ], + [ + 1, + -1, + -2 + ], + [ + 1, + -1, + -2 + ], + [ + 3, + 3, + 3 + ], + [ + 3, + 3, + 3 + ] + ], + "Q": [ + [ + 1, + -3, + 2 + ], + [ + 1, + -3, + 2 + ], + [ + 1, + -3, + 2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + 2 + ], + [ + 3, + -1, + 2 + ] + ], + "box": 6, + "first": [ + 0, + 1, + 2 + ], + "five_witness": { + "a": [ + 3, + 3, + 3, + 1, + 1, + 0, + 0, + 0 + ], + "b": [ + 1, + 1, + 1, + 3, + 3, + 0, + 0, + 0 + ], + "kept": [ + 0, + 1, + 2, + 3, + 4 + ], + "order": [ + 0, + 1, + 2, + 3, + 4 + ] + }, + "last": [ + 3, + 4 + ], + "rank": 3, + "six_witness": { + "a": [ + 1, + 1, + 1, + 2, + 2, + 2, + 0, + 0 + ], + "b": [ + 1, + 1, + 1, + 2, + 2, + 2, + 0, + 0 + ], + "kept": [ + 0, + 1, + 2, + 3, + 4, + 5 + ], + "order": [ + 0, + 1, + 2, + 3, + 4, + 5 + ] + }, + "symmetric_unit_mutation_rejected": true, + "tau": [ + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2 + ], + "upper_bound": "Every seven-set meets three zero-separated blocks; a triangular rank3 label minor exceeds the two-dimensional target-label span." + }, + "formal_proof_claimed": false, + "oracle_sha256": "6792f0c92943e418d93ae6bc8b616447efc2a505612c87c011a36025d98f814d", + "schema_version": 1, + "scope": "Finite controls supporting the separate analytic proof", + "source_corruption_rejected_before_execution": true +} diff --git a/research/fstar-eight-line-floor/SOURCES.json b/research/fstar-eight-line-floor/SOURCES.json new file mode 100644 index 0000000000..88ae6049d6 --- /dev/null +++ b/research/fstar-eight-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, PR3393; independently implemented target-first Gaussian oracle, Apache-2.0. Its predecessor comparison and original fixture controls remain in that package.", + "definition_and_sharp_core": "Aaron Wang/navinor: directed sub-anchor box and SG/valuation lineage through PR2914 and PR3031; PR2978 three-line rational core. The exact definition engine retained by PR3031 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_predecessor": "Arham Tahir/Arham-Tahir64, PR3105; joint triple classification. It is not a premise of the new real-matrix theorem.", + "this_package": "Sagar Thakrar with substantial OpenAI Codex assistance; analytic real rank-three matrix lemma, two-block label transfer and exact controls. No independent human review or formal proof claimed." + } +} diff --git a/research/fstar-eight-line-floor/TASK.json b/research/fstar-eight-line-floor/TASK.json new file mode 100644 index 0000000000..01b84e8814 --- /dev/null +++ b/research/fstar-eight-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 the eight-line rational three-total anchor-box floor box(M)>=5 under nonzero diagonal and canonical tau>=1, following the concrete PR3393 handoff.", + "scope_change_reason": "Handoff-first continuation after refreshing canonical main and revision 6, replaying the original baseline, and checking complete open/closed PR and Discussion snapshots. This answers the next unresolved scoped F-star line-count implication, rather than duplicating joint-frame pricing audits.", + "bottleneck_link": "Closes the next floor(2v/3) threshold in the tau>=1 anchor-box route. It does not admit a supplier or change the selected kappa.", + "budget_minutes": 60, + "stop_rule": "Structural checkpoint after 20 minutes; stop this round with a scoped proof/counterexample or an exact reusable obstruction by approximately 60 minutes. No unstructured 56-arc census.", + "outcome": "completed", + "evidence": "PROOF.md gives a real rank-three ordered-triple theorem and an asymmetric two-block box witness. verify.py supplies exact rational construction controls and authenticates the frozen PR3393 independent oracle; RESULT.json records the finite checks separately from the analytic proof.", + "author": "Sagar Thakrar, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance, including separate proof, exact-control and independent-review agents. Separate AI runs are not independent human review.", + "open_questions": [ + { + "question": "Do nine rational three-total lines with nonzero diagonal and tau>=1 always have box>=6?", + "why_it_matters": "This is the next threshold in floor(2v/3); the present ordered triple plus pair only keeps five.", + "first_step": "Test whether rank three forces two disjoint transitive nonzero triples on nine indices. Begin with the three-block 3,3,3 duplication, which has box six, and distinguish this sufficient matrix condition from the full anchor-box question.", + "blocked_by": "One transitive triple leaves six vertices, which can themselves have no transitive triple. Choosing a better first triple or using additional anchor information requires a new argument." + } + ] +} diff --git a/research/fstar-eight-line-floor/VERIFY.json b/research/fstar-eight-line-floor/VERIFY.json new file mode 100644 index 0000000000..3bf715b30d --- /dev/null +++ b/research/fstar-eight-line-floor/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 ordered-triple/two-block construction, frozen independent-oracle agreement, rational fixture and semantic rank/parity/order controls. The general theorem is the analytic PROOF.md, not a finite census or machine proof." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-Werror", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat all exact controls with Python isolation and optimization; proof-relevant rejection checks remain active without assertions." + } + ] +} diff --git a/research/fstar-eight-line-floor/inputs/pr3393-independent_box.py b/research/fstar-eight-line-floor/inputs/pr3393-independent_box.py new file mode 100644 index 0000000000..d15e05f45e --- /dev/null +++ b/research/fstar-eight-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-eight-line-floor/verify.py b/research/fstar-eight-line-floor/verify.py new file mode 100644 index 0000000000..232ceab8ec --- /dev/null +++ b/research/fstar-eight-line-floor/verify.py @@ -0,0 +1,283 @@ +#!/usr/bin/env python3 +"""Finite exact controls for the separate written eight-line proof. + +SPDX-License-Identifier: Apache-2.0 +Sagar Thakrar, with substantial OpenAI Codex assistance. +""" + +import argparse +from fractions import Fraction +import hashlib +from itertools import combinations, permutations +import json +from pathlib import Path +import types + +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, package=HERE): + manifest = json.loads((package / "SOURCES.json").read_text()) + rows = [(root, row) for row in manifest["files"] if row["usage"] == "input"] + rows += [(package, row) for row in manifest.get("frozen_sources", [])] + inputs = {} + for base, row in rows: + data = (base / row["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == row["sha256"], "Input changed: " + row["path"]) + inputs[row["path"]] = data + require(ORACLE in inputs, "Missing authenticated independent oracle") + return inputs + + +def load_oracle(inputs): + module = types.ModuleType("frozen_independent_box") + module.__file__ = str(HERE / ORACLE) + exec(compile(inputs[ORACLE], module.__file__, "exec"), module.__dict__) + return module + + +def rank(matrix): + rows = [list(map(Fraction, row)) for row in matrix] + current = 0 + for column in range(len(rows[0]) if rows else 0): + pivot = next((i for i in range(current, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[current], rows[pivot] = rows[pivot], rows[current] + divisor = rows[current][column] + rows[current] = [x / divisor for x in rows[current]] + for i in range(current + 1, len(rows)): + multiplier = rows[i][column] + rows[i] = [x - multiplier * y for x, y in zip(rows[i], rows[current])] + current += 1 + return current + + +def product_matrix(P, Q): + return [[sum(Fraction(x) * y for x, y in zip(p, q)) for q in Q] for p in P] + + +def zero_arcs(matrix): + return [(i, j) for i in range(len(matrix)) for j in range(len(matrix)) + if i != j and matrix[i][j] == 0] + + +def parity(left, right): + return (left & right).bit_count() & 1 + + +def admit(matrix, A, B): + require(len(matrix) == len(A) == len(B) == 8 and all(len(row) == 8 for row in matrix), + "Expected eight lines") + require(all(type(mask) is int and 0 <= mask < 8 for mask in A + B), "Invalid anchor mask") + require(all(matrix[i][i] != 0 for i in range(8)), "Zero diagonal") + require(all(A[i] & B[i] for i in range(8)), "Empty tied set") + require(rank(matrix) <= 3, "Rank exceeds three") + require(all(parity(A[i], B[j]) == 0 for i, j in zero_arcs(matrix)), "SG violation") + + +def forward_nonzero(matrix, order): + return all(matrix[i][j] != 0 for position, i in enumerate(order) for j in order[position + 1:]) + + +def ordered_triple(matrix): + return next((list(order) for order in permutations(range(len(matrix)), 3) + if forward_nonzero(matrix, order)), None) + + +def two_block_witness(matrix, A, B, first, last): + kept = list(first) + list(last) + require(len(kept) == len(set(kept)), "Overlapping blocks") + require(forward_nonzero(matrix, first) and forward_nonzero(matrix, last), "Forward zero within block") + a, b = [0] * len(matrix), [0] * len(matrix) + for line in kept: + tied = A[line] & B[line] + require(tied != 0, "Empty tied set") + unit = tied & -tied + a[line], b[line] = (A[line], unit) if line in first else (unit, B[line]) + return {"a": a, "b": b, "kept": kept, "order": kept} + + +def literal_witness(matrix, A, B, witness): + a, b, kept, order = (witness[key] for key in ("a", "b", "kept", "order")) + if len(a) != len(A) or len(b) != len(B) or len(set(kept)) != len(kept): + return False + if sorted(kept) != sorted(order) or any(type(i) is not int or not 0 <= i < len(A) 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] & ~A[i] or b[i] & ~B[i] + or parity(a[i], b[i]) != 1 for i in kept): + return False + return all(matrix[i][j] != 0 or parity(a[i], b[j]) == 0 + for position, i in enumerate(order) for j in order[position + 1:]) + + +def construct(matrix, A, B): + admit(matrix, A, B) + first = ordered_triple(matrix) + require(first is not None, "No directed nonzero triple found") + remaining = [i for i in range(8) if i not in first] + last = next(([i, j] for i, j in permutations(remaining, 2) if matrix[i][j] != 0), None) + require(last is not None, "No complementary nonzero edge found") + witness = two_block_witness(matrix, A, B, first, last) + require(literal_witness(matrix, A, B, witness), "Constructed witness failed its definition") + return first, last, witness + + +def rejected(call, text): + try: + call() + except ValueError as error: + require(text in str(error), "Unexpected rejection: " + str(error)) + else: + raise ValueError("Required rejection did not occur: " + text) + + +def fixture(oracle): + P0 = [(-1, -3, 0), (1, -1, -2), (3, 3, 3)] + Q0 = [(1, -3, 2), (3, -1, -2), (3, -1, 2)] + sizes = (3, 3, 2) + P = [P0[i] for i, size in enumerate(sizes) for _ in range(size)] + Q = [Q0[i] for i, size in enumerate(sizes) for _ in range(size)] + matrix = product_matrix(P, Q) + data = oracle.rational_data(P, Q) + A, B = [3] * 6 + [7] * 2, [3] * 8 + require(data["M"] == matrix and data["a0"] == A and data["b0"] == B + and data["tau"] == [2] * 8 and data["gamma"] == 0, "Frozen normalization differs") + first, last, witness = construct(matrix, A, B) + require(oracle.check_witness(A, B, zero_arcs(matrix), witness), "Frozen witness replay failed") + labels = [1] * 3 + [2] * 3 + [0] * 2 + six = {"a": labels, "b": labels, "kept": list(range(6)), "order": list(range(6))} + require(literal_witness(matrix, A, B, six) and oracle.check_witness(A, B, zero_arcs(matrix), six), + "Six-line positive witness failed") + groups = [0] * 3 + [1] * 3 + [2] * 2 + require(all(len({groups[i] for i in kept}) == 3 for kept in combinations(range(8), 7)), + "Seven-set block coverage failed") + require(all(matrix[i][j] == 0 for i in range(8) for j in range(8) if groups[i] != groups[j]), + "Cross-block zeros failed") + unit_mutant = {**witness, "a": [1 if i in witness["kept"] else 0 for i in range(8)], + "b": [1 if i in witness["kept"] else 0 for i in range(8)]} + require(not literal_witness(matrix, A, B, unit_mutant), "Symmetric unit mutation was accepted") + receipt = {"P": P, "Q": Q, "M": [[int(x) for x in row] for row in matrix], "rank": rank(matrix), + "A": A, "B": B, "tau": [2] * 8, "first": first, "last": last, "five_witness": witness, + "six_witness": six, "box": 6, "symmetric_unit_mutation_rejected": True, + "upper_bound": "Every seven-set meets three zero-separated blocks; a triangular rank3 label minor exceeds the two-dimensional target-label span."} + return matrix, A, B, P, Q, receipt + + +def admission_controls(oracle, matrix, A, B): + rank4 = [[int(i // 2 == j // 2) for j in range(8)] for i in range(8)] + require(rank(rank4) == 4 and ordered_triple(rank4) is None, "Rank-four graph control") + require(all(parity(3, 3) == 0 for _i, _j in zero_arcs(rank4)), "Rank-four SG control") + rejected(lambda: admit(rank4, [3] * 8, [3] * 8), "Rank exceeds") + ones = [1] * 8 + rejected(lambda: admit(matrix, ones, ones), "SG violation") + require(oracle.find_kept(ones, ones, zero_arcs(matrix), 4) is None, + "SG-failing all-unit anchors unexpectedly keep four") + three = two_block_witness(matrix, ones, ones, [0, 1, 2], []) + require(literal_witness(matrix, ones, ones, three), "All-unit three-witness failed") + bad_B = B.copy() + bad_B[0] = 4 + rejected(lambda: admit(matrix, A, bad_B), "Empty tied set") + bad_matrix = [row.copy() for row in matrix] + bad_matrix[0][0] = 0 + rejected(lambda: admit(bad_matrix, A, B), "Zero diagonal") + return {"rank4_has_no_ordered_triple": True, "rank4_admission_rejected": True, + "sg_failing_anchors_box": 3, "empty_ties_rejected": True, "zero_diagonal_rejected": True} + + +def directed_controls(): + P = [(1, 1, 0), (1, 3, 0), (3, 1, 0)] + Q = [(1, -3, 0), (1, -1, 0), (3, -1, 0)] + matrix = product_matrix(P, Q) + require(rank(matrix) == 2 and all(matrix[i][i] for i in range(3)), "Directed cycle rank") + require(all(matrix[i][j] or matrix[j][i] for i, j in combinations(range(3), 2)), "Missing graph triangle") + require(ordered_triple(matrix) is None, "Unordered triangle was confused with directed triple") + rejected(lambda: two_block_witness(matrix, [3] * 3, [3] * 3, [0, 1, 2], []), "Forward zero") + circulant = [[int(i == j or (j - i) % 8 in (2, 3)) for j in range(8)] for i in range(8)] + require(ordered_triple(circulant) is None and rank(circulant) > 3, "Circulant boundary") + require(all(any(circulant[i][j] or circulant[j][i] for i, j in combinations(triple, 2)) + for triple in combinations(range(8), 3)), "Circulant has an independent triple") + return {"rank2_directed_cycle": [[int(x) for x in row] for row in matrix], + "unordered_triangle_is_insufficient": True, "circulant_rank": rank(circulant), + "circulant_has_no_ordered_triple_or_independent_triple": True} + + +def check_schur(matrix, indices): + require(all(matrix[i][i] != 0 and all(i == j or matrix[i][j] == 0 for j in indices) + for i in indices), "Schur basis is not invertible diagonal") + for u in range(len(matrix)): + for v in range(len(matrix)): + reconstructed = sum(Fraction(matrix[u][i]) * matrix[i][v] / matrix[i][i] for i in indices) + require(matrix[u][v] == reconstructed, "Schur identity mismatch") + + +def trace_product(left, right): + return sum(left[i][j] * right[j][i] for i in range(len(left)) for j in range(len(left))) + + +def algebra_controls(matrix, P, Q): + check_schur(matrix, [0, 3, 6]) + altered = [row.copy() for row in matrix] + altered[1][2] += 1 + rejected(lambda: check_schur(altered, [0, 3, 6]), "Schur identity mismatch") + terms = [[[q[i] * p[j] for j in range(3)] for i in range(3)] for p, q in zip(P, Q)] + require(all(trace_product(terms[i], terms[j]) == matrix[i][j] * matrix[j][i] + for i in range(8) for j in range(8)), "Rank-factor trace identity") + require(all(trace_product(terms[i], terms[i]) == matrix[i][i] ** 2 > 0 for i in range(8)), + "Positive diagonal trace identity") + symmetric = [[1, 2, 0], [2, -1, 3], [0, 3, 2]] + skew = [[0, 1, 2], [-1, 0, 3], [-2, -3, 0]] + require(trace_product(symmetric, symmetric) == sum(x * x for row in symmetric for x in row), + "Symmetric trace sign") + require(trace_product(skew, skew) == -sum(x * x for row in skew for x in row) == -28, + "Skew trace sign") + return {"schur_entries_checked": 64, "schur_altered_entry_rejected": True, + "factor_trace_pairs_checked": 64, "skew_trace_square": -28, + "symmetric_trace_square": trace_product(symmetric, symmetric)} + + +def source_control(): + from unittest.mock import patch + original = Path.read_bytes + def counterfeit(path): + return b"raise RuntimeError('unauthenticated oracle executed')\n" if path == HERE / ORACLE else original(path) + with patch.object(Path, "read_bytes", counterfeit): + rejected(build, "Input changed: " + ORACLE) + return True + + +def build(): + inputs = authenticate() + oracle = load_oracle(inputs) + matrix, A, B, P, Q, receipt = fixture(oracle) + result = {"schema_version": 1, "scope": "Finite controls supporting the separate analytic proof", + "fixture": receipt, "admission_controls": admission_controls(oracle, matrix, A, B), + "directed_controls": directed_controls(), "algebra_controls": algebra_controls(matrix, P, Q), + "oracle_sha256": hashlib.sha256(inputs[ORACLE]).hexdigest(), + "source_corruption_rejected_before_execution": source_control(), + "formal_proof_claimed": False, "exhaustive_matrix_census_claimed": False} + return json.loads(json.dumps(result)) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true") + args = parser.parse_args() + receipt = build() + if args.emit: + print(json.dumps(receipt, indent=2, sort_keys=True)) + else: + require(receipt == json.loads((HERE / "RESULT.json").read_text()), "Receipt mismatch") + print("PASS_FSTAR_EIGHT_LINE_CONTROLS constructed=5 fixture_box=6") + + +if __name__ == "__main__": + main()