diff --git a/research/stage-zero-forced-translation/README.md b/research/stage-zero-forced-translation/README.md new file mode 100644 index 0000000000..190333ccb2 --- /dev/null +++ b/research/stage-zero-forced-translation/README.md @@ -0,0 +1,72 @@ +# Independent check of #4464: stage-zero commutation, and the translation is forced + +**Claim type:** an independent exact check plus a closed form. **No new κ.** It covers mihir-s-05's +[#4464](https://github.com/CrocSwap/integer-mult-bounds/pull/4464) (head `82c7db42`). That PR answers +open question 1 of Matarener's #4457: does the actual complex caller satisfy `[D0, Q] = 0`? + +## Setting + +For `a ∈ F₂⁹`, write `T_a e_x = e_{x⊕a}` and `C_a = ((1+i)I + (1−i)T_a)/2`. The character of +`C_a` is `i^{a·ξ}`. The stage-zero operator is `D0 = F9·Q^{−1}`, with `F9 = Π_j C_{2^j}` and +`Q = C_q`. At each port the source records a complement `B = (b_1..b_8)` of `q` and a translation +`t` (`translation_after` in `DATA-PHASES.json`). + +## What is checked, with separately written code + +1. **Orthonormality.** `{q, b_1, …, b_8}` is an orthonormal basis of `F₂⁹`. So `M = [q; B]` is + orthogonal over `F₂`, and every column count `c_i` is odd. +2. **The character identity.** `|ξ| − q·ξ ≡ Σ_j b_j·ξ + 2·t·ξ (mod 4)` holds for all 512 characters + at every port. That is, `D0 = T_t·G_B` with `G_B = Π C_{b_j}`. Dropping `t` changes every + character with `t·ξ` odd. +3. **New: the translation is forced, in closed form.** Evaluating the identity at `ξ = e_i` gives + `1 − c_i ≡ 2t_i (mod 4)`, so + + t_i = [c_i ≡ 3 (mod 4)]. + + This closed form equals the recorded `translation_after` at **all 112 ports**. The translation + is therefore determined by `q` and `B`; it is not a free choice. That explains #4464's observation + that every rank-eight normalization needs its nonzero translation. For example, at port 0 the + first four columns of `M` have count 3, so `t = 15`. +4. **Commutation.** `[D0, Q] = 0`, checked by exact XOR convolution of kernels in `ℚ(i)` at port 0 + and at the first weight-7 port. Each `D0` kernel has 256 entries of modulus `1/16`. +5. **The port-0 witness.** `(D0 − G_B)[0, 0] = −1/16` exactly, by independent Fourier inversion, at + `q = 11`, `B = [13,14,7,16,32,64,128,256]`, `t = 15`. +6. **New: every idle normalization is forced.** Apply the same closed form, prepending `q` when a + frame meets the nine port bits. It reproduces `translation_after` for **all 2,016 non-empty + recorded idle normalizations**: ranks 8, 16, 32 and 48, across 20 entries per port, with 224 empty + entries skipped. The orthonormality of each frame is checked as well. +7. **Profiles.** `q` has weight 3 at 77 ports and weight 7 at 35. `t` has weight 4 at 77 ports and + weight 8 at 35. Both match #4464. + +## Not covered + +- #4464's binding to `P3-NATIVE-COVER.json.gz`, the THREE-base canonical word, and the #4440 + controller. This check reads only `DATA-PHASES.json`. +- Native realization, rounded implementation, BIT, and cost accounting. +- Any new κ. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/stage-zero-forced-translation --check-only +python3.12 -B scripts/research_package.py --package research/stage-zero-forced-translation +``` + +The verifier prints `PASS_STAGE_ZERO_FORCED_TRANSLATION` in about a second, using only the standard +library. + +## Open next questions + +1. **Can the native caller compute translations from the closed form instead of storing them?** + - *Why it matters:* item 6 shows that every recorded translation is determined by its frame. A + derived value removes one class of transcription error. + - *First step:* replace the stored field by the formula in a copy of the phase emitter, and diff + the outputs. + +## Credit + +- The audit and the question are mihir-s-05's (#4464) and Matarener's (#4457). +- The phase data come from the retained QQ16/native phase lineage recorded in #4464. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/stage-zero-forced-translation/SOURCES.json b/research/stage-zero-forced-translation/SOURCES.json new file mode 100644 index 0000000000..ad397ce759 --- /dev/null +++ b/research/stage-zero-forced-translation/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + } + ] +} diff --git a/research/stage-zero-forced-translation/TASK.json b/research/stage-zero-forced-translation/TASK.json new file mode 100644 index 0000000000..c6ef1c5db5 --- /dev/null +++ b/research/stage-zero-forced-translation/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Independent check of #4464's stage-zero commutation, plus a closed form showing the recorded translation is forced by q and B.", + "scope_change_reason": "Independent check of a fresh PR answering #4457's open question.", + "bottleneck_link": "Side result: independent support for one controller premise of the kappa ~0.003 claims.", + "budget_minutes": 30, + "stop_rule": "Stop at DATA-PHASES-level checks.", + "outcome": "completed", + "evidence": "112/112 ports: orthonormal basis, character identity, forced translation t_i=[c_i=3 mod 4] equals recorded translation_after; exact commutator zero at two ports; port-0 witness -1/16. The closed form also reproduces all 2,016 nonempty recorded idle-normalization translations.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Can the native caller compute translations from the closed form instead of storing them?", + "why_it_matters": "Removes a class of transcription error.", + "first_step": "Replace the stored field by the formula in a copy of the phase emitter and diff.", + "blocked_by": "None." + } + ] +} diff --git a/research/stage-zero-forced-translation/VERIFY.json b/research/stage-zero-forced-translation/VERIFY.json new file mode 100644 index 0000000000..c61ffecacf --- /dev/null +++ b/research/stage-zero-forced-translation/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 112 ports of DATA-PHASES.json: orthonormal [q;B], mod-4 character identity D0 = T_t G_B for all 512 characters, closed form t_i = [c_i = 3 mod 4] equals recorded translation_after, exact [D0,Q]=0 kernels at two ports, port-0 witness -1/16, weight profiles. Closed form also reproduces all 2,016 nonempty idle-normalization translations." + } + ] +} diff --git a/research/stage-zero-forced-translation/verify.py b/research/stage-zero-forced-translation/verify.py new file mode 100644 index 0000000000..23a9df5543 --- /dev/null +++ b/research/stage-zero-forced-translation/verify.py @@ -0,0 +1,128 @@ +#!/usr/bin/env python3 +"""Independent check of #4464: stage-zero commutation and the forced translation, all 112 ports. + +For a in F_2^9, T_a e_x = e_(x xor a) and C_a = ((1+i)I + (1-i)T_a)/2, with Fourier character i^(a.xi mod 2). +D0 = F9 Q^-1 with F9 = prod_j C_(2^j), Q = C_q. For the recorded complement B = (b_1..b_8) of q and translation t: + (1) {q, b_1..b_8} is an orthonormal basis of F_2^9, so M = [q; B] is orthogonal and every column count c_i is odd; + (2) the character identity |xi| - q.xi == sum_j b_j.xi + 2 t.xi (mod 4) holds for all 512 xi, i.e. D0 = T_t G_B; + (3) closed form: evaluating (2) at xi = e_i forces t_i = [c_i == 3 (mod 4)]; this equals the recorded + translation_after at every port (so the translation is determined by q and B, never optional); + (4) [D0, Q] = 0 by an exact XOR convolution in Q(i) (kernels as dicts of Gaussian rationals); + (5) port-0 witness: (D0 - G_B)[0, 0] = -1/16 by Fourier inversion; + (6) the same closed form (with q prepended when a frame meets the nine port bits) reproduces translation_after for + every one of the 2,016 nonempty recorded idle normalizations (224 empty ones are skipped). +Independent code reading the pinned DATA-PHASES.json only. Ryanson Jonathan with Claude Code (Claude Opus 5.5) +assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PHASES = "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json" +N = 512 +I4 = [(1, 0), (0, 1), (-1, 0), (0, -1)] # i^k as (re, im) + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def dot(a, b): + return bin(a & b).count("1") & 1 + + +def kernel_from_char(char): + """char[xi] in Z/4 -> exact kernel K[x] = (1/512) sum_xi i^char(xi) (-1)^(xi.x), as (F re, F im)""" + K = {} + for x in range(N): + re = im = 0 + for xi in range(N): + s = -1 if dot(xi, x) else 1 + a, b = I4[char[xi] % 4] + re += s * a + im += s * b + if re or im: + K[x] = (F(re, N), F(im, N)) + return K + + +def conv(A, B): + out = {} + for x, (ar, ai) in A.items(): + for y, (br, bi) in B.items(): + z = x ^ y + r, i = out.get(z, (0, 0)) + out[z] = (r + ar * br - ai * bi, i + ar * bi + ai * br) + return {k: v for k, v in out.items() if v != (0, 0)} + + +def main(): + for row in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"]: + need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], row["path"]) + recipes = sorted(json.loads((ROOT / PHASES).read_text(encoding="utf-8"))["recipes"], key=lambda r: r["port"]) + need([r["port"] for r in recipes] == list(range(112)), "112 ports") + qw, tw, forced_equal = Counter(), Counter(), 0 + for rec in recipes: + q = rec["q"] + child = rec["idle_children"][0] + B, t = child["orthogonal_axes"][:8], child["translation_after"] + need(child["orthogonal_axes"][8:] == [1 << i for i in range(9, 17)], "remaining axes are D1's fresh axes") + rows = [q] + B + need(all(0 < r < N for r in rows) and 0 <= t < N, "nine-bit support") + need(all(dot(a, b) == int(i == j) for i, a in enumerate(rows) for j, b in enumerate(rows)), "(1) orthonormal") + c = [sum(r >> i & 1 for r in rows) for i in range(9)] + need(all(ci % 2 == 1 for ci in c), "(1) odd column counts") + forced = sum(1 << i for i in range(9) if c[i] % 4 == 3) + need(forced == t, f"(3) port {rec['port']}: recorded translation is the forced one") + forced_equal += 1 + need(t != 0, "translation nonzero") + for xi in range(N): + lhs = (bin(xi).count("1") - dot(q, xi)) % 4 + rhs = (sum(dot(b, xi) for b in B) + 2 * dot(t, xi)) % 4 + need(lhs == rhs, "(2) character identity") + if dot(t, xi): + need(lhs != sum(dot(b, xi) for b in B) % 4, "dropping t changes this character") + qw[bin(q).count("1")] += 1 + tw[bin(t).count("1")] += 1 + all_idle = 0 + for rec in recipes: + for ch in rec["idle_children"]: + ax = ch["orthogonal_axes"] + if not ax: + continue + rows = ([rec["q"]] if any(a & (N - 1) for a in ax) else []) + ax + need(all(dot(a, b) == int(i == j) for i, a in enumerate(rows) for j, b in enumerate(rows)), "(6) orthonormal") + width = max(x.bit_length() for x in rows) + cnt = [sum(x >> i & 1 for x in rows) for i in range(width)] + need(sum(1 << i for i in range(width) if cnt[i] % 4 == 3) == ch["translation_after"], "(6) forced translation") + all_idle += 1 + need(all_idle == 2016, "(6) all 2,016 nonempty idle normalizations") + need(qw == Counter({3: 77, 7: 35}) and tw == Counter({4: 77, 8: 35}), "weight profiles") + # (4), (5) exact kernels at port 0 and at the first weight-7 port + witness = None + for rec in (recipes[0], next(r for r in recipes if bin(r["q"]).count("1") == 7)): + q, B = rec["q"], rec["idle_children"][0]["orthogonal_axes"][:8] + t = rec["idle_children"][0]["translation_after"] + D0 = kernel_from_char([(bin(xi).count("1") - dot(q, xi)) % 4 for xi in range(N)]) + Qk = kernel_from_char([dot(q, xi) for xi in range(N)]) + GB = kernel_from_char([sum(dot(b, xi) for b in B) % 4 for xi in range(N)]) + need(conv(D0, Qk) == conv(Qk, D0), "(4) [D0, Q] = 0") + need(len(D0) == 256 and all(r * r + i * i == F(1, 256) for r, i in D0.values()), "256 entries of modulus 1/16") + diff = D0.get(0, (0, 0))[0] - GB.get(0, (0, 0))[0], D0.get(0, (0, 0))[1] - GB.get(0, (0, 0))[1] + if rec["port"] == 0: + need(diff == (F(-1, 16), 0) and t == 15 and q == 11, "(5) port-0 witness -1/16") + witness = {"q": q, "B": B, "t": t, "entry_00_of_D0_minus_GB": str(diff[0])} + print(json.dumps({"status": "PASS_STAGE_ZERO_FORCED_TRANSLATION", "ports": 112, + "forced_translation_matches_recorded": forced_equal, + "all_idle_normalizations_forced": all_idle, "q_weights": dict(qw), + "t_weights": dict(tw), "port0_witness": witness, "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())