From 9076f7e912cee985aff25af33d326d5d713d861e Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sat, 24 Oct 2026 15:08:18 -0500 Subject: [PATCH] Prove sharp five-thirds bounds for two binary helper classes --- .../CERTIFICATE.json | 798 ++++++++++++++++++ research/binary-helper-five-thirds/PROOF.md | 189 +++++ research/binary-helper-five-thirds/README.md | 105 +++ .../binary-helper-five-thirds/RESULT.json | 45 + .../binary-helper-five-thirds/SOURCES.json | 24 + research/binary-helper-five-thirds/TASK.json | 96 +++ .../binary-helper-five-thirds/VERIFY.json | 18 + research/binary-helper-five-thirds/verify.py | 327 +++++++ 8 files changed, 1602 insertions(+) create mode 100644 research/binary-helper-five-thirds/CERTIFICATE.json create mode 100644 research/binary-helper-five-thirds/PROOF.md create mode 100644 research/binary-helper-five-thirds/README.md create mode 100644 research/binary-helper-five-thirds/RESULT.json create mode 100644 research/binary-helper-five-thirds/SOURCES.json create mode 100644 research/binary-helper-five-thirds/TASK.json create mode 100644 research/binary-helper-five-thirds/VERIFY.json create mode 100644 research/binary-helper-five-thirds/verify.py diff --git a/research/binary-helper-five-thirds/CERTIFICATE.json b/research/binary-helper-five-thirds/CERTIFICATE.json new file mode 100644 index 0000000000..e15d415b76 --- /dev/null +++ b/research/binary-helper-five-thirds/CERTIFICATE.json @@ -0,0 +1,798 @@ +{ + "cycle": [ + { + "gain": 1, + "kind": "FULL", + "parameters": { + "h": 5, + "p": 4, + "u": 1, + "v": 6 + }, + "source": [], + "target": [ + 0, + 1 + ] + }, + { + "gain": 1, + "kind": "FULL", + "parameters": { + "h": 5, + "p": 4, + "u": 1, + "v": 6 + }, + "source": [ + 0, + 1 + ], + "target": [ + 2, + 1 + ] + }, + { + "gain": 3, + "kind": "FULL", + "parameters": { + "h": 7, + "p": 4, + "u": 3, + "v": 7 + }, + "source": [ + 2, + 1 + ], + "target": [] + } + ], + "edge_count": 10035, + "operators": 315, + "schema": "binary-helper-five-thirds/1", + "states": [ + { + "matrix": [], + "potential": 6 + }, + { + "matrix": [ + 0, + 0, + 3 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 0, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 1 + ], + "potential": 4 + }, + { + "matrix": [ + 0, + 1, + 1 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 1, + 2 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 1, + 3 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 1, + 5 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 1, + 6 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 1, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 2, + 3 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 2, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 0, + 3 + ], + "potential": 3 + }, + { + "matrix": [ + 0, + 3, + 2 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 3, + 3 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 3, + 5 + ], + "potential": 0 + }, + { + "matrix": [ + 0, + 3, + 6 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 3, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 4, + 3 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 4, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 5, + 3 + ], + "potential": 0 + }, + { + "matrix": [ + 0, + 5, + 6 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 5, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 6, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 0, + 7, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 1, + 1 + ], + "potential": 3 + }, + { + "matrix": [ + 1, + 1, + 1 + ], + "potential": 1 + }, + { + "matrix": [ + 1, + 1, + 2 + ], + "potential": 1 + }, + { + "matrix": [ + 1, + 1, + 3 + ], + "potential": 1 + }, + { + "matrix": [ + 1, + 1, + 5 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 1, + 6 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 1, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 2, + 3 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 2, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 3 + ], + "potential": 2 + }, + { + "matrix": [ + 1, + 3, + 2 + ], + "potential": 1 + }, + { + "matrix": [ + 1, + 3, + 3 + ], + "potential": 1 + }, + { + "matrix": [ + 1, + 3, + 5 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 3, + 6 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 3, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 4, + 3 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 4, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 5, + 3 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 5, + 6 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 5, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 1, + 6, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 1, + 7, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 2, + 1 + ], + "potential": 2 + }, + { + "matrix": [ + 2, + 1, + 1 + ], + "potential": 1 + }, + { + "matrix": [ + 2, + 1, + 3 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 1, + 5 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 1, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 3 + ], + "potential": 2 + }, + { + "matrix": [ + 2, + 3, + 1 + ], + "potential": 1 + }, + { + "matrix": [ + 2, + 3, + 2 + ], + "potential": 1 + }, + { + "matrix": [ + 2, + 3, + 3 + ], + "potential": 1 + }, + { + "matrix": [ + 2, + 3, + 5 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 3, + 6 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 3, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 4, + 1 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 4, + 3 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 4, + 5 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 4, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 5, + 2 + ], + "potential": 1 + }, + { + "matrix": [ + 2, + 5, + 3 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 5, + 5 + ], + "potential": 1 + }, + { + "matrix": [ + 2, + 5, + 6 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 5, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 2, + 6, + 3 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 6, + 5 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 6, + 6 + ], + "potential": 1 + }, + { + "matrix": [ + 2, + 6, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 7, + 2 + ], + "potential": 1 + }, + { + "matrix": [ + 2, + 7, + 3 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 7, + 5 + ], + "potential": 1 + }, + { + "matrix": [ + 2, + 7, + 6 + ], + "potential": 0 + }, + { + "matrix": [ + 2, + 7, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 3, + 3 + ], + "potential": 4 + }, + { + "matrix": [ + 3, + 3, + 3 + ], + "potential": 1 + }, + { + "matrix": [ + 3, + 3, + 5 + ], + "potential": 1 + }, + { + "matrix": [ + 3, + 3, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 3, + 5, + 3 + ], + "potential": 1 + }, + { + "matrix": [ + 3, + 5, + 5 + ], + "potential": 1 + }, + { + "matrix": [ + 3, + 5, + 6 + ], + "potential": 1 + }, + { + "matrix": [ + 3, + 5, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 3, + 6, + 5 + ], + "potential": 1 + }, + { + "matrix": [ + 3, + 6, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 3, + 7, + 3 + ], + "potential": 1 + }, + { + "matrix": [ + 3, + 7, + 6 + ], + "potential": 0 + }, + { + "matrix": [ + 3, + 7, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 6, + 5, + 3 + ], + "potential": 0 + }, + { + "matrix": [ + 6, + 5, + 7 + ], + "potential": 0 + }, + { + "matrix": [ + 6, + 7, + 7 + ], + "potential": 1 + }, + { + "matrix": [ + 7, + 7, + 7 + ], + "potential": 0 + } + ] +} diff --git a/research/binary-helper-five-thirds/PROOF.md b/research/binary-helper-five-thirds/PROOF.md new file mode 100644 index 0000000000..4049b1eb50 --- /dev/null +++ b/research/binary-helper-five-thirds/PROOF.md @@ -0,0 +1,189 @@ +# Two sharp binary bounds with different scopes + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. + +All vector spaces and matrices in this note are over F2. A matrix rank is an +integer. A trace is an element of F2. The two theorems have different +hypotheses. Neither theorem states a limit for every native controller. + +## A. Commuting supports of rank three + +Let E_1,...,E_f be pairwise commuting idempotents of rank three on a finite +vector space V. For each i, assume + + E_i R_i = R_i E_i = R_i, + R_i is similar to J_2(0) direct-sum [1] direct-sum 0. + +Here J_2(0) is the two-dimensional nilpotent Jordan block. Thus each R_i has +rank two, trace one, and is not idempotent. Suppose + + sum_i R_i = P, + +where P is an idempotent that commutes with every E_i. Then + + rank(P) <= 5*f/3. (A) + +In particular, if P=I_n, then n<=5*f/3. The statement permits zero target +coordinates. It imposes no order on the calls and no prefix condition. + +### Common coordinates and components + +An idempotent has minimal polynomial dividing x(x+1). These two roots are +distinct in F2. Commuting idempotents therefore have a common eigenbasis: +split V into the kernel and image of one idempotent, then repeat the split +on each invariant part. Include P in these splits. + +In this basis, E_i selects a three-element coordinate set S_i. The two-sided +support condition confines every nonzero entry of R_i to S_i times S_i. +Form a graph on the calls. Join i and j when |S_i intersect S_j|>=2. + +For one connected component C, put T_C=sum_{i in C} R_i. This matrix is +diagonal. To see this, fix distinct coordinates a,b. Any call that contributes +to entry (a,b) has both coordinates in its support. All such calls belong to +one component. Their total is zero because P is diagonal. Thus the entry is +zero in that component and is zero in all other components. + +A component with c calls has a support union of size at most c+2. Start at one +vertex of a spanning tree. Its support has size three. Each next vertex +shares at least two coordinates with a previous vertex and adds at most one. +Hence, when c>=3, + + rank(T_C) <= c+2 <= 5*c/3. (1) + +### Components with one or two calls + +A one-call component cannot occur: its sum would be R_i, which is diagonal +and hence idempotent over F2. This contradicts the stated Jordan type. + +For two calls, the support union has size at most four. Its diagonal sum D +has trace 1+1=0, so rank(D) is even. Rank four is impossible by the following +rank-additivity fact. + +Suppose A+B=D, where D is an idempotent of rank four and A,B each have rank +two. Since image(D) is contained in image(A)+image(B), equality of dimensions +gives + + image(D) = image(A) direct-sum image(B). + +For x in image(A), D x=x. The decomposition A x+B x=x into these two images is +unique, so A x=x and B x=0. Thus A is identity on its image, and A^2=A. +The same argument gives B^2=B. Apply this fact to the two R terms to obtain +a contradiction. Therefore rank(T_C)<=2 for a two-call component, which is +also at most 5*c/3. + +Finally, rank is subadditive. Sum the component bounds: + + rank(P) = rank(sum_C T_C) <= sum_C rank(T_C) <= 5*f/3. + +This proves (A). Components can share one coordinate; the rank inequality +does not assume that their diagonal supports are disjoint. + +### A sharp example + +Use coordinates a,b,c,d,e and let P_x denote the coordinate projector at x. +Set + + N_1 = (b+c)(b*+c*), N_3 = (c+d)(c*+d*), + R_1 = P_a + N_1, + R_2 = P_b + P_c + P_d + N_1 + N_3, + R_3 = P_e + N_3. + +The supports are abc, bcd, cde. Each term has the required Jordan type and +the sum is I_5. Thus three calls attain five outputs. + +This example also satisfies the stage order condition + + [E_i, sum_{j0 the maximum ratio (g-h)/f is exactly 5/3. + +### Complete finite certificate + +The code enumerates every parameter tuple in the stated FULL alphabet and +retains its matrix. There are 315 distinct matrices. It enumerates every +nonzero u,v pair for each THIN support size. Breadth-first closure from the +empty state reaches 94 canonical states and 20,020 legal raw transitions. + +For each source, target, and operation type, retaining only the largest gain +leaves 10,035 transitions. A discarded smaller gain cannot improve the +claimed bound. The verifier checks the potential on all raw transitions too. + +The certificate assigns an integer z(S) to each reachable state S. For every +edge S->T with counts (g,h,f), it verifies + + z(T)-z(S) >= 3*g-3*h-5*f. (2) + +Sum (2) along a closed word. The potentials cancel, proving (B). Each +certificate transition is also checked against the declared matrix rule. +The retained witness starts at the empty state, uses three FULL operations, +and returns there with five outputs and no THIN. This proves sharpness. + +The mathematical implication from a valid potential to (B) is elementary. +The finite enumeration and the retained potential are checked by the supplied +program. This is a finite computational certificate, not proof-assistant +acceptance or a claim about an unrestricted controller grammar. + +## Verification boundaries + +The verifier also checks all 84 three-dimensional matrices of the stated +Jordan type and all 28,224 two-call embeddings into a four-coordinate union. +The only diagonal sum ranks are zero and two. This finite check supports the +written two-call argument; it does not replace the general proof above. + +Rejected controls include a lowered tight potential, a missing reachable +state, an unpaid THIN query, a non-nilpotent native direction, and a changed +motif coefficient. The identity on three coordinates is retained as a +counterexample after the Jordan-type hypothesis is dropped. + +Neither theorem permits an unproved complex reduction modulo two. Neither +proves native input access, helper restoration, supplier admission, complete +pricing, or a multiplication exponent. Those obligations remain separate. diff --git a/research/binary-helper-five-thirds/README.md b/research/binary-helper-five-thirds/README.md new file mode 100644 index 0000000000..cba553ae7e --- /dev/null +++ b/research/binary-helper-five-thirds/README.md @@ -0,0 +1,105 @@ +# Sharp 5/3 bounds for two binary helper-controller classes + +This package gives a scoped negative result and a sharp binary construction. +It proves two distinct bounds on Q outputs per FULL call. The complete kappa +calculation does not improve. + +- **Global support theorem:** commuting rank-three stage projectors, with each + query term supported on its stage and of type `J_2(0) direct-sum [1]`, give + at most `5*f/3` Q outputs from f FULL terms. The proof also permits D-only + target coordinates and needs no call order. +- **Finite adaptive theorem:** a grammar with at most three live coordinates + permits outside-support helper feedback and paid THIN queries. Its 94-state, + 10,035-edge graph has exact maximum `(Q outputs - THIN calls)/FULL = 5/3`. + +Read [the proof and exact scope](PROOF.md), +[the integer potential and attaining word](CERTIFICATE.json), and +[the deterministic verification receipt](RESULT.json). The two theorems have +different hypotheses. The finite graph is not an exhaustive model of native +controllers. A three-FULL, five-output example attains both bounds; its full +binary polynomial endpoint is checked. + +A later local-only +[catalyst extension](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19156336) +reports 188 states and 32,110 edges with the same 5/3 bound. It permits one +completed Q coordinate to remain live and credits the released 94-state +search. This package does not claim that broader result or that its own +finite grammar is the largest checked class. + +## Reproduce + +Python 3.12 or later and its standard library are sufficient. No native source, +network call, solver, or pending PR is a runtime dependency. + +```sh +python3.12 -B scripts/research_package.py --package research/binary-helper-five-thirds +python3.12 -O -B research/binary-helper-five-thirds/verify.py +``` + +The first command ends with: + +```text +PASS_REGISTERED_RESEARCH_PACKAGE research/binary-helper-five-thirds outcome=negative-result +``` + +The direct verifier prints `PASS_BINARY_HELPER_FIVE_THIRDS` in its JSON result +and compares the result with `RESULT.json`. It checks all 20,020 raw graph +transitions, the integer potential, the sharp binary polynomial word, and +28,224 two-term support cases. Meaningful perturbations must fail: a changed +potential, omitted state, unpaid THIN query, invalid native direction, and +wrong endpoint coefficient. Normal and optimized Python use explicit checks. + +For a trusted source export, run the same direct verifier after extraction. +The registered runner needs Git history for the provenance pins. The direct +verifier does not. `--write` regenerates the receipt and is an authoring option. + +## Scope and effect on kappa + +The current publication base is `32890bc5de034ab8fc93ac88ead7279a6a416d04`. +The selected record and task card at that base are historical provenance in +[SOURCES.json](SOURCES.json). The assigned task changed from caller design to +publication of these scoped bounds; [TASK.json](TASK.json) records that change. + +There is no new recursive invoice or claimed kappa. The operation ratio is +not a multiplication exponent. The source interface, fixed cover maps, +owned state, complex phases, recursive pricing, and supplier admission are +not checked here. No selected source or frontier file is changed. Earlier +floating-point tariff screens are excluded from the proof and verifier. + +The original search also tested larger finite components, kernel packets, +D-only Gram factors, and fresh-axis cuts. Those bounded records are retained +in the coordinated closeout archive. They supply no general impossibility +claim and are not dependencies of this package. + +## Open next questions + +The one-catalyst finite extension already has a local result at the link +above; repeating that census is not the proposed next task. A useful next +question is whether a source-compatible packet outside the global support +hypothesis and outside both finite grammars can beat the bound. First give +its exact binary matrices and full source obligations. A favorable matrix +word would still need a signed complex identity and complete paid and target +accounting. This package does not reserve that work. + +A separate review can check the component proof and the grammar-to-native +boundary. The program certifies the finite graph, not the physical scope of +all possible native words. These questions are also recorded in TASK.json. + +## Credit + +Cinna Davis / 1337isnot1337 supplied the earlier commuting-projector tangent +reduction and support-pair obstruction in the +[productive-controller proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/productive-controller-basis-search/GLOBAL-PROOF.md). +The present rank-three component argument changes that two-coordinate +support model. The earlier package retains credit for the controller, native, +mixed-target, Clifford, and outer-recursion contributors. + +Dillon's [PR #5388](https://github.com/CrocSwap/integer-mult-bounds/pull/5388) +motivated the early helper-observation interface. The physical source and +wrapper work remain separate from this abstract binary certificate. The +later catalyst extension is credited above as broader finite coverage. + +New proof, code, and certificate by Ali Romman, with substantial OpenAI Codex +assistance. Parallel Codex workers checked the component argument and the +separation from the rank-four simple-graph model. This is not independent +human review. New work is under Apache-2.0. diff --git a/research/binary-helper-five-thirds/RESULT.json b/research/binary-helper-five-thirds/RESULT.json new file mode 100644 index 0000000000..40479f70d2 --- /dev/null +++ b/research/binary-helper-five-thirds/RESULT.json @@ -0,0 +1,45 @@ +{ + "controls": { + "free_thin_query_rejected": true, + "identity_term_violates_bound_without_Jordan_condition": true, + "lowered_potential_rejected": true, + "missing_state_rejected": true, + "non_nilpotent_source_rejected": true, + "wrong_motif_endpoint_rejected": true + }, + "graph": { + "cycle": { + "full": 3, + "gain": 5, + "thin": 0 + }, + "dominant_edges": 10035, + "exact_maximum": "5/3", + "full_matrices": 315, + "raw_edges": 20020, + "sha256": "314cc195731ca1ea933e6fab812107629ab087425e40c86e6018c2113b349e1f", + "states": 94 + }, + "scope": "Two separate binary classes; no complex lift, native admission, or kappa improvement.", + "sharp_motif": { + "exact_binary_polynomial_endpoint": true, + "full": 3, + "outputs": 5, + "stage_degrees": [ + 1, + 2, + 3, + 2, + 1 + ] + }, + "status": "PASS_BINARY_HELPER_FIVE_THIRDS", + "two_call_control": { + "diagonal_rank_counts": { + "0": 84, + "2": 81 + }, + "pairs": 28224, + "three_dimensional_terms": 84 + } +} diff --git a/research/binary-helper-five-thirds/SOURCES.json b/research/binary-helper-five-thirds/SOURCES.json new file mode 100644 index 0000000000..ad5b04d107 --- /dev/null +++ b/research/binary-helper-five-thirds/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/productive-controller-basis-search/GLOBAL-PROOF.md", + "usage": "provenance", + "git_blob": "74b67e22e6c063193a83825207cdec19a8fef7a4", + "sha256": "adc377b13924701bf5b0b50b091d8b69c90195d50ce0f6808f7fb4c7e0b16457" + } + ] +} diff --git a/research/binary-helper-five-thirds/TASK.json b/research/binary-helper-five-thirds/TASK.json new file mode 100644 index 0000000000..47ad9066a2 --- /dev/null +++ b/research/binary-helper-five-thirds/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer", + "4166", + "qq16-caller-install" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a sharp global rank-three support bound and certify a separate finite adaptive helper grammar.", + "scope_change_reason": "The user assigned publication of saved controller results after the kappa search. This package does not pursue the historical QQ16 caller card.", + "bottleneck_link": "Early helper queries change the caller alphabet. These two scoped bounds show where that change still cannot exceed five outputs per three FULL terms after paid THIN costs.", + "budget_minutes": 60, + "stop_rule": "Publish the two stated scopes with a complete finite certificate and sharp example. Do not extend either result to general controllers or claim kappa.", + "outcome": "negative-result", + "evidence": "PROOF.md, CERTIFICATE.json, RESULT.json, and the registered standard-library verifier.", + "author": "Ali Romman, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, code, experiments, and writing. Parallel Codex workers checked the component argument; no independent human review is claimed.", + "open_questions": [ + { + "question": "Can a source-compatible packet outside the global support model and the finite grammars beat five thirds?", + "why_it_matters": "Such a packet would change a proved local restriction before another pricing search.", + "first_step": "Give exact binary matrices and identify the failed hypothesis; preserve the full physical input and return contract.", + "blocked_by": "No profitable admitted packet or signed complex lift is supplied." + }, + { + "question": "Does an independent review accept the component proof and the exact grammar boundary?", + "why_it_matters": "The finite certificate does not authenticate an unrestricted physical model.", + "first_step": "Check the two-call rank argument and every state reduction rule against PROOF.md.", + "blocked_by": "The current checks use code and parallel AI review, not independent human acceptance." + } + ] +} diff --git a/research/binary-helper-five-thirds/VERIFY.json b/research/binary-helper-five-thirds/VERIFY.json new file mode 100644 index 0000000000..e7dc9b9cb8 --- /dev/null +++ b/research/binary-helper-five-thirds/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact full graph enumeration, integer potential, attaining binary polynomial word, two-call support census, and rejected mathematical perturbations." + } + ] +} diff --git a/research/binary-helper-five-thirds/verify.py b/research/binary-helper-five-thirds/verify.py new file mode 100644 index 0000000000..4fe6f2ce9b --- /dev/null +++ b/research/binary-helper-five-thirds/verify.py @@ -0,0 +1,327 @@ +#!/usr/bin/env python3 +"""Check two scoped binary helper bounds. Apache-2.0. + +Ali Romman, with substantial OpenAI Codex assistance. +This is an exact finite certificate check, not a formal proof checker. +""" +import argparse +from copy import deepcopy +from hashlib import sha256 +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def parity(value): + return value.bit_count() & 1 + + +def outer(column, row, size): + return tuple(row if column >> i & 1 else 0 for i in range(size)) + + +def add(*matrices): + result = [0] * len(matrices[0]) + for matrix in matrices: + for i, row in enumerate(matrix): + result[i] ^= row + return tuple(result) + + +def multiply(left, right): + result = [] + for row in left: + value = 0 + for j, other in enumerate(right): + if row >> j & 1: + value ^= other + result.append(value) + return tuple(result) + + +def rank(matrix): + pivots = {} + for row in matrix: + while row: + pivot = row.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = row + break + row ^= pivots[pivot] + return len(pivots) + + +def identity(size): + return tuple(1 << i for i in range(size)) + + +def reduce_state(rows): + size = len(rows) + isolated = [i for i in range(size) if rows[i] in (0, 1 << i) + and not any(rows[j] >> i & 1 for j in range(size) if j != i)] + gain = sum(bool(rows[i]) for i in isolated) + live = [i for i in range(size) if i not in isolated] + if len(live) > 3: + return None + options = [] + for order in itertools.permutations(live): + result = tuple(sum(((rows[i] >> j) & 1) << k for k, j in enumerate(order)) + for i in order) + options.append(result) + return min(options) if options else (), gain + + +def full_matrix(parameters): + u, v, p, h = (parameters[key] for key in ('u', 'v', 'p', 'h')) + need(all(isinstance(x, int) and not isinstance(x, bool) for x in (u, v, p, h)), + 'FULL parameters must be integers') + need(0 < u < 8 and 0 < v < 8 and 0 < p < 8 and 0 <= h < 16, + 'FULL support is outside the stated alphabet') + need(not parity(u & v) and not parity(u & p) and p != v, + 'FULL nilpotent and helper-row conditions failed') + return add(outer(u, v, 4), outer(h, p, 4)) + + +def full_alphabet(): + matrices = {} + for u, v, p, h in itertools.product(range(1, 8), range(1, 8), range(1, 8), range(16)): + if parity(u & v) or parity(u & p) or p == v: + continue + parameters = dict(u=u, v=v, p=p, h=h) + matrix = full_matrix(parameters) + matrices[matrix] = parameters + return list(matrices.items()) + + +def raw_edges(state, alphabet): + before = state + (0,) * (4 - len(state)) + for matrix, parameters in alphabet: + result = reduce_state(add(before, matrix)) + if result is not None: + target, gain = result + yield target, gain, 0, 1, parameters + size = min(4, len(state) + 1) + before = state + (0,) * (size - len(state)) + for u, v in itertools.product(range(1, 1 << size), repeat=2): + result = reduce_state(add(before, outer(u, v, size))) + if result is not None: + target, gain = result + yield target, gain, 1, 0, dict(u=u, v=v) + + +def build_graph(): + alphabet = full_alphabet() + states = [()] + seen = {()} + edges = [] + raw_count = 0 + for state in states: + best = {} + for target, gain, thin, full, parameters in raw_edges(state, alphabet): + raw_count += 1 + key = (target, thin, full) + if key not in best or gain > best[key][1]: + best[key] = (target, gain, thin, full, parameters) + for target, gain, thin, full, parameters in best.values(): + if target not in seen: + seen.add(target) + states.append(target) + edges.append((state, target, gain, thin, full, parameters)) + return alphabet, states, edges, raw_count + + +def check_potential(potential, edges): + for source, target, gain, thin, full, _ in edges: + need(potential[target] - potential[source] >= 3 * gain - 3 * thin - 5 * full, + 'An edge violates the integer potential') + + +def check_certificate(certificate, alphabet, states, edges): + need(certificate['schema'] == 'binary-helper-five-thirds/1', 'Certificate schema') + entries = certificate['states'] + potential = {tuple(row['matrix']): row['potential'] for row in entries} + need(len(entries) == len(potential) and set(potential) == set(states), + 'Certificate state coverage differs from reachable states') + need(all(isinstance(z, int) and not isinstance(z, bool) for z in potential.values()), + 'The potential must use integers') + need(certificate['operators'] == len(alphabet) == 315, 'FULL matrix census') + need(certificate['edge_count'] == len(edges) == 10035, 'Dominant edge census') + check_potential(potential, edges) + # Check all retained and discarded edges. A smaller reward must not escape. + for source in states: + raw = [(source, *edge) for edge in raw_edges(source, alphabet)] + check_potential(potential, raw) + state = () + gain = thin = full = 0 + for step in certificate['cycle']: + need(tuple(step['source']) == state, 'The witness does not start at its stated state') + parameters = step['parameters'] + if step['kind'] == 'FULL': + matrix = full_matrix(parameters) + before = state + (0,) * (4 - len(state)) + full += 1 + else: + need(step['kind'] == 'THIN', 'Unknown witness operation') + size = min(4, len(state) + 1) + u, v = parameters['u'], parameters['v'] + need(0 < u < (1 << size) and 0 < v < (1 << size), 'THIN support') + matrix = outer(u, v, size) + before = state + (0,) * (size - len(state)) + thin += 1 + result = reduce_state(add(before, matrix)) + need(result is not None, 'The witness leaves the finite grammar') + state, increment = result + need(state == tuple(step['target']) and increment == step['gain'], 'Witness edge mismatch') + gain += increment + need(state == () and full > 0 and 3 * (gain - thin) == 5 * full, + 'The witness does not attain the closed-word bound') + return potential, dict(gain=gain, thin=thin, full=full) + + +def jordan_type(matrix): + square = multiply(matrix, matrix) + return rank(matrix) == 2 and rank(square) == 1 and multiply(square, matrix) == square + + +def embed(matrix, support, size): + return tuple(sum(((matrix[support.index(i)] >> j) & 1) << k + for j, k in enumerate(support)) if i in support else 0 + for i in range(size)) + + +def two_call_control(): + terms = [tuple((bits >> (3 * i)) & 7 for i in range(3)) for bits in range(512)] + terms = [matrix for matrix in terms if jordan_type(matrix)] + need(len(terms) == 84, 'The three-dimensional Jordan-type census changed') + diagonal = {} + trials = 0 + for second_support in itertools.combinations(range(4), 3): + for first, second in itertools.product(terms, repeat=2): + total = add(embed(first, (0, 1, 2), 4), embed(second, second_support, 4)) + trials += 1 + if all(row in (0, 1 << i) for i, row in enumerate(total)): + degree = rank(total) + diagonal[degree] = diagonal.get(degree, 0) + 1 + need(degree <= 2, 'Two terms produced a diagonal of rank greater than two') + return dict(three_dimensional_terms=len(terms), pairs=trials, + diagonal_rank_counts={str(k): v for k, v in sorted(diagonal.items())}) + + +def polynomial_multiply(left, right): + size = len(left) + result = [[set() for _ in range(size)] for _ in range(size)] + for i, j, k in itertools.product(range(size), repeat=3): + for a, b in itertools.product(left[i][k], right[k][j]): + if a & b & 8: + continue + need(not (a & b & 7), 'A fresh stage symbol occurs twice') + term = a | b + if term in result[i][j]: + result[i][j].remove(term) + else: + result[i][j].add(term) + return result + + +def motif_terms(): + n1, n3 = outer(6, 6, 5), outer(12, 12, 5) + return [add(outer(1, 1, 5), n1), add((0, 2, 4, 8, 0), n1, n3), + add(outer(16, 16, 5), n3)] + + +def check_motif_endpoint(terms): + supports = [7, 14, 28] + word = [[{0} if i == j else set() for j in range(5)] for i in range(5)] + for stage, (support, matrix) in enumerate(zip(supports, terms)): + local = [[set() for _ in range(5)] for _ in range(5)] + for i, j in itertools.product(range(5), repeat=2): + d = (1 << stage) if support >> i & 1 else 0 + if i == j: + local[i][j].add(d) + if matrix[i] >> j & 1: + local[i][j].add(d | 8) + word = polynomial_multiply(local, word) + expected = [[set() for _ in range(5)] for _ in range(5)] + for i in range(5): + d = sum((1 << stage) for stage, support in enumerate(supports) if support >> i & 1) + expected[i][i] = {d, d | 8} + need(word == expected, 'The exact binary polynomial endpoint failed') + + +def motif_control(): + terms = motif_terms() + partial = (0,) * 5 + for support, matrix in zip((7, 14, 28), terms): + projector = tuple((1 << i) if support >> i & 1 else 0 for i in range(5)) + need(jordan_type(matrix), 'A motif term has the wrong Jordan type') + need(multiply(projector, matrix) == multiply(matrix, projector) == matrix, + 'A motif term leaves its stage support') + need(multiply(projector, partial) == multiply(partial, projector), + 'A motif stage does not commute with the prefix') + partial = add(partial, matrix) + need(partial == identity(5), 'The motif target is not identity') + check_motif_endpoint(terms) + return dict(full=3, outputs=5, stage_degrees=[1, 2, 3, 2, 1], + exact_binary_polynomial_endpoint=True) + + +def reject(action): + try: + action() + except ValueError: + return True + raise ValueError('A negative control was accepted') + + +def run(certificate): + alphabet, states, edges, raw_count = build_graph() + potential, cycle = check_certificate(certificate, alphabet, states, edges) + tight = next(edge for edge in edges if edge[0] != edge[1] + and potential[edge[1]] - potential[edge[0]] == 3 * edge[2] - 3 * edge[3] - 5 * edge[4]) + bad_potential = potential.copy() + bad_potential[tight[1]] -= 1 + missing = deepcopy(certificate) + missing['states'].pop() + wrong_terms = motif_terms() + wrong_terms[1] = tuple(row ^ (1 if i == 0 else 0) for i, row in enumerate(wrong_terms[1])) + controls = { + 'lowered_potential_rejected': reject(lambda: check_potential(bad_potential, edges)), + 'missing_state_rejected': reject(lambda: check_certificate(missing, alphabet, states, edges)), + 'free_thin_query_rejected': reject(lambda: check_potential(potential, [((), (), 1, 0, 0, {})])), + 'non_nilpotent_source_rejected': reject(lambda: full_matrix(dict(u=1, v=1, p=2, h=4))), + 'wrong_motif_endpoint_rejected': reject(lambda: check_motif_endpoint(wrong_terms)), + } + # Dropping the Jordan-type condition permits a one-call counterexample. + need(not jordan_type(identity(3)) and 3 * 3 > 5, 'Hypothesis control') + controls['identity_term_violates_bound_without_Jordan_condition'] = True + canonical_edges = sorted([list(a), list(b), g, h, f] for a, b, g, h, f, _ in edges) + graph_hash = sha256(json.dumps(canonical_edges, separators=(',', ':')).encode()).hexdigest() + return dict(status='PASS_BINARY_HELPER_FIVE_THIRDS', graph=dict( + full_matrices=len(alphabet), states=len(states), dominant_edges=len(edges), + raw_edges=raw_count, sha256=graph_hash, exact_maximum='5/3', cycle=cycle), + two_call_control=two_call_control(), sharp_motif=motif_control(), controls=controls, + scope='Two separate binary classes; no complex lift, native admission, or kappa improvement.') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true', help='Write the deterministic result receipt') + args = parser.parse_args() + result = run(json.loads((HERE / 'CERTIFICATE.json').read_text())) + path = HERE / 'RESULT.json' + if args.write: + path.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + need(json.loads(path.read_text()) == result, 'The retained result receipt differs') + print(json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main()