diff --git a/research/paired-stage-chronology-m4/PROOF.md b/research/paired-stage-chronology-m4/PROOF.md new file mode 100644 index 0000000000..fd0ceffdc4 --- /dev/null +++ b/research/paired-stage-chronology-m4/PROOF.md @@ -0,0 +1,101 @@ +# Exact paired-stage loss at m = 4 under the mixed chronology cut + +## Model + +This is the binary normalized paired-stage controller of +[PR #5631](https://github.com/CrocSwap/integer-mult-bounds/pull/5631) +(`research/paired-stage-chronology-cut`), which builds on PR #5617. Work +over F2. There are n main fields and L = n + 2 = 2m full calls, listed in +chronological order. Call i has a query + + R_i = u_i v_i, v_i u_i = 0, sum_i R_i = I_n, + +and a rank-two idempotent P_i with P_i R_i = R_i P_i = R_i. The calls are +partitioned into m stages of two calls each. Stage c with calls i, j has +target derivative E_c = P_i + P_j. The targets must be idempotent and +diagonal in one common output basis, and every stage must satisfy the mixed +coefficient condition of PR #5631 Section 4: + + [P_i, S_i] + [P_j, S_j] = 0, S_i = sum_(l > i) R_l. (*) + +Put r_c = rank E_c and D = 4m - sum_c r_c. PR #5631 proves D >= 2 for +m >= 4 from the rank and pairing cuts, and asks whether a family of bounded +loss can satisfy (*) at all sizes. + +## Theorem (finite, m = 4) + +At m = 4 (n = 6, L = 8), every query system, chronological order, stage +pairing and projector choice that satisfies the conditions above has +D >= 10. Equivalently sum_c r_c <= 6. The bound is attained. + +Of the 35,008 query Gram systems, 23,564 admit no assignment at all. The +remaining 11,444 have minimum loss distributed as +`{10: 2400, 12: 4760, 14: 3084, 16: 1200}`. The previous lower bound at +m = 4 was D >= 2. + +These are necessary conditions only. The theorem is a lower bound for any +complete word in this model. A system that passes is not a caller: the +other word coefficients, native realization and price are not checked. + +## Reduction to a finite enumeration + +**Lemma 1 (Gram normal form).** Put U = [u_0 ... u_(L-1)] and let V have +rows v_i. Then UV = I_n, and K = VU is an L x L idempotent of rank n with +zero diagonal. If two systems have the same K, they are conjugate by an +element of GL(n, F2). Proof: set G = U V'. Then G U' = U K = U and +V G = K V' = V', and G (U' V) = U K V = I. So u_i = G u'_i and +v'_i = v_i G, and R'_i = G^-1 R_i G. Conjugation preserves compatibility, +ranks, commutation, idempotence and (*). Conversely every such K arises: +take V a basis matrix of its column space and U the coordinates of its +columns. + +I + K is a rank-two idempotent with all diagonal entries one. Every +rank-two idempotent factors as XY with X of size L x 2, Y of size 2 x L +and YX = I_2. Its diagonal is x_i . y_i. The verifier therefore enumerates +all sequences of pairs (x_i, y_i), x_i nonzero in F2^2 and x_i . y_i = 1, +with sum y_i x_i^T = I_2, and keeps the distinct K. There are 35,008 at +L = 8 and 976 at L = 6. Order is part of K, so every chronology is covered. + +**Lemma 2 (projectors).** PR #5617 Section 2 shows that the compatible +rank-two idempotents for call i are exactly P = u_i b + a v_i with +v_i a = b u_i = 1 and b a = 0. The verifier enumerates all such (a, b). Each P arises from exactly two +parameter pairs, (a, b) and (a + u_i, b + v_i), so candidates are deduplicated. + +**Lemma 3 (reversal).** Since sum R = I and [P_i, R_i] = 0, +[P_i, sum_(l < i) R_l] = [P_i, sum_(l > i) R_l]. Hence reversing the call +order and transposing every matrix maps a valid assignment to a valid one +with the same ranks. In Gram terms this is K -> J K^T J, with J the +reversal. The census computes one representative per orbit and weights +it by orbit size. The m = 3 weighted census reproduces an unreduced run. + +**Stage algebra.** In characteristic two, (P_i + P_j)^2 = P_i + P_j exactly +when P_i and P_j commute. A family of commuting idempotents is diagonal in a +common basis, and the converse is immediate. For each call pair the +verifier groups projectors by the value of [P_i, S_i], so (*) becomes +equality of keys. It keeps all commuting pairs, records each distinct E and +its rank, then takes the maximum of sum r_c over all 105 pairings and all +pairwise commuting choices of E, by exhaustive branch and bound. The bound +4 per remaining stage is exact because r_c <= 4. + +## Controls + +- m = 3: the same code finds D = 0 on 146 Gram systems, so the program is + not vacuous. PR #5631 reports a genuine six-query word that passes. +- An optimal m = 4 word is rebuilt and passed to PR #5631's own + `chronology.mixed` routine, unchanged. It reports no defect. Exchanging + the first two calls makes it report a defect. +- Reversing the call order of the witness keeps every mixed coefficient, + as Lemma 3 predicts. + +A separate implementation using NumPy and no orbit reduction reproduced the +m = 4 histogram over all 35,008 systems. That run is local evidence and is +not registered. + +## What this does and does not settle + +The data show (*) is strong at m = 4: the best target mass is 6 of 16. +This does not prove that D grows with m. The m = 5 census is larger +(n = 8 gives 2^13 projectors per call) and was not run. No asymptotic +lemma is proved. The theorem does not cover thin calls, idle maps, coupled +ports, characteristic other than two or other word coefficients. It changes +no price exclusion: PR #5631 already rejects m <= 47 with D >= 2. diff --git a/research/paired-stage-chronology-m4/README.md b/research/paired-stage-chronology-m4/README.md new file mode 100644 index 0000000000..8fd922403a --- /dev/null +++ b/research/paired-stage-chronology-m4/README.md @@ -0,0 +1,94 @@ +# Paired-stage loss at m = 4 under the chronology cut is exactly 10 + +**Finite certificate, scoped to a necessary-condition model. No new κ.** + +In the binary normalized paired-stage controller of +[PR #5631](https://github.com/CrocSwap/integer-mult-bounds/pull/5631), take +m = 4 stages (n = 6 fields, L = 8 calls). Impose the earlier rank and pairing +conditions together with PR #5631's mixed chronology coefficient (*). Then every +query system, chronological order, stage pairing and compatible projector +choice has loss + + D = 4m - sum_c rank E_c >= 10, + +and 10 is attained. The earlier bound at this size was D >= 2. Stage targets +can keep at most 6 of the 16 possible ranks. + +PR #5631 asks whether a constant-loss family can satisfy chronology at all +sizes. This answers the first open size. It does not decide the asymptotic +question. See [PROOF.md](PROOF.md) for the model, the reduction lemmas and the +controls. + +## Census + +| | Gram systems | +|---|---:| +| all query Gram systems at L = 8 (every order) | 35,008 | +| no assignment satisfies the conditions | 23,564 | +| minimum D = 10 | 2,400 | +| minimum D = 12 | 4,760 | +| minimum D = 14 | 3,084 | +| minimum D = 16 | 1,200 | + +The census is exhaustive over three things. First, it covers every Gram matrix +K = (v_i u_j). Equal K means the systems are conjugate. Second, it covers every +compatible rank-two projector u b + a v for each call. Third, it covers all 105 +pairings, with every pairwise-commuting choice of stage targets. A reversal +symmetry halves the work, and the histogram is reweighted by orbit size. + +Controls: + +- At m = 3 the same code finds D = 0, so the search is not vacuous. +- An optimal m = 4 word, with stage ranks 0, 0, 2 and 4, passes PR #5631's own + `chronology.mixed` routine unchanged. +- Exchanging that word's first two calls makes the routine report a defect. + +Locally, a second implementation in NumPy, without the orbit reduction, +reproduced the full histogram. A sample with (*) removed gave minimum D of +4 to 6 on 11 of 12 random systems, so the cut is what raises the loss to 10. +Those two runs are local evidence and are not registered. + +## Limits + +These are necessary conditions. Passing them does not make a caller: other word +coefficients, native realization, restoration and price are unchecked. The +model has no thin calls, no idle maps, separate ports and characteristic two. +The result moves no price exclusion. PR #5631 already rejects m <= 47 using +D >= 2. No m = 5 census and no all-size lemma is claimed. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/paired-stage-chronology-m4 +# or directly: +python3.12 -B research/paired-stage-chronology-m4/verify.py # witness and controls, < 5 s +python3.12 -O -B research/paired-stage-chronology-m4/verify.py --shard K --shards 7 # K = 0..6 +``` + +Each shard checks about 2,500 orbit representatives against its histogram and SHA256 +in [RESULT.json](RESULT.json). A shard takes about 130 CPU seconds, or about +35 s of wall time with four processes. `--jobs` sets the process count. +The verifier imports the pinned `research/paired-stage-chronology-cut/chronology.py` +unchanged; its hash is in [SOURCES.json](SOURCES.json). + +## Open next questions + +1. **Does the loss grow with m?** If D grows linearly, PR #5631's argument + excludes every paired-stage size at κ >= 0.003. The first step is an m = 5 + census, or a paired analogue of Cinna Davis's minimum-query + private-projector lemma that bounds the number of rank-four stages. The + blocker is size: n = 8 gives 2^13 projectors per call, so pure enumeration + needs a structural reduction. +2. **Why is the rank sum at most 6?** Classifying the 2,400 optimal systems + and their rank patterns could give a proof that generalizes. + +Structured versions are in [TASK.json](TASK.json). + +## Credit + +Model, mixed coefficient cut and `chronology.mixed`: Ali Romman (PR #5631), +building on PR #5617, Cinna Davis's private-projector lemma, and the P104 +source contributors credited there. The m = 4 census, reduction lemmas and +verifier were produced by Nick Petalas. Apache-2.0. diff --git a/research/paired-stage-chronology-m4/RESULT.json b/research/paired-stage-chronology-m4/RESULT.json new file mode 100644 index 0000000000..e7e0dab8c2 --- /dev/null +++ b/research/paired-stage-chronology-m4/RESULT.json @@ -0,0 +1,212 @@ +{ + "local_control_without_mixed_cut": "12 random m=4 systems (seed 11) with (*) dropped: minimum D values [4,4,None,6,4,4,6,4,6,4,4,4]; local NumPy evidence, not registered", + "m3_control": { + "systems_hist": { + "0": 146, + "10": 116, + "12": 46, + "4": 4, + "6": 52, + "8": 98, + "none": 514 + } + }, + "m4_min_D": 10, + "m4_shards": [ + { + "L": 8, + "reps_hist": { + "10": 178, + "12": 316, + "14": 224, + "16": 74, + "none": 1709 + }, + "sha256": "bca6fab491c8a0cfd60966ffab507210e873c63adc112aa0353381d0e824df6a", + "shard": 0, + "shards": 7, + "systems": 2501, + "systems_hist": { + "10": 356, + "12": 632, + "14": 448, + "16": 148, + "none": 3418 + } + }, + { + "L": 8, + "reps_hist": { + "10": 167, + "12": 340, + "14": 226, + "16": 71, + "none": 1697 + }, + "sha256": "9c21ac36e365df1e1240f284087aa49339f3c7808a7d2be59292fd474fc6e430", + "shard": 1, + "shards": 7, + "systems": 2501, + "systems_hist": { + "10": 334, + "12": 680, + "14": 452, + "16": 142, + "none": 3394 + } + }, + { + "L": 8, + "reps_hist": { + "10": 192, + "12": 340, + "14": 215, + "16": 86, + "none": 1668 + }, + "sha256": "5006ca2cc4ecf84ca25a11db7d056a07116b32b3406495cd23934aac3a92898d", + "shard": 2, + "shards": 7, + "systems": 2501, + "systems_hist": { + "10": 384, + "12": 680, + "14": 430, + "16": 172, + "none": 3336 + } + }, + { + "L": 8, + "reps_hist": { + "10": 157, + "12": 354, + "14": 222, + "16": 94, + "none": 1674 + }, + "sha256": "d78ad492f5eef721424643ff24503649a2a8eb1d023ad7ceafdd52c2d35cc3d5", + "shard": 3, + "shards": 7, + "systems": 2501, + "systems_hist": { + "10": 314, + "12": 708, + "14": 444, + "16": 188, + "none": 3348 + } + }, + { + "L": 8, + "reps_hist": { + "10": 186, + "12": 352, + "14": 210, + "16": 73, + "none": 1679 + }, + "sha256": "0ebff4a42b00ba3048183d9670f75c1c9a21e68cd0b6cd45afbb6599dbf830f4", + "shard": 4, + "shards": 7, + "systems": 2500, + "systems_hist": { + "10": 372, + "12": 704, + "14": 420, + "16": 146, + "none": 3358 + } + }, + { + "L": 8, + "reps_hist": { + "10": 157, + "12": 339, + "14": 211, + "16": 106, + "none": 1687 + }, + "sha256": "0d04bb9f1df0612dc5bac3eb53a079ab764c18f06a77d604db8bdbe3a6d8eccd", + "shard": 5, + "shards": 7, + "systems": 2500, + "systems_hist": { + "10": 314, + "12": 678, + "14": 422, + "16": 212, + "none": 3374 + } + }, + { + "L": 8, + "reps_hist": { + "10": 163, + "12": 339, + "14": 234, + "16": 96, + "none": 1668 + }, + "sha256": "251cf289ecb86b22054d155ca923afab94a42e640f0a01788649fcf58cb1c63f", + "shard": 6, + "shards": 7, + "systems": 2500, + "systems_hist": { + "10": 326, + "12": 678, + "14": 468, + "16": 192, + "none": 3336 + } + } + ], + "m4_systems_hist": { + "10": 2400, + "12": 4760, + "14": 3084, + "16": 1200, + "none": 23564 + }, + "m4_witness": { + "D": 10, + "K": [ + 34, + 33, + 217, + 213, + 238, + 3, + 157, + 93 + ], + "pairing": [ + [ + 0, + 5 + ], + [ + 1, + 2 + ], + [ + 3, + 4 + ], + [ + 6, + 7 + ] + ], + "ranks": [ + [ + 0, + 0, + 2, + 4 + ] + ] + }, + "model": "PR5631 binary paired-stage controller, L=n+2=2m, F2, conditions: compatible rank-two projectors, idempotent stage sums, commuting targets, mixed coefficient (*)", + "schema": "paired-stage-chronology-m4/v1" +} diff --git a/research/paired-stage-chronology-m4/SOURCES.json b/research/paired-stage-chronology-m4/SOURCES.json new file mode 100644 index 0000000000..333533b84e --- /dev/null +++ b/research/paired-stage-chronology-m4/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e30cc1a99cf127c7fd8cb8d83a2db2597a851b74", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/paired-stage-chronology-cut/chronology.py", + "usage": "input", + "git_blob": "29e821e6ccbffa76fe5f2c305dbfd2e22d8a2baf", + "sha256": "4fa33f6736bf313d73304e050ab8ec7e80a5fdea11998aa2ff27c9282972fedd" + } + ] +} diff --git a/research/paired-stage-chronology-m4/TASK.json b/research/paired-stage-chronology-m4/TASK.json new file mode 100644 index 0000000000..3817b943df --- /dev/null +++ b/research/paired-stage-chronology-m4/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "e30cc1a99cf127c7fd8cb8d83a2db2597a851b74", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact minimum paired-stage loss D at m = 4 in PR #5631's binary normalized controller model, under the rank, pairing, commuting-target and mixed chronology (*) conditions, over every query Gram system, order, pairing and compatible projector.", + "scope_change_reason": "The card asks for a changed caller with a complete bill. This answers, at the first open size, PR #5631's open question whether bounded loss can satisfy its chronology cut. It is a necessary-condition census, not a caller.", + "bottleneck_link": "Side result for joint-query controllers: any paired-stage caller at m = 4 loses at least 10 of 16 stage ranks once chronology is imposed, versus 2 from the earlier cuts. It changes no price exclusion and no kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the complete m = 4 census with an independent witness check; do not start the m = 5 census in this session.", + "outcome": "completed", + "evidence": "verify.py (standard library), RESULT.json with seven exhaustive shard histograms and hashes, PROOF.md reduction lemmas; a separate unregistered NumPy implementation reproduced the full histogram locally.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the chronology-cut loss D grow without bound with m, or is it eventually constant?", + "why_it_matters": "PR #5631's price exclusion uses only D >= 2 or 4; a loss growing linearly in m would exclude every paired-stage size at kappa >= 0.003.", + "first_step": "Run the same census at m = 5 (n = 8) with the Gram normal form and reversal reduction, or prove a paired analogue of the minimum-query private-projector lemma bounding the number of rank-four stages.", + "blocked_by": "At n = 8 there are 2^13 projectors per call and many more Gram systems; the pure-Python census here does not scale without a structural reduction." + }, + { + "question": "Which structure forces sum r_c <= 6 at m = 4?", + "why_it_matters": "A human-readable reason could generalize where enumeration cannot.", + "first_step": "Classify the 2,400 optimal Gram systems and their stage rank patterns (the witness has ranks 0,0,2,4).", + "blocked_by": "No classification was attempted in this session." + } + ] +} diff --git a/research/paired-stage-chronology-m4/VERIFY.json b/research/paired-stage-chronology-m4/VERIFY.json new file mode 100644 index 0000000000..a6806ee340 --- /dev/null +++ b/research/paired-stage-chronology-m4/VERIFY.json @@ -0,0 +1,118 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/paired-stage-chronology-cut/chronology.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "m=3 census and positive control; rebuilds the m=4 D=10 witness and checks it with the unchanged PR5631 chronology.mixed routine; adjacent-swap negative control; reversal lemma." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py", + "--shard", + "0", + "--shards", + "7" + ], + "timeout_seconds": 150, + "checks": "Exhaustive m=4 census, shard 0 of 7: every Gram system, pairing and projector choice; per-shard histogram and sha256 must equal RESULT.json." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py", + "--shard", + "1", + "--shards", + "7" + ], + "timeout_seconds": 150, + "checks": "Exhaustive m=4 census, shard 1 of 7: every Gram system, pairing and projector choice; per-shard histogram and sha256 must equal RESULT.json." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py", + "--shard", + "2", + "--shards", + "7" + ], + "timeout_seconds": 150, + "checks": "Exhaustive m=4 census, shard 2 of 7: every Gram system, pairing and projector choice; per-shard histogram and sha256 must equal RESULT.json." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py", + "--shard", + "3", + "--shards", + "7" + ], + "timeout_seconds": 150, + "checks": "Exhaustive m=4 census, shard 3 of 7: every Gram system, pairing and projector choice; per-shard histogram and sha256 must equal RESULT.json." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py", + "--shard", + "4", + "--shards", + "7" + ], + "timeout_seconds": 150, + "checks": "Exhaustive m=4 census, shard 4 of 7: every Gram system, pairing and projector choice; per-shard histogram and sha256 must equal RESULT.json." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py", + "--shard", + "5", + "--shards", + "7" + ], + "timeout_seconds": 150, + "checks": "Exhaustive m=4 census, shard 5 of 7: every Gram system, pairing and projector choice; per-shard histogram and sha256 must equal RESULT.json." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py", + "--shard", + "6", + "--shards", + "7" + ], + "timeout_seconds": 150, + "checks": "Exhaustive m=4 census, shard 6 of 7: every Gram system, pairing and projector choice; per-shard histogram and sha256 must equal RESULT.json." + } + ] +} diff --git a/research/paired-stage-chronology-m4/verify.py b/research/paired-stage-chronology-m4/verify.py new file mode 100644 index 0000000000..da7d473c91 --- /dev/null +++ b/research/paired-stage-chronology-m4/verify.py @@ -0,0 +1,317 @@ +"""Exact minimum paired-stage loss under the mixed chronology cut at m = 4. + +Model: Ali Romman's PR #5631 binary normalized paired-stage controller +(n = 2m - 2 fields, L = 2m rank-one square-zero queries, two calls per stage). +For every query Gram system K, every stage pairing and every compatible +rank-two projector choice this computes the largest total target rank +sum r_c subject to: pair commutation (E_c idempotent), pairwise commuting +targets, and the mixed coefficient cut (*) of PR #5631 Section 4. +D = 4m - sum r_c. Standard library only. Produced by Nick Petalas. Apache-2.0. +""" +import argparse, hashlib, itertools, json, os, sys +from multiprocessing import Pool + +HERE = os.path.dirname(os.path.abspath(__file__)) +H = 2 # rank of I - K: L = n + 2 + + +def need(c, msg): + if not c: + raise AssertionError(msg) + + +def dot(a, b): + return bin(a & b).count('1') & 1 + + +def outer(u, v, n): + return tuple(v if u >> i & 1 else 0 for i in range(n)) + + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b)) + + +def table(b, n): + t = [0] * (1 << n) + for x in range(1, 1 << n): + lo = x & -x + t[x] = t[x ^ lo] ^ b[lo.bit_length() - 1] + return t + + +def mul(a, b, n): + tb = table(b, n) + return tuple(tb[x] for x in a) + + +def rank(a): + piv = {} + for x in a: + while x: + i = x.bit_length() - 1 + if i not in piv: + piv[i] = x + break + x ^= piv[i] + return len(piv) + + +def gram_systems(L): + """All L x L idempotents K = I + XY over F2 with zero diagonal, rank(XY) = 2.""" + pairs = [(x, y) for x in range(1, 1 << H) for y in range(1 << H) if dot(x, y)] + ks = set() + for seq in itertools.product(pairs, repeat=L): + m = [0] * H + for x, y in seq: + for a in range(H): + if y >> a & 1: + m[a] ^= x + if m != [1 << a for a in range(H)]: + continue + ks.add(tuple((1 << i) ^ sum(dot(seq[i][0], seq[j][1]) << j + for j in range(L)) for i in range(L))) + return sorted(ks) + + +def reverse_transpose(k): + L = len(k) + return tuple(sum((k[L - 1 - j] >> (L - 1 - i) & 1) << j for j in range(L)) + for i in range(L)) + + +def orbit_reps(ks): + kset = set(ks) + reps = [] + for k in ks: + r = reverse_transpose(k) + need(r in kset, 'reversal closure') + if k <= r: + reps.append((k, 1 if k == r else 2)) + return reps + + +def field_frame(k): + """Return (u_i, v_i) with sum u_i v_i = I_n and v_i u_j = K[i][j].""" + L = len(k) + n = L - H + cols = [sum((k[r] >> c & 1) << r for r in range(L)) for c in range(L)] + piv = {} + basis = [] + + def reduce(x): + co = 0 + for i in sorted(piv, reverse=True): + if x >> i & 1: + x ^= piv[i][0] + co ^= piv[i][1] + return x, co + for c in cols: + red, co = reduce(c) + if red: + piv[red.bit_length() - 1] = (red, co ^ (1 << len(basis))) + basis.append(c) + need(len(basis) == n, 'rank n') + us = [] + for c in cols: + red, co = reduce(c) + need(red == 0, 'column in span') + us.append(co) + vs = [sum((basis[q] >> i & 1) << q for q in range(n)) for i in range(L)] + for i in range(L): + for j in range(L): + need(dot(vs[i], us[j]) == (k[i] >> j & 1), 'Gram') + return n, us, vs + + +def stage_candidates(n, us, vs): + """For each ordered call pair ii} R_l.""" + L = len(us) + zero = (0,) * n + tails = [zero] * L + t = zero + for i in reversed(range(L)): + tails[i] = t + t = add(t, outer(us[i], vs[i], n)) + need(t == tuple(1 << i for i in range(n)), 'sum R = I') + groups = [] + for i in range(L): + u, v, s = us[i], vs[i], tails[i] + ts = table(s, n) + su = sum(dot(s[r], u) << r for r in range(n)) + vs_ = 0 + for q in range(n): + if v >> q & 1: + vs_ ^= s[q] + g = {} + for a in range(1 << n): + if not dot(v, a): + continue + sa = sum(dot(s[r], a) << r for r in range(n)) + base = add(outer(a, vs_, n), outer(sa, v, n)) + av = outer(a, v, n) + for b in range(1 << n): + if not dot(b, u) or dot(b, a): + continue + bs = ts[b] + p = add(outer(u, b, n), av) + comm = add(add(base, outer(u, bs, n)), outer(su, b, n)) + g.setdefault(comm, {})[p] = None + groups.append(g) + out = {} + for i, j in itertools.combinations(range(L), 2): + es = {} + for key, pis in groups[i].items(): + pjs = list(groups[j].get(key, ())) + if not pjs: + continue + tjs = [table(p, n) for p in pjs] + for pi in pis: + ti = table(pi, n) + for pj, tj in zip(pjs, tjs): + if tuple(tj[x] for x in pi) == tuple(ti[x] for x in pj): + e = add(pi, pj) + if e not in es: + es[e] = (rank(e), pi, pj) + out[(i, j)] = es + return out + + +def pairings(rem): + if not rem: + yield [] + return + a = rem[0] + for q in range(1, len(rem)): + for rest in pairings(rem[1:q] + rem[q + 1:]): + yield [(a, rem[q])] + rest + + +def best(n, L, cands): + lists = {p: sorted(((r[0], e, table(e, n), r) for e, r in d.items()), + key=lambda z: -z[0]) for p, d in cands.items()} + top = [-1, None] + + def bt(ls, k, chosen, s, pr): + if s + 4 * (len(ls) - k) <= top[0]: + return + if k == len(ls): + top[0] = s + top[1] = (pr, [c[2] for c in chosen]) + return + for r, e, te, info in ls[k]: + if all(tuple(te[x] for x in f) == tuple(tf[x] for x in e) + for f, tf, _ in chosen): + chosen.append((e, te, info)) + bt(ls, k + 1, chosen, s + r, pr) + chosen.pop() + for pr in pairings(list(range(L))): + ls = [lists[p] for p in pr] + if all(ls): + bt(ls, 0, [], 0, pr) + return top + + +def solve(k): + L = len(k) + n, us, vs = field_frame(k) + top = best(n, L, stage_candidates(n, us, vs)) + return None if top[0] < 0 else 2 * L - top[0] + + +def census(L, shard, shards, jobs): + reps = orbit_reps(gram_systems(L)) + mine = [r for idx, r in enumerate(reps) if idx % shards == shard] + with Pool(jobs) as pool: + ds = pool.map(solve, [k for k, _ in mine], chunksize=8) + hist = {} + weighted = {} + for (k, w), d in zip(mine, ds): + key = 'none' if d is None else str(d) + hist[key] = hist.get(key, 0) + 1 + weighted[key] = weighted.get(key, 0) + w + h = hashlib.sha256(json.dumps([[list(k), d] for (k, _), d in zip(mine, ds)]).encode()).hexdigest() + return dict(L=L, shard=shard, shards=shards, systems=len(mine), + reps_hist=dict(sorted(hist.items())), systems_hist=dict(sorted(weighted.items())), + sha256=h) + + +def load_mixed(): + sys.path.insert(0, os.path.join(HERE, '..', 'paired-stage-chronology-cut')) + import chronology + return chronology + + +def witness_check(k): + """Rebuild one optimal word and check it with PR #5631's own mixed routine.""" + L = len(k) + n, us, vs = field_frame(k) + top = best(n, L, stage_candidates(n, us, vs)) + pr, infos = top[1] + ps = [None] * L + labels = [None] * L + for c, ((i, j), (r, pi, pj)) in enumerate(zip(pr, infos)): + ps[i], ps[j] = list(pi), list(pj) + labels[i] = labels[j] = c + for i in range(L): + p = tuple(ps[i]) + r = outer(us[i], vs[i], n) + need(mul(p, p, n) == p and rank(p) == 2, 'rank-two idempotent') + need(mul(p, r, n) == r and mul(r, p, n) == r, 'compatible') + need(dot(vs[i], us[i]) == 0, 'square zero') + es = [] + for c in range(L // 2): + i, j = pr[c] + e = add(tuple(ps[i]), tuple(ps[j])) + need(mul(e, e, n) == e, 'stage idempotent') + es.append(e) + for e, f in itertools.combinations(es, 2): + need(mul(e, f, n) == mul(f, e, n), 'commuting targets') + chron = load_mixed() + cand = dict(n=n, u=list(us), v=list(vs)) + need(chron.mixed(cand, ps, labels) == {}, 'PR5631 mixed coefficient') + d = 2 * L - sum(rank(e) for e in es) + # control: exchanging the first two calls changes chronology and must + # break the mixed coefficient for some stage. + sw = [1, 0] + list(range(2, L)) + bad = dict(n=n, u=[us[i] for i in sw], v=[vs[i] for i in sw]) + broke = chron.mixed(bad, [ps[i] for i in sw], [labels[i] for i in sw]) != {} + # reversal symmetry (Lemma 2): reversing the call order keeps every + # mixed coefficient because [P_i, sum_{ji} R_j]. + rev = dict(n=n, u=list(reversed(us)), v=list(reversed(vs))) + need(chron.mixed(rev, list(reversed(ps)), list(reversed(labels))) == {}, 'reversal lemma') + return d, [list(p) for p in pr], [sorted(rank(e) for e in es)], broke + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--m', type=int, default=4) + ap.add_argument('--shard', type=int) + ap.add_argument('--shards', type=int, default=7) + ap.add_argument('--jobs', type=int, default=os.cpu_count() or 1) + ap.add_argument('--print', action='store_true') + a = ap.parse_args() + result = json.load(open(os.path.join(HERE, 'RESULT.json'))) + if a.shard is None: + small = census(6, 0, 1, a.jobs) + need(small['systems_hist'] == result['m3_control']['systems_hist'], 'm=3 census') + need(min(int(x) for x in small['systems_hist'] if x != 'none') == 0, 'm=3 positive control D=0') + w = result['m4_witness'] + d, pr, ranks, broke = witness_check(tuple(w['K'])) + need(d == w['D'] == result['m4_min_D'], 'witness D') + need(pr == w['pairing'] and ranks == w['ranks'], 'witness shape') + need(broke, 'reversed-order control must fail') + need(sum(result['m4_systems_hist'].values()) == 35008, 'system count') + print('PASS_PAIRED_STAGE_CHRONOLOGY_M4_WITNESS', json.dumps(dict(D=d, pairing=pr, ranks=ranks))) + return + res = census(2 * a.m, a.shard, a.shards, a.jobs) + if a.print: + print(json.dumps(res, sort_keys=True)) + return + need(res == result['m4_shards'][a.shard], 'shard %d differs from RESULT.json' % a.shard) + print('PASS_PAIRED_STAGE_CHRONOLOGY_M4_SHARD', a.shard, json.dumps(res['systems_hist'], sort_keys=True)) + + +if __name__ == '__main__': + main()