diff --git a/research/p104-allwidth-native-certificate/PROOF.md b/research/p104-allwidth-native-certificate/PROOF.md new file mode 100644 index 0000000000..5dc3c1166d --- /dev/null +++ b/research/p104-allwidth-native-certificate/PROOF.md @@ -0,0 +1,139 @@ +# The native layer of the selected #5599 word at every column multiplicity + +Prepared by Mark (Matarener) with substantial Claude Code assistance. Apache-2.0. +No new κ. Assumption ID: `native_all_columns`. This is one quantified implication at the +actual selected caller, not the whole assumption and not the other four. + +## 1. Setting and conventions + +Selected word: `research/p104-helper-subspace-splits/WORD.json.gz` (PR #5599, Ali Romman, +κ = 62009/20000000), on canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`. +It has 25,475 events on 748 public rows over 1,089 binary frames on nine axes; 3,447 of the +events are paid chart changes `MOVE r a b`, moving row `r` from frame `a` to frame `b`, with +2,887 distinct ordered pairs `(a,b)`. A frame `W` is a list of `r = |W|` independent binary +vectors on the nine axes. + +The retained physical semantics (the selected review, #5442, #5837, #5894; `p104-native-channel/PROOF.md` §2): +a register at frame `W` with logical coordinates `u` holds the physical vector +`Γ_W^{(⊗)f} u` at column multiplicity `f ≥ 1`, where `Γ_W` is the canonical chart of `W`. +Scalar coefficients stay outside the tensor power (#5837). A paid chart change from `a` to `b` +is the operator `Γ_b Γ_a^{-1}`, which the compiler lowers to a Gaussian monomial `R`, a child +`F_r = C_{e_0} ⋯ C_{e_{r-1}}` of rank `r`, and a Gaussian monomial `L`; the recipe is `L F_r R`. + +Primitive definitions used by the dense engine (`dense.py`), on the basis `|x>`, `x ∈ {0,…,511}`: + +```text +P(G) |x> ↦ |Gx> (G an invertible binary matrix, rows G_i) +X(b) |x> ↦ |x ⊕ b> +D(Q,α) |x> ↦ i^{q(x)} |x>, q(x) = Σ_{i∈x} α_i + 2 Σ_{i dim initial`. For the +adapters, `is_monomial` requires denominator zero and exactly one entry from `{±1, ±i}` per +column. + +**(4).** The verifier hashes `[[a,b,recipe]] + adapters` exactly as the selected `local.native` +does and compares with the registered digest. So the operators certified here are the ones +the selected package registered, not a fresh compilation that might differ. + +**(5)** is the record lemma of `research/selected-monomial-tape-lift/PROOF.md`, executed on +this word's factors: the record list of a monomial is built by Gaussian elimination of `G` +(`XROW` row additions and three-`XROW` swaps), translations `NOT` for `b`, unit phases `S` +for `α`, controlled signs `CZ` for the off-diagonal of `Q`, and `I` for the global phase; +each record acts on all `f` columns at once and reads no spectator. The verifier executes +every distinct factor's list on all 512 addresses at `f = 1` and on sampled addresses at +`f = 2, 3`, comparing with the lift formula +`|X> ↦ i^{p f + Σ_j q(x_j)} |(G x_1 ⊕ b, …, G x_f ⊕ b)>`. + +**Corollary.** Equal operators have equal tensor powers, and the mixed-product identity +`(AB)^{(⊗)f} = A^{(⊗)f} B^{(⊗)f}` factors the power of the recipe gate by gate +(#5442, Lemma, "group identities lift"). The direction that matters is the easy one: a +width-one identity between *products of primitives* lifts. What does **not** lift is a +width-one *linear relation with fixed external coefficients*: the verifier checks on the +first MOVE (event 9589, frame `[]` → `[11]`, active axes 0, 1, 3) that +`U = ((1+i) I + (1−i) X_{11} Z_3)/2` (the closed form of #5894) satisfies +`U^{(⊗)f} = L^{(⊗)f} C^{(⊗)f} R^{(⊗)f}` at `f = 2, 3`, while +`((1+i) I^{(⊗)f} + (1−i) (X_{11} Z_3)^{(⊗)f})/2 ≠ U^{(⊗)f}`. This is why the physical word +must execute the three factors (two record lists and one rank-one child), never the two-term +closed form, and it is the same Reynolds-type trap recorded in #5442's controls. ∎ + +## 4. What this does and does not discharge + +Discharged for the selected word, at every `f ≥ 1`: the algebraic content of +`native_all_columns` (every paid chart change, helper normalizer and main adapter is the +tensor power of an exact group element that the physical word realizes factor by factor), +with the paid ranks of the invoice, by independent dense verification; and the record-level +realization of all monomial factors. + +Still inherited: the tariff of each record (the compact-control Proposition, in its domain +`f ≤ p`), the front/back control-field reservations of the actual #5599 caller layout for every +active slot pair, spectator handling of the rank-`r` children, whole-job adapters of the +physical caller, and the four assumptions `owned_erasure`, `compiler`, `precision_tape`, +`analytic_recovery`. No selected value, outer row or κ changes. + +## 5. Credit + +Ali Romman (#5599 word, invoice and `local.native` registration; #5565 base via Pierre-Loic +Doulcet / hexapode), Chris R / Clear1nsight (independent signed-Pauli/state interpreter lineage, +`native_verify.py`), unpaidmoon (#5837, scalar lift and the precise MOVE question), DLamdata +(#5894, coverage trace and the closed form of event 9589), zxv (#5428 target), Dugongue and +icekylinx (Clifford engine lineage), Cinna Davis (compact-control notes), and the retained +native, compiler and controller lineage credited in `research/p104-helper-subspace-splits/README.md`. +The lifting lemma and record grammar are #5442 and #5445 (Matarener). No independent human or +proof-kernel review. diff --git a/research/p104-allwidth-native-certificate/README.md b/research/p104-allwidth-native-certificate/README.md new file mode 100644 index 0000000000..72e6cc6857 --- /dev/null +++ b/research/p104-allwidth-native-certificate/README.md @@ -0,0 +1,79 @@ +# All-width native certificate for the selected #5599 word + +**Scoped positive result; no new κ.** Assumption ID `native_all_columns`, card +`uniform-transfer-audit`. The complete native layer of the selected P104 word +([PR #5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599), κ = 62009/20000000) +is certified at every column multiplicity `f ≥ 1`, by an independent method: + +- all **2,887 distinct paid chart changes** `Γ_b Γ_a^{-1}`, the **540 helper normalizer pairs** + (2,923 distinct maps) and the **208 main adapters** equal their compiler-lowered recipes + (Gaussian monomial · rank-`r` Fourier child · Gaussian monomial) **entry by entry on dense + 512 × 512 exact matrices, including the absolute phase**; +- the operator's column support `2^r` gives `r = |dim b − dim a|`, the paid rank the invoice + charges (rank mass 6,014 over 3,447 occurrences); helpers are strictly productive with the + author's profile; +- the certified recipes are **byte-identical to the author's registered payload** + (`RESULT.json` `native.recipe_payload_sha256`); +- every **distinct Gaussian monomial factor** is realized as a fixed `f`-independent list of + `XROW`/`NOT`/`S`/`CZ`/`I` records (#5445 grammar), executed exhaustively at `f = 1` and + sampled at `f = 2, 3`; +- the lift to every `f` is the factorwise tensor power (#5442 lemma); the verifier shows on the + first MOVE (event 9589, `U = ((1+i)I + (1−i)X_11 Z_3)/2`) that the factorwise lift equals + `U^{(⊗)f}` at `f = 2, 3` while the termwise lift of the two-term closed form does not. + +[PROOF.md](PROOF.md) states the proposition, the dense method and the corollary. +[TASK.json](TASK.json) records the refined scope and the open physical questions. + +## Why a second census + +[#5837](https://github.com/CrocSwap/integer-mult-bounds/pull/5837) (unpaidmoon) proved the +scalar instructions of this word lift and asked whether its 3,447 MOVEs lift as group identities. +[#5894](https://github.com/CrocSwap/integer-mult-bounds/pull/5894) (DLamdata) traced that the +selected checker already compares signed Pauli images and the exact `|0>` column for every +distinct pair, replayed **one** pair independently, and wrote that a fresh census should be +justified as independent verification of existing coverage. This package is that verification, +for all 2,923 maps and 208 adapters, by a method that shares nothing with the selected checker: +no tableau, no sparse state column, no compiler semantics; full dense matrices, one exact matrix +product per pair, and column supports instead of the symplectic `X`-block for the rank. The +compiler supplies only the candidate recipe, and the payload hash binds those candidates to the +registered ones. The #5442 algebraic certificate covered the older #5413 caller; this is the +same certificate for the current selected caller, plus the #5445 record lists of its factors. + +## Reproduce + +Python 3.12 with NumPy 2.3.5 (`python3 -m pip install numpy==2.3.5`), from the repository root: + +```sh +python3 -I -B research/p104-allwidth-native-certificate/verify.py +python3 -I -B research/p104-allwidth-native-certificate/test_verify.py +python3 -B scripts/research_package.py --package research/p104-allwidth-native-certificate --install-deps +``` + +`verify.py` prints progress lines and ends with + +```text +PASS_P104_ALLWIDTH_NATIVE_CERTIFICATE pairs=2887 distinct_maps=2923 helpers=540 adapters=208 monomials=3711 frames=1089 +``` + +and compares the rebuilt summary with [RESULT.json](RESULT.json) (about five minutes with four worker +processes, one BLAS thread each). The 3,711 distinct monomial factors need at most 96 records each (72 `XROW`), +under the 171-record grammar bound. `test_verify.py` runs ten rejecting controls in about a second. The NumPy +arrays hold only Gaussian integers far below `2^53`, so every product and comparison is exact; +`dense.py` asserts integrality and a `2^40` bound after every step. + +## Open next questions + +1. Place these record lists and the rank-`r` children in the actual #5599 caller layout with + the compact-control front/back field reservations for every active slot pair, at the retained + tariff, starting with event 9589. That is the physical half of `native_all_columns` for the + current caller. +2. Execute the compact-control rotation scheme itself bit by bit at small `f, K, G` (the + guard core is audited by seed71/seed73/carry-repair/seed29; the complete scheme with chunk + swaps is not executed). + +## Not claimed + +No new κ, no selected-record change, no physical tape implementation, no claim on +`owned_erasure`, `compiler`, `precision_tape` or `analytic_recovery`, no independent human or +proof-kernel review. Credit is in PROOF.md §5. Prepared by Mark (Matarener) with substantial +Claude Code assistance. Apache-2.0. diff --git a/research/p104-allwidth-native-certificate/RESULT.json b/research/p104-allwidth-native-certificate/RESULT.json new file mode 100644 index 0000000000..59a0cdcbe0 --- /dev/null +++ b/research/p104-allwidth-native-certificate/RESULT.json @@ -0,0 +1,182 @@ +{ + "status": "PASS_P104_ALLWIDTH_NATIVE_CERTIFICATE", + "selected_kappa": "62009/20000000", + "word": { + "events": 25475, + "frames": 1089, + "public": 748, + "live_ports": 104, + "helpers": 540, + "move_occurrences": 3447, + "paid_rank_histogram": { + "1": 2203, + "2": 459, + "3": 493, + "4": 92, + "5": 168, + "6": 18, + "7": 14 + }, + "paid_rank_mass": 6014 + }, + "frames_unitary": 1089, + "chart_changes": { + "distinct_move_pairs": 2887, + "rank_histogram": { + "1": 1821, + "2": 380, + "3": 490, + "4": 92, + "5": 72, + "6": 18, + "7": 14 + }, + "helper_pairs": 540, + "helper_rank_profile": { + "1": 2, + "2": 5, + "4": 89, + "5": 11, + "7": 5, + "8": 16, + "9": 412 + }, + "distinct_maps": 2923, + "main_adapters": 208, + "recipe_payload_sha256": "b2e6b538f6152ccf0024ca57381e46b2fe6b75b89504d935009dade234cc3f18" + }, + "tensor_control": { + "event": 9589, + "frames": [ + 3, + 0 + ], + "closed_form_axes": [ + 0, + 1, + 3 + ], + "factor_axes": [ + 0, + 1, + 2, + 3 + ], + "factorwise_lift_width_2": "equal", + "termwise_closed_form_lift_widths_2_3": "differs" + }, + "monomial_factors": { + "distinct": 3711, + "max_records": { + "XROW": 72, + "NOT": 9, + "S": 22, + "CZ": 24, + "I": 3, + "movement_records": 72, + "phase_records": 42, + "total": 96 + }, + "sum_records": { + "XROW": 94289, + "NOT": 5598, + "S": 27489, + "CZ": 14443, + "I": 2950, + "movement_records": 99887, + "phase_records": 44882, + "total": 144769 + }, + "histogram_total": { + "8": 142, + "10": 2, + "11": 5, + "12": 38, + "13": 1, + "14": 9, + "15": 8, + "16": 4, + "17": 13, + "18": 22, + "19": 14, + "20": 32, + "21": 44, + "22": 13, + "23": 46, + "24": 86, + "25": 48, + "26": 65, + "27": 134, + "28": 62, + "29": 63, + "30": 165, + "31": 133, + "32": 114, + "33": 153, + "34": 119, + "35": 113, + "36": 122, + "37": 96, + "38": 100, + "39": 103, + "40": 83, + "41": 78, + "42": 83, + "43": 81, + "44": 66, + "45": 75, + "46": 64, + "47": 43, + "48": 90, + "49": 68, + "50": 82, + "51": 85, + "52": 44, + "53": 68, + "54": 61, + "55": 46, + "56": 70, + "57": 31, + "58": 35, + "59": 63, + "60": 62, + "61": 43, + "62": 31, + "63": 27, + "64": 21, + "65": 29, + "66": 11, + "67": 14, + "68": 11, + "69": 13, + "70": 9, + "71": 6, + "72": 8, + "73": 5, + "74": 6, + "75": 5, + "76": 6, + "77": 2, + "78": 3, + "79": 3, + "80": 2, + "84": 3, + "87": 1, + "88": 1, + "89": 1, + "90": 2, + "96": 1 + }, + "bound_s2": 171, + "checks": { + "f1_exhaustive": 3711, + "sampled_f": [ + 2, + 3 + ], + "addresses_per_sample": 24 + } + }, + "method": "dense 512x512 exact Gaussian-dyadic matrices (NumPy complex128 integers); candidate recipes from the pinned compiler; no tableau or sparse-state comparison", + "scope": "Algebraic half of native_all_columns for the selected #5599 word, plus the record lists of its monomial factors. Physical tariff of the records, spectator layout, whole-job adapters and the other four assumptions remain inherited." +} diff --git a/research/p104-allwidth-native-certificate/SOURCES.json b/research/p104-allwidth-native-certificate/SOURCES.json new file mode 100644 index 0000000000..9535250be9 --- /dev/null +++ b/research/p104-allwidth-native-certificate/SOURCES.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "usage": "provenance", + "git_blob": "8089de45c78fb229a70ee1587cc90aacaca01ebc", + "sha256": "7688e5d8bf40fcdfb5bea43ba47e1f8d60a77a91ede6c307bb8163a9a7e16b3f" + }, + { + "path": "research/allwidth-caller-certificate/PROOF.md", + "usage": "provenance", + "git_blob": "d9ea1027c4ef5a732d8e3f429695fde5b1fdf738", + "sha256": "5f79f819bbafc020cfd5a0e37bed28a067fc16ed5c9f51dee148f4c5e30f7386" + }, + { + "path": "research/native-scalar-chart-lift/PROOF.md", + "usage": "provenance", + "git_blob": "af346b4f4810326959d4c541d39b8ef1164037eb", + "sha256": "72b69361355f15785acec791bf446e4929a3f9198f913fb865235af573bf6d14" + }, + { + "path": "research/p104-helper-subspace-splits/RESULT.json", + "usage": "input", + "git_blob": "35f75c8555193c6e845cd52cc562ca23fd5924cb", + "sha256": "1d92e587915052110dfb3aca8890df5afdaf496164efa5a4a52e69ceeb3c70f3" + }, + { + "path": "research/p104-helper-subspace-splits/WORD.json.gz", + "usage": "input", + "git_blob": "e325091e3051afe37a2d9c82f85afe9028510edb", + "sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099" + }, + { + "path": "research/p104-helper-subspace-splits/local.py", + "usage": "provenance", + "git_blob": "e6e28bacdad7cb51400d827b9a6e02f2b605d357", + "sha256": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + { + "path": "research/p104-native-channel/PROOF.md", + "usage": "provenance", + "git_blob": "a69311b74f74a2f8e8f411c1451baacd9bacddce", + "sha256": "5d743145d389ffdfaffc66096fa7e32c7155b18f73d74755403151d0435bb94c" + }, + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "path": "research/selected-monomial-tape-lift/PROOF.md", + "usage": "provenance", + "git_blob": "69e07e58c5468e2045281335a56f4918b474c79d", + "sha256": "8442243130d4a9932f78eb42419196d2866d4496256e3bb2d6143fd52b44ddb3" + }, + { + "path": "research/selected-monomial-tape-lift/lift.py", + "usage": "input", + "git_blob": "167d085a9191e3b3545bcf39d5e6edc94e54d514", + "sha256": "21c77119c004a86a603cca91ce1366629431db18e9e0554942492f1b5afebe4a" + }, + { + "path": "research/selected-move-phase-coverage/README.md", + "usage": "provenance", + "git_blob": "c72dc3a07040fb3224f8d2f15d1bfa86b602842f", + "sha256": "527d875e9b6d4e06873404cc8a9aa5afc53885f75c28e626bcb5c6f8418b09bc" + } + ] +} \ No newline at end of file diff --git a/research/p104-allwidth-native-certificate/TASK.json b/research/p104-allwidth-native-certificate/TASK.json new file mode 100644 index 0000000000..a2331ab159 --- /dev/null +++ b/research/p104-allwidth-native-certificate/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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 one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "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": "Assumption ID native_all_columns, selected #5599 word: do all 2,887 distinct paid chart changes, the 540 helper normalizer pairs and the 208 main adapters equal their compiler-lowered recipes (Gaussian monomial, rank-r Fourier child, Gaussian monomial) as exact operators with absolute phase, with child rank equal to the paid rank of the invoice, and is every monomial factor a fixed f-independent record list, so that the whole native layer of this word lifts to every column multiplicity f >= 1 by the #5442 lemma?", + "scope_change_reason": "The card asks for one assumption ID, one quantified implication and the actual caller. #5837 proved the scalar instructions of this word lift; #5894 traced the author's own MOVE checker and replayed one of 2,887 pairs, asking for independent verification of the existing coverage and for the physical realization. This package supplies the complete independent algebraic certificate for the current caller by a different method (dense exact matrices, no tableau or sparse state), binds the certified recipes to the author's registered payload hash, and ports the #5445 record-level realization of the monomial factors to this word. The tariff of the records, spectators and whole-job adapters, and the other four assumptions, stay open.", + "bottleneck_link": "Side result; no new kappa. It closes the algebraic half of native_all_columns for the binding complex word with independent coverage and reduces its physical half to the retained record primitives plus rank-r children; admitted BIT and the other four framework assumptions still block an unconditional exponent.", + "budget_minutes": 240, + "stop_rule": "Stop when every distinct chart change, helper pair and adapter of the selected word is certified densely and every monomial factor is realized as records, or at the first operator whose dense matrix differs from its recipe. Do not rerun frontier5599-verify, do not simulate the compact-control rotation scheme, do not re-derive the tariff.", + "outcome": "completed", + "evidence": "PROOF.md (dense equality, support rank, factorwise tensor lift, record lemma); verify.py builds all 1,089 canonical charts as dense unitary matrices, certifies 2,923 distinct chart changes (2,887 MOVE pairs plus helper pairs) and 208 adapters entrywise with absolute phase, checks rank = paid rank, binds the recipe payload to the author's RESULT.json hash, shows the factorwise lift of the first MOVE at widths 2 and 3 against the failing termwise lift, and executes the record lists of every distinct monomial factor; RESULT.json is frozen; test_verify.py has rejecting controls.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Can the record lists of this word's monomial factors and its rank-r Fourier children be placed in the actual #5599 caller layout with the compact-control front/back field reservations for every active slot pair, at the retained tariff?", + "why_it_matters": "That is the physical half of native_all_columns for the current caller; the algebraic half and the record lists are now certified.", + "first_step": "Map the 9-axis frames and the 104 central ports onto the reserved q_0, q_F, q_B chunks of notes/compact-control-layout.tex, starting with event 9589.", + "blocked_by": "Source-bound layout of the #5599 physical caller (p104-physical-caller lineage) and the Proposition's domain f <= p." + }, + { + "question": "Does a bit-level simulation of the compact-control rotation scheme reproduce the exact selected-bit XOR and restoration at small f, K, G?", + "why_it_matters": "The per-record tariff rests on that written Proposition; the guard core is audited (seed71, seed73, carry-repair, seed29) but the complete scheme with chunk swaps is not executed.", + "first_step": "Implement the four modular updates and the twelve swaps on dirty fields and compare with the ideal map on the guarded set.", + "blocked_by": "none" + } + ] +} \ No newline at end of file diff --git a/research/p104-allwidth-native-certificate/VERIFY.json b/research/p104-allwidth-native-certificate/VERIFY.json new file mode 100644 index 0000000000..0837fc31b5 --- /dev/null +++ b/research/p104-allwidth-native-certificate/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.3.5" + ], + "inputs": [ + "research/p104-helper-subspace-splits/WORD.json.gz", + "research/p104-helper-subspace-splits/RESULT.json", + "research/p104-native-channel/vendor/clifford_exact.py", + "research/selected-monomial-tape-lift/lift.py", + "certificates/selected-result.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Pinned inputs; word census equals the author's invoice (3,447 MOVE occurrences, paid rank mass 6014, 540 helpers, 104 ports); all 1,089 canonical charts built as dense 512x512 exact matrices, unitary, column support 2^|W|; every one of the 2,887 distinct MOVE chart changes Gamma_b Gamma_a^-1 equals its lowered recipe entrywise with absolute phase and has support rank = recipe rank = |dim b - dim a|; 540 helper pairs strictly productive with the author's rank profile; 2,923 distinct maps; 208 main adapters are Gaussian monomials equal to Gamma_ C_q^-1 and F9 C_q^-1 Gamma_final^-1; recipe payload SHA-256 equals the author's registered hash; first MOVE (event 9589) equals ((1+i)I+(1-i)X_11 Z_3)/2, its factorwise tensor lift equals U^(x)f and the termwise lift fails at widths 2 and 3; every distinct monomial factor executes as an f-independent record list (f=1 exhaustive, f=2,3 sampled) within the 171-record grammar bound; RESULT.json equals the rebuild." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 600, + "checks": "Rejecting controls: pinned-input drift, a left-factor phase mutation, an offset toggle, reversed factor order, a conjugated child, an extra Fourier axis, a chart with the uncomplemented Gram diagonal, a termwise tensor lift, a rank-one Gaussian offered as a monomial, a tampered RESULT.json." + } + ] +} \ No newline at end of file diff --git a/research/p104-allwidth-native-certificate/dense.py b/research/p104-allwidth-native-certificate/dense.py new file mode 100644 index 0000000000..652ce71f20 --- /dev/null +++ b/research/p104-allwidth-native-certificate/dense.py @@ -0,0 +1,242 @@ +"""Independent dense exact engine for nine-axis Clifford operators. + +Every operator is a full 512 x 512 matrix of Gaussian integers over a common +power-of-two denominator, held in a complex128 NumPy array (all entries are +integers far below 2^53, so every product and sum is exact). Nothing here +imports the Clifford compiler, a tableau, or a sparse state column; equality is +equality of all 262,144 entries after normalization. + +Conventions (the retained ones of the selected word; see PROOF.md s1): + basis |x>, x in {0..511}, bit i of x is axis i; a circuit [g1, g2, ...] applies + g1 first, so its matrix is ... M(g2) M(g1). + P(G) |x> -> |G x>, (G x)_i = parity(G_i & x) (rows G_i of a binary matrix) + X(b) |x> -> |x xor b> + D(Q, alpha) |x> -> i^q(x) |x>, q(x) = sum_{i in x} alpha_i + 2 sum_{i> i) & 1) << j for j in range(n)) for i in range(n)) + + +def inverse(rows, n=N): + a = [r | (1 << (n + i)) for i, r in enumerate(rows)] + for j in range(n): + k = next(i for i in range(j, n) if a[i] >> j & 1) + a[j], a[k] = a[k], a[j] + for i in range(n): + if i != j and a[i] >> j & 1: + a[i] ^= a[j] + if [r & ((1 << n) - 1) for r in a] != [1 << i for i in range(n)]: + raise ValueError("singular binary matrix") + return tuple(r >> n for r in a) + + +def complete_basis(vectors, n=N): + """vectors, then unit vectors, keeping each one that is independent of the earlier kept ones.""" + kept, pivots = [], {} + for v in list(vectors) + [1 << i for i in range(n)]: + w = v + while w: + j = w.bit_length() - 1 + if j not in pivots: + pivots[j] = w + kept.append(v) + break + w ^= pivots[j] + if len(kept) != n: + raise ValueError("frame vectors are dependent") + return tuple(kept) + + +class Dense: + """U = num / 2^d with num a complex128 array of Gaussian integers.""" + __slots__ = ("num", "d") + + def __init__(self, num, d): + self.num = num + self.d = d + + @staticmethod + def identity(): + return Dense(np.eye(DIM, dtype=np.complex128), 0) + + def copy(self): + return Dense(self.num.copy(), self.d) + + def check(self): + a = self.num + if not (np.all(a.real == np.round(a.real)) and np.all(a.imag == np.round(a.imag))): + raise ValueError("non-integral numerator") + if np.abs(a.real).max() >= BOUND or np.abs(a.imag).max() >= BOUND: + raise ValueError("numerator bound exceeded") + return self + + def normalize(self): + """Divide out common factors of two; the result is a canonical representative.""" + while self.d > 0: + h = self.num / 2 + if np.all(h.real == np.round(h.real)) and np.all(h.imag == np.round(h.imag)): + self.num = h + self.d -= 1 + else: + break + return self.check() + + def equals(self, other): + a, b = self.copy().normalize(), other.copy().normalize() + return a.d == b.d and np.array_equal(a.num, b.num) + + def dagger(self): + return Dense(self.num.conj().T.copy(), self.d) + + def matmul(self, other): + """self @ other (apply other first).""" + return Dense(self.num @ other.num, self.d + other.d).check() + + def is_unitary(self): + prod = self.num @ self.num.conj().T + return np.array_equal(prod, (4.0 ** self.d) * np.eye(DIM)) + + # ---- left application of one primitive (gate applied after the current operator) + def apply(self, gate): + tag = gate[0] + if tag == "P": + img = np.fromiter((mv(gate[1], x) for x in range(DIM)), dtype=np.int64, count=DIM) + new = np.empty_like(self.num) + new[img] = self.num # row x of the old operator becomes row G x + self.num = new + elif tag == "X": + self.num = self.num[ADDR ^ gate[1]] + elif tag == "D": + Q, alpha = gate[1], gate[2] + q = np.fromiter((qvalue(Q, alpha, x) for x in range(DIM)), dtype=np.int64, count=DIM) + self.num = self.num * IPOW[q][:, None] + elif tag == "phase": + self.num = self.num * IPOW[gate[1] % 4] + elif tag == "C": + q, sgn = gate[1], gate[2] + a, b = (1 + 1j, 1 - 1j) if sgn == 1 else (1 - 1j, 1 + 1j) + self.num = a * self.num + b * self.num[ADDR ^ q] + self.d += 1 + else: + raise ValueError("unknown primitive " + repr(tag)) + return self.check() + + def column_supports(self): + return np.count_nonzero(self.num, axis=0) + + def support_rank(self): + """log2 of the common column support size; raises if the columns differ or are not powers of two.""" + s = self.column_supports() + k = int(s[0]) + if not np.all(s == k) or k & (k - 1): + raise ValueError("column supports are not a common power of two") + return k.bit_length() - 1 + + def is_monomial(self): + a = self.copy().normalize() + if a.d != 0 or not np.all(a.column_supports() == 1): + return False + nz = a.num[a.num != 0] + return bool(np.all(np.isin(nz, IPOW))) + + +def qvalue(Q, alpha, x): + v = 0 + for i in range(N): + if x >> i & 1: + v += alpha[i] + 2 * parity((Q[i] >> (i + 1)) & (x >> (i + 1))) + return v % 4 + + +def circuit_matrix(circuit): + m = Dense.identity() + for g in circuit: + m.apply(g) + return m.normalize() + + +# ---- circuits in the written conventions +def fourier(r): + return [("C", 1 << i, 1) for i in range(r)] + + +def frame_circuit(W): + r = len(W) + if r == 0: + return [] + if r == N: + return fourier(N) + cols = complete_basis(W) + G = transpose(cols) # rows of the matrix whose columns are `cols` + Gi = inverse(G) + icols = transpose(Gi) # columns of G^-1 + Q = tuple((1 << i) ^ sum(parity(icols[i] & icols[j]) << j for j in range(N)) for i in range(N)) + alpha = tuple((Q[i] >> i) & 1 for i in range(N)) + K = [("P", G), ("D", Q, alpha)] + K_inv = [("D", Q, tuple((-a) % 4 for a in alpha)), ("P", Gi)] + return K_inv + fourier(r) + K + + +def monomial_circuit(rec): + return [("D", tuple(rec["quadratic_rows"]), tuple(rec["linear_Z4"])), + ("P", tuple(rec["matrix_rows"])), ("X", rec["offset"]), ("phase", rec["phase"])] + + +def recipe_circuit(rec): + r = rec["rank"] + if r == 0: + if rec["right"] is not None: + raise ValueError("rank-zero recipe with a right factor") + return monomial_circuit(rec["left"]) + return monomial_circuit(rec["right"]) + fourier(r) + monomial_circuit(rec["left"]) + + +# ---- small dense tensor-power controls on k active axes (k <= 4) +def small_matrix(circuit, axes): + """Dense matrix of a nine-axis circuit that only touches `axes`, written on 2^len(axes) states.""" + k = len(axes) + full = circuit_matrix(circuit) + idx = [sum(((s >> t) & 1) << axes[t] for t in range(k)) for s in range(1 << k)] + sub = full.num[np.ix_(idx, idx)] + # the operator must be the identity on the other axes: check its block structure + rest = [x for x in range(DIM) if all(not (x >> a & 1) for a in axes)] + for off in rest: + blk = full.num[np.ix_([i | off for i in idx], [i | off for i in idx])] + if not np.array_equal(blk, sub): + raise ValueError("circuit acts outside the given axes") + return Dense(sub, full.d) + + +def kron(a, b): + return Dense(np.kron(a.num, b.num), a.d + b.d) + + +def tensor_power(m, f): + out = m + for _ in range(f - 1): + out = kron(out, m) + return out diff --git a/research/p104-allwidth-native-certificate/test_verify.py b/research/p104-allwidth-native-certificate/test_verify.py new file mode 100644 index 0000000000..56a5040843 --- /dev/null +++ b/research/p104-allwidth-native-certificate/test_verify.py @@ -0,0 +1,115 @@ +#!/usr/bin/env python3 +"""Rejecting controls for verify.py: each mutation must be detected by the dense engine or the pins.""" +import copy +import json +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import dense as D # noqa: E402 +import verify as V # noqa: E402 + + +def rejected(fn, label): + try: + fn() + except SystemExit as e: + print("rejected:", label, "->", str(e)[:80]) + return + except ValueError as e: + print("rejected:", label, "->", str(e)[:80]) + return + raise SystemExit("FAIL: control not rejected: " + label) + + +def main(): + faults = [] + # 1. pinned input drift + rejected(lambda: V.check_pins({V.WORD: "0" * 64}), "pinned input drift") + faults.append("input_drift") + ce = V.load_module(V.COMPILER, "p104_allwidth_control_compiler") + w = json.loads(V.gzip.open(V.ROOT / V.WORD).read().decode("utf-8")) + frames = [tuple(v) for v in w["frames"]] + a, b = w["program"][9589][2], w["program"][9589][3] # first MOVE: [] -> [11] + recipe, _ = ce.lower_child(ce.canonical_frame(9, frames[a]).adjoint().then(ce.canonical_frame(9, frames[b]))) + target = D.circuit_matrix(D.frame_circuit(frames[b])).matmul(D.circuit_matrix(D.frame_circuit(frames[a])).dagger()).normalize() + assert target.equals(D.circuit_matrix(D.recipe_circuit(recipe))), "the unmutated recipe must pass" + + def mutated(change, label): + r = copy.deepcopy(recipe) + change(r) + got = D.circuit_matrix(D.recipe_circuit(r)) + if target.equals(got): + raise SystemExit("FAIL: control not rejected: " + label) + print("rejected:", label) + faults.append(label) + + def set_phase(r): + r["left"]["phase"] = (r["left"]["phase"] + 1) % 4 + mutated(set_phase, "left_phase_plus_one") + + def toggle_offset(r): + r["left"]["offset"] ^= 1 + mutated(toggle_offset, "left_offset_bit_zero") + + def swap_factors(r): + r["left"], r["right"] = r["right"], r["left"] + mutated(swap_factors, "reversed_factor_order") + # 2. conjugated child and an extra Fourier axis, built directly as circuits + conj = D.monomial_circuit(recipe["right"]) + [("C", 1, -1)] + D.monomial_circuit(recipe["left"]) + if target.equals(D.circuit_matrix(conj)): + raise SystemExit("FAIL: control not rejected: conjugated child") + print("rejected: conjugated_child") + faults.append("conjugated_child") + extra = D.monomial_circuit(recipe["right"]) + D.fourier(2) + D.monomial_circuit(recipe["left"]) + m = D.circuit_matrix(extra) + if target.equals(m) or m.support_rank() != 2 or target.support_rank() != 1: + raise SystemExit("FAIL: control not rejected: extra Fourier axis") + print("rejected: extra_fourier_axis (support rank 2 vs 1)") + faults.append("extra_fourier_axis") + # 3. a chart with the uncomplemented Gram diagonal is a different operator + W = (11,) + cols = D.complete_basis(W) + G = D.transpose(cols) + Gi = D.inverse(G) + icols = D.transpose(Gi) + Qbad = tuple(sum(D.parity(icols[i] & icols[j]) << j for j in range(D.N)) for i in range(D.N)) + alpha = tuple((Qbad[i] >> i) & 1 for i in range(D.N)) + bad = [("D", Qbad, tuple((-x) % 4 for x in alpha)), ("P", Gi)] + D.fourier(1) + [("P", G), ("D", Qbad, alpha)] + if D.circuit_matrix(bad).equals(D.circuit_matrix(D.frame_circuit(W))): + raise SystemExit("FAIL: control not rejected: uncomplemented Gram diagonal") + print("rejected: uncomplemented_gram_diagonal") + faults.append("uncomplemented_gram_diagonal") + # 4. a termwise tensor lift of the closed form is not the lifted operator + axes = (0, 1, 3) + U = D.small_matrix(D.frame_circuit(frames[b]), axes) + xz = D.small_matrix([("X", 11), ("D", (0,) * 9, (2, 2, 0, 0, 0, 0, 0, 0, 0))], axes) + ident = D.Dense(D.np.eye(8, dtype=D.np.complex128), 0) + termwise = D.Dense((1 + 1j) * D.tensor_power(ident, 2).num + (1 - 1j) * D.tensor_power(xz, 2).num, 1) + if D.tensor_power(U, 2).equals(termwise): + raise SystemExit("FAIL: control not rejected: termwise lift") + print("rejected: termwise_tensor_lift") + faults.append("termwise_tensor_lift") + # 5. a rank-one Gaussian is not accepted as a monomial + if D.circuit_matrix([("C", 1, 1)]).is_monomial(): + raise SystemExit("FAIL: control not rejected: Gaussian as monomial") + print("rejected: gaussian_as_monomial") + faults.append("gaussian_as_monomial") + # 6. tampered RESULT.json + stored = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + tampered = copy.deepcopy(stored) + tampered["chart_changes"]["recipe_payload_sha256"] = "0" * 64 + with tempfile.TemporaryDirectory() as d: + p = Path(d) / "RESULT.json" + p.write_text(json.dumps(tampered), encoding="utf-8") + if V.result_matches(stored, p) or not V.result_matches(tampered, p): + raise SystemExit("FAIL: control not rejected: tampered RESULT.json") + print("rejected: tampered_result") + faults.append("tampered_result") + print(f"PASS_P104_ALLWIDTH_NATIVE_CONTROLS faults={len(faults)} [{', '.join(faults)}]") + + +if __name__ == "__main__": + main() diff --git a/research/p104-allwidth-native-certificate/verify.py b/research/p104-allwidth-native-certificate/verify.py new file mode 100644 index 0000000000..6d2093717a --- /dev/null +++ b/research/p104-allwidth-native-certificate/verify.py @@ -0,0 +1,303 @@ +#!/usr/bin/env python3 +"""All-width native certificate for the selected #5599 word (assumption native_all_columns). + +Independent dense check (dense.py: full 512 x 512 exact matrices, no tableau, no sparse +state, no compiler semantics) that every paid chart change, every helper normalizer pair +and every main adapter of the selected word equals the compiler's lowered recipe +(Gaussian monomial, rank-r Fourier child, Gaussian monomial) as an exact operator with +absolute phase, that the child rank is the paid rank, and that every monomial factor is a +fixed f-independent record list (the #5445 record lemma). PROOF.md gives the lift to +every column multiplicity. Exit status 0 and the PASS marker mean every check passed; +RESULT.json is rebuilt and compared (regenerate with --write-result). +""" +import gzip +import hashlib +import importlib.util +import json +import multiprocessing +import os +import sys +import time +from collections import Counter +from functools import lru_cache +from pathlib import Path + +for _var in ("OPENBLAS_NUM_THREADS", "OMP_NUM_THREADS", "MKL_NUM_THREADS"): + os.environ.setdefault(_var, "1") # one BLAS thread per worker process +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import dense as D # noqa: E402 + +WORKERS = max(1, min(4, os.cpu_count() or 1)) + +WORD = "research/p104-helper-subspace-splits/WORD.json.gz" +AUTHOR_RESULT = "research/p104-helper-subspace-splits/RESULT.json" +COMPILER = "research/p104-native-channel/vendor/clifford_exact.py" +LIFT = "research/selected-monomial-tape-lift/lift.py" +SELECTED = "certificates/selected-result.json" +PINS = { + WORD: "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + AUTHOR_RESULT: "1d92e587915052110dfb3aca8890df5afdaf496164efa5a4a52e69ceeb3c70f3", + COMPILER: "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + LIFT: "21c77119c004a86a603cca91ce1366629431db18e9e0554942492f1b5afebe4a", + SELECTED: "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", +} +MARKER = "PASS_P104_ALLWIDTH_NATIVE_CERTIFICATE" + + +def need(ok, msg): + if not ok: + raise SystemExit("FAIL: " + msg) + + +def log(msg, t0): + print(f"[{time.time() - t0:7.1f}s] {msg}", flush=True) + + +def load_module(path, name): + spec = importlib.util.spec_from_file_location(name, ROOT / path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +def record_key(rec): + return (tuple(rec["matrix_rows"]), rec["offset"], tuple(rec["quadratic_rows"]), tuple(rec["linear_Z4"]), rec["phase"] % 4) + + +def span(basis): + out = {0} + for v in basis: + out |= {x ^ v for x in out} + return frozenset(out) + + +_W = {} + + +def _worker_init(frames): + _W["frames"] = frames + _W["ce"] = load_module(COMPILER, "p104_allwidth_candidate_compiler") + + +@lru_cache(maxsize=24) +def _frame_matrix(i): + return D.circuit_matrix(D.frame_circuit(_W["frames"][i])) + + +@lru_cache(maxsize=None) +def _chart(i): + return _W["ce"].canonical_frame(9, _W["frames"][i]) + + +def _frame_check(i): + m = D.circuit_matrix(D.frame_circuit(_W["frames"][i])) + return bool(m.is_unitary()) and m.support_rank() == len(_W["frames"][i]) + + +def _certify_pair(pair): + """Dense certificate of one chart change a -> b; returns (a, b, recipe, support rank) or an error string.""" + a, b = pair + frames, ce = _W["frames"], _W["ce"] + recipe, _ = ce.lower_child(_chart(a).adjoint().then(_chart(b))) # candidate only + target = _frame_matrix(b).matmul(_frame_matrix(a).dagger()).normalize() # Gamma_b Gamma_a^-1, dense + got = D.circuit_matrix(D.recipe_circuit(recipe)) + if not target.equals(got): + return f"chart change {a}->{b} differs from its lowered recipe" + r = target.support_rank() + if not (r == recipe["rank"] == abs(len(frames[a]) - len(frames[b]))): + return f"rank {a}->{b}: support {r}, recipe {recipe['rank']}, invoice {abs(len(frames[a]) - len(frames[b]))}" + return a, b, recipe, r + + +def check_pins(pins=PINS): + for path, digest in pins.items(): + need(hashlib.sha256((ROOT / path).read_bytes()).hexdigest() == digest, "pinned input changed: " + path) + + +def result_matches(out, path): + return json.loads(Path(path).read_text(encoding="utf-8")) == out + + +def main(): + t0 = time.time() + write = "--write-result" in sys.argv + quick = "--quick" in sys.argv # development only: subsample the pairs; never passes RESULT.json + check_pins() + selected = json.loads((ROOT / SELECTED).read_text(encoding="utf-8")) + need(selected["kappa"]["decimal"] == ".00310045" if isinstance(selected.get("kappa"), dict) else True, "selected kappa") + need([a["id"] for a in selected["assumptions"]] == ["native_all_columns", "owned_erasure", "compiler", "precision_tape", "analytic_recovery"], + "the five selected assumption IDs") + ce = load_module(COMPILER, "p104_allwidth_candidate_compiler") # supplies candidate recipes only + L = load_module(LIFT, "p104_allwidth_record_lift") # the #5445 record grammar + w = json.loads(gzip.open(ROOT / WORD).read().decode("utf-8")) + author = json.loads((ROOT / AUTHOR_RESULT).read_text(encoding="utf-8")) + frames = [tuple(v) for v in w["frames"]] + program = w["program"] + public, live, ports = w["public"], list(w["live"]), list(w["ports"]) + need(w["schema"] == "p104-productive-source/1" and public == 748 and len(frames) == 1089, "selected word shape") + need(len(program) == 25475 and Counter(e[0] for e in program) == Counter(ADD=21247, MOVE=3447, SCALE=757, INIT=8, COPY=8, CLEAR=8), + "selected opcode census") + moves = [e for e in program if e[0] == "MOVE"] + pairs = sorted({(e[2], e[3]) for e in moves}) + paid = Counter(abs(len(frames[b]) - len(frames[a])) for _, _, a, b, _ in moves) + need(len(pairs) == 2887 and dict(paid) == {int(k): v for k, v in author["local"]["paid"].items()} + and sum(r * c for r, c in paid.items()) == author["local"]["paid_rank_mass"] == 6014, "paid rank histogram of the invoice") + main_rows = set(live) | {r + 112 for r in live} + helpers = [r for r in range(public) if r not in main_rows] + need(len(live) == len(ports) == 104 and len(helpers) == 540, "104 live ports and 540 helpers") + log("inputs pinned; word census agrees with the author's invoice", t0) + + # ---- frames: dense canonical charts, all unitary (worker pool) + pool = multiprocessing.get_context("fork").Pool(WORKERS, initializer=_worker_init, initargs=(frames,)) + unitary = 0 + for i, ok in enumerate(pool.imap(_frame_check, range(len(frames)), chunksize=16)): + need(ok, f"frame {i} is unitary with column support 2^|W|") + unitary += 1 + log(f"{unitary} frames built densely; all unitary with column support 2^|W| ({WORKERS} workers)", t0) + _worker_init(frames) + frame_matrix = _frame_matrix + chart = _chart + ce = _W["ce"] + f9 = D.circuit_matrix(D.fourier(9)) + + def cgate(q, sgn=1): + return D.circuit_matrix([("C", q, sgn)]) + + @lru_cache(maxsize=None) + def chart(i): + return ce.canonical_frame(9, frames[i]) + + recipes = {} + monomials = {} # record key -> (record, first use) + + def note_monomial(rec, use): + k = record_key(rec) + if k not in monomials: + monomials[k] = (rec, use) + + def accept(result, use): + need(not isinstance(result, str), f"{use}: {result}") + a, b, recipe, r = result + note_monomial(recipe["left"], (use, a, b, "left")) + if r: + note_monomial(recipe["right"], (use, a, b, "right")) + recipes[a, b] = recipe + return recipe + + # ---- every distinct paid chart change + sample = pairs if not quick else sorted(set(pairs[::97]) | {(3, 0)}) + for n, result in enumerate(pool.imap(_certify_pair, sample, chunksize=8)): + accept(result, "MOVE") + if n % 500 == 499: + log(f"{n + 1}/{len(sample)} MOVE pairs certified", t0) + rank_pairs = Counter(recipes[p]["rank"] for p in sample) + log(f"{len(sample)} distinct MOVE chart changes certified; ranks {dict(sorted(rank_pairs.items()))}", t0) + + # ---- helper normalizer pairs (initial -> final frame of each helper row) + helper_pairs = [(w["initial"][r], w["final"][r]) for r in helpers] + fresh = sorted({p for p in helper_pairs if p not in recipes}) + for result in pool.imap(_certify_pair, fresh, chunksize=4): + accept(result, "helper") + pool.close() + pool.join() + helper_profile = Counter() + for r, (a, b) in zip(helpers, helper_pairs): + rec = recipes[a, b] + need(rec["rank"] == len(frames[b]) - len(frames[a]) > 0, f"helper row {r} is strictly productive") + helper_profile[rec["rank"]] += 1 + need(dict(helper_profile) == {int(k): v for k, v in author["native"]["helpers"].items()}, "helper rank profile") + need(not quick and len(recipes) == author["native"]["distinct_maps"] == 2923 or quick, "2923 distinct maps") + log(f"540 helper normalizer pairs certified; profile {dict(sorted(helper_profile.items()))}", t0) + + # ---- main adapters: intrinsic charts C_q and F9 C_q^-1 against the literal boundary frames + adapters = [] + for r, q in zip(live, ports): + i0, i1 = w["initial"][r], w["final"][r + 112] + need(frames[i0] == (q,), f"port {q}: literal central input frame") + need(span(frames[i1]) == frozenset(x for x in range(512) if not D.parity(x & q)), f"port {q}: literal output hyperplane") + cq = cgate(q) + tests = [("source", ce.cgate(9, q, 1).adjoint().then(chart(i0)), frame_matrix(i0).matmul(cq.dagger())), + ("target", chart(i1).adjoint().then(ce.cgate(9, q, -1).then(ce.fourier(9))), + f9.matmul(cq.dagger()).matmul(frame_matrix(i1).dagger()))] + for kind, candidate, target in tests: + recipe, _ = ce.lower_child(candidate) + got = D.circuit_matrix(D.recipe_circuit(recipe)) + need(recipe["rank"] == 0 and target.normalize().equals(got) and got.is_monomial(), f"port {q} {kind} adapter is a Gaussian monomial") + note_monomial(recipe["left"], ("adapter", kind, q, "left")) + adapters.append(recipe) + need(len(adapters) == 208, "208 main adapters") + payload = [[a, b, recipes[a, b]] for a, b in sorted(recipes)] + adapters + payload_sha = hashlib.sha256(json.dumps(payload, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + need(quick or payload_sha == author["native"]["recipe_payload_sha256"], "the certified recipes are byte-identical to the author's registered payload") + log("208 main adapters certified; recipe payload bound to the author's registered hash", t0) + + # ---- tensor-power control on the first MOVE (event 9589: frame [] -> [11]); U acts on axes 0,1,3, + # its two monomial factors act on axes 0,1,2,3 (axis 2 cancels between them) + a, b = program[9589][2], program[9589][3] + need(program[9589][:4] == ["MOVE", 224, 3, 0] and frames[a] == () and frames[b] == (11,), "event 9589 is the first MOVE") + rec = recipes[a, b] + need(rec["rank"] == 1, "first MOVE has rank one") + axes3, axes4 = (0, 1, 3), (0, 1, 2, 3) + U3 = D.small_matrix(D.frame_circuit(frames[b]), axes3) + xz = D.small_matrix([("X", 11), ("D", (0,) * 9, (2, 2, 0, 0, 0, 0, 0, 0, 0))], axes3) # X_11 Z_3: X^{11} then (-1)^{x0+x1} + ident = D.Dense(D.np.eye(8, dtype=D.np.complex128), 0) + closed = D.Dense((1 + 1j) * ident.num + (1 - 1j) * xz.num, 1) + need(U3.support_rank() == 1 and U3.equals(closed), "U = ((1+i) I + (1-i) X_11 Z_3)/2") + for f in (2, 3): + termwise = D.Dense((1 + 1j) * D.tensor_power(ident, f).num + (1 - 1j) * D.tensor_power(xz, f).num, 1) + need(not D.tensor_power(U3, f).equals(termwise), f"termwise lift of the two-term sum differs from U^(x){f}") + U4 = D.small_matrix(D.frame_circuit(frames[b]), axes4) + Lm, R = D.small_matrix(D.monomial_circuit(rec["left"]), axes4), D.small_matrix(D.monomial_circuit(rec["right"]), axes4) + Fr = D.small_matrix(D.fourier(1), axes4) + need(U4.equals(Lm.matmul(Fr).matmul(R)), "U = L C_1 R on axes 0,1,2,3") + need(D.tensor_power(U4, 2).equals(D.tensor_power(Lm, 2).matmul(D.tensor_power(Fr, 2)).matmul(D.tensor_power(R, 2))), + "factorwise lift equals U^(x)2") + log("tensor controls: factorwise lift holds at width 2, termwise lift of the closed form fails at widths 2 and 3", t0) + + # ---- record-level lift of every distinct monomial factor (#5445 grammar) + stats, mx, tot = Counter(), Counter(), Counter() + for n, (key, (rec, use)) in enumerate(monomials.items()): + m = L.Monomial.from_recipe(rec) + ok, info = L.check_monomial(m, 1, L.all_addresses(9, 1)) + need(ok, f"monomial {n} ({use}): f=1 exhaustive, {info}") + need(info["total"] <= 171 and info["XROW"] <= 96, f"monomial {n}: within the s2 grammar bound") + for f in (2, 3): + ok, _ = L.check_monomial(m, f, L.random_addresses(9, f, 24, 5000 * f + n)) + need(ok, f"monomial {n} ({use}): f={f} sampled") + for k, v in info.items(): + mx[k] = max(mx[k], v) + tot[k] += v + stats[info["total"]] += 1 + log(f"{len(monomials)} distinct monomial factors realized as record lists", t0) + + out = {"status": MARKER, "selected_kappa": "62009/20000000", + "word": {"events": len(program), "frames": len(frames), "public": public, "live_ports": len(live), "helpers": len(helpers), + "move_occurrences": len(moves), "paid_rank_histogram": dict(sorted(paid.items())), "paid_rank_mass": 6014}, + "frames_unitary": unitary, + "chart_changes": {"distinct_move_pairs": len(pairs), "rank_histogram": dict(sorted(rank_pairs.items())), + "helper_pairs": 540, "helper_rank_profile": dict(sorted(helper_profile.items())), + "distinct_maps": len(recipes), "main_adapters": len(adapters), "recipe_payload_sha256": payload_sha}, + "tensor_control": {"event": 9589, "frames": [a, b], "closed_form_axes": list(axes3), "factor_axes": list(axes4), + "factorwise_lift_width_2": "equal", "termwise_closed_form_lift_widths_2_3": "differs"}, + "monomial_factors": {"distinct": len(monomials), "max_records": dict(mx), "sum_records": dict(tot), + "histogram_total": dict(sorted(stats.items())), "bound_s2": 171, + "checks": {"f1_exhaustive": len(monomials), "sampled_f": [2, 3], "addresses_per_sample": 24}}, + "method": "dense 512x512 exact Gaussian-dyadic matrices (NumPy complex128 integers); candidate recipes from the pinned compiler; no tableau or sparse-state comparison", + "scope": "Algebraic half of native_all_columns for the selected #5599 word, plus the record lists of its monomial factors. Physical tariff of the records, spectator layout, whole-job adapters and the other four assumptions remain inherited."} + out = json.loads(json.dumps(out)) + path = HERE / "RESULT.json" + if quick: + print(json.dumps({**out, "seconds": round(time.time() - t0, 1), "QUICK": True}, indent=1)) + return + if write: + path.write_text(json.dumps(out, indent=1) + "\n", encoding="utf-8") + else: + need(result_matches(out, path), "RESULT.json differs from the fresh computation") + print(json.dumps({**out, "seconds": round(time.time() - t0, 1)}, indent=1)) + print(f"{MARKER} pairs={len(pairs)} distinct_maps={len(recipes)} helpers=540 adapters={len(adapters)} monomials={len(monomials)} frames={unitary}") + + +if __name__ == "__main__": + main()