diff --git a/research/crossed-connector-caller/DISCOVERY.md b/research/crossed-connector-caller/DISCOVERY.md new file mode 100644 index 0000000000..cde7987ae1 --- /dev/null +++ b/research/crossed-connector-caller/DISCOVERY.md @@ -0,0 +1,95 @@ +# Discovery record + +The new theorem replaces these bounded searches. It does not derive an +unbounded claim from their counts. `discovery/RESULTS.json.gz` retains the +JSON outputs under their original file names. The archive uses fixed gzip +metadata. It is data, not instructions or a registered proof dependency. + +| Experiment | Coverage and result | +| --- | --- | +| Different C,D forward/reverse splits | All 75,600 relative orders: 71,880 degree-two and 3,720 degree-three contradictions | +| Four arbitrary minimum-rank aggregate connectors | All 3,150 relative orders: 2,995 degree-two and 155 degree-three contradictions | +| Arbitrary aggregate map in every gap | Fifteen paired-stage orders; each has a degree-three contradiction | +| Three calls per stage, arbitrary aggregate gaps | All 280 orders: 279 degree-three contradictions; word reduction gives a degree-four certificate for the remaining cyclic sweep | +| Four calls per stage | The cyclic sweep only; a bounded word-reduction certificate. This is not an order census | +| Three-way, zero-B matrix frames | 168 binary frames, 24 pair-compatible frames, 144 complete stage words; no compatible aggregate chronology found | +| Six arbitrary thin queries, three paired stages | Twenty orders; solver reports 17 unsat and 3 unknown. This first screen did not impose the separate stage-word conditions | +| Eight arbitrary thin queries | Sixty orders; 23 sat, 19 unsat, 18 unknown. Sat means necessary conditions only. The full word rejects some sat candidates | +| At most seven active queries in eight thin slots | Seventy orders; 22 unsat and 48 unknown | +| Grow a complete escape word by two leaves | Four fixed-source extension tests reported unsat: case11 with identical and independent new signatures, and cases13/20 with identical signatures. All retain eight thin factors and the old call order | +| Coupled ports, five rank-two thin queries | Eight orders at three leaves: two unsat and six unknown; no positive word | +| Three-stage cycle, two thin queries | Fifty basis-parameterized orders: 42 unsat, 8 unknown. Fifty direct-projector orders: 43 unsat, 7 unknown | + +`ESCAPE-WORD.json` selects case 11 of the eight-query search. Its complete +word is checked again by the separate default checker. All fields and all +independent stage exponents are retained. Case 8 in that same search is an +example that passes the pure stage word and first mixed coefficients but +fails higher mixed coefficients. `MIXED-ONLY-CANDIDATE.json` preserves it, and +the separate checker rejects it. + +## Discovery commands + +The algebra searches use the standard library. Run them from the package +folder or give the full path. They write new JSON files beside their scripts; +the archived results remain unchanged. + +```sh +python3 -B discovery/order_search.py --degree 2 +python3 -B discovery/aggregate_search.py --degree 2 +python3 -B discovery/gap_search.py +python3 -B discovery/multisplit_search.py --splits 3 --degree 3 +python3 -B discovery/ideal_completion.py --splits 3 --degree 4 +python3 -B discovery/m3_frame_search.py +python3 -B discovery/tournament_search.py +``` + +The original degree-four dense monomial expansion was interrupted before a +result because it was too large. `ideal_completion.py` uses bounded word +reduction and literal certificate expansion instead. It produced the retained +three- and four-way cyclic-sweep certificates. It is discovery code; it is +not a general decision procedure. + +The finite matrix searches used Python 3.12.13 and `z3-solver==5.3.2.0`. +The default verifier needs neither Z3 nor the search code. The published +cycle tool uses the direct-projector parameterization; the earlier +basis-parameterized results are historical discovery data. The current +six-query tool includes stage-word constraints added after its first run. +These changes are stated so that a different replay is not treated as the +same frozen experiment. + +```sh +python3 -B discovery/leaf_echo_search.py --thin 8 --cases 60 --timeout 4000 --seed 3 +python3 -B discovery/leaf_echo_search.py --thin 8 --budget 7 --cases 70 --timeout 4000 --seed 3 +python3 -B discovery/cycle_search.py --g 3 --thin 2 --cases 50 --timeout 5000 --seed 91 +python3 -B discovery/coupled_five_search.py --cases 8 --timeout 10000 +python3 -B discovery/grow_escape.py --case 11 --distinct --timeout 30000 +python3 -B discovery/grow_escape.py --case 13 --timeout 30000 +python3 -B discovery/grow_escape.py --case 20 --timeout 30000 +``` + +The growth model retains every old query factor on the old coordinates and +the old call order. New full calls can enter any gap. It allows either equal +or independent signatures for the two new leaves. Its four negative results +do not exclude changing an old query or order, or other source words. + +Time limits are milliseconds per solver call. A timeout is unknown. The +solver models and timing-dependent statuses are not independent theorem +certificates. A rerun can choose a different model. Use `check.py` to verify +the frozen full positive word, rather than expect a solver to emit identical +bytes. + +## Orientation and boundaries + +Canonical main was refreshed before selection and before the aggregate and +cycle pivots. Its base was `df0137efd35e11b4445734bf612bdd4c7ebc330c`, with +selected kappa .00310045 and priority revision seven. The complete remote +overlap refresh at 03:10 UTC covered 344 PRs and 4,952 Discussion records; +7,655 local HEAD note paths were not searched by the sparse overlap scan. +Targeted historical controller notes were then read. No claim of exhaustive +novelty is made. Active P104, Cao and G20 native-word claims were kept separate. + +The scoped claim and changes are in Discussion5593, starting with +[the claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5593#discussioncomment-19187529). +PR5650 and PR5440 were comparison points, not source upgrades to the bill. +The pinned PR5599 tariff stays fixed. The stronger open BIT admission in +PR5653 does not itself supply a compatible complex caller. diff --git a/research/crossed-connector-caller/ESCAPE-WORD.json b/research/crossed-connector-caller/ESCAPE-WORD.json new file mode 100644 index 0000000000..aae71c6ad2 --- /dev/null +++ b/research/crossed-connector-caller/ESCAPE-WORD.json @@ -0,0 +1,351 @@ +{ + "source": "Finite search case11, seed3; all matrices over F2", + "scope": "Binary normalized operator only; six full calls and eight rank-one thin calls", + "case": 11, + "order": [ + 1, + 3, + 8, + 11, + 7, + 6, + 12, + 13, + 2, + 9, + 4, + 0, + 10, + 5 + ], + "status": "sat", + "calls": [ + { + "stage": 0, + "p": [ + 1, + 1, + 4, + 4, + 0, + 0, + 0, + 0 + ], + "r": [ + 5, + 5, + 5, + 5, + 0, + 0, + 0, + 0 + ] + }, + { + "stage": 0, + "p": [ + 0, + 3, + 0, + 12, + 0, + 0, + 0, + 0 + ], + "r": [ + 0, + 15, + 0, + 15, + 0, + 0, + 0, + 0 + ] + }, + { + "stage": 1, + "p": [ + 0, + 3, + 0, + 0, + 0, + 48, + 0, + 0 + ], + "r": [ + 0, + 51, + 0, + 0, + 0, + 51, + 0, + 0 + ] + }, + { + "stage": 1, + "p": [ + 1, + 1, + 0, + 0, + 16, + 16, + 0, + 0 + ], + "r": [ + 17, + 17, + 0, + 0, + 17, + 17, + 0, + 0 + ] + }, + { + "stage": 2, + "p": [ + 1, + 1, + 0, + 0, + 0, + 0, + 64, + 64 + ], + "r": [ + 65, + 65, + 0, + 0, + 0, + 0, + 65, + 65 + ] + }, + { + "stage": 2, + "p": [ + 0, + 3, + 0, + 0, + 0, + 0, + 0, + 192 + ], + "r": [ + 0, + 195, + 0, + 0, + 0, + 0, + 0, + 195 + ] + }, + { + "stage": 3, + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 0, + 104, + 0, + 104, + 104, + 0, + 104, + 0 + ] + }, + { + "stage": 3, + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 111, + 111, + 111, + 111, + 0, + 0, + 0, + 111 + ] + }, + { + "stage": 3, + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 2, + 0, + 2, + 0, + 0, + 2, + 0, + 2 + ] + }, + { + "stage": 3, + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 0, + 195, + 0, + 0, + 0, + 0, + 0, + 195 + ] + }, + { + "stage": 3, + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 5, + 5, + 5, + 5, + 0, + 0, + 0, + 0 + ] + }, + { + "stage": 3, + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 0, + 172, + 172, + 0, + 172, + 0, + 172, + 172 + ] + }, + { + "stage": 3, + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 60, + 60, + 60, + 0, + 60, + 0, + 60, + 0 + ] + }, + { + "stage": 3, + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 0, + 249, + 249, + 0, + 249, + 0, + 249, + 0 + ] + } + ], + "choices": [ + 5, + 1, + 5 + ] +} diff --git a/research/crossed-connector-caller/MIXED-ONLY-CANDIDATE.json b/research/crossed-connector-caller/MIXED-ONLY-CANDIDATE.json new file mode 100644 index 0000000000..ccce3c2910 --- /dev/null +++ b/research/crossed-connector-caller/MIXED-ONLY-CANDIDATE.json @@ -0,0 +1,349 @@ +{ + "calls": [ + { + "p": [ + 2, + 2, + 8, + 8, + 0, + 0, + 0, + 0 + ], + "r": [ + 10, + 10, + 10, + 10, + 0, + 0, + 0, + 0 + ], + "stage": 0 + }, + { + "p": [ + 3, + 0, + 12, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 15, + 0, + 15, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 0 + }, + { + "p": [ + 1, + 0, + 0, + 0, + 16, + 0, + 0, + 0 + ], + "r": [ + 17, + 0, + 0, + 0, + 17, + 0, + 0, + 0 + ], + "stage": 1 + }, + { + "p": [ + 0, + 2, + 0, + 0, + 0, + 32, + 0, + 0 + ], + "r": [ + 0, + 34, + 0, + 0, + 0, + 34, + 0, + 0 + ], + "stage": 1 + }, + { + "p": [ + 0, + 2, + 0, + 0, + 0, + 0, + 0, + 128 + ], + "r": [ + 0, + 130, + 0, + 0, + 0, + 0, + 0, + 130 + ], + "stage": 2 + }, + { + "p": [ + 1, + 0, + 0, + 0, + 0, + 0, + 64, + 0 + ], + "r": [ + 65, + 0, + 0, + 0, + 0, + 0, + 65, + 0 + ], + "stage": 2 + }, + { + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 80, + 0, + 80, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 3 + }, + { + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 3, + 3, + 3, + 0, + 3, + 0, + 3, + 0 + ], + "stage": 3 + }, + { + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 0, + 0, + 88, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 3 + }, + { + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 0, + 161, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 3 + }, + { + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 0, + 0, + 2, + 2, + 0, + 0, + 0, + 2 + ], + "stage": 3 + }, + { + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 5, + 5, + 5, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 3 + }, + { + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 0, + 15, + 15, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 3 + }, + { + "p": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "r": [ + 2, + 0, + 2, + 0, + 2, + 2, + 2, + 0 + ], + "stage": 3 + } + ], + "case": 8, + "choices": [ + 8, + 4, + 0 + ], + "order": [ + 5, + 13, + 7, + 3, + 9, + 8, + 6, + 4, + 12, + 2, + 1, + 10, + 0, + 11 + ], + "status": "sat" +} diff --git a/research/crossed-connector-caller/PAIR-CERTIFICATES.json b/research/crossed-connector-caller/PAIR-CERTIFICATES.json new file mode 100644 index 0000000000..d67c6fe17e --- /dev/null +++ b/research/crossed-connector-caller/PAIR-CERTIFICATES.json @@ -0,0 +1,1131 @@ +[ + { + "order": [ + [ + 0, + 0 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 1 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "terms": [ + [ + 13, + [], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 1 + ], + [ + 2, + 1 + ] + ], + "terms": [ + [ + 4, + [], + [ + 2 + ] + ], + [ + 8, + [], + [] + ], + [ + 8, + [], + [ + 1 + ] + ], + [ + 8, + [ + 1 + ], + [] + ], + [ + 8, + [ + 1 + ], + [ + 1 + ] + ], + [ + 13, + [], + [] + ], + [ + 13, + [], + [ + 1 + ] + ], + [ + 13, + [], + [ + 2 + ] + ], + [ + 13, + [ + 1 + ], + [] + ], + [ + 13, + [], + [ + 2, + 1 + ] + ], + [ + 14, + [], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ], + [ + 1, + 1 + ] + ], + "terms": [ + [ + 13, + [], + [] + ], + [ + 14, + [], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ], + [ + 1, + 1 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "terms": [ + [ + 0, + [ + 1 + ], + [] + ], + [ + 12, + [], + [] + ], + [ + 12, + [], + [ + 0 + ] + ], + [ + 13, + [], + [] + ], + [ + 13, + [], + [ + 0 + ] + ], + [ + 13, + [ + 0 + ], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 1, + 1 + ], + [ + 2, + 1 + ] + ], + "terms": [ + [ + 4, + [], + [] + ], + [ + 4, + [], + [ + 0 + ] + ], + [ + 4, + [], + [ + 2 + ] + ], + [ + 12, + [ + 1 + ], + [] + ], + [ + 13, + [], + [] + ], + [ + 13, + [], + [ + 1 + ] + ], + [ + 13, + [ + 1 + ], + [] + ], + [ + 14, + [], + [] + ], + [ + 14, + [ + 1 + ], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ], + [ + 1, + 1 + ] + ], + "terms": [ + [ + 4, + [], + [] + ], + [ + 12, + [ + 1 + ], + [] + ], + [ + 13, + [], + [ + 1 + ] + ], + [ + 14, + [], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 1, + 1 + ], + [ + 0, + 1 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "terms": [ + [ + 12, + [], + [] + ], + [ + 13, + [], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 1, + 1 + ], + [ + 2, + 0 + ], + [ + 0, + 1 + ], + [ + 2, + 1 + ] + ], + "terms": [ + [ + 12, + [], + [] + ], + [ + 13, + [], + [] + ], + [ + 13, + [], + [ + 2 + ] + ], + [ + 13, + [ + 2 + ], + [] + ], + [ + 14, + [], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 1, + 1 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ], + "terms": [ + [ + 13, + [], + [] + ], + [ + 14, + [], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ], + [ + 0, + 1 + ], + [ + 1, + 1 + ], + [ + 2, + 1 + ] + ], + "terms": [ + [ + 0, + [ + 2 + ], + [] + ], + [ + 4, + [], + [ + 0 + ] + ], + [ + 4, + [], + [ + 1 + ] + ], + [ + 4, + [], + [ + 2 + ] + ], + [ + 4, + [ + 2 + ], + [] + ], + [ + 4, + [], + [ + 0, + 1 + ] + ], + [ + 4, + [], + [ + 2, + 1 + ] + ], + [ + 8, + [], + [] + ], + [ + 8, + [ + 1 + ], + [] + ], + [ + 12, + [ + 1 + ], + [] + ], + [ + 12, + [ + 2 + ], + [] + ], + [ + 13, + [], + [] + ], + [ + 13, + [], + [ + 2 + ] + ], + [ + 13, + [ + 1 + ], + [] + ], + [ + 13, + [ + 2 + ], + [] + ], + [ + 13, + [ + 1 + ], + [ + 1 + ] + ], + [ + 14, + [], + [] + ], + [ + 14, + [], + [ + 0 + ] + ], + [ + 14, + [], + [ + 1 + ] + ], + [ + 14, + [], + [ + 2 + ] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ], + [ + 0, + 1 + ], + [ + 2, + 1 + ], + [ + 1, + 1 + ] + ], + "terms": [ + [ + 0, + [ + 2 + ], + [] + ], + [ + 12, + [], + [] + ], + [ + 12, + [], + [ + 0 + ] + ], + [ + 13, + [ + 0 + ], + [] + ], + [ + 14, + [], + [] + ], + [ + 14, + [], + [ + 0 + ] + ], + [ + 14, + [ + 0 + ], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 1 + ], + [ + 0, + 1 + ], + [ + 2, + 1 + ] + ], + "terms": [ + [ + 4, + [], + [ + 2 + ] + ], + [ + 4, + [], + [ + 2, + 2 + ] + ], + [ + 8, + [], + [] + ], + [ + 8, + [], + [ + 0 + ] + ], + [ + 8, + [], + [ + 1 + ] + ], + [ + 8, + [ + 1 + ], + [] + ], + [ + 8, + [ + 1 + ], + [ + 0 + ] + ], + [ + 8, + [ + 1 + ], + [ + 1 + ] + ], + [ + 12, + [], + [] + ], + [ + 12, + [], + [ + 0 + ] + ], + [ + 12, + [], + [ + 1 + ] + ], + [ + 12, + [ + 1 + ], + [] + ], + [ + 13, + [], + [ + 0 + ] + ], + [ + 13, + [], + [ + 1 + ] + ], + [ + 13, + [], + [ + 2 + ] + ], + [ + 13, + [ + 1 + ], + [] + ], + [ + 13, + [], + [ + 2, + 0 + ] + ], + [ + 13, + [], + [ + 2, + 1 + ] + ], + [ + 13, + [ + 1 + ], + [ + 2 + ] + ], + [ + 14, + [], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 1 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ] + ], + "terms": [ + [ + 4, + [], + [ + 2 + ] + ], + [ + 4, + [ + 2 + ], + [] + ], + [ + 13, + [], + [] + ], + [ + 13, + [], + [ + 1 + ] + ], + [ + 13, + [ + 1 + ], + [] + ], + [ + 14, + [], + [] + ], + [ + 14, + [], + [ + 1 + ] + ], + [ + 14, + [ + 1 + ], + [] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ], + [ + 0, + 1 + ], + [ + 1, + 1 + ] + ], + "terms": [ + [ + 0, + [], + [] + ], + [ + 4, + [], + [] + ], + [ + 12, + [], + [] + ], + [ + 13, + [], + [] + ], + [ + 14, + [], + [ + 0 + ] + ], + [ + 14, + [], + [ + 1 + ] + ] + ] + }, + { + "order": [ + [ + 0, + 0 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ], + [ + 1, + 1 + ], + [ + 0, + 1 + ] + ], + "terms": [ + [ + 13, + [], + [] + ], + [ + 14, + [], + [] + ] + ] + } +] diff --git a/research/crossed-connector-caller/PROOF.md b/research/crossed-connector-caller/PROOF.md new file mode 100644 index 0000000000..e3800fbcf1 --- /dev/null +++ b/research/crossed-connector-caller/PROOF.md @@ -0,0 +1,231 @@ +# A connector must distinguish leaves in both directions + +This is a theorem about finite matrices in characteristic two. It is not a +native multiplication theorem. No new kappa is established. + +## 1. Contract + +Let the main space be `W_0 + W_1 + ... + W_g`, with each block of dimension +`d > 0`. Block zero is the core. Stage j acts on the core and leaf j. On these +two blocks put + +```text +E_j = diag(I,I), T_j = [[I,I],[I,I]]. +``` + +Thus `T_j^2=0`. Stage j can have any finite number of full calls. Their +projectors `P_jh` form an orthogonal resolution of `E_j`, and commute with +`T_j`. Their query maps are `R_jh=P_jh T_j`. There is no bound on the number +of stages, the number of splits, the block dimension, or their call order. + +In the normalized ring `F[e,D_1,...,D_g]/(e^2)`, a full call is + +```text +(I+(D_j+1)P_jh)(I+e R_jh). +``` + +A thin call is `I+e Z`. The proof permits arbitrary matrices Z. In particular, +it does not impose a rank, a square-zero condition, or a count on thin calls. +The required word is `Q product_j (I+(D_j+1)E_j)`, where `Q=1+e`. +The main fields are independent. All D variables remain independent. + +This is the star stage contract from PR5631/5649, with arbitrary stage splits +and a much larger connector class. It excludes no general complex or dyadic +caller. It also excludes no caller with a different grouped stage map, a +nonfull stage, a different output, or paid idle multipliers. + +## 2. The one-sided theorem + +**Theorem.** A successful word cannot have three distinct leaves whose block +columns are identical in every thin matrix Z. It also cannot have three +leaves whose block rows are identical in every thin matrix Z. + +Only one of these two equalities is needed for exclusion. Thus changing the +forward split, adding more queries, increasing their rank, or adding more +stage splits cannot repair connectors which only see the sum of the leaves. + +### Local form and chronology + +Commutation with T and the local support give + +```text +P_jh = [[A_jh+B_jh, B_jh], [B_jh, A_jh+B_jh]], +R_jh = [[A_jh, A_jh], [A_jh, A_jh]]. +``` + +The A matrices form an orthogonal resolution of I. In particular, +`A_jh A_jk=0` for `h!=k`, `A_jh^2=A_jh`, and `sum_h A_jh=I`. +These statements do not require the A matrices of different stages to commute. +The orthogonal-resolution hypothesis also follows from full rank use: if the +projectors sum to E and their ranks sum to rank E, their images form a direct +sum. Each projector is then the corresponding coordinate projection on that +sum. Stages with a rank deficit are a different contract. + +Set all D variables to one. The coefficient of e requires `sum R=I`, including +thin queries. The mixed coefficient of `e(D_j+1)` then requires + +```text +sum_(full call i in stage j) [P_i, sum_(calls l later than i) R_l] = 0. (1) +``` + +This necessary condition follows by expanding the literal ordered word. +No full-word converse is used. + +For distinct selected stages j,k define + +```text +S_jk = sum_(call (j,h) before call (k,l)) A_jh A_kl. (2) +``` + +In (1), add block rows zero and j, and read block column k. The contribution +of good calls is S_jk. The contribution of a later thin map Z is +`A_jh (Z_0k+Z_jk)`. If the three selected leaf columns of every Z are equal, +this thin contribution is the same for the two choices of k other than j. +Consequently + +```text +S_jk = S_jl for each permutation (j,k,l) of the three stages. (3) +``` + +Other good stages do not contribute to these blocks. Thus the argument +restricts to any three selected leaves in a larger star. + +### The prefix determinant argument + +Read just the calls of the three selected stages in their original order. +Before a call with projection A from stage j, let P_k be the sum of the A +projections already read from stage k. Left multiplication of (2) by A and +orthogonality within stage j give + +```text +A S_jk = A(I+P_k). +``` + +Equation (3) gives `A P_k=A P_l`. Also `A P_j=0`. Therefore, for the total +prefix `S=P_0+P_1+P_2`, every update satisfies + +```text +A S=0. (4) +``` + +Introduce an independent central variable x. Equation (4) implies + +```text +(I+xA)(I+xS) = I+x(S+A). +``` + +Starting at S=0, the product of all these factors is `I+xS_final`. +At the end, `S_final=I+I+I=I`. On the other hand, an idempotent of rank r +has determinant `det(I+xA)=(1+x)^r`. Each stage is a resolution of I, +so its ranks sum to d. Taking determinants now gives + +```text +(1+x)^(3d) = det(product(I+xA)) = det((1+x)I) = (1+x)^d. +``` + +This is impossible for positive d. This proves the column statement for +all finite dimensions and all finite split counts. It uses no list of orders. +Transpose all matrices and reverse the order to obtain the row statement. + +## 3. A paid-rank and finite-field cut + +Assume g is at least three. The sum of the good queries is +`sum T_j`. Hence the thin sum must be + +```text +K = I+sum T_j = epsilon E_core + F+G, +epsilon = (g+1) mod 2, +F: each leaf -> core by I, G: core -> each leaf by I. +``` + +The rank of K is `2d`. Its column space is the core plus the diagonal leaf +space, and its row space is the core plus the leaf-sum space. + +Let U be the span of all thin images, and V the span of all thin row spaces. +Write `dim U=2d+a`, `dim V=2d+b`, and let R be the sum of thin ranks. +Factor each thin map at its actual rank, then concatenate those factors. +Sylvester's rank inequality gives + +```text +R >= dim U + dim V - rank K = 2d+a+b. (5) +``` + +Both a and b must be positive. Otherwise one side of the one-sided theorem +applies to all leaves. In particular **R >= 2d+2**, over any field of +characteristic two. + +For a finite field of size s, choose b additional row basis vectors beyond +the row space of K. Their restriction to one leaf is a `b by d` matrix. +There are at most `s^(bd)` such signatures. Equal signatures imply equal +leaf columns for every thin map. Each signature can occur at most twice. +The column-space argument is the same. Therefore + +```text +g <= 2 s^(bd), g <= 2 s^(ad), +R >= 2d + 2 h, h = min {z >= 0 : g <= 2 s^(dz)}. (6) +``` + +This is a necessary condition, not a construction or a sufficient test. +It concerns a common field and a fixed block basis. For one-port binary +copies, d=2. It gives R>=6 for g=3..8, R>=8 for g=9..32, and R>=10 for +g=33..128. For coupled ports, use the actual larger d. Do not apply the +one-port bound per port after ports have been coupled. + +At g=31, five rank-one connectors fail this cut. Five rank-two connectors +with d=4 meet it exactly: `2d+2=10`. Thus coupled pairs of ports are a precise +remaining target. The cut does not prove that such a word exists. + +## 4. Constructive escape and its price + +`ESCAPE-WORD.json` contains a complete eight-field binary word. It has three +paired stages, six full calls with rank-one queries, and eight rank-one thin calls. +Every local projector, query rank and compatibility relation is checked. +The verifier retains every exponent of each independent D variable and +checks every coefficient of the full word. It also checks that the thin +maps distinguish all three leaves in both directions. + +Thus the changed connector contract has a real positive operator. It does +not give a profitable supplier. At the pinned PR5599 tariff, 104 copies have +complete optimistic moment coefficients + +```text +208 H25 + 624 H9 + 6 helpers - 6 paid - 832 H1. +``` + +Its linear margin is -336. After common ranks are cancelled, all positive +terms have rank at least eight and all negative terms have rank at most +seven. For every `0<=t<=1`, the margin is at most `8^(t-1)*(-336)<0`. +Additional physical adapters cannot repair that price. + +The new cut still leaves a useful target. At g=127, ten thin queries are +allowed by (6) for one-port binary copies. The optimistic PR5599 profile +has a positive exact margin at saving `7/2000=.0035`, and its numerical +crossing is about .00364156. **No 127-leaf word is supplied.** This screen +also does not establish a characteristic-zero lift, native frame adapters, +compiler admission, an outer transfer, or a new kappa. + +A smaller coupled target is g=31 with five rank-two connectors per two-port +block. Its optimistic bill, scaled to 104 ports, also has positive exact +margin at .0035. It needs only 62 full calls. No such word is supplied either. +Coupling physical ports can require new frame maps; their costs must be +charged before this screen can become a supplier claim. + +## 5. Evidence and limits + +The main result is a written finite-dimensional matrix proof. The checker +also verifies fifteen exact free-algebra certificates for the paired-stage +case, without a solver or the discovery implementation. Matrix and formal +polynomial controls test the chronology extraction, restriction to three +leaves, prefix factorization and determinant formula. They support the +proof; finite tests alone do not prove its unbounded statements. + +The discovery archive retains changed C,D splits, arbitrary aggregate maps, +extra thin queries, a different cycle frame, and three-/four-way splits. +Timeouts remain unknown. Passing first mixed coefficients is not passing the +full word. No proof assistant or independent human acceptance is claimed. + +Credit Cinna Davis's controller and simplex work; PR5617/5631/5649 for the +query-frame and fixed-star line; and the complete P104/native/helper/compiler +lineage for the tariff. This proof, cut, search and escape word were prepared +for Ali Romman with substantial OpenAI Codex assistance. No subagents. +New work is Apache-2.0. diff --git a/research/crossed-connector-caller/README.md b/research/crossed-connector-caller/README.md new file mode 100644 index 0000000000..1ed7848890 --- /dev/null +++ b/research/crossed-connector-caller/README.md @@ -0,0 +1,87 @@ +# One-sided connector obstruction, rank cuts, and a complete escape word + +**No new kappa.** The new result is an unbounded obstruction with a short +proof, an explicit positive word outside it, and a precise search target +whose optimistic price remains favorable. + +In the full-rank star stage contract, no three leaves can have identical +columns in every thin connector. The same statement holds for rows. This +covers every finite port dimension, every finite number of orthogonal stage +splits, every call order, and any number or rank of connector queries. It +strictly extends [PR5649](https://github.com/CrocSwap/integer-mult-bounds/pull/5649), +which kept four prescribed connectors and two calls per stage. + +[PROOF.md](PROOF.md) replaces the order census by a prefix identity. The +forbidden chronology would make a matrix product have both determinants +`(1+x)^(3d)` and `(1+x)^d`. It also gives a rank and signature cut for arbitrary +connectors. For one-port binary copies, 127 leaves require at least ten thin +queries. Coupled ports must use their actual block dimension in this cut. + +[ESCAPE-WORD.json](ESCAPE-WORD.json) is a real binary escape: eight fields, +six full calls, eight thin queries, and sixteen exact coefficients in the +complete polynomial endpoint. Its connectors distinguish individual leaves. +The proof prices it and rejects every concave moment at the pinned P104 +bill. The separate 127-leaf, ten-query profile has an exact positive price +margin at saving .0035, but **has no operator**. A smaller target with 31 +leaves and five rank-two connectors also passes that price test. The new +cut permits its coupled-port budget and rejects the corresponding one-port +budget. Both are search targets. + +The cycle-frame and smaller-connector searches remain incomplete. Their +solver timeouts are retained as unknown. [DISCOVERY.md](DISCOVERY.md) records +what was searched and which positive candidates failed higher coefficients. +It also gives commands for the saved discovery tools and archive. + +## Reproduce + +Python 3.12 and the standard library suffice for the read-only checks. The +registered metadata check also needs the explicitly pinned PR5649 Git object. +In a fresh clone, fetch that provenance object first: + +```sh +git fetch https://github.com/CrocSwap/integer-mult-bounds.git 0c27282f56a0e8ec6c1fbad0f2ccca646d0d8442 +python3.12 -B scripts/research_package.py --package research/crossed-connector-caller +python3.12 -I -O -B research/crossed-connector-caller/verify.py +python3.12 -I -O -B research/crossed-connector-caller/test_verify.py +``` + +Expected status: `PASS_ONE_SIDED_CONNECTOR_OBSTRUCTION`. +[RESULT.json](RESULT.json) records the exact evidence. The independent checker +uses no solver or discovery module. It checks fifteen paired-order identities, +the full positive word, coupled chronology controls, the prefix factorization, +rank cuts, exact integer-power price intervals, and corruptions. + +The general theorem is a written matrix proof. Finite controls support it; +they do not constitute proof-assistant or independent human acceptance. The +binary word does not establish a characteristic-zero lift, native frame +adapters, ownership, a complete compiler, or a new outer bound. Selected +kappa remains .00310045 at the pinned base. This package changes no frontier. + +## Open next questions + +- Construct a long word whose connectors have distinct leaf signatures in + both directions. Start with 31 leaves and five rank-two queries per coupled + port pair, or 127 leaves and ten rank-one queries per binary copy. Both + optimistic prices pass at .0035. Use the saved word as a positive control. + The fixed-source growth tests fail; resynthesize old connector restrictions + or call order, then test every polynomial coefficient. +- Solve or certify the remaining finite searches. Seven thin queries at three + leaves and the separate cycle frame have timeout cases. First use exact + certificates or longer bounded solves on those saved cases. A timeout is + not an obstruction. +- Give a native lift and complete invoice for any profitable binary word. + Charge every adapter, helper, query, copy, clear, return and route. The + current P104 tariff is only an optimistic comparison for this algebra. + +Structured versions are in [TASK.json](TASK.json). Work began on canonical +main `df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority revision seven. +The canonical investigation is [Discussion5593](https://github.com/CrocSwap/integer-mult-bounds/discussions/5593). +The live remote overlap check covered 344 open PRs and 4,952 Discussion +records; the sparse local notes were incomplete. Active native-word claims +were kept separate. [SOURCES.json](SOURCES.json) records exact source pins. + +Credit Cinna Davis's controller/simplex work; PR5617/5631/5649 for the +query-frame and fixed-star work; and all retained P104, native, helper, +compiler and outer contributors. The vendored discovery alphabet retains +Cinna Davis's notice. Prepared for Ali Romman with substantial OpenAI Codex +assistance; no subagents. Apache-2.0. diff --git a/research/crossed-connector-caller/RESULT.json b/research/crossed-connector-caller/RESULT.json new file mode 100644 index 0000000000..879461d539 --- /dev/null +++ b/research/crossed-connector-caller/RESULT.json @@ -0,0 +1,170 @@ +{ + "authenticated_inputs": 1, + "controls": { + "chronology": { + "coupled_frames": 6, + "literal_mixed_coefficients": 18, + "one_sided_nonaggregate_frames": 6, + "prefix_equations": 84 + }, + "escape": { + "deleted_query_rejected": true, + "distinct_leaf_column_signatures": 3, + "distinct_leaf_row_signatures": 3, + "fields": 8, + "first_mixed_false_positive_rejected": true, + "full_calls": 6, + "full_polynomial_coefficients": 16, + "moved_call_rejected": true, + "thin_queries": 8 + }, + "paired_certificates": { + "deleted_term_rejected": true, + "maximum_degree": 4, + "orders": 15, + "terms": 105 + }, + "prefix": { + "matrix_flags": 60, + "prefix_updates": 180, + "projection_determinants": 60, + "restarted_walks_rejected": 60 + }, + "rank_cut_cases": [ + { + "d": 2, + "field_size": 2, + "g": 3, + "thin_rank_lower_bound": 6 + }, + { + "d": 2, + "field_size": 2, + "g": 4, + "thin_rank_lower_bound": 6 + }, + { + "d": 2, + "field_size": 2, + "g": 7, + "thin_rank_lower_bound": 6 + }, + { + "d": 2, + "field_size": 2, + "g": 8, + "thin_rank_lower_bound": 6 + }, + { + "d": 2, + "field_size": 2, + "g": 9, + "thin_rank_lower_bound": 8 + }, + { + "d": 2, + "field_size": 2, + "g": 31, + "thin_rank_lower_bound": 8 + }, + { + "d": 2, + "field_size": 2, + "g": 32, + "thin_rank_lower_bound": 8 + }, + { + "d": 2, + "field_size": 2, + "g": 33, + "thin_rank_lower_bound": 10 + }, + { + "d": 2, + "field_size": 2, + "g": 63, + "thin_rank_lower_bound": 10 + }, + { + "d": 2, + "field_size": 2, + "g": 127, + "thin_rank_lower_bound": 10 + }, + { + "d": 2, + "field_size": 2, + "g": 128, + "thin_rank_lower_bound": 10 + }, + { + "d": 2, + "field_size": 2, + "g": 129, + "thin_rank_lower_bound": 12 + }, + { + "d": 2, + "field_size": 2, + "g": 255, + "thin_rank_lower_bound": 12 + } + ] + }, + "limits": [ + "No kappa increase", + "The full escape word is binary algebra, not a physical native caller", + "The 127-leaf price profile has no operator", + "No proof-assistant or independent human acceptance" + ], + "pricing": { + "escape": { + "all_concave_moments_rejected": true, + "g": 3, + "linear_margin": -336, + "q": 104, + "signed_profile": { + "1": -14038, + "2": -2724, + "25": 208, + "3": -2958, + "4": -18, + "5": -942, + "6": -108, + "7": -54, + "8": 96, + "9": 3096 + }, + "thin_queries_per_copy": 8 + }, + "pinned_supplier": "PR5599 09dd0965711ca7eeb169057a420abab1c9052137", + "unconstructed_candidates": [ + { + "full_calls": 254, + "g": 127, + "moment_denominator": "1099511627776", + "moment_lower_numerator": "481572756146950", + "moment_upper_numerator": "481572756570322", + "ports_per_binary_block": 1, + "q": 104, + "saving": "7/2000", + "status": "POSITIVE_OPTIMISTIC_PRICE_ONLY; NO CALLER OR KAPPA CLAIM", + "thin_queries_per_native_port": 10 + }, + { + "full_calls": 62, + "g": 31, + "moment_denominator": "1099511627776", + "moment_lower_numerator": "268079792788678", + "moment_upper_numerator": "268079792892178", + "ports_per_binary_block": 2, + "q": 104, + "saving": "7/2000", + "status": "POSITIVE_OPTIMISTIC_PRICE_ONLY; NO CALLER OR KAPPA CLAIM", + "thin_queries_per_native_port": 5 + } + ] + }, + "scope": "Finite matrices over every characteristic-two field; any finite star stage splits and call order; one-sided equal leaf signatures", + "status": "PASS_ONE_SIDED_CONNECTOR_OBSTRUCTION" +} diff --git a/research/crossed-connector-caller/SOURCES.json b/research/crossed-connector-caller/SOURCES.json new file mode 100644 index 0000000000..3bc934f537 --- /dev/null +++ b/research/crossed-connector-caller/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/p104-helper-subspace-splits/RESULT.json", + "usage": "input", + "git_blob": "35f75c8555193c6e845cd52cc562ca23fd5924cb", + "sha256": "1d92e587915052110dfb3aca8890df5afdaf496164efa5a4a52e69ceeb3c70f3" + }, + { + "path": "research/productive-controller-basis-search/algebra.py", + "usage": "provenance", + "pin": "head:df0137efd35e11b4445734bf612bdd4c7ebc330c:research/productive-controller-basis-search/algebra.py", + "git_blob": "2f0d4f290c280cfdfc17714009a2ae0f220556d4", + "sha256": "ab85b113cd70e20c38f6b0c0e0501876b751206bcd2a7ea5a61054ce3b92f2b2" + }, + { + "path": "research/productive-controller-basis-search/GLOBAL-PROOF.md", + "usage": "provenance", + "pin": "head:df0137efd35e11b4445734bf612bdd4c7ebc330c:research/productive-controller-basis-search/GLOBAL-PROOF.md", + "git_blob": "74b67e22e6c063193a83825207cdec19a8fef7a4", + "sha256": "adc377b13924701bf5b0b50b091d8b69c90195d50ce0f6808f7fb4c7e0b16457" + }, + { + "path": "research/longer-coupled-port-caller/PROOF.md", + "usage": "provenance", + "pin": "head:0c27282f56a0e8ec6c1fbad0f2ccca646d0d8442:research/longer-coupled-port-caller/PROOF.md", + "git_blob": "7df31b1dac06fe966f190bcc0798dc9bba77eeb0", + "sha256": "b9784e6ab84e55ab13c44834a54c29d12a51aaae5c91ae2e4fc7fbfd24999f5d" + }, + { + "path": "research/longer-coupled-port-caller/nc_star.py", + "usage": "provenance", + "pin": "head:0c27282f56a0e8ec6c1fbad0f2ccca646d0d8442:research/longer-coupled-port-caller/nc_star.py", + "git_blob": "f9eb610002a9c28e0829c5755671f0824d035442", + "sha256": "d4f16d6800633143888d26d5e12be5f086f6d92e255883c287fe32da098840a4" + }, + { + "path": "research/longer-coupled-port-caller/search_orders.py", + "usage": "provenance", + "pin": "head:0c27282f56a0e8ec6c1fbad0f2ccca646d0d8442:research/longer-coupled-port-caller/search_orders.py", + "git_blob": "afbdb06c552d61c61e4a7a08c4a68fb1faa0a3e3", + "sha256": "f54fb7da58a790c2df61835e45d41780e3b80bf66685c2073d7c5da2a00eb573" + }, + { + "path": "research/longer-coupled-port-caller/search_star.py", + "usage": "provenance", + "pin": "head:0c27282f56a0e8ec6c1fbad0f2ccca646d0d8442:research/longer-coupled-port-caller/search_star.py", + "git_blob": "3091607d92bbbd2716a662af33929f7dd12b1827", + "sha256": "e5d0b0d335a7153438685f8a89373cfd035b4d4189e45a036915474b903cbb66" + } + ] +} diff --git a/research/crossed-connector-caller/TASK.json b/research/crossed-connector-caller/TASK.json new file mode 100644 index 0000000000..9bac84b1ad --- /dev/null +++ b/research/crossed-connector-caller/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "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": "One-sided connector obstruction for all finite full-rank star splits; paid-rank signature cuts; a complete binary escape word; different-frame discovery searches", + "scope_change_reason": "The user requests a changed connector or query frame. Four prescribed connectors were replaced by arbitrary one-sided connectors, then by leaf-specific queries and a cycle frame. The theorem now uses a prefix determinant argument and no order census.", + "bottleneck_link": "A different connector can retain useful full-call stages while using cheap thin queries; success requires a complete endpoint and paid bill.", + "budget_minutes": 120, + "stop_rule": "Complete and verify the unbounded theorem and real escape word. Do not claim a kappa increase from a price screen or an incomplete search.", + "outcome": "completed", + "evidence": "PROOF.md, ESCAPE-WORD.json, RESULT.json, PAIR-CERTIFICATES.json, DISCOVERY.md", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents.", + "open_questions": [ + { + "question": "Can 31 leaves use five rank-two thin queries per coupled port pair, or can 127 leaves use ten rank-one thin queries?", + "why_it_matters": "The new signature cut permits this profile and its optimistic P104 price passes at saving .0035.", + "first_step": "Resynthesize connector restrictions or call order, using the rank/signature cut and the saved coupled-five and full-word tools. The four fixed-source growth tests fail; do not repeat those templates unchanged.", + "blocked_by": "No such long word is known; signatures and price alone do not construct it." + }, + { + "question": "Do the remaining seven-query and cycle-frame cases have solutions?", + "why_it_matters": "These change the excluded contract and could guide a longer caller.", + "first_step": "Use the archived orders for longer bounded solves or exact contradiction certificates.", + "blocked_by": "The saved solver timeouts are unknown, not negative proofs." + }, + { + "question": "Can a profitable binary word be lifted to the actual native supplier?", + "why_it_matters": "Only a full physical bill and admitted outer transfer can improve kappa.", + "first_step": "Compile native maps, frame adapters, ownership and returns before pricing the complete caller.", + "blocked_by": "No profitable binary word or native lift is supplied by this package." + } + ] +} diff --git a/research/crossed-connector-caller/VALIDATION.json b/research/crossed-connector-caller/VALIDATION.json new file mode 100644 index 0000000000..5aaea2c9f0 --- /dev/null +++ b/research/crossed-connector-caller/VALIDATION.json @@ -0,0 +1,17 @@ +{ + "python": "3.12.13 (main, May 10 2026, 19:20:41) [Clang 22.1.3 ]", + "platform": "macOS-26.6.1-arm64-arm-64bit", + "base": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "registered": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed", + "optimized": "PASS_ONE_SIDED_CONNECTOR_OBSTRUCTION", + "mutations": 5, + "git_free_read_only": { + "path": "/var/folders/ph/5swjdlqd3997q5j1y6zvmty80000gp/T/imb-one-sided-final-e_mhg2tm", + "cwd": "/", + "PATH": "/nonexistent", + "status": "PASS_ONE_SIDED_CONNECTOR_OBSTRUCTION" + }, + "source_history": "Not run: PR5649 is an explicitly pinned open provenance source, not an ancestor of the new main base.", + "hosted_ci": "Not yet submitted", + "independent_human_review": "Not claimed" +} diff --git a/research/crossed-connector-caller/VERIFY.json b/research/crossed-connector-caller/VERIFY.json new file mode 100644 index 0000000000..90f5cf0861 --- /dev/null +++ b/research/crossed-connector-caller/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper-subspace-splits/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source authentication, full escape word, projected chronology, prefix determinant controls, exact pair certificates, rank cuts and integer-power pricing" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Reject changed certificate, query, source bill and result receipt" + } + ] +} diff --git a/research/crossed-connector-caller/check.py b/research/crossed-connector-caller/check.py new file mode 100644 index 0000000000..96570d3a1b --- /dev/null +++ b/research/crossed-connector-caller/check.py @@ -0,0 +1,296 @@ +"""Independent exact checks for the connector theorem and escape word. + +The default replay uses no search program, solver, or predecessor code. +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import itertools +import json +from pathlib import Path +import random + +PACKAGE=Path(__file__).resolve().parent + +def require(value,message): + if not value:raise ValueError(message) + +def eye(n):return tuple(1<>k&1)*(b[k]>>j&1) for k in range(len(b)))%2)<>j&1);rows[j],rows[p]=rows[p],rows[j] + for i in range(n): + if i!=j and rows[i]>>j&1:rows[i]^=rows[j] + return tuple(row>>n for row in rows) + +def product(a,b): + n=len(next(iter(a.values())));out={} + for x,ax in a.items(): + for y,by in b.items(): + if x[0]+y[0]>1:continue + key=tuple(u+v for u,v in zip(x,y));out[key]=add(out.get(key,zero(n)),mul(ax,by)) + return {k:v for k,v in out.items() if any(v)} + +def replay(calls,order,g): + n=len(calls[0]['p']);base=(0,)*(g+1);ebit=(1,)+(0,)*g + word={base:eye(n)};expected={base:eye(n),ebit:eye(n)};targets=[zero(n) for _ in range(g)] + for c in calls: + if c['stage']>j)&1 for i in range(n) for j in block) for c in thin)) + rows.append(tuple(tuple(c['r'][i] for i in block) for c in thin)) + require(len(set(columns))==3 and len(set(rows))==3,'The word must leave both equal-signature classes') + trap=json.loads((PACKAGE/'MIXED-ONLY-CANDIDATE.json').read_text());wrong,wanted=replay(trap['calls'],trap['order'],g) + for j in range(g): + key=[1,0,0,0];key[j+1]=1 + require(wrong.get(tuple(key),zero(n))==wanted.get(tuple(key),zero(n)),'First mixed coefficient control') + require(all(wrong.get(k,zero(n))==wanted.get(k,zero(n)) for k in wrong.keys()|wanted.keys() if k[0]==0),'Pure stage word control') + require(wrong!=wanted,'Full-word trap must fail') + return {'first_mixed_false_positive_rejected':True,'fields':n,'full_calls':6,'thin_queries':8,'full_polynomial_coefficients':len(word),'deleted_query_rejected':True,'moved_call_rejected':True,'distinct_leaf_column_signatures':3,'distinct_leaf_row_signatures':3} + +# Polynomials in three free, noncommuting variables over F2. +ONE=frozenset(((),));Z=frozenset() +def times(a,b): + result=set() + for x in a: + for y in b: + w=x+y + if w in result:result.remove(w) + else:result.add(w) + return frozenset(result) + +def pair_equations(order): + projections=[(frozenset(((j,),)),ONE^frozenset(((j,),))) for j in range(3)];eq=[] + for j in range(3): + for h,k in itertools.product(range(2),repeat=2): + p=times(projections[j][h],projections[j][k])^(projections[j][h] if h==k else Z) + if p:eq.append(p) + ordered={} + for j,k in itertools.permutations(range(3),2): + p=Z + for pos,(c,h) in enumerate(order): + if c!=j:continue + for d,l in order[pos+1:]: + if d==k:p^=times(projections[j][h],projections[k][l]) + ordered[j,k]=p + for j in range(3): + k,l=[x for x in range(3) if x!=j];eq.append(ordered[j,k]^ordered[j,l]) + return eq + +def orders(): + result=[] + for word in sorted(set(itertools.permutations((0,0,1,1,2,2)))): + if not word.index(0)>=1;a<<=1 + return out + +def determinant_polynomial(matrix): + n=len(matrix);out=0 + for permutation in itertools.permutations(range(n)): + value=1 + for i,j in enumerate(permutation):value=scalar_multiply(value,matrix[i][j]) + out^=value + return out + +def prefix_controls(): + checked=0;updates=0;rejections=0;rng=random.Random(20261026) + for n in (2,3,4): + for trial in range(20): + change=list(eye(n)) + for _ in range(5*n): + i,j=rng.sample(range(n),2);change[i]^=change[j] + change=tuple(change);back=inverse(change) + flags=[mul(mul(change,tuple(1<>j)&1)<<1) for j in range(n)] for i in range(n)]) + expected=1 + for _ in range(n):expected=scalar_multiply(expected,3) + require(determinant==expected,'Projection determinant');checked+=1 + require(mul(flags[0],prefix)!=zero(n),'A completed resolution cannot restart this prefix walk');rejections+=1 + return {'matrix_flags':checked,'prefix_updates':updates,'projection_determinants':checked,'restarted_walks_rejected':rejections} + +def rank_cut(g,d,field_size): + require(g>=3 and d>=1 and field_size>=2 and field_size&(field_size-1)==0,'Rank-cut parameters');h=0 + while 2*field_size**(d*h)=g and (h==0 or 2*2**(2*(h-1))>(col*d))&((1<0,'One-sided connector must fail a necessary equation') + z=calls[-2]['r'];one_sided+=block(z,1,0,d)!=block(z,2,0,d);cases+=1 + require(one_sided>0,'Controls must leave the old two-sided aggregate contract') + return {'coupled_frames':cases,'literal_mixed_coefficients':coefficient_checks,'prefix_equations':prefix_checks,'one_sided_nonaggregate_frames':one_sided} + + +def run(): + return {'escape':escape(),'paired_certificates':certificates(),'prefix':prefix_controls(),'rank_cut_cases':rank_controls(),'chronology':chronology_controls()} + +if __name__=='__main__':print(json.dumps(run(),indent=2)) diff --git a/research/crossed-connector-caller/discovery/RESULTS.json.gz b/research/crossed-connector-caller/discovery/RESULTS.json.gz new file mode 100644 index 0000000000..8b3223c079 Binary files /dev/null and b/research/crossed-connector-caller/discovery/RESULTS.json.gz differ diff --git a/research/crossed-connector-caller/discovery/aggregate_search.py b/research/crossed-connector-caller/discovery/aggregate_search.py new file mode 100644 index 0000000000..771673d8e1 --- /dev/null +++ b/research/crossed-connector-caller/discovery/aggregate_search.py @@ -0,0 +1,81 @@ +"""Search arbitrary connectors on the core and the leaf sum. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import itertools +import json +from pathlib import Path +import time +import free_algebra as F +Z=F.ZERO; I=F.ONE + +def orders(): + for good in sorted(set(itertools.permutations((0,0,1,1,2,2)))): + if not good.index(0)0)][int(c>0)] for c in range(n)] for r in range(n)] for k in ks] + tail=[[Z]*n for _ in range(n)];out=[[[Z]*n for _ in range(n)] for _ in range(g)] + for j,k in reversed(order): + if j=args.limit:break + r=F.certificate(3,o,args.degree) + if 'one' in r['certificates']: + hits+=1 + if len(first)<3:first.append(r) + else:miss.append(o) + if (i+1)%100==0:print(i+1,hits,len(miss),round(time.monotonic()-start,2),flush=True) + report={'degree':args.degree,'orders':hits+len(miss),'certificates':hits,'unresolved':miss,'examples':first} + Path(__file__).with_name(f'AGGREGATE-D{args.degree}.json').write_text(json.dumps(report,indent=2)+'\n') + print('FINAL',hits,len(miss),flush=True) +if __name__=='__main__':main() diff --git a/research/crossed-connector-caller/discovery/coupled_five_search.py b/research/crossed-connector-caller/discovery/coupled_five_search.py new file mode 100644 index 0000000000..96e019e86d --- /dev/null +++ b/research/crossed-connector-caller/discovery/coupled_five_search.py @@ -0,0 +1,57 @@ +"""Search five rank-two connectors with coupled four-channel stages. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import itertools +import json +from pathlib import Path +import random +import time +import z3 +import cycle_search as C + +def setup(): + d=4;n=16;solver=z3.Solver();calls=[] + for stage in range(3): + a=[[z3.Bool(f'a{stage}_{i}_{j}') for j in range(d)] for i in range(d)] + b=[[z3.Bool(f'b{stage}_{i}_{j}') for j in range(d)] for i in range(d)] + square=C.product(a,a);relation=C.plus(C.product(a,b),C.product(b,a)) + for i,j in itertools.product(range(d),repeat=2):solver.add(square[i][j]==a[i][j],relation[i][j]==b[i][j]) + solver.add(z3.Not(C.xor(*(a[i][i] for i in range(d))))) + solver.add(z3.Or(*[a[i][j] for i,j in itertools.product(range(d),repeat=2)])) + solver.add(z3.Or(*[z3.Xor(a[i][j],z3.BoolVal(i==j)) for i,j in itertools.product(range(d),repeat=2)])) + for half in range(2): + p=C.zero(n);r=C.zero(n) + for row,col in itertools.product((0,stage+1),repeat=2): + for i,j in itertools.product(range(d),repeat=2): + value=z3.Xor(a[i][j],b[i][j]) if row==col else b[i][j] + if half and row==col and i==j:value=z3.Not(value) + p[row*d+i][col*d+j]=value + r[row*d+i][col*d+j]=z3.Xor(a[i][j],z3.BoolVal(bool(half and i==j))) + calls.append((stage,p,r)) + for k in range(5): + u=[[z3.Bool(f'u{k}_{i}_{j}') for j in range(2)] for i in range(n)] + v=[[z3.Bool(f'v{k}_{i}_{j}') for j in range(n)] for i in range(2)] + for j in range(2):solver.add(z3.Or(*(u[i][j] for i in range(n))),z3.Or(*v[j])) + solver.add(z3.Or(*(z3.Xor(u[i][0],u[i][1]) for i in range(n))),z3.Or(*(z3.Xor(v[0][i],v[1][i]) for i in range(n)))) + for row in C.product(v,u): + for x in row:solver.add(z3.Not(x)) + calls.append((3,C.zero(n),C.product(u,v))) + total=C.zero(n) + for _,_,r in calls:total=C.plus(total,r) + for i,j in itertools.product(range(n),repeat=2):solver.add(total[i][j]==(i==j)) + return solver,calls + +def main(): + parser=argparse.ArgumentParser();parser.add_argument('--cases',type=int,default=8);parser.add_argument('--timeout',type=int,default=10000);args=parser.parse_args();rng=random.Random(271828);rows=[];start=time.monotonic() + for case in range(args.cases): + solver,calls=setup();solver.set(timeout=args.timeout);order=list(range(11));rng.shuffle(order);C.constraints(solver,calls,order,3);status=solver.check();row={'case':case,'order':order,'status':str(status)} + if status==z3.sat: + model=solver.model();row['calls']=[{'stage':j,'p':[sum(int(z3.is_true(model.eval(x,model_completion=True)))<>i&1] + # Independent literal expansion of the relation. + check=ZERO + for ei,left,right in terms:check^=frozenset(tuple(left)+w+tuple(right) for w in eq[ei][1]) + if check!=p:raise ValueError('Bad ideal certificate') + tested[label]=terms + return {'g':g,'order':order,'degree':degree,'names':names,'equations':[(label,[list(w) for w in sorted(p)]) for label,p in eq],'monomials':len(words),'rows':len(generators),'rank':len(basis),'certificates':tested} + + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--degree',type=int,default=3);ap.add_argument('--limit',type=int,default=1);args=ap.parse_args() + g=3;records=[];start=time.monotonic() + for second in itertools.permutations(range(g)): + for bad in itertools.permutations(((3,0),(3,1),(4,0),(4,1))): + order=[(j,0) for j in range(g)]+list(bad)+[(j,1) for j in second] + r=certificate(g,order,args.degree);records.append(r) + print(json.dumps({k:r[k] for k in ('order','rows','rank','monomials')}|{'certificates':{k:len(v) for k,v in r['certificates'].items()},'seconds':round(time.monotonic()-start,2)}),flush=True) + if len(records)>=args.limit:break + if len(records)>=args.limit:break + Path(__file__).with_name(f'NC-STAR-D{args.degree}.json').write_text(json.dumps(records,indent=2)+'\n') + +if __name__=='__main__':main() diff --git a/research/crossed-connector-caller/discovery/gap_search.py b/research/crossed-connector-caller/discovery/gap_search.py new file mode 100644 index 0000000000..73b7b6c708 --- /dev/null +++ b/research/crossed-connector-caller/discovery/gap_search.py @@ -0,0 +1,52 @@ +"""Allow an arbitrary aggregate matrix in every gap of the good word. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import itertools +import json +from pathlib import Path +import free_algebra as F +Z=F.ZERO;I=F.ONE + +def orders(): + for good in sorted(set(itertools.permutations((0,0,1,1,2,2)))): + if good.index(0)0)][int(c>0)] for c in range(n)] for r in range(n)]) + tail=[[Z]*n for _ in range(n)];out=[[[Z]*n for _ in range(n)] for _ in range(g)] + for i,(j,k) in reversed(list(enumerate(order))): + p,r=good[j][k];total=F.add(tail,tails[i]) + out[j]=F.add(out[j],F.add(F.mul(p,total),F.mul(total,p)));tail=F.add(tail,r) + for j,m in enumerate(out): + for r,row in enumerate(m): + for c,poly in enumerate(row): + if r in (0,j+1) and c in (0,j+1):continue + if poly:eq.append((f'chronology {j}:{r},{c}',poly)) + return names,eq + +def main(): + F.equations=equations;records=[] + for o in orders(): + r=F.certificate(3,o,3);records.append(r) + print(o,{k:len(v) for k,v in r['certificates'].items()},flush=True) + Path(__file__).with_name('GAP-SEARCH.json').write_text(json.dumps(records,indent=2)+'\n') +if __name__=='__main__':main() diff --git a/research/crossed-connector-caller/discovery/grow_escape.py b/research/crossed-connector-caller/discovery/grow_escape.py new file mode 100644 index 0000000000..a035eaff70 --- /dev/null +++ b/research/crossed-connector-caller/discovery/grow_escape.py @@ -0,0 +1,103 @@ +"""Add a pair of leaves while keeping the eight thin query factors. + +The old call order is retained. New calls can enter any gap. +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import itertools +import gzip +import json +from pathlib import Path +import sys +import time +import z3 +import cycle_search as C +import leaf_echo_search as L + +PARENT=Path(__file__).resolve().parents[1] + +def embed(a,indices,n): + out=C.zero(n) + for i,row in enumerate(a): + for j in range(4):out[indices[i]][indices[j]]=z3.BoolVal(bool(row>>j&1)) + return out + +def build(case,distinct): + if case==11:original=json.loads((PARENT/'ESCAPE-WORD.json').read_text()) + else: + corpus=json.load(gzip.open(Path(__file__).with_name('RESULTS.json.gz'),'rt')) + original=corpus['LEAF-THIN8-SEED3.json'][case] + sys.path.insert(0,str(PARENT));from word_replay import replay + if original['status']!='sat' or not replay(original['calls'],original['order'])['passed']:raise ValueError('The source must be a complete positive word') + n=12;solver=z3.Solver();calls=[] + for c in original['calls'][:6]: + p=C.zero(n);r=C.zero(n) + for i,j in itertools.product(range(8),repeat=2):p[i][j]=z3.BoolVal(bool(c['p'][i]>>j&1));r[i][j]=z3.BoolVal(bool(c['r'][i]>>j&1)) + calls.append((c['stage'],p,r)) + new_u=[[z3.Bool(f'u{k}_{i}') for i in range(4 if distinct else 2)] for k in range(8)] + new_v=[[z3.Bool(f'v{k}_{i}') for i in range(4 if distinct else 2)] for k in range(8)] + old_u=[];old_v=[] + for k,c in enumerate(original['calls'][6:]): + v=next(row for row in c['r'] if row);u=sum(1<>i&1)) for i in range(8)]+(new_u[k] if distinct else new_u[k]*2) + vv=[z3.BoolVal(bool(v>>i&1)) for i in range(8)]+(new_v[k] if distinct else new_v[k]*2) + solver.add(z3.Not(C.xor(*(z3.And(a,b) for a,b in zip(uu,vv))))) + calls.append((5,C.zero(n),[[z3.And(a,b) for b in vv] for a in uu])) + # Reject three equal signatures among the new leaves and an old leaf. + for leaf in range(3): + solver.add(z3.Or(*[z3.Xor(new_u[k][i],z3.BoolVal(bool(old_u[k]>>(2+2*leaf+(i%2))&1))) for k in range(8) for i in range(4 if distinct else 2)])) + solver.add(z3.Or(*[z3.Xor(new_v[k][i],z3.BoolVal(bool(old_v[k]>>(2+2*leaf+(i%2))&1))) for k in range(8) for i in range(4 if distinct else 2)])) + local=(5,10,5,10);unit=(1,2,4,8);options=[] + for p in sorted(set(p for p,_ in L.source.FULL)): + if L.mul(p,local)!=L.mul(local,p):continue + r=L.mul(p,local) + if L.source.rank(r)!=1:continue + options.append(((p,r),(L.add(p,unit),L.add(r,local)))) + choices=[] + for leaf in (3,4): + chosen=[z3.Bool(f'c{leaf}_{k}') for k in range(24)];choices.extend(chosen);solver.add(z3.PbEq([(c,1) for c in chosen],1));indices=(0,1,2+2*leaf,3+2*leaf) + for half in range(2): + matrices=[] + for kind in range(2): + vals=[embed(o[half][kind],indices,n) for o in options] + matrices.append([[z3.Or(*[chosen[k] for k,a in enumerate(vals) if z3.is_true(a[i][j])]) for j in range(n)] for i in range(n)]) + calls.append((leaf,*matrices)) + positions=[z3.Int(f'pos{i}') for i in range(18)];solver.add(z3.Distinct(*positions)) + for p in positions:solver.add(p>=0,p<18) + for a,b in zip(original['order'],original['order'][1:]):solver.add(positions[a]>j&1)) for j in range(N)] for row in a] +def embed(a,indices): + out=[0]*N + for i,row in enumerate(a):out[indices[i]]=sum(1<>j&1) + return tuple(out) +def add(a,b):return tuple(x^y for x,y in zip(a,b)) +def mul(a,b):return tuple(sum((sum((row>>k&1)*(b[k]>>j&1) for k in range(len(a)))%2)<>col&1]) for col in range(N)] for row in range(N)]) + good.append((j,*matrices)) + thin=[];active=[] + for k in range(thin_count): + u=[z3.Bool(f'u{k}_{i}') for i in range(N)];v=[z3.Bool(f'v{k}_{i}') for i in range(N)] + enabled=z3.Bool(f'enabled{k}');active.append(enabled) + solver.add(enabled==z3.And(z3.Or(*u),z3.Or(*v)),z3.Not(xor(*(z3.And(a,b) for a,b in zip(u,v))))) + if budget is None:solver.add(enabled) + r=[[z3.And(u[i],v[j]) for j in range(N)] for i in range(N)] + thin.append((3,zero(),r)) + if budget is not None:solver.add(z3.PbLe([(x,1) for x in active],budget)) + calls=good+thin;total=zero() + for _,_,r in calls:total=matxor(total,r) + for i,j in itertools.product(range(N),repeat=2):solver.add(total[i][j]==(i==j)) + return solver,calls,choices,options + +def constraints(solver,calls,order): + tail=zero();out=[zero() for _ in range(3)] + for index in reversed(order): + stage,p,r=calls[index] + if stage<3:out[stage]=matxor(out[stage],matxor(product(p,tail),product(tail,p))) + tail=matxor(tail,r) + for mat in out: + for row in mat: + for val in row:solver.add(z3.Not(val)) + +def stage_constraints(solver,calls,order): + # Pairwise scalar-stage coefficients are necessary for the full word. + places={k:order.index(k) for k in range(6)} + for j,k in itertools.combinations(range(3),2): + a,b=sorted((places[2*j],places[2*j+1]));c,d=sorted((places[2*k],places[2*k+1])) + if b>j&1:val^=b[j] + out.append(val) + return tuple(out) +def rank(a): + basis={} + for v in a: + while v: + j=v.bit_length()-1 + if j not in basis:basis[j]=v;break + v^=basis[j] + return len(basis) +def inv(a): + n=len(a);r=[x|(1<<(n+i)) for i,x in enumerate(a)] + for j in range(n): + k=next(i for i in range(j,n) if r[i]>>j&1);r[j],r[k]=r[k],r[j] + for i in range(n): + if i!=j and r[i]>>j&1:r[i]^=r[j] + return tuple(x>>n for x in r) +def frame(a): + b=inv(a) + return [tuple(b[k] if row>>k&1 else 0 for row in a) for k in range(3)] +def poly_product(a,b): + out={};z=(0,0,0) + for i,ai in a.items(): + for j,bj in b.items(): + k=tuple(x+y for x,y in zip(i,j));out[k]=add(out.get(k,z),mul(ai,bj)) + return {k:v for k,v in out.items() if any(v)} +def word(fs): + g=len(fs);base=(0,)*g;w={base:eye(3)} + for h in range(3): + for j in range(g): + d=list(base);d[j]=1;w=poly_product({base:eye(3),tuple(d):fs[j][h]},w) + return w=={x:eye(3) for x in itertools.product((0,1),repeat=g)} + +def linear(fs): + order=[(j,k) for k in range(3) for j in range(3)];names,eq=M.equations(3,order) + fixed=[] + for f in fs:fixed.extend((f[0],(0,0,0),f[1],(0,0,0))) + unknowns=(len(names)-len(fixed))*9;rows=[] + for label,p in eq: + values=[0]*9 + for w in p: + letters=[(i,fixed[i] if i>c)&1)<>c)&1)<<(start+3*rr+cc) + rows.extend(values) + basis={};mask=(1<>unknowns:return None + solution=0 + for j,row in sorted(basis.items()): + if ((row&solution).bit_count()^(row>>unknowns))&1:solution|=1<>(9*k+3*r))&7 for r in range(3)) for k in range(unknowns//9)] + +def main(): + start=time.monotonic();frames=[frame(a) for a in itertools.product(range(8),repeat=3) if rank(a)==3];base=frame(eye(3)) + compatible=[f for f in frames if word([base,f])];print('frames',len(frames),'pair-compatible',len(compatible),flush=True) + count=0;surv=[] + for a,b in itertools.product(compatible,repeat=2): + fs=[base,a,b] + if not word(fs):continue + count+=1;sol=linear(fs) + if sol is not None:surv.append({'frames':fs,'tails':sol});print('FOUND',len(surv),flush=True) + print('FINAL',count,len(surv),'seconds',round(time.monotonic()-start,2),flush=True) + Path(__file__).with_name('M3-FRAME-SEARCH.json').write_text(json.dumps({'frames':len(frames),'pair_compatible':len(compatible),'full_stage_words':count,'survivors':surv},indent=2)+'\n') +if __name__=='__main__':main() diff --git a/research/crossed-connector-caller/discovery/multisplit_search.py b/research/crossed-connector-caller/discovery/multisplit_search.py new file mode 100644 index 0000000000..4be46df7c6 --- /dev/null +++ b/research/crossed-connector-caller/discovery/multisplit_search.py @@ -0,0 +1,67 @@ +"""Test three or more native calls per shared stage. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import itertools +import json +from pathlib import Path +import time +import free_algebra as F +Z=F.ZERO;I=F.ONE +SPLITS=3 + +def orders(m): + def rec(word,counts,max_seen): + if len(word)==3*m:yield [(j,word[:i].count(j)) for i,j in enumerate(word)];return + for j in range(min(2,max_seen+1)+1): + if counts[j]0)][int(c>0)] for c in range(n)] for r in range(n)]) + tail=[[Z]*n for _ in range(n)];out=[[[Z]*n for _ in range(n)] for _ in range(g)] + for i,(j,k) in reversed(list(enumerate(order))): + p,r=good[j][k];total=F.add(tail,tails[i]);out[j]=F.add(out[j],F.add(F.mul(p,total),F.mul(total,p)));tail=F.add(tail,r) + for j,mat in enumerate(out): + for row,values in enumerate(mat): + for col,poly in enumerate(values): + if row in (0,j+1) and col in (0,j+1):continue + if poly:eq.append((f'chronology {j}:{row},{col}',poly)) + return names,eq + +def main(): + global SPLITS + ap=argparse.ArgumentParser();ap.add_argument('--splits',type=int,default=3);ap.add_argument('--degree',type=int,default=2);ap.add_argument('--limit',type=int,default=280);args=ap.parse_args();SPLITS=args.splits + F.equations=equations;start=time.monotonic();hit=0;miss=[] + for i,o in enumerate(orders(SPLITS)): + if i>=args.limit:break + r=F.certificate(3,o,args.degree) + if 'one' in r['certificates']:hit+=1 + else:miss.append(o) + if (i+1)%20==0:print(i+1,hit,len(miss),round(time.monotonic()-start,2),flush=True) + Path(__file__).with_name(f'MULTISPLIT-M{SPLITS}-D{args.degree}.json').write_text(json.dumps({'orders':hit+len(miss),'certificates':hit,'unresolved':miss},indent=2)+'\n') + print('FINAL',hit,len(miss),flush=True) +if __name__=='__main__':main() diff --git a/research/crossed-connector-caller/discovery/order_search.py b/research/crossed-connector-caller/discovery/order_search.py new file mode 100644 index 0000000000..3727f5c500 --- /dev/null +++ b/research/crossed-connector-caller/discovery/order_search.py @@ -0,0 +1,56 @@ +"""Search all order types of three leaves and four fixed connectors. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import itertools +import json +from pathlib import Path +import time +import free_algebra as N + +_original=N.equations + +def pair_equations(g,order): + names,eq=_original(g,order);out=[] + for label,p in eq: + if not label.startswith('chronology'): + out.append((label,p));continue + head,rc=label.split(':');c=int(head.split()[1]);r,col=map(int,rc.split(',')) + if c>=g:continue + if r in (0,c+1) and col in (0,c+1):continue + out.append((label,p)) + return names,out + + +def orders(): + good_words=sorted(set(itertools.permutations((0,0,1,1,2,2)))) + good_words=[w for w in good_words if w.index(0)=args.limit:break + r=N.certificate(3,order,args.degree) + if 'one' in r['certificates']: + hits+=1 + if len(examples)<3:examples.append(r) + else:misses.append(order) + if (i+1)%1000==0:print(json.dumps({'orders':i+1,'certificates':hits,'unresolved':len(misses),'seconds':round(time.monotonic()-start,2)}),flush=True) + report={'scope':'All order types of three good pairs and the four fixed connectors; no matrix size bound','degree':args.degree,'orders':hits+len(misses),'certificates':hits,'unresolved':misses,'examples':examples} + Path(__file__).with_name(f'ORDER-SEARCH-D{args.degree}.json').write_text(json.dumps(report,indent=2)+'\n') + print(json.dumps({k:report[k] for k in ('scope','degree','orders','certificates')}|{'unresolved':len(misses)}),flush=True) + +if __name__=='__main__':main() diff --git a/research/crossed-connector-caller/discovery/tournament_search.py b/research/crossed-connector-caller/discovery/tournament_search.py new file mode 100644 index 0000000000..417595a2f0 --- /dev/null +++ b/research/crossed-connector-caller/discovery/tournament_search.py @@ -0,0 +1,42 @@ +"""Test the projected chronology equations without connector matrices. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import json,itertools +from pathlib import Path +import free_algebra as F,gap_search as G +MODE='rows';SPLITS=2 + +def equations(g,order): + m=SPLITS;names=[];aa=[];eq=[] + for j in range(g): + row=[];last=F.ONE + for h in range(m-1):row.append(F.var(len(names)));names.append(f'A{j}_{h}');last^=row[-1] + row.append(last);aa.append(row) + for h,k in itertools.product(range(m),repeat=2): + v=F.prod(row[h],row[k])^(row[h] if h==k else F.ZERO) + if v:eq.append((f'A{j}:{h},{k}',v)) + s={} + for j,k in itertools.permutations(range(g),2): + v=F.ZERO + for i,(c,h) in enumerate(order): + if c!=j:continue + for d,l in order[i+1:]: + if d==k:v^=F.prod(aa[j][h],aa[k][l]) + s[j,k]=v + for j in range(g): + k,l=[i for i in range(g) if i!=j] + if MODE in ('rows','both'):eq.append((f'row {j}',s[j,k]^s[j,l])) + if MODE in ('cols','both'):eq.append((f'col {j}',s[k,j]^s[l,j])) + return names,eq + +def main(): + global MODE + F.equations=equations;out={} + for MODE in ('rows','cols','both'): + records=[] + for o in G.orders(): + r=F.certificate(3,o,4);records.append(r) + print(MODE,len(records),sum('one' in r['certificates'] for r in records),flush=True);out[MODE]=records + Path(__file__).with_name('TOURNAMENT-SEARCH.json').write_text(json.dumps(out,indent=2)+'\n') +if __name__=='__main__':main() diff --git a/research/crossed-connector-caller/test_verify.py b/research/crossed-connector-caller/test_verify.py new file mode 100644 index 0000000000..99ab626e8b --- /dev/null +++ b/research/crossed-connector-caller/test_verify.py @@ -0,0 +1,33 @@ +"""Reject changed mathematical evidence and a changed source bill. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +PACKAGE=Path(__file__).resolve().parent +ROOT=PACKAGE.parents[1] + +def require(value,message): + if not value:raise ValueError(message) + +def main(): + for kind,expected in [('certificate','Free-algebra certificate'),('query','Query rank and square'),('source','Source digest:'),('receipt','Committed result differs'),('mixed','Full-word trap must fail')]: + with tempfile.TemporaryDirectory() as folder: + root=Path(folder);package=root/'research/crossed-connector-caller';shutil.copytree(PACKAGE,package,ignore=shutil.ignore_patterns('__pycache__')) + source=root/'research/p104-helper-subspace-splits/RESULT.json';source.parent.mkdir(parents=True);shutil.copyfile(ROOT/'research/p104-helper-subspace-splits/RESULT.json',source) + if kind=='certificate': + path=package/'PAIR-CERTIFICATES.json';x=json.loads(path.read_text());x[0]['terms']=[];path.write_text(json.dumps(x)) + elif kind=='query': + path=package/'ESCAPE-WORD.json';x=json.loads(path.read_text());x['calls'][6]['r']=[0]*8;path.write_text(json.dumps(x)) + elif kind=='source':source.write_text(source.read_text()+' ') + elif kind=='mixed':shutil.copyfile(package/'ESCAPE-WORD.json',package/'MIXED-ONLY-CANDIDATE.json') + else:(package/'RESULT.json').write_text('{}\n') + result=subprocess.run([sys.executable,'-I','-O','-B',str(package/'verify.py')],cwd=root,capture_output=True,text=True,timeout=30) + require(result.returncode!=0 and expected in result.stderr,'Mutation was not rejected: '+kind) + print('PASS_CONNECTOR_MUTATIONS: 5 corrupted packages rejected') +if __name__=='__main__':main() diff --git a/research/crossed-connector-caller/vendor/algebra.py b/research/crossed-connector-caller/vendor/algebra.py new file mode 100644 index 0000000000..2f0d4f290c --- /dev/null +++ b/research/crossed-connector-caller/vendor/algebra.py @@ -0,0 +1,110 @@ +"""Literal GF(2) polynomial matrices, independently of the GF(16) search. + +Apache-2.0. Cinna Davis, with substantial OpenAI Codex assistance. +""" +from collections import Counter + +EVEN = sum(1 << i for i in range(0, 256, 2)) + + +def query(poly): + """Multiply by the formal involution Q, without setting Q = 1.""" + return ((poly & EVEN) << 1) | ((poly & (EVEN << 1)) >> 1) + + +def rank(rows): + basis = {} + for value in rows: + while value: + pivot = value.bit_length() - 1 + if pivot not in basis: + basis[pivot] = value + break + value ^= basis[pivot] + return len(basis) + + +def gate_inventory(): + """All rank-one nilpotents and their rank-two projector extensions.""" + full, thin = [], [] + for u in range(1, 16): + for v in range(1, 16): + if (u & v).bit_count() % 2: + continue + nilpotent = tuple(v if u >> i & 1 else 0 for i in range(4)) + thin.append(((0,) * 4, nilpotent)) + seen = set() + for a in range(1, 16): + if not (v & a).bit_count() % 2: + continue + for b in range(1, 16): + if not (u & b).bit_count() % 2 or (a & b).bit_count() % 2: + continue + projector = tuple((b if u >> i & 1 else 0) ^ + (v if a >> i & 1 else 0) for i in range(4)) + if projector not in seen: + seen.add(projector) + full.append((projector, nilpotent)) + return full, thin + + +FULL, THIN = gate_inventory() + + +def identity(): + return [[int(i == j) for j in range(4)] for i in range(4)] + + +def literal(mask, ids): + """Each bit is a monomial Q^q product(D_s); no D is specialized.""" + matrix = identity() + for stage, gate_id in enumerate(ids): + thick = bool(mask >> stage & 1) + projector, nilpotent = (FULL if thick else THIN)[gate_id] + sums = [[0] * 4 for _ in range(16)] + for subset in range(1, 16): + low = (subset & -subset).bit_length() - 1 + sums[subset] = [a ^ b for a, b in + zip(sums[subset & (subset - 1)], matrix[low])] + changed = [row[:] for row in matrix] + for i in range(4): + for j in range(4): + p = sums[projector[i]][j] + n = query(sums[nilpotent[i]][j]) + if thick: + shift = 1 << (stage + 1) + changed[i][j] ^= p ^ (p << shift) ^ (n << shift) + else: + changed[i][j] ^= n + matrix = changed + return matrix + + +def coefficients(matrix): + result = {} + groups = {g for row in matrix for poly in row + for g in range(poly.bit_length()) if poly >> g & 1} + for g in groups: + result[g] = [sum(((matrix[i][j] >> g) & 1) << j for j in range(4)) + for i in range(4)] + return result + + +def stats(matrix): + coeff = coefficients(matrix) + return { + 'central_query_on_every_output': all(g & 1 for g in coeff), + 'coefficient_rank_sum': sum(rank(rows) for rows in coeff.values()), + 'ranks': dict(sorted((g, rank(rows)) for g, rows in coeff.items())), + } + + +def elementary(source, destination): + nilpotent = tuple((1 << source) if i == destination else 0 for i in range(4)) + projector = tuple((1 << i) if i in (source, destination) else 0 for i in range(4)) + return FULL.index((projector, nilpotent)) + + +def multiply_binary(a, b): + return [sum(((sum(((row >> k) & 1) * ((b[k] >> j) & 1) + for k in range(4))) % 2) << j for j in range(4)) for row in a] diff --git a/research/crossed-connector-caller/verify.py b/research/crossed-connector-caller/verify.py new file mode 100644 index 0000000000..78a5af8da9 --- /dev/null +++ b/research/crossed-connector-caller/verify.py @@ -0,0 +1,62 @@ +#!/usr/bin/env python3 +"""Replay the connector theorem package and its paid profiles. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +PACKAGE=Path(__file__).resolve().parent +ROOT=PACKAGE.parents[1] + +def require(value,message): + if not value:raise ValueError(message) + +def load_check(): + spec=importlib.util.spec_from_file_location('connector_check',PACKAGE/'check.py') + module=importlib.util.module_from_spec(spec);spec.loader.exec_module(module);return module + +def power_bound(rank,numerator,denominator,bits=40): + scale=1<1: + mid=(lo+hi)//2 + if pow(mid,denominator)<=goal:lo=mid + else:hi=mid + return lo,lo if pow(lo,denominator)==goal else lo+1 + +def profile(source,g,thin): + counts={int(r):-2*g*v for r,v in source['paid'].items()} + for r,v in source['helpers'].items():counts[int(r)]=counts.get(int(r),0)+2*g*v + counts[8*g+1]=counts.get(8*g+1,0)+208;counts[9]=counts.get(9,0)+208*g;counts[1]-=104*thin + return {r:c for r,c in counts.items() if c} + +def pricing(): + source=json.loads((ROOT/'research/p104-helper-subspace-splits/RESULT.json').read_text())['local'];bad=profile(source,3,8) + linear=sum(r*c for r,c in bad.items());require(linear==-336,'Escape price mass') + require(min(r for r,c in bad.items() if c>0)==8,'Positive escape rank floor') + require(max(r for r,c in bad.items() if c<0)==7,'Negative escape rank ceiling') + candidates=[] + for g,thin,ports in ((127,10,1),(31,5,2)): + candidate=profile(source,g,thin);lo=hi=0 + for r,c in candidate.items(): + a,b=power_bound(r,1993,2000) + lo+=c*(a if c>=0 else b);hi+=c*(b if c>=0 else a) + require(lo>0,'The long relaxation must retain a positive exact price margin') + candidates.append({'q':104,'g':g,'ports_per_binary_block':ports,'full_calls':2*g,'thin_queries_per_native_port':thin,'saving':'7/2000','moment_lower_numerator':str(lo),'moment_upper_numerator':str(hi),'moment_denominator':str(1<<40),'status':'POSITIVE_OPTIMISTIC_PRICE_ONLY; NO CALLER OR KAPPA CLAIM'}) + return {'pinned_supplier':'PR5599 09dd0965711ca7eeb169057a420abab1c9052137','escape':{'q':104,'g':3,'thin_queries_per_copy':8,'signed_profile':{str(r):v for r,v in sorted(bad.items())},'linear_margin':linear,'all_concave_moments_rejected':True},'unconstructed_candidates':candidates} + +def run(): + sources=json.loads((PACKAGE/'SOURCES.json').read_text());count=0 + for row in sources['files']: + if row['usage']=='input': + require(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'Source digest: '+row['path']);count+=1 + checker=load_check();controls=checker.run() + result={'status':'PASS_ONE_SIDED_CONNECTOR_OBSTRUCTION','scope':'Finite matrices over every characteristic-two field; any finite star stage splits and call order; one-sided equal leaf signatures','authenticated_inputs':count,'controls':controls,'pricing':pricing(),'limits':['No kappa increase','The full escape word is binary algebra, not a physical native caller','The 127-leaf price profile has no operator','No proof-assistant or independent human acceptance']} + encoded=json.dumps(result,indent=2,sort_keys=True)+'\n' + if '--write-result' in sys.argv:(PACKAGE/'RESULT.json').write_text(encoded) + else:require((PACKAGE/'RESULT.json').read_text()==encoded,'Committed result differs') + print(encoded,end='') +if __name__=='__main__':run() diff --git a/research/crossed-connector-caller/word_replay.py b/research/crossed-connector-caller/word_replay.py new file mode 100644 index 0000000000..037ed3f765 --- /dev/null +++ b/research/crossed-connector-caller/word_replay.py @@ -0,0 +1,49 @@ +"""Replay the complete binary word with independent stage variables. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import json +from pathlib import Path + +def eye(n):return tuple(1<1:continue + key=tuple(a+b for a,b in zip(x,y));out[key]=add(out.get(key,zero),mul(ax,by)) + return {k:v for k,v in out.items() if any(v)} + +def replay(calls,order): + n=len(calls[0]['p']);g=max(c['stage'] for c in calls);base=(0,)*(g+1);ebit=(1,)+(0,)*g + word={base:eye(n)};expected={base:eye(n),ebit:eye(n)};targets=[(0,)*n for _ in range(g)] + for c in calls: + if c['stage']