diff --git a/research/owner-indexed-x1-obstruction/PROOF.md b/research/owner-indexed-x1-obstruction/PROOF.md new file mode 100644 index 0000000000..59c07ec901 --- /dev/null +++ b/research/owner-indexed-x1-obstruction/PROOF.md @@ -0,0 +1,221 @@ +# No D-exponent-0 owner index clears the three-term x1 block + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +No new κ is claimed. The selected frontier is unchanged. + +Evidence class: **proof** in the predecessor's formal algebra, under the +hypotheses below. The multiplier space is infinite. This is not an +enumeration of words, not a bounded search, and not a theorem about every +quotient or every physical caller. + +## Object + +Use the published two-edge feed in +[research/coded-active-feedback](../coded-active-feedback/PROOF.md), +replayed by `search.replay(one, C1 Q^2)`. After the left endpoint the +replay stores four banks. Bank 2 carries + +```text +A = D1 Q^{-1} +``` + +together with the y0 coupling and the three-term x1 block. The reading on +one owner is a left combination of these four banks by D-exponent-0 +elements `m0, m1, m2, m3` of the predecessor's `Q, C1, C3` algebra. It +does not mix owners. The four stored banks are only read. A fresh image is +this combination and nothing else. + +Negative D exponents, owner-mixing maps, and a feedback edge outside the +published two-edge feed are outside this statement. The declared +alternating-family lock and the one-edge `C1 Q` row are not re-proved. + +The algebra is the one installed by `search.algebra()`: words in the free +product `C4(Q) * C2(C1) * C2(C3)`, with formal D exponents, and with `D_i` +conjugating only `C_i` by `Q^{-1}`. A D-exponent-0 left factor therefore +concatenates words and preserves the D degree of the right factor. + +## The banks + +The replay equals the following columns. Here `D(1,0)` is `D1` and +`D(1,1)` is `D1 D3`. + +```text +bank 0: x0 = (Q^{-1} C1 + Q^2 C1) D1 + y0 = Q^{-1} D1 + x1 = -Q^2 C1 D1 + y1 = 0 +bank 1: y0 = C1 Q D1 + x0 = x1 = y1 = 0 +bank 2: x0 = A = Q^{-1} D1 + y0 = (Q^{-1} C1 Q - Q^{-1} C1 Q^2) D1 + x1 = (Q^{-1} C1 Q C1 - Q^{-1}) D1 + Q^{-1} C3 D1 D3 + y1 = 0 +bank 3: x0 = C3 Q^{-1} C1 D1 D3 + y0 = C3 D1 D3 + x1 = (-I - C3 Q^{-1} C1 + C3 C1) D1 D3 + y1 = C3 Q D1 D3 +``` + +`verify.py` compares these polynomials with the replay. Bank 3's x0 column +is the only x0 column on the `D1 D3` line, and it is a monomial. Its +two-sided inverse in the algebra sends `m3` times that column to `m3`. +The target `A` has no `D3` component, so every solution of `S_x0 = A` has +`m3 = 0`. + +## The forced shape + +Write `x` for bank 0's x0 column times `A^{-1}`, and write + +```text +const = Q^{-1}(C1 Q C1 - I) = -Q^{-1} + Q^{-1} C1 Q C1. +``` + +Direct multiplication gives + +```text +x = (Q^{-1} + Q^2) C1 Q = Q^2 (I + Q) C1 Q, +Q^{-1} + Q^2 = Q^2 (I + Q), +bank0_x0 = x A, +bank2_x1 = const D1 + Q^{-1} C3 D1 D3. +``` + +The second formula for `x` uses `Q^2 Q = Q^3 = Q^{-1}`. Thus every +D-exponent-0 solution of `S_x0 = A` has + +```text +m2 = 1 - m0 x. +``` + +Bank 1 has zero x1, and `m3 = 0`, so + +```text +S_x1 = bank2_x1 + m0 (bank0_x1 - x bank2_x1) + = (const - m0 C1) D1 + (1 - m0 x) Q^{-1} C3 D1 D3. +``` + +The same two element identities + +```text +bank2_y0 + const · bank1_y0 = 0, +bank0_y0 - C1 · bank1_y0 - x bank2_y0 = 0 +``` + +give, for `m1 = const - m0 C1`, the y0 column `S_y0 = 0`. Banks 0, 1, and +2 have zero y1, so `S_y1 = 0` as well. Imposing y0 zero fixes `m1` and +does not appear in `S_x1`. + +## The D1 D3 summand never vanishes + +Right multiplication by the group element `Q^{-1} C3` is bijective on the +D-exponent-0 algebra: its two-sided inverse is `C3 Q`, and + +```text +(Q^{-1} C3)(C3 Q) = I = (C3 Q)(Q^{-1} C3). +``` + +A D-exponent-0 left factor does not change D degree, so + +```text +(1 - m0 x) Q^{-1} C3 D1 D3 = 0 +``` + +if and only if `1 - m0 x = 0`. + +Suppose `m0 x = 1`. Substitute the factorization of `x` and cancel the +unit `C1 Q` on the right: + +```text +m0 Q^2 (I + Q) = Q^{-1} C1. +``` + +Let `φ` be the linear map on the D-exponent-0 algebra that sends a word +to `(-1)` raised to the number of letters of absolute value 1, and a +linear combination to the corresponding combination of those signs. Then +`φ(I + Q) = 1 + (-1) = 0` and `φ(Q^{-1} C1) = -1`. + +This `φ` is an algebra homomorphism. Multiplication concatenates words +and then runs the installed reducer. Each reducer step preserves the +parity of the Q-letter count: + +- cancelling an adjacent pair `C_i C_i` removes two letters that are not + Q letters; +- a Q run of `n` letters `±1` has exponent sum `s ≡ n (mod 2)`, and the + normal form of the exponent modulo 4 has letter count `0, 1, 2, 1` in + the four residue classes, hence letter count congruent to `s` modulo 2. + +Concatenation adds the counts, so `φ` multiplies on words and therefore +on the whole algebra. Apply it to the displayed equation: + +```text +φ(m0 Q^2) φ(I + Q) = 0 ≠ -1 = φ(Q^{-1} C1). +``` + +No such `m0` exists. Therefore `1 - m0 x` is never zero, and neither is +the `D1 D3` summand of `S_x1`. + +In particular, no fresh image of this form has `S_x1 = 0` while +`S_x0 = A`. Clearing the block means that zero column: together with +`S_y0 = S_y1 = 0` it would be the autonomous row `[A, 0, 0, 0]`. The +subfamily that also keeps `S_y0 = 0` is included. A later +D-exponent-0 left multiple `u` of such an image still has x0 block `u A`. +Since `A` is a monomial, `u A = A` forces `u = I`, so that later multiple +does not clear the summand either. + +## The unique index that clears the D1 line + +Right multiplication by `C1` is bijective because `C1^2 = I`. The `D1` +summand vanishes if and only if + +```text +m0 = const C1 = Q^{-1} C1 Q - Q^{-1} C1, +``` + +and the y0 equation then forces `m1 = 0`. For this single index the four +products in `m0 x` are + +```text +(-Q^{-1} C1)(Q^{-1} C1 Q) = -Q^{-1} C1 Q^{-1} C1 Q, +(-Q^{-1} C1)(Q^2 C1 Q) = -Q^{-1} C1 Q^2 C1 Q, +(Q^{-1} C1 Q)(Q^{-1} C1 Q) = I, +(Q^{-1} C1 Q)(Q^2 C1 Q) = Q^{-1} C1 Q^{-1} C1 Q. +``` + +The first and fourth cancel, so + +```text +m0 x = I - Q^{-1} C1 Q^2 C1 Q, +m2 = Q^{-1} C1 Q^2 C1 Q. +``` + +Right multiplication by `Q^{-1} C3` cancels `Q Q^{-1}` and leaves the +fresh image + +```text +S = m0 · bank 0 + m2 · bank 2, +S_x0 = A, S_y0 = 0, S_y1 = 0, +S_x1 = Q^{-1} C1 Q^2 C1 C3 D1 D3. +``` + +That x1 column is one monomial, not zero, and it is not the published +three-term block. The three multiplier monomials are the algebraic charge +of this near-miss. They do not clear the block. No scalar-field minimum +and no tape cost are claimed for them. + +The constant index `m0 = 0`, `m1 = const`, `m2 = 1` is the predecessor's +image. Its x1 column is the original three monomials. Both indexes obey +the same nonvanishing statement. + +## What is not proved + +A multiplier with a nonzero D exponent can mix the `D1` and `D1 D3` +lines; this note does not classify it. Owner-mixing maps and any feedback +operator other than the published pair `(I, C1 Q^2)` are not classified. +The formal algebra does not impose `D^4 = I` or any further physical +relation. In a quotient that sends `Q^{-1} C1 Q^2 C1 C3` to zero while +keeping the displayed character argument's target nonzero, the image of +the identity `m0 x - 1 = m2` remains true, but this particular monomial +could vanish. No such quotient is proved here. + +The result is not an autonomous decoder, not a new caller bill, and not +a change of the selected conditional κ. diff --git a/research/owner-indexed-x1-obstruction/README.md b/research/owner-indexed-x1-obstruction/README.md new file mode 100644 index 0000000000..0aebec6865 --- /dev/null +++ b/research/owner-indexed-x1-obstruction/README.md @@ -0,0 +1,127 @@ +# No owner index clears the three-term x1 block + +**Scoped proof; no new κ.** On the published two-edge feed, every +owner-indexed D-exponent-0 left map of the four final banks that keeps +`x0 = D1 Q^{-1}` has x1 coefficient + +```text +(const - m0 C1) D1 + (1 - m0 x) Q^{-1} C3 D1 D3. +``` + +The second summand is never zero, so the x1 column is never the zero +element. Keeping y0 zero fixes `m1` and does not cancel that summand. The +four stored endpoint banks are not overwritten. The autonomous row would +be `[A, 0, 0, 0]`. Removing the three published keys still leaves one +monomial, so that row is not reached. + +Exactly one index also clears the `D1` line. It keeps y0 zero and leaves +the single monomial `Q^{-1} C1 Q^2 C1 C3 D1 D3`. That image is not a +clearance of the three-term block. [PROOF.md](PROOF.md) gives the products +and the parity character. + +The selected frontier is unchanged. This does not rerun the y0 defect, +the declared alternating-family lock, or a feedback-edge test. + +## Result + +The predecessor replay stores `A = D1 Q^{-1}` on final bank 2 together +with the published three-term x1 block, and stores a pure y0 monomial on +final bank 1. For each D-exponent-0 element `m0`, the other coefficients +that keep `x0 = A` and clear y0 are uniquely + +```text +m3 = 0, m2 = 1 - m0 x, m1 = const - m0 C1. +``` + +Here + +```text +x = Q^2 (I + Q) C1 Q, const = Q^{-1}(C1 Q C1 - I). +``` + +The element `I + Q` is sent to zero by the Q-letter parity character, +while `Q^{-1} C1` is sent to `-1`. That forbids `m0 x = 1`, so the +`D1 D3` summand cannot vanish. + +The sharp index `m0 = const C1` uses the two monomials +`-Q^{-1} C1 + Q^{-1} C1 Q` and the one monomial +`m2 = Q^{-1} C1 Q^2 C1 Q`. Its fresh image has x0 block `A`, y0 block 0, +y1 block 0, and x1 block the single monomial above. This is an identity +in the predecessor's algebra, not a search over a bounded ansatz. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3 -B scripts/research_package.py --package research/owner-indexed-x1-obstruction --check-only +python3 -B scripts/research_package.py --package research/owner-indexed-x1-obstruction +``` + +Direct replay: + +```sh +python3 -I -W error -B research/owner-indexed-x1-obstruction/verify.py +python3 -I -O -W error -B research/owner-indexed-x1-obstruction/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. + +## 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 the x1-column question in +[research/owner-indexed-y0-clearance](../owner-indexed-y0-clearance/README.md), +which is the remainder of handoff +[discussion comment 19138525](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19138525) +after that package cleared y0 and left the published x1 coefficient in +place. + +Base commit: `17469fff78c22941280f04d39dc5a1faee09c840`. Pins are in +[SOURCES.json](SOURCES.json). The catalogue and selected record are +provenance. `search.py` and `gauge.py` are live inputs. The selected +conditional value is the selected record, `781451/250000000`. + +Overlap at this base used `scripts/find_overlap.py` against a snapshot +fetched on 2026-11-10: local notes at +`17469fff78c22941280f04d39dc5a1faee09c840` (10178 paths, complete +inventory), 317 open-PR records at 08:49:48Z, and 6971 discussion records +at 08:50:49Z. Requiring both phrases `three-term x1` and `owner-indexed` +matches the predecessor package and +[discussion reply 19507118](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19507118), +which ask this question, and no open PR. That search is not a novelty +certificate. Closed PR bodies were not part of that snapshot. + +## Open next questions + +Can one owner-indexed multiplier whose D exponent is not zero cancel +`Q^{-1} C1 Q^2 C1 C3 D1 D3` while keeping `x0 = D1 Q^{-1}`, keeping y0 +zero, and leaving the four final banks stored? The argument here separates +the `D1` and `D1 D3` lines only for a D-exponent-0 factor. The first step +is to add one term of D exponent `(0,-1)` to the sharp index above and +recompute the four columns. This package does not solve that term. + +Does one physical relation omitted by this formal algebra send the +residual word `Q^{-1} C1 Q^2 C1 C3` to zero without collapsing +`Q^{-1} C1`? Nonvanishing is an identity in the predecessor's sufficient +algebra, not a faithful physical impossibility. The first step is to name +one source relation outside `Q^4 = C1^2 = C3^2 = I` and the inherited D +conjugation rule, then reduce only that word. No such relation is imposed +here. + +## Credit + +The trace, algebra, and published row are Cinna Davis's +`research/coded-active-feedback`, using Dugongue's PR4948 chronology, +Dillon's PR4933 code, and the passive ceiling packaged by Chris R / +Clear1nsight. The y0 defect and the constant-index charge are +`research/owner-indexed-y0-clearance`. The declared-family obstruction is +`research/active-feedback-coupling-lock`. The one-edge `C1 Q` row is +`research/active-feedback-outside-edge`. The gauge engine remains the +inherited `research/coded-native-caller/gauge.py`. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. +Apache-2.0. diff --git a/research/owner-indexed-x1-obstruction/SOURCES.json b/research/owner-indexed-x1-obstruction/SOURCES.json new file mode 100644 index 0000000000..8bba455056 --- /dev/null +++ b/research/owner-indexed-x1-obstruction/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/coded-active-feedback/search.py", + "usage": "input", + "git_blob": "60de5a87d3f64fc69e2595cdb2df771c91a0fe6e", + "sha256": "1383010827af29a1b0e595e2c1aa2ffad461b266ffc9f936efce1603ff9f5eb6" + }, + { + "path": "research/coded-native-caller/gauge.py", + "usage": "input", + "git_blob": "44ae72b314cccf677b44d75c374be6dcac1c8167", + "sha256": "390391d291353741c89daea999d483660ca185987ed96a15b82576280c487cad" + } + ] +} diff --git a/research/owner-indexed-x1-obstruction/TASK.json b/research/owner-indexed-x1-obstruction/TASK.json new file mode 100644 index 0000000000..4ab5c13fa4 --- /dev/null +++ b/research/owner-indexed-x1-obstruction/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": "On the published two-edge feed, no owner-indexed D-exponent-0 left map of the four final banks keeps x0 equal to D1 Q^{-1}, keeps y0 zero, and clears the three-term x1 block. Exactly one such index clears the D1 line of x1, and that index leaves the single monomial Q^{-1} C1 Q^2 C1 C3 D1 D3. The four banks stay stored.", + "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 y0 defect, the declared alternating-family lock, or a feedback-edge test. It answers the x1-column question left by research/owner-indexed-y0-clearance, using the same four final banks. Nonzero D exponents, owner mixing, and a new feedback edge stay outside.", + "bottleneck_link": "A productive main job has to be autonomous. An owner-indexed reading can clear y0 and the D1 part of x1, but every D-exponent-0 index that keeps x0 leaves a nonzero D1 D3 monomial in x1, so this feed still does not earn a new kappa.", + "budget_minutes": 60, + "stop_rule": "Stop once every D-exponent-0 owner index that keeps x0 is shown to leave a nonzero x1 D1 D3 component, including the unique index that also clears y0 and the D1 line of x1. Do not search a new feedback edge or a nonzero D exponent.", + "outcome": "negative-result", + "evidence": "PROOF.md and verify.py. The nonvanishing statement is an identity in the predecessor algebra plus the Q-letter parity character. The syllable-length-3 product check is a control, not an enumeration of the multiplier space. No kappa change.", + "author": "unpaidmoon, with substantial Cursor Grok assistance", + "ai_assistance": "Substantial Cursor Grok assistance. No subagents. The predecessor replay and group algebra are imported unchanged.", + "open_questions": [ + { + "question": "Can one owner-indexed multiplier whose D exponent is not zero cancel Q^{-1} C1 Q^2 C1 C3 D1 D3 while keeping x0 equal to D1 Q^{-1}, keeping y0 zero, and leaving the four final banks stored?", + "why_it_matters": "The D-exponent-0 proof separates the D1 line from the D1 D3 line. A coefficient with a nonzero D exponent can move one of those lines, so this obstruction does not forbid every owner-indexed map.", + "first_step": "Start from the unique D-exponent-0 index m0 = const C1, m1 = 0, m2 = Q^{-1} C1 Q^2 C1 Q, m3 = 0, and add one term of D exponent (0,-1) on a single bank. Recompute the four columns and require x0 and y0 to stay fixed.", + "blocked_by": "This package classifies only D-exponent 0. The predecessor excluded nonzero D exponents, and no such term is solved here." + }, + { + "question": "Does one physical relation omitted by this formal algebra send the residual word Q^{-1} C1 Q^2 C1 C3 to zero without collapsing Q^{-1} C1?", + "why_it_matters": "Nonvanishing is proved in the predecessor's sufficient algebra. A quotient that kills only the residual would remove this formal obstruction and would still not be an autonomous caller.", + "first_step": "Name one source relation that is not implied by Q^4 = C1^2 = C3^2 = I together with the inherited D conjugation rule, and reduce only the residual word by that relation.", + "blocked_by": "No further physical relation is imposed here. The predecessor already records that D^4 = I is not part of this algebra." + } + ] +} diff --git a/research/owner-indexed-x1-obstruction/VERIFY.json b/research/owner-indexed-x1-obstruction/VERIFY.json new file mode 100644 index 0000000000..1c634890a3 --- /dev/null +++ b/research/owner-indexed-x1-obstruction/VERIFY.json @@ -0,0 +1,38 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "checks": "Pins, bank polynomials, x1 identity, parity character, sharp residual, and failure controls.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "checks": "Same x1 obstruction under optimization. Checks are explicit failures, not assertions.", + "timeout_seconds": 120 + } + ], + "inputs": [ + "certificates/selected-result.json", + "research/coded-active-feedback/search.py", + "research/coded-native-caller/gauge.py" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/owner-indexed-x1-obstruction/verify.py b/research/owner-indexed-x1-obstruction/verify.py new file mode 100644 index 0000000000..47d6916229 --- /dev/null +++ b/research/owner-indexed-x1-obstruction/verify.py @@ -0,0 +1,301 @@ +#!/usr/bin/env python3 +"""D-exponent-0 owner indexes cannot clear the active-feedback x1 block. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +The predecessor replay and group algebra are imported unchanged. +The syllable product loop is a control. The proof is the identity in PROOF.md. +""" +from hashlib import sha256 +import importlib.util +import json +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +QINV = (-1,) +LONG = (-1, 2, 1, 2) +SHARP_M2 = (-1, 2, 1, 1, 2, 1) +RESIDUAL = (-1, 2, 1, 1, 2, 3) + + +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 q_letter_count(word): + return sum(1 for letter in word if abs(letter) == 1) + + +def phi(element): + total = Fraction(0) + for (word, degree), value in element.items(): + need(degree == (0, 0), "character left the D-exponent-0 line") + sign = -1 if q_letter_count(word) % 2 else 1 + total += value * sign + return total + + +def degree_part(element, degree): + return {key: value for key, value in element.items() if key[1] == degree} + + +def syllable_count(max_syllables): + """Independent count of alternating free-product words, Q then C1 or C3.""" + factors = ("Q", "C1", "C3") + sizes = {"Q": 3, "C1": 1, "C3": 1} + previous = {factor: sizes[factor] for factor in factors} + total = 1 + sum(previous.values()) + for _length in range(2, max_syllables + 1): + current = {} + for factor in factors: + current[factor] = sizes[factor] * sum( + previous[other] for other in factors if other != factor) + total += current[factor] + previous = current + return total + + +def normal_words(algebra, max_syllables): + syllables = { + "Q": ((1,), (1, 1), (-1,)), + "C1": ((2,),), + "C3": ((3,),), + } + found = {(): None} + frontier = [()] + while frontier: + current = frontier + frontier = [] + for word in current: + if syllable_length(word) >= max_syllables: + continue + previous = found[word] + for factor, choices in syllables.items(): + if factor == previous: + continue + for syllable in choices: + produced = algebra.mul(algebra.term(word, (0, 0)), + algebra.term(syllable, (0, 0))) + need(len(produced) == 1, "syllable product left the group") + (new, degree), value = next(iter(produced.items())) + need(degree == (0, 0) and value == 1, "syllable product was not a unit") + if new not in found: + found[new] = factor + frontier.append(new) + return found + + +def syllable_length(word): + count = 0 + previous = None + for letter in word: + factor = "Q" if abs(letter) == 1 else letter + if factor != previous: + count += 1 + previous = factor + return count + + +def support(element): + return {(word, degree): int(value) if value.denominator == 1 else value + for (word, degree), value in element.items()} + + +def main(): + pinned = { + "research/coded-active-feedback/search.py": + "1383010827af29a1b0e595e2c1aa2ffad461b266ffc9f936efce1603ff9f5eb6", + "research/coded-native-caller/gauge.py": + "390391d291353741c89daea999d483660ca185987ed96a15b82576280c487cad", + "certificates/selected-result.json": + "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + } + for name, digest in pinned.items(): + need(sha256((ROOT / name).read_bytes()).hexdigest() == digest, "changed pin " + name) + selected = json.loads((ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")) + need(selected["kappa"] == "781451/250000000", "selected frontier value moved") + + search = load_search() + algebra = search.algebra() + q, c1, c3 = algebra.gen(1), algebra.gen(2), algebra.gen(3) + qinv, d1, d3 = algebra.inv(q), algebra.D(0), algebra.D(1) + observed, _targets, rows = search.replay(algebra, algebra.one, algebra.mul(c1, q, q)) + need(len(observed) == 39, "saved-bank count moved") + left = [row for label, row in observed if label.startswith("left:")] + need(left == rows, "final rows are not the left endpoint banks") + stored = tuple(tuple(tuple(sorted(entry.items())) for entry in row) for row in rows) + + blank = {} + bank0 = [ + algebra.add(algebra.term((-1, 2), (1, 0)), algebra.term((1, 1, 2), (1, 0))), + algebra.term((-1,), (1, 0)), + algebra.term((1, 1, 2), (1, 0), -1), + blank, + ] + bank1 = [blank, algebra.term((2, 1), (1, 0)), blank, blank] + const = algebra.add(algebra.term(QINV, (0, 0), -1), algebra.term(LONG, (0, 0))) + mono = algebra.term((-1, 3), (1, 1)) + bank2 = [ + algebra.term(QINV, (1, 0)), + algebra.add(algebra.term((-1, 2, 1), (1, 0)), + algebra.term((-1, 2, 1, 1), (1, 0), -1)), + algebra.add(algebra.mul(const, d1), mono), + blank, + ] + bank3 = [ + algebra.term((3, -1, 2), (1, 1)), + algebra.term((3,), (1, 1)), + algebra.add(algebra.term((), (1, 1), -1), + algebra.term((3, -1, 2), (1, 1), -1), + algebra.term((3, 2), (1, 1))), + algebra.term((3, 1), (1, 1)), + ] + need(rows == [bank0, bank1, bank2, bank3], "final banks moved") + need(len(bank2[2]) == 3, "published x1 block lost a monomial") + need(bank2[2] != blank, "published x1 block was already zero") + + one_plus_q = algebra.add(algebra.one, q) + x = algebra.mul(algebra.mul(q, q), one_plus_q, c1, q) + need(algebra.mul(rows[0][0], algebra.inv(rows[2][0])) == x, "x is not Q^2(I+Q)C1 Q") + need(algebra.add(qinv, algebra.mul(q, q)) == algebra.mul(algebra.mul(q, q), one_plus_q), + "Q^{-1}+Q^2 did not factor") + need(rows[0][0] == algebra.mul(x, rows[2][0]), "bank0 x0 is not x A") + factored_const = algebra.mul(qinv, algebra.add(algebra.mul(c1, q, c1), algebra.neg(algebra.one))) + need(factored_const == const, "const factorisation moved") + g = algebra.mul(qinv, c3) + ginv = algebra.mul(c3, q) + need(g == algebra.term((-1, 3), (0, 0)), "Q^{-1} C3 normal form moved") + need(algebra.mul(g, ginv) == algebra.one and algebra.mul(ginv, g) == algebra.one, + "Q^{-1} C3 is not a unit") + need(algebra.mul(c1, c1) == algebra.one, "C1 is not an involution") + bank3_inverse = algebra.inv(rows[3][0]) + need(algebra.mul(bank3_inverse, rows[3][0]) == algebra.one + and algebra.mul(rows[3][0], bank3_inverse) == algebra.one, + "bank3 x0 monomial is not a unit") + a_inverse = algebra.inv(rows[2][0]) + need(algebra.mul(a_inverse, rows[2][0]) == algebra.one + and algebra.mul(rows[2][0], a_inverse) == algebra.one, + "A is not a unit") + + linear = algebra.add(rows[0][2], algebra.neg(algebra.mul(x, rows[2][2]))) + need(linear == algebra.add(algebra.mul(algebra.neg(c1), d1), algebra.neg(algebra.mul(x, mono))), + "x1 linear coefficient moved") + y0_constant = algebra.add(rows[2][1], algebra.mul(const, rows[1][1])) + y0_linear = algebra.add(rows[0][1], algebra.neg(algebra.mul(c1, rows[1][1])), + algebra.neg(algebra.mul(x, rows[2][1]))) + need(y0_constant == blank and y0_linear == blank, "y0 identity does not cover every m0") + + # Character. Reducer steps used by the homomorphism argument. + need(search.reduce_word((1, 1, 1, 1)) == (), "Q^4 did not reduce to I") + need(search.reduce_word((2, 2)) == () and search.reduce_word((3, 3)) == (), + "a code square did not reduce to I") + cascade = (1, 1, 3, 3, -1) + need(search.reduce_word(cascade) == (1,), "exposed Q run did not collapse") + need(q_letter_count(cascade) % 2 == q_letter_count(search.reduce_word(cascade)) % 2, + "Q-run collapse changed character parity") + for exponent in range(8): + raw = (1,) * exponent + reduced = search.reduce_word(raw) + need(q_letter_count(raw) % 2 == q_letter_count(reduced) % 2, + "Q normal form changed character parity") + need(phi(one_plus_q) == 0, "I+Q was not in the character kernel") + need(phi(algebra.mul(qinv, c1)) == -1, "Q^{-1} C1 lost its character") + need(algebra.mul(qinv, c1) == algebra.term((-1, 2), (0, 0)), "Q^{-1} C1 normal form moved") + + # Finite control: every normal word of at most three syllables, counted + # independently of the reducer. This does not enumerate the theorem. + words = normal_words(algebra, 3) + need(len(words) == syllable_count(3) == 64, "three-syllable normal forms are incomplete") + for left in words: + for right in words: + product = algebra.mul(algebra.term(left, (0, 0)), algebra.term(right, (0, 0))) + need(phi(product) == phi(algebra.term(left, (0, 0))) * phi(algebra.term(right, (0, 0))), + "character failed on a three-syllable product") + need(phi(algebra.mul(algebra.term(left, (0, 0)), one_plus_q)) == 0, + "a three-syllable word met the forbidden right-hand side") + + samples = [ + {}, + algebra.one, + algebra.term((2, 3, 1, 1), (0, 0), 1), + algebra.add(algebra.term((3,), (0, 0), 2), algebra.term((1, 2, -1), (0, 0), -3)), + algebra.mul(algebra.neg(qinv), c1), + algebra.term((2, 1, 3, 1, 1, 2, -1, 3), (0, 0), 5), + ] + for m0 in samples: + m2 = algebra.add(algebra.one, algebra.neg(algebra.mul(m0, x))) + m1 = algebra.add(const, algebra.neg(algebra.mul(m0, c1))) + image = [algebra.add(algebra.mul(m0, rows[0][column]), + algebra.mul(m1, rows[1][column]), + algebra.mul(m2, rows[2][column])) + for column in range(4)] + need(image[0] == rows[2][0] and image[1] == blank and image[3] == blank, + "sample index failed to keep x0 and clear y0 and y1") + d1_line = algebra.mul(algebra.add(const, algebra.neg(algebra.mul(m0, c1))), d1) + d3_line = algebra.mul(m2, mono) + need(image[2] == algebra.add(d1_line, d3_line), "sample x1 left the proved shape") + need(d3_line, "sample D1 D3 summand vanished") + need(phi(algebra.mul(m0, algebra.mul(algebra.mul(q, q), one_plus_q))) == 0, + "sample met the forbidden equation in the character") + + # Unique index that clears the D1 line. It still keeps y0 zero. + sharp_m0 = algebra.mul(const, c1) + need(support(sharp_m0) == {((-1, 2), (0, 0)): -1, ((-1, 2, 1), (0, 0)): 1}, + "sharp m0 support moved") + left = algebra.mul(algebra.neg(qinv), c1) + right_a = algebra.mul(qinv, c1, q) + right_b = algebra.mul(q, q, c1, q) + term1 = algebra.mul(left, right_a) + term2 = algebra.mul(left, right_b) + term3 = algebra.mul(right_a, right_a) + term4 = algebra.mul(right_a, right_b) + need(term3 == algebra.one, "third sharp product is not I") + need(algebra.add(term1, term4) == blank, "first and fourth sharp products did not cancel") + sharp_m2 = algebra.add(algebra.one, algebra.neg(algebra.add(term1, term2, term3, term4))) + need(sharp_m2 == algebra.add(algebra.one, algebra.neg(algebra.mul(sharp_m0, x))), + "four-term expansion is not m0 x") + need(sharp_m2 == algebra.term(SHARP_M2, (0, 0)), "sharp m2 is not one monomial") + sharp_m1 = algebra.add(const, algebra.neg(algebra.mul(sharp_m0, c1))) + need(sharp_m1 == blank, "clearing the D1 line reopened the y0 multiplier") + fresh = [algebra.add(algebra.mul(sharp_m0, rows[0][column]), + algebra.mul(sharp_m2, rows[2][column])) + for column in range(4)] + residual = algebra.term(RESIDUAL, (1, 1)) + need(fresh[0] == rows[2][0] and fresh[1] == blank and fresh[3] == blank, + "sharp image did not keep x0 and clear y0 and y1") + need(fresh[2] == residual and fresh[2] != blank, "sharp x1 is not the forced monomial") + need(fresh[2] != rows[2][2], "sharp index failed to change the three-term block") + need(degree_part(fresh[2], (1, 0)) == blank, "sharp index left a D1 term") + need(len(fresh[2]) == 1, "sharp residual is not a single monomial") + + # Failure controls. Reopening a hypothesis, or dropping a monomial, is not a solution. + constant = [algebra.add(rows[2][column], algebra.mul(const, rows[1][column])) for column in range(4)] + need(constant[0] == rows[2][0] and constant[1] == blank and constant[2] == rows[2][2], + "constant index no longer reproduces the unpaid three-term block") + spoiled = [algebra.add(rows[2][column], rows[3][column]) for column in range(4)] + need(spoiled[0] != rows[2][0], "a nonzero bank-3 coefficient kept x0") + partial = {key: value for key, value in sharp_m0.items() if key[0] != (-1, 2)} + partial_image = algebra.add(algebra.mul(partial, rows[0][2]), algebra.mul(sharp_m2, rows[2][2])) + need(degree_part(partial_image, (1, 0)), "dropping one sharp monomial still cleared the D1 line") + need(tuple(stored) == tuple(tuple(tuple(sorted(entry.items())) for entry in row) for row in rows), + "stored endpoint banks were overwritten") + + print("PASS_OWNER_INDEXED_X1_OBSTRUCTION") + print("evidence_class", "proof") + print("residual", "Q^{-1} C1 Q^2 C1 C3 D1 D3") + print("x1_terms_at_sharp_index", len(fresh[2])) + print("new_kappa", None) + + +if __name__ == "__main__": + main()