From 8478d087599b63180b1189415cfa0c7804eee377 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 10:25:17 +0000 Subject: [PATCH] Prove D1^4 = I leaves the residual x1 monomial nonzero. The formal two-edge algebra omits the fresh-Gaussian equation D1^4 = I. Quotienting by that one central relation keeps Q^{-1} C1 Q^2 C1 C3 D1 D3 at coefficient 1 and keeps Q^{-1} C1 nonzero. No kappa change. Co-authored-by: unpaidmoon --- research/residual-d1-fourth-power/PROOF.md | 152 +++++++++ research/residual-d1-fourth-power/README.md | 127 ++++++++ .../residual-d1-fourth-power/SOURCES.json | 48 +++ research/residual-d1-fourth-power/TASK.json | 90 ++++++ research/residual-d1-fourth-power/VERIFY.json | 41 +++ research/residual-d1-fourth-power/verify.py | 301 ++++++++++++++++++ 6 files changed, 759 insertions(+) create mode 100644 research/residual-d1-fourth-power/PROOF.md create mode 100644 research/residual-d1-fourth-power/README.md create mode 100644 research/residual-d1-fourth-power/SOURCES.json create mode 100644 research/residual-d1-fourth-power/TASK.json create mode 100644 research/residual-d1-fourth-power/VERIFY.json create mode 100644 research/residual-d1-fourth-power/verify.py diff --git a/research/residual-d1-fourth-power/PROOF.md b/research/residual-d1-fourth-power/PROOF.md new file mode 100644 index 0000000000..8b77c222f2 --- /dev/null +++ b/research/residual-d1-fourth-power/PROOF.md @@ -0,0 +1,152 @@ +# The omitted relation D1^4 = I does not kill the residual x1 word + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +No new κ is claimed. The selected frontier stays +`781451/250000000`. + +Evidence class: **proof** that one named central relation does not send +one explicit monomial to zero. The quotient is the predecessor group +algebra modulo the principal ideal `(D1^4 - 1)`. The check reduces that +one word. It is not an enumeration of words, not a search, and not a +theorem about every physical quotient at once. + +## The named relation + +The predecessor algebra is the one installed by +`research/coded-active-feedback/search.py`: the rational group algebra +of the free product `C4(Q) * C2(C1) * C2(C3)`, with formal integer D +exponents, and with `D_i` conjugating only `C_i` by `Q^{-1}`. That is +`Q^4 = C1^2 = C3^2 = I` together with the inherited D conjugation rule +from `research/coded-native-caller/gauge.py`. In that algebra `D1^4` is +the normal form with empty word and degree `(4, 0)`, which is not `I`. + +The relation imposed here is the single extra equation + +```text +D1^4 = I. +``` + +`research/coded-active-feedback/PROOF.md` names this law as omitted: +the formal search adds `C1^2 = C3^2 = I` and `Q^4 = I`, keeps fresh D +exponents as integers, and records that `D^4 = I` is a physical source +relation not imposed there. `D1` is the stage-1 fresh eight-axis +Gaussian in that note. The same note's opening conventions identify +those stage operators with the fresh Gaussians. + +The displayed one-axis factor of that Gaussian law is the normalized +matrix in `research/moving-stage-restoration-tariff/PROOF.md`, + +```text +A = [[a, b], [b, a]], a = (1+i)/2, b = (1-i)/2. +``` + +Clearing the denominator, `2A = [[1+i, 1-i], [1-i, 1+i]]`. Exact +arithmetic in `Z[i]` gives `(2A)^2 = 4 X` and `(2A)^4 = 16 I`, where +`X = [[0, 1], [1, 0]]`. Therefore `A^2 = X` and `A^4 = I`, which is the +sentence `D^2 = X` and `D^4 = I` in that note. The tariff applies the +same normalized block Gaussian at width 8 to the eight-axis blocks. +`research/coded-native-caller/PHYSICAL.md` writes each stage factor as +a coordinate C gate and the fresh stage Gaussian as the product of the +eight noncentral gates. This package does not replay that native +product. The equation imposed on the residual is the one formal +equation `D1^4 = I`. `D3^4 = I` is not imposed. + +## Reduction of the residual word + +Rightmost factors apply first in the engine, and the product is written +left to right. The residual word of open question 2 in PR #7033 is + +```text +Q^{-1} C1 Q^2 C1 C3 D1 D3. +``` + +The Q letters in the middle are adjacent and already form the normal +syllable `Q^2`. The leading `Q^{-1}` is separated from them by `C1`, so +the free-product reducer does not combine those runs. The two `C1` +letters are separated by `Q^2`, so they do not cancel. `C3` remains at +the right of the coefficient. The two D factors contribute degree +`(1, 1)` and an empty word. The engine product is the single basis +element + +```text +word (-1, 2, 1, 1, 2, 3), degree (1, 1), coefficient 1. +``` + +`D1^4` commutes with each generator `Q, C1, C3, D1, D3`. It therefore +commutes with their inverses and with every word. On this monomial the +commutation is a pure shift: left or right multiplication by `D1^4` +replaces the basis element by the same word at degree `(5, 1)`. The +action of degree `(4, 0)` inserts `Q^{-4}` and `Q^4` around each `C1`, +and those runs are empty because `Q^4 = I`. No coefficient is cancelled. + +The quotient by the central element `D1^4` identifies a normal form +`(w, (e1, e3))` with `(w, (e1 + 4k, e3))` and with nothing else. Coset +sums of coefficients are the quotient coordinates. The residual has one +term, already at D1 exponent `1`, so its coset sum is `1` at + +```text +((-1, 2, 1, 1, 2, 3), (1, 1)). +``` + +That coordinate is not zero. The same quotient sends `D1^4 - I` to zero, +and it sends `D1^5` and `D1^{-3}` to the class of `D1`, which is not +the class of `I`. + +## Q^{-1} C1 stays nonzero and distinct + +The comparison element is the single basis element + +```text +Q^{-1} C1 = word (-1, 2), degree (0, 0), coefficient 1. +``` + +Its D1 exponent is `0`, so the coset of `D1^4` does not mix it with any +other degree-`(0, 0)` word. The quotient coordinate is `1` at +`((-1, 2), (0, 0))`. That is not the residual class. The Q-letter parity +character, the sign of the number of letters of absolute value `1`, +still sends this representative to `-1`. + +Thus `D1^4 = I` does not send the residual word to zero and does not +collapse `Q^{-1} C1`. + +## Separating representation + +Let the basis of `C^8` be indexed by `q + 2 d1 + 4 d3` with each bit in +`{0, 1}`. Define + +```text +Q = diag(i^q), D1 = diag(i^{d1}), D3 = diag(i^{d3}), +C1 = swap of bits q and d1, C3 = swap of bits q and d3. +``` + +These matrices are monomial, hence invertible. They satisfy `Q^4 = I`, +`C1^2 = C3^2 = I`, commutation of each `D` with `Q` and with each other, +commutation of `D1` with `C3` and of `D3` with `C1`, the two conjugation +identities `D_s C_s = Q^{-1} C_s Q D_s`, and `D1^4 = I`. They also +satisfy the further equations `D3^4 = I` and `(C1 C3)^3 = I`. Those +further equations are relations of this representation only. They are +not imposed on the formal quotient above. + +The representation is therefore a ring homomorphism out of the quotient +by `D1^4 - I` into 8 by 8 matrices over the Gaussian integers. The image +of the residual is an invertible monomial matrix, and the image of +`Q^{-1} C1` is a different invertible monomial matrix. A homomorphism +that sends an element to a nonzero matrix witnesses that the element +was nonzero, and unequal images witness that the two elements were not +equal. + +`C1` does not commute with `Q` in this representation, so the witness +does not force the predecessor noncommutation `[C1, Q] = 0`. + +## What this does not claim + +The quotient does not produce an autonomous row. No owner-indexed +multiplier is exhibited, and the four published banks are not reread. +A later quotient that did kill the residual would still need its own +multiplier before anyone could call the result an autonomous caller. + +`D3^4 = I` is a different equation and is not part of the quotient. +Nonzero D exponents, owner mixing, and any feedback edge other than the +published pair stay outside. The result is not a change of the selected +conditional κ. diff --git a/research/residual-d1-fourth-power/README.md b/research/residual-d1-fourth-power/README.md new file mode 100644 index 0000000000..323e31e4f8 --- /dev/null +++ b/research/residual-d1-fourth-power/README.md @@ -0,0 +1,127 @@ +# D1^4 = I leaves the residual x1 monomial nonzero + +**Scoped proof; no new κ.** The formal algebra of the published two-edge +feed imposes `Q^4 = C1^2 = C3^2 = I` and the inherited rule that `D_i` +conjugates only `C_i` by `Q^{-1}`. One physical relation omitted by that +algebra is the fresh-Gaussian equation `D1^4 = I`. In the quotient by +that single central equation, the residual word + +```text +Q^{-1} C1 Q^2 C1 C3 D1 D3 +``` + +keeps the representative with word `(-1, 2, 1, 1, 2, 3)` and degree +`(1, 1)`, coefficient 1. The comparison element `Q^{-1} C1` keeps the +distinct representative with word `(-1, 2)` and degree `(0, 0)`, and the +Q-letter parity character still sends that representative to `-1`. + +[PROOF.md](PROOF.md) gives the coset reduction and an 8-dimensional +separating representation. The representation also satisfies `D3^4 = I` +and `(C1 C3)^3 = I`. Those two equations are extra relations of the +matrices. They are not part of the formal quotient. + +The selected frontier is unchanged. This quotient is not an autonomous +caller. No multiplier is exhibited. + +## Result + +`research/coded-active-feedback` records that `D^4 = I` is a physical +source relation not imposed on its formal algebra. The stage-1 instance +of that law is `D1^4 = I`. In the predecessor algebra this element is +the empty word at degree `(4, 0)`, so the equation is not already true. + +Multiplying the residual by `D1^4` only adds 4 to the D1 exponent. The +quotient therefore leaves the exponent-1 representative in place, with +coefficient 1. `D1^4 - I` itself reduces to zero, and `D1` does not. + +The one-axis factor `A = [[a, b], [b, a]]` with `a = (1+i)/2` and +`b = (1-i)/2` satisfies `A^2 = X` and `A^4 = I` by exact arithmetic in +`Z[i]`. That is the matrix law named in the moving-stage tariff. The +native eight-axis word is not replayed. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3 -B scripts/research_package.py --package research/residual-d1-fourth-power --check-only +python3 -B scripts/research_package.py --package research/residual-d1-fourth-power +``` + +Direct replay: + +```sh +python3 -I -W error -B research/residual-d1-fourth-power/verify.py +python3 -I -O -W error -B research/residual-d1-fourth-power/verify.py +``` + +The optimized command still executes the checks. They are `need` +failures, not assertions. No network, native build, or full multiplier +replay is used. The run prints `PASS_RESIDUAL_D1_FOURTH_POWER` and +`new_kappa null`. + +## Scope + +Original card: `joint-query-controller`. Scope status: **refined**. The +card asks for one source-bound caller identity, or an obstruction to +that change, together with its charges. This package does not change +the query demand. It takes open question 2 of the D-exponent-0 x1 +obstruction, the question posed by +[PR #7033](https://github.com/CrocSwap/integer-mult-bounds/pull/7033) +and recorded in +[discussion comment 19513870](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19513870). +The first step named there is one source relation outside +`Q^4 = C1^2 = C3^2 = I` and the inherited D conjugation rule. The +relation used here is `D1^4 = I`. + +Base commit: `17469fff78c22941280f04d39dc5a1faee09c840`. Pins are in +[SOURCES.json](SOURCES.json). The catalogue is provenance. The selected +record, `search.py`, `gauge.py`, and the three cited proofs are live +inputs. The selected conditional value is the selected record, +`781451/250000000`. + +Overlap at this base used `scripts/find_overlap.py`. Local notes at +`17469fff78c22941280f04d39dc5a1faee09c840` (10178 paths, complete +inventory), 339 open-PR records fetched at 2026-11-10T10:19:05Z, and +7013 discussion records fetched at 2026-11-10T10:20:14Z. The phrase +`Q^{-1} C1 Q^2 C1 C3` matches PR #7033 and +[discussion comment 19513867](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19513867), +which ask this question. Requiring both `physical relation` and `D^4`, +and both `omitted` and `D^4=I`, matched nothing in that snapshot. The +search is not a novelty certificate. Closed PR bodies were outside the +open-PR snapshot. + +## Open next questions + +Does one linear source relation, compatible with +`Q^4 = C1^2 = C3^2 = I` and the inherited D conjugation rule, send the +coefficient word `Q^{-1} C1 Q^2 C1 C3` to zero while leaving +`Q^{-1} C1` nonzero? `D1^4 = I` meets this word only by adding multiples +of 4 to a D exponent that is already zero on the coefficient, so the +coset sum stays 1. A linear dependence among distinct degree-zero words +could behave differently. The first step is to evaluate +`C = diag(K_i)^{-1} F diag(K_i)` from +`research/native-involutive-dual/PROOF.md` on one shared central axis +and reduce this coefficient there. This package does not evaluate `F`. + +If a later quotient does send the residual to zero and keeps +`Q^{-1} C1` nonzero, which owner-indexed multiplier on the four +published banks becomes the autonomous row `[A, 0, 0, 0]`? Killing the +monomial in a quotient is not yet a caller. The first step is to name +that quotient and recompute the four columns. No such quotient is +constructed here. + +## Credit + +The trace, algebra, and omitted-relation sentence are Cinna Davis's +`research/coded-active-feedback`, using Dugongue's PR4948 chronology, +Dillon's PR4933 code, and the gauge engine in +`research/coded-native-caller/gauge.py`. The normalized one-axis law +`D^2 = X`, `D^4 = I` is Nick Petalas's +`research/moving-stage-restoration-tariff`. The residual monomial and +the question are the open remainder of the D-exponent-0 x1 obstruction. +The nonzero D-exponent multiplier question from that obstruction is a +separate question and is not answered here. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. +Apache-2.0. diff --git a/research/residual-d1-fourth-power/SOURCES.json b/research/residual-d1-fourth-power/SOURCES.json new file mode 100644 index 0000000000..f041659b73 --- /dev/null +++ b/research/residual-d1-fourth-power/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/coded-active-feedback/PROOF.md", + "usage": "input", + "git_blob": "9716baebb4895b07acf9db0cbce010590b03945a", + "sha256": "c6233d2759811190c7ea1be455c9351b61c29f6a8afc8584e7bc0dfbc00f3a3d" + }, + { + "path": "research/coded-active-feedback/search.py", + "usage": "input", + "git_blob": "60de5a87d3f64fc69e2595cdb2df771c91a0fe6e", + "sha256": "1383010827af29a1b0e595e2c1aa2ffad461b266ffc9f936efce1603ff9f5eb6" + }, + { + "path": "research/coded-native-caller/PHYSICAL.md", + "usage": "input", + "git_blob": "da8837ba67423ef08ef1afb8e8297a8032aafe9f", + "sha256": "4321b159ff8d3fe705419adaaa1beef75606e869e34341bda553f17d598a6078" + }, + { + "path": "research/coded-native-caller/gauge.py", + "usage": "input", + "git_blob": "44ae72b314cccf677b44d75c374be6dcac1c8167", + "sha256": "390391d291353741c89daea999d483660ca185987ed96a15b82576280c487cad" + }, + { + "path": "research/moving-stage-restoration-tariff/PROOF.md", + "usage": "input", + "git_blob": "a571bb602aefe6d1eddcd15b189751bef5b31ebe", + "sha256": "36d3b13ab3919559fde46b1c33f856379cd5b2bab06d835ddf7e177c96868712" + } + ] +} diff --git a/research/residual-d1-fourth-power/TASK.json b/research/residual-d1-fourth-power/TASK.json new file mode 100644 index 0000000000..2fe25536aa --- /dev/null +++ b/research/residual-d1-fourth-power/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "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": "refined", + "actual_scope": "In the predecessor formal algebra, the single extra equation D1^4 = I leaves the residual word Q^{-1} C1 Q^2 C1 C3 D1 D3 equal to the nonzero class with word (-1, 2, 1, 1, 2, 3) and degree (1, 1), and leaves Q^{-1} C1 equal to the distinct nonzero class with word (-1, 2) and degree (0, 0).", + "scope_change_reason": "The card allows one source-bound caller identity or an obstruction to that change. This package does not change the query demand and does not rerun the D-exponent-0 classification. It answers open question 2 of that obstruction by reducing one named omitted relation, D1^4 = I. Nonzero D exponents, owner mixing, D3^4 = I, and a new feedback edge stay outside.", + "bottleneck_link": "A productive main job has to be autonomous. The formal x1 obstruction is a nonzero monomial. Quotienting by D1^4 = I does not delete that monomial and does not collapse Q^{-1} C1, so this relation still does not earn a new kappa.", + "budget_minutes": 60, + "stop_rule": "Stop once the residual word and Q^{-1} C1 have been reduced under the single equation D1^4 = I. Do not impose a second relation and do not search a nonzero D exponent.", + "outcome": "negative-result", + "evidence": "PROOF.md and verify.py. The coset sum of the residual is 1, and an 8-dimensional representation of a further quotient sends both words to distinct invertible matrices. The one-axis Gaussian identity A^4 = I is exact arithmetic in Z[i]. No kappa change.", + "author": "unpaidmoon, with substantial Cursor Grok assistance", + "ai_assistance": "Substantial Cursor Grok assistance. No subagents. The predecessor group algebra is imported unchanged.", + "open_questions": [ + { + "question": "Does one linear source relation, compatible with Q^4 = C1^2 = C3^2 = I and the inherited D conjugation rule, send the coefficient word Q^{-1} C1 Q^2 C1 C3 to zero while leaving Q^{-1} C1 nonzero?", + "why_it_matters": "D1^4 = I only shifts a D exponent by multiples of 4. The coefficient word has D degree (0, 0) and one term, so its coset sum stays 1. A linear dependence among distinct degree-zero words could remove it.", + "first_step": "Evaluate C = diag(K_i)^{-1} F diag(K_i) from research/native-involutive-dual/PROOF.md on one shared central axis, and reduce the coefficient word in that operator algebra.", + "blocked_by": "This package imposes only D1^4 = I. It does not evaluate F or the 112 normalizers." + }, + { + "question": "If a later quotient sends the residual to zero and keeps Q^{-1} C1 nonzero, which owner-indexed multiplier on the four published banks becomes the autonomous row [A, 0, 0, 0]?", + "why_it_matters": "A quotient that kills the monomial is not an autonomous caller until some multiplier realizes the row.", + "first_step": "Name the quotient and the multiplier, then recompute the four columns of the published banks.", + "blocked_by": "The quotient tested here does not kill the residual, so there is no image to recompute." + } + ] +} diff --git a/research/residual-d1-fourth-power/VERIFY.json b/research/residual-d1-fourth-power/VERIFY.json new file mode 100644 index 0000000000..f028503429 --- /dev/null +++ b/research/residual-d1-fourth-power/VERIFY.json @@ -0,0 +1,41 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "checks": "Pins, one-axis fourth power, residual coset, parity character, and the separating representation.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "checks": "Same D1^4 quotient under optimization. Checks are explicit failures, not assertions.", + "timeout_seconds": 120 + } + ], + "inputs": [ + "research/coded-active-feedback/search.py", + "research/coded-native-caller/gauge.py", + "research/coded-active-feedback/PROOF.md", + "research/coded-native-caller/PHYSICAL.md", + "research/moving-stage-restoration-tariff/PROOF.md", + "certificates/selected-result.json" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/residual-d1-fourth-power/verify.py b/research/residual-d1-fourth-power/verify.py new file mode 100644 index 0000000000..ec6ef2f21c --- /dev/null +++ b/research/residual-d1-fourth-power/verify.py @@ -0,0 +1,301 @@ +#!/usr/bin/env python3 +"""D1^4 = I does not kill the residual word Q^{-1} C1 Q^2 C1 C3 D1 D3. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +The predecessor group algebra is imported unchanged. Checks are explicit +need failures, so the optimized run still executes them. +""" +from fractions import Fraction +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +RESIDUAL = (-1, 2, 1, 1, 2, 3) +TARGET = (-1, 2) +PINS = { + "research/coded-active-feedback/search.py": + "1383010827af29a1b0e595e2c1aa2ffad461b266ffc9f936efce1603ff9f5eb6", + "research/coded-native-caller/gauge.py": + "390391d291353741c89daea999d483660ca185987ed96a15b82576280c487cad", + "research/coded-active-feedback/PROOF.md": + "c6233d2759811190c7ea1be455c9351b61c29f6a8afc8584e7bc0dfbc00f3a3d", + "research/coded-native-caller/PHYSICAL.md": + "4321b159ff8d3fe705419adaaa1beef75606e869e34341bda553f17d598a6078", + "research/moving-stage-restoration-tariff/PROOF.md": + "36d3b13ab3919559fde46b1c33f856379cd5b2bab06d835ddf7e177c96868712", + "certificates/selected-result.json": + "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", +} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_search(): + path = ROOT / "research/coded-active-feedback/search.py" + spec = importlib.util.spec_from_file_location("active_feedback_search_pinned", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def gadd(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def gmul(a, b): + return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) + + +def matmul(left, right): + size = len(left) + out = [[(0, 0)] * size for _ in range(size)] + for i in range(size): + for k in range(size): + if left[i][k] == (0, 0): + continue + for j in range(size): + if right[k][j] != (0, 0): + out[i][j] = gadd(out[i][j], gmul(left[i][k], right[k][j])) + return out + + +def matpow(matrix, exponent): + size = len(matrix) + out = [[(1 if i == j else 0, 0) for j in range(size)] for i in range(size)] + while exponent: + if exponent & 1: + out = matmul(out, matrix) + matrix = matmul(matrix, matrix) + exponent >>= 1 + return out + + +def eye(size): + return [[(1 if i == j else 0, 0) for j in range(size)] for i in range(size)] + + +def same(left, right): + return all(left[i][j] == right[i][j] + for i in range(len(left)) for j in range(len(left))) + + +def residue(element): + """Coset sums for the central quotient by D1^4 = I. D3 is not reduced.""" + totals = {} + for (word, degree), value in element.items(): + key = (word, (degree[0] % 4, degree[1])) + totals[key] = totals.get(key, Fraction(0)) + value + if totals[key] == 0: + del totals[key] + return totals + + +def q_parity(element): + total = Fraction(0) + for (word, degree), value in element.items(): + need(degree == (0, 0), "parity character left the D-exponent-0 line") + sign = -1 if sum(1 for letter in word if abs(letter) == 1) % 2 else 1 + total += value * sign + return total + + +def one_axis_gaussian(): + """(2A)^2 = 4X and (2A)^4 = 16 I for A = [[a, b], [b, a]].""" + two = [[(1, 1), (1, -1)], [(1, -1), (1, 1)]] + square = matmul(two, two) + fourth = matmul(square, square) + need(square == [[(0, 0), (4, 0)], [(4, 0), (0, 0)]], + "One-axis Gaussian square is not 4X") + need(fourth == [[(16, 0), (0, 0)], [(0, 0), (16, 0)]], + "One-axis Gaussian fourth power is not 16 I") + + +def separating_representation(algebra, qi, c1, q, c3, d1, d3): + """Monomial 8-dimensional image. Also satisfies D3^4 = I, which is extra.""" + identity = eye(8) + phase = (0, 1) + + def diagonal(bit): + matrix = eye(8) + for index in range(8): + if (index >> bit) & 1: + matrix[index][index] = phase + return matrix + + def swap(bit_a, bit_b): + matrix = [[(0, 0)] * 8 for _ in range(8)] + for index in range(8): + bits = [(index >> bit) & 1 for bit in range(3)] + bits[bit_a], bits[bit_b] = bits[bit_b], bits[bit_a] + destination = bits[0] + 2 * bits[1] + 4 * bits[2] + matrix[destination][index] = (1, 0) + return matrix + + q_matrix = diagonal(0) + d1_matrix = diagonal(1) + d3_matrix = diagonal(2) + c1_matrix = swap(0, 1) + c3_matrix = swap(0, 2) + q_inverse = matpow(q_matrix, 3) + need(same(matpow(q_matrix, 4), identity), "Representation lost Q^4 = I") + need(same(matmul(c1_matrix, c1_matrix), identity), "Representation lost C1^2 = I") + need(same(matmul(c3_matrix, c3_matrix), identity), "Representation lost C3^2 = I") + need(same(matpow(d1_matrix, 4), identity), "Representation lost D1^4 = I") + need(same(matpow(d3_matrix, 4), identity), + "Representation was expected to satisfy the extra equation D3^4 = I") + braid = c1_matrix + for factor in (c3_matrix, c1_matrix, c3_matrix, c1_matrix, c3_matrix): + braid = matmul(braid, factor) + need(same(braid, identity), + "Representation was expected to satisfy the extra equation (C1 C3)^3 = I") + need(same(matmul(d1_matrix, q_matrix), matmul(q_matrix, d1_matrix)), + "Representation lost [D1, Q] = 0") + need(same(matmul(d3_matrix, q_matrix), matmul(q_matrix, d3_matrix)), + "Representation lost [D3, Q] = 0") + need(same(matmul(d1_matrix, d3_matrix), matmul(d3_matrix, d1_matrix)), + "Representation lost [D1, D3] = 0") + need(same(matmul(d1_matrix, c3_matrix), matmul(c3_matrix, d1_matrix)), + "Representation lost [D1, C3] = 0") + need(same(matmul(d3_matrix, c1_matrix), matmul(c1_matrix, d3_matrix)), + "Representation lost [D3, C1] = 0") + need(not same(matmul(c1_matrix, q_matrix), matmul(q_matrix, c1_matrix)), + "Representation collapsed [C1, Q]") + conjugated = matmul(q_inverse, matmul(c1_matrix, matmul(q_matrix, d1_matrix))) + need(same(matmul(d1_matrix, c1_matrix), conjugated), + "Representation lost the D1 conjugation rule") + conjugated = matmul(q_inverse, matmul(c3_matrix, matmul(q_matrix, d3_matrix))) + need(same(matmul(d3_matrix, c3_matrix), conjugated), + "Representation lost the D3 conjugation rule") + + def letter_matrix(letter): + if letter == 1: + return q_matrix + if letter == -1: + return q_inverse + if letter == 2: + return c1_matrix + if letter == 3: + return c3_matrix + raise ValueError("unexpected formal letter") + + def image(element): + """Normal form is the free-product word on the left and the D monomial on the right.""" + total = [[(0, 0)] * 8 for _ in range(8)] + for (word, degree), value in element.items(): + need(degree[0] >= 0 and degree[1] >= 0, "image expects a nonnegative D degree") + matrix = matmul(matpow(d1_matrix, degree[0]), matpow(d3_matrix, degree[1])) + for letter in reversed(word): + matrix = matmul(letter_matrix(letter), matrix) + scale = (int(value), 0) if value.denominator == 1 else None + need(scale is not None, "representation expected an integer coefficient") + for row in range(8): + for column in range(8): + total[row][column] = gadd(total[row][column], gmul(scale, matrix[row][column])) + return total + + def monomial_and_bijective(matrix): + rows = set() + for column in range(8): + support = [row for row in range(8) if matrix[row][column] != (0, 0)] + need(len(support) == 1, "image column is not monomial") + rows.add(support[0]) + need(len(rows) == 8, "image is singular") + + residual = algebra.mul(qi, c1, q, q, c1, c3, d1, d3) + target = algebra.mul(qi, c1) + explicit = q_inverse + for factor in (c1_matrix, q_matrix, q_matrix, c1_matrix, c3_matrix, d1_matrix, d3_matrix): + explicit = matmul(explicit, factor) + residual_image = image(residual) + target_image = image(target) + need(same(residual_image, explicit), + "normal-form image disagrees with the generator product") + monomial_and_bijective(residual_image) + monomial_and_bijective(target_image) + need(not same(residual_image, target_image), + "representation identified the residual with Q^{-1} C1") + need(not same(residual_image, [[(0, 0)] * 8 for _ in range(8)]), + "representation killed the residual") + images = {} + images["residual_nonzero"] = True + images["target_nonzero"] = True + images["images_distinct"] = True + images["extra_relations_in_this_representation"] = ["D3^4 = I", "(C1 C3)^3 = I"] + return images + + +def main(): + for name, digest in PINS.items(): + blob = (ROOT / name).read_bytes() + need(sha256(blob).hexdigest() == digest, "source pin changed: " + name) + feedback = (ROOT / "research/coded-active-feedback/PROOF.md").read_text(encoding="utf-8") + physical = (ROOT / "research/coded-native-caller/PHYSICAL.md").read_text(encoding="utf-8") + tariff = (ROOT / "research/moving-stage-restoration-tariff/PROOF.md").read_text(encoding="utf-8") + need("D^4=I and other additional physical source relations are not" in feedback, + "omitted-relation sentence missing") + need("Let Q be the central C gate, D the product of the other eight C gates" in physical, + "stage-Gaussian sentence missing") + need("`D^2=X` and `D^4=I`" in tariff, "one-axis fourth-power sentence missing") + selected = json.loads((ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")) + need(selected["kappa"] == "781451/250000000", "selected frontier kappa changed") + + one_axis_gaussian() + algebra = load_search().algebra() + q, c1, c3 = algebra.gen(1), algebra.gen(2), algebra.gen(3) + d1, d3 = algebra.D(0), algebra.D(1) + qi = algebra.inv(q) + residual = algebra.mul(qi, c1, q, q, c1, c3, d1, d3) + target = algebra.mul(qi, c1) + need(residual == algebra.term(RESIDUAL, (1, 1)), "residual normal form changed") + need(target == algebra.term(TARGET, (0, 0)), "Q^{-1} C1 normal form changed") + + fourth = algebra.mul(d1, d1, d1, d1) + need(fourth == algebra.term((), (4, 0)), "D1^4 is not the degree-(4, 0) monomial") + need(fourth != algebra.one, "D1^4 is already I in the predecessor algebra") + for name, generator in (("Q", q), ("C1", c1), ("C3", c3), ("D1", d1), ("D3", d3)): + need(algebra.mul(fourth, generator) == algebra.mul(generator, fourth), + "D1^4 failed to commute with " + name) + shifted = algebra.term(RESIDUAL, (5, 1)) + need(algebra.mul(fourth, residual) == shifted, "left D1^4 did not shift only the exponent") + need(algebra.mul(residual, fourth) == shifted, "right D1^4 did not shift only the exponent") + + residual_class = {(RESIDUAL, (1, 1)): Fraction(1)} + target_class = {(TARGET, (0, 0)): Fraction(1)} + need(residue(residual) == residual_class, "residual coset sum is not 1") + need(residue(target) == target_class, "Q^{-1} C1 coset sum is not 1") + need(residual_class != target_class, "quotient identified the two words") + need(q_parity(target) == -1, "parity character collapsed Q^{-1} C1") + need(residue(algebra.add(fourth, algebra.neg(algebra.one))) == {}, + "quotient failed to impose D1^4 = I") + fifth = algebra.mul(d1, d1, d1, d1, d1) + inverse_cube = algebra.mul(algebra.inv(d1), algebra.inv(d1), algebra.inv(d1)) + need(residue(fifth) == residue(d1), "D1^5 did not reduce to D1") + need(residue(inverse_cube) == residue(d1), "D1^{-3} did not reduce to D1") + need(residue(d1) != residue(algebra.one), "D1 collapsed to I") + witness = separating_representation(algebra, qi, c1, q, c3, d1, d3) + + receipt = { + "relation": "D1^4 = I", + "residual_class": [list(RESIDUAL), [1, 1], 1], + "target_class": [list(TARGET), [0, 0], 1], + "residual_is_zero": False, + "target_is_zero": False, + "classes_distinct": True, + "target_q_parity": -1, + "witness": witness, + "evidence_class": "proof", + "selected_kappa": selected["kappa"], + "new_kappa": None, + } + print(json.dumps(receipt, sort_keys=True)) + print("PASS_RESIDUAL_D1_FOURTH_POWER") + + +if __name__ == "__main__": + main()