From 82c7db427100033aa1275ecdb16ebc2e2ef10b91 Mon Sep 17 00:00:00 2001 From: Mihir Srivastava Date: Wed, 21 Oct 2026 16:04:58 -0700 Subject: [PATCH] research: certify stage-zero caller commutation Prepared with substantial OpenAI Codex assistance. Apache-2.0. --- .../stage-zero-commutation-audit/README.md | 177 ++++++++++++ .../stage-zero-commutation-audit/RESULT.json | 60 +++++ .../stage-zero-commutation-audit/SOURCES.json | 73 +++++ .../stage-zero-commutation-audit/TASK.json | 162 +++++++++++ .../stage-zero-commutation-audit/VERIFY.json | 35 +++ .../check_export.py | 59 ++++ .../pr4440-COMPLEX-CONTROLLER.json.gz | Bin 0 -> 2653 bytes .../stage-zero-commutation-audit/verify.py | 255 ++++++++++++++++++ 8 files changed, 821 insertions(+) create mode 100644 research/stage-zero-commutation-audit/README.md create mode 100644 research/stage-zero-commutation-audit/RESULT.json create mode 100644 research/stage-zero-commutation-audit/SOURCES.json create mode 100644 research/stage-zero-commutation-audit/TASK.json create mode 100644 research/stage-zero-commutation-audit/VERIFY.json create mode 100644 research/stage-zero-commutation-audit/check_export.py create mode 100644 research/stage-zero-commutation-audit/pr4440-COMPLEX-CONTROLLER.json.gz create mode 100644 research/stage-zero-commutation-audit/verify.py diff --git a/research/stage-zero-commutation-audit/README.md b/research/stage-zero-commutation-audit/README.md new file mode 100644 index 0000000000..5562284ce3 --- /dev/null +++ b/research/stage-zero-commutation-audit/README.md @@ -0,0 +1,177 @@ +# Actual stage-zero Gaussian commutation + +**Scoped written proof and exact source-bound check; no new kappa.** This answers +open question 1 of Mark / Matarener's [PR #4457](https://github.com/CrocSwap/integer-mult-bounds/pull/4457) +at `dd40f88a4d45a0ae2487eb24f935516f749cefef`: the source-specified complex +caller satisfies `[D0,Q]=0`, including its actual port phases. The argument +does not require the port direction to be a standard coordinate axis. + +The check binds all **112 ports** to native labels and initial caller maps. +It reconstructs the rank-eight normalization **with its nonzero translation +at every port**. Omitting that translation changes the operator; retaining +it preserves commutation. The native implementation and whole-call adapter +contract remain premises. This does not replay the complete 632-field word, +admit a supplier, or change the selected result. + +## Operator proof + +For `a` in `F_2^9`, let `T_a e_x = e_(x xor a)` and define + + C_a = ((1+i) I + (1-i) T_a) / 2. + +These are the literal line-column coefficients in the pinned +`native_common.py`, not a claim about arbitrary canonical-frame Cliffords. +Its Fourier character at `xi` is `i^(a dot xi mod 2)`. +Since `T_a T_b = T_(a xor b) = T_b T_a`, all `C_a`, inverses and translations +commute. In particular, + + C_a^-1 = ((1-i) I + (1+i) T_a) / 2 = T_a C_a. + +For the actual port normal `q`, set `Q=C_q` and +`F9=product_(j=0..8) C_(2^j)`. The caller's `stage_frame` definition is + + D0 = F9 Q^-1, + D0 Q = Q D0 = F9. + +Every noninitial multiplier is a product on fresh axes; thin stages substitute +the identity. These and the retained idle products commute with the same +port's `Q` and `D0`. Different ports may have different `q`: the controller's +pair operations and scalar boundaries act separately on each port. This +justifies the per-port substitution into the commuting Laurent identity, +without allowing arbitrary replacements of `F9` or port-mixing gates. + +Complex conjugation preserves the identity. For every positive column +multiplicity `f`, tensor-product composition gives + + D0^tensor(f) Q^tensor(f) = (D0 Q)^tensor(f) + = (Q D0)^tensor(f) = Q^tensor(f) D0^tensor(f). + +Spectator identities also preserve it. This tensors **completed operators**; +it never distributes a tensor power over a sum. It does not prove that the +inherited native implementation realizes those operators at every multiplicity. + +## Actual caller binding + +Base: canonical main `2a13eb1827784206202db90e5dc8327cf8a250db`, priority +revision 7, selected conditional kappa `23/10000`. [SOURCES.json](SOURCES.json) +pins every main input by Git blob and SHA256. The verifier executes no +predecessor Python code; those source pins identify the audited definitions +and trigger replay if the contract changes. + +1. `DATA-PHASES.json` and the THREE-base canonical word agree on the 112 + ordered port normals, X input lines, identity Y entrances, full X exits, + and complementary eight-spaces at Y exits. The normals have Hamming + weights **3 (77 ports)** and **7 (35 ports)**. +2. `p3_native_cover.py::contacts` specifies initial references `(Q,I)` and + completed references `(F9,F9 Q^-1)`. Both diagonal reference ratios are + therefore `D0`. The 112 stage-zero entries in `P3-NATIVE-COVER.json.gz` + contain **448 identity coordinate maps**, with zero affine shift and + global phase. Every map and inverse is checked, fixing a common coordinate + system. This is a check of the declared caller records; their full native + realization is retained as a separate premise. +3. `complex_controller_factor.py::serialize_case` states `D0=F9 Q^-1`. + `native_common.py` and `frame_exchange.py` identify the reference operators + as commuting `C_a` products, keeping phase corrections separate from + abstract frame labels. +4. The #4440 controller (compressed here, preserving its exact original bytes) at + `40e22a83ed660d3d6074c4f2dbf14bfb621eee51` starts with + `LOCAL(0,0,forward)`, then stages 1 through 34 exactly once: 19 full calls + and 16 query shears. Its + [proof, sections 1–2](https://github.com/1337isnot1337/integer-mult-bounds/blob/40e22a83ed660d3d6074c4f2dbf14bfb621eee51/research/query-thinned-controllers/PROOF.md) + retains the initial native call unchanged. This check binds the emitted + caller and retains that local raw-map implementation premise. + +## The required translation + +For the recorded orthonormal complement `B=(b_1,...,b_8)` perpendicular to +`q`, set `G_B=product C_(b_j)`. The first retained idle is `D0 D1`; its last +eight axes are exactly the fresh standard axes of `D1`. Removing them leaves + + D0 = T_t G_B, + F9 = T_t Q G_B. + +Here `t` is the source's `translation_after`, nonzero in **all 112 cases**: +weight 4 in 77 cases and weight 8 in 35. Thus `F9=Q G_B` without the recorded +translation would be false in these coordinates. The translation is an +existing fixed monomial operation, not a new free recursive job. It commutes +with `Q`; no cost improvement is claimed. + +Port 0 gives a concrete witness: + + q = 11; B = [13,14,7,16,32,64,128,256]; t = 15. + +On input `e_0`, output 0 of `D0-G_B` is exactly **-1/16**. Independently of +the kernel calculation, all 512 Fourier characters per port verify + + |xi| - (q dot xi mod 2) + = sum_j (b_j dot xi mod 2) + 2(t dot xi mod 2) (mod 4). + +This includes the absolute phase at zero. A separate Gaussian-dyadic +convolution calculation, using integer pairs and powers of two only, gives +the same operator. Each `D0` kernel has 256 nonzero coefficients of squared +modulus `1/256`. Kernel equality proves equality on **every** address input: +all other basis columns are translates of the zero-input column. + +## Evidence and reproduction + +Python 3.12, standard library only: + +```sh +python -B scripts/research_package.py --package research/stage-zero-commutation-audit --check-only +python -B scripts/research_package.py --package research/stage-zero-commutation-audit +python -I -O -B research/stage-zero-commutation-audit/verify.py +python -B research/stage-zero-commutation-audit/check_export.py +``` + +[RESULT.json](RESULT.json) is deterministic; normal replay compares it and +`--write` is authoring only. Checks cover 114,688 commutator coefficients in +both conjugate orientations, 57,344 Fourier characters, the 448 initial maps +and the retained p17 initial call. + +Controls reject all 112 omitted translations, 112 substitutions of `Q` for +`Q^-1`, and 112 deliberately noncommuting phase insertions. Two additional +controls reject a wrong port normal and an altered initial map. At port 0, +putting `Z_1` before `F9` yields commutator coefficient `(1+i)/16` on input +`e_0`, output 0. This exposes the boundary of the convolution argument. + +Environment and verification status are in [TASK.json](TASK.json). The selected +baseline orientation command was attempted but stopped on an omitted selected +claim file in this sparse checkout. No full selected cold replay, BIT caller, +outer ledger, rounded implementation, resource-cost audit, formal proof-kernel +check or independent human review is claimed. + +The registered replay also creates a disposable export containing only this +package and its declared inputs. It runs with `-I -O -B`, compares the exact +receipt, and rejects changed source bytes and a changed expected receipt. +No Git checkout, network request or predecessor module import is needed in +that exported verifier. + +## Overlap and credit + +Canonical thread: [Discussion #4461](https://github.com/CrocSwap/integer-mult-bounds/discussions/4461). +The initial refresh covered 314 open PRs, 3,312 Discussion records and all +5,731 local README/TASK notes. #4457 already covered the transport audit first +considered; this follows its explicit open question 1 instead. #4455's +invoice/moment checks and #4448's native tariff audit remain complementary. + +Credit to **Mark / Matarener** for #4457's commutation question and adversarial +example; **zxv** for the physical caller, phase utilities, controller and +#4359 construction; **Cinna Davis / 1337isnot1337** for #4440's query-thinned +controller and #4441/#4447 successors; **Jacob Alan Sussman** for the +mixed-target compiler. Phase conventions retain the QQ16/native lineage and +**ywz65**'s `qq16-current-frame-consumer/native_support.py`, as credited by +the source. Retained controller data is Apache-2.0 with this predecessor +attribution. No priority claim is made for commuting translations. + +Prepared for **mihir-s-05** with substantial **OpenAI Codex assistance**; +no subagents. New work is Apache-2.0. + +## Open next questions + +The named commutation implication is closed for these source-specified +operators. The remaining separate question is whether each inherited native +invocation and whole-call adapter realizes the raw maps at every column +multiplicity. Start with a pinned audit of one complete invocation, keeping +phase, spectators and return conditions. That requires a separately scoped +physical replay; neither this algebra nor #4457's finite sampled lifts +substitutes for it. [TASK.json](TASK.json) records the same boundary. diff --git a/research/stage-zero-commutation-audit/RESULT.json b/research/stage-zero-commutation-audit/RESULT.json new file mode 100644 index 0000000000..682e0af1ff --- /dev/null +++ b/research/stage-zero-commutation-audit/RESULT.json @@ -0,0 +1,60 @@ +{ + "all_column_reason": "Equality of convolution kernels proves every translated basis column.", + "all_f_reason": "The written tensor-product composition lemma applies for every positive integer f.", + "commutator_coefficients_checked_both_orientations": 114688, + "controls": { + "noncommuting_character": 112, + "omitted_translation": 112, + "wrong_Q_inverse": 112, + "wrong_initial_map": 1, + "wrong_port": 1 + }, + "first_port": { + "complement": [ + 13, + 14, + 7, + 16, + 32, + 64, + 128, + 256 + ], + "noncommuting_character_witness": { + "denominator_power_of_two": 5, + "numerator_real_imag": [ + 2, + 2 + ], + "output_address": 0 + }, + "omitted_translation_witness": { + "denominator_power_of_two": 4, + "numerator_real_imag": [ + -1, + 0 + ], + "output_address": 0 + }, + "port": 0, + "q": 11, + "translation": 15 + }, + "fourier_characters_checked": 57344, + "initial_boundary_maps": 448, + "p17_full_calls": 19, + "p17_thin_calls": 16, + "ports": 112, + "query_hamming_weights": { + "3": 77, + "7": 35 + }, + "rank_eight_support_per_column": 256, + "scope": "Source-specified complex caller commutation and stage-zero phase normalization; not native supplier admission or a new kappa.", + "source_files_authenticated": 8, + "status": "PASS_STAGE_ZERO_GAUSSIAN_COMMUTATION", + "translation_hamming_weights": { + "4": 77, + "8": 35 + } +} diff --git a/research/stage-zero-commutation-audit/SOURCES.json b/research/stage-zero-commutation-audit/SOURCES.json new file mode 100644 index 0000000000..18053b3c5e --- /dev/null +++ b/research/stage-zero-commutation-audit/SOURCES.json @@ -0,0 +1,73 @@ +{ + "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/native_common.py", + "usage": "input", + "git_blob": "df276cc71f954b72ac4de4f07d2172d547772ba6", + "sha256": "ca1f913d6c104d456fdbebcecfdaf9a1ea12d647d74fe009b69689b9e678f0a4" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + { + "path": "research/kappa-rebuild/controller/p3_native_cover.py", + "usage": "input", + "git_blob": "8756693610a8dc8352629d8270cb4c6aed087cb8", + "sha256": "fae71fcbbd20b9ee73b049cf6f43ea1d048217fb15feb6055a007e47da3363fe" + }, + { + "path": "research/kappa-rebuild/controller/P3-NATIVE-COVER.json.gz", + "usage": "input", + "git_blob": "51a09b3952a491f06780bf6ce5f69b385f026b21", + "sha256": "facfc6d6ecde151afb7e6a167776f3fdaac1c816e785a21a39f7f0bfd9140f3f" + }, + { + "path": "research/kappa-rebuild/controller/frame_exchange.py", + "usage": "input", + "git_blob": "0e3213ed01bc29f7e1cb8c09c12b203927d47e35", + "sha256": "b4f8c79450edca57f3a359e09d1206a253e399308f01e89e469044149116c2e8" + }, + { + "path": "research/kappa-rebuild/bit/complex_controller_factor.py", + "usage": "input", + "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947", + "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "usage": "input", + "git_blob": "4a8c4ed26e53a72362d571c972e65aff546be784", + "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61" + } + ], + "retained_external_artifacts": [ + { + "local_path": "pr4440-COMPLEX-CONTROLLER.json.gz", + "repository": "1337isnot1337/integer-mult-bounds", + "commit": "40e22a83ed660d3d6074c4f2dbf14bfb621eee51", + "path": "research/query-thinned-controllers/COMPLEX-CONTROLLER.json", + "url": "https://github.com/1337isnot1337/integer-mult-bounds/blob/40e22a83ed660d3d6074c4f2dbf14bfb621eee51/research/query-thinned-controllers/COMPLEX-CONTROLLER.json", + "git_blob": "39318f6ad9baf0838a274ca1042b1e3ba0e74bf9", + "sha256": "bf1143325d8380fab40cd5a85449f9a5412f0340deba7f4693714c92ae320088", + "attribution": "Cinna Davis / 1337isnot1337, with OpenAI Codex assistance; Apache-2.0. Native/controller lineage by zxv, mixed-target compiler by Jacob Alan Sussman.", + "hash_encoding": "Decompressed exact original UTF-8 bytes; compressed container bytes do not determine mathematical equality." + } + ] +} diff --git a/research/stage-zero-commutation-audit/TASK.json b/research/stage-zero-commutation-audit/TASK.json new file mode 100644 index 0000000000..f9c5990338 --- /dev/null +++ b/research/stage-zero-commutation-audit/TASK.json @@ -0,0 +1,162 @@ +{ + "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": "PR4457 open question 1: exact commutation of the actual port Q and stage-zero D0=F9 Q^-1, bound to all 112 native caller records; retain the rank-eight translation correction.", + "scope_change_reason": "The newer p17 arithmetic is already audited by PR4455, and the live PR4457 covers the native/transport check originally considered. Its concrete open caller premise is complementary source-bound coverage for the changed mechanism.", + "bottleneck_link": "Closes one named interface assumption needed to substitute physical operators into the commuting Laurent controller. It supplies no new invoice or supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop after this caller implication, its exact finite source bindings and semantic controls. No whole-supplier replay or frame search.", + "outcome": "completed", + "evidence": "README.md written proof and RESULT.json, regenerated by verify.py without importing any predecessor evaluator.", + "author": "mihir-s-05", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents. No independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Does each inherited native/adapter implementation realize the source-specified raw local maps for arbitrary column multiplicity?", + "why_it_matters": "This audit proves commutation once those actual raw-map contracts hold; it does not execute the entire 632-field supplier.", + "first_step": "Audit a pinned full native invocation and its whole-call frame adapters against the retained physical coordinate contract, keeping phase and spectator behavior.", + "blocked_by": "Requires a separately scoped native supplier replay; PR4457 finite sampled lifts do not establish a universal physical implementation." + } + ], + "coordination": { + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4461", + "handoff": "PR4457 open question 1", + "handoff_head": "dd40f88a4d45a0ae2487eb24f935516f749cefef", + "upstream_checkpoint": { + "commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "priority_revision": 7, + "checked_utc": "2026-10-21T22:54:00Z" + }, + "overlap": { + "open_prs": 314, + "discussion_records": 3312, + "local_notes": 5731, + "complete_head_note_inventory": true, + "timestamps_utc": [ + "2026-10-21T22:50:14Z", + "2026-10-21T22:51:36Z" + ], + "limits": "Closed work via local notes and ledger; no exhaustive code-diff search." + }, + "submission_refresh": { + "upstream_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "priority_revision": 7, + "main_and_guidance_unchanged": true, + "coverage": { + "local": { + "head": "2a13eb1827784206202db90e5dc8327cf8a250db", + "records": 5733, + "head_records": 5731, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-21T23:03:08.112822+00:00", + "complete_pagination": true, + "records": 317 + }, + "discussions": { + "fetched_at": "2026-10-21T23:04:21.658409+00:00", + "complete_pagination": true, + "records": 3318 + } + }, + "warnings": [], + "decision": "Continue: PR4457 head unchanged; no other scoped stage-zero commutation claim found. Discussion4461 is this contribution." + } + }, + "orientation": { + "task_card": "independent-moment", + "baseline_command": "python -B scripts/research_baseline.py", + "baseline_result": "Not completed: sparse checkout lacks research/kappa-rebuild/CLAIM.json and the full selected source closure. Selected record, review and manifest were read; no selected baseline/cold replay is claimed." + }, + "validation": { + "python": "3.12.0", + "platform": "Windows-11-10.0.26300-SP0", + "registered_replay": "PASS", + "metadata_and_pins": "PASS (not scientific acceptance)", + "isolated_optimized_replay": "PASS", + "git_free_export": "PASS via committed check_export.py; optimized exact receipt equality, changed source and receipt rejected", + "full_selected_replay": "Not run; independent scoped audit only", + "hosted_ci": "Not yet run" + } +} diff --git a/research/stage-zero-commutation-audit/VERIFY.json b/research/stage-zero-commutation-audit/VERIFY.json new file mode 100644 index 0000000000..4c3fa3841f --- /dev/null +++ b/research/stage-zero-commutation-audit/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/native_common.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "research/kappa-rebuild/controller/p3_native_cover.py", + "research/kappa-rebuild/controller/P3-NATIVE-COVER.json.gz", + "research/kappa-rebuild/controller/frame_exchange.py", + "research/kappa-rebuild/bit/complex_controller_factor.py", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact Gaussian-dyadic kernels at all 112 source ports, both orientations; all 512 Fourier characters; actual initial coordinate maps; retained p17 initial call; omitted-translation, wrong-inverse, noncommuting-character, wrong-port and wrong-map controls." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/check_export.py" + ], + "timeout_seconds": 120, + "checks": "Git-free optimized replay with exact receipt equality, plus changed-source and changed-receipt rejection in a disposable export." + } + ] +} diff --git a/research/stage-zero-commutation-audit/check_export.py b/research/stage-zero-commutation-audit/check_export.py new file mode 100644 index 0000000000..6d0f628097 --- /dev/null +++ b/research/stage-zero-commutation-audit/check_export.py @@ -0,0 +1,59 @@ +#!/usr/bin/env python3 +"""Exercise Git-free optimized replay and corrupted-input/receipt rejection. + +Prepared for mihir-s-05 with substantial OpenAI Codex assistance. Apache-2.0. +All mutations take place in a disposable export, never in source inputs. +""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +REL = HERE.relative_to(ROOT) + + +def main(): + manifest = json.loads((HERE / 'VERIFY.json').read_text(encoding='utf-8')) + with tempfile.TemporaryDirectory(prefix='stage-zero-cold-') as tmp: + dest = Path(tmp).resolve() + if not dest.is_relative_to(Path(tempfile.gettempdir()).resolve()): + raise ValueError('Export is outside the temporary directory') + shutil.copytree(HERE, dest / REL, ignore=shutil.ignore_patterns('__pycache__')) + for entry in manifest['inputs']: + target = dest / entry + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / entry, target) + command = [sys.executable, '-I', '-O', '-B', str(dest / REL / 'verify.py')] + + def run(): + return subprocess.run(command, cwd=dest, capture_output=True, + text=True, encoding='utf-8', timeout=120) + + good = run() + if good.returncode: + raise ValueError(good.stderr) + if json.loads(good.stdout) != json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')): + raise ValueError('Export receipt mismatch') + source = dest / next(p for p in manifest['inputs'] if p.endswith('/DATA-PHASES.json')) + original = source.read_bytes() + source.write_bytes(original + b' ') + bad_source = run() + if bad_source.returncode == 0 or 'Changed source:' not in bad_source.stderr: + raise ValueError('Source-corruption control did not reject') + source.write_bytes(original) + receipt = dest / REL / 'RESULT.json' + result = json.loads(receipt.read_text(encoding='utf-8')) + result['ports'] = 111 + receipt.write_text(json.dumps(result), encoding='utf-8') + bad_receipt = run() + if bad_receipt.returncode == 0 or 'Changed expected result' not in bad_receipt.stderr: + raise ValueError('Receipt-corruption control did not reject') + print('PASS_GIT_FREE_OPTIMIZED_EXPORT exact_receipt=1 changed_source_rejected=1 changed_receipt_rejected=1') + + +if __name__ == '__main__': + main() diff --git a/research/stage-zero-commutation-audit/pr4440-COMPLEX-CONTROLLER.json.gz b/research/stage-zero-commutation-audit/pr4440-COMPLEX-CONTROLLER.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..395056fc7341f363777fb07192bbd789d5cab465 GIT binary patch literal 2653 zcmV-j3ZnHNiwFP!000023hiCnZrex_efL)wdJciU@H%hCB-j}snBARVu~-Zif?_ic zVOjD@ax#M;|GuJQvx{s}sjhBC5>@k%5lMA*^*L457plr%E-o)8v-|f|x!6osv&G%y zr%RdWSM}}p%g4pdY*m%(?aeRSJKKBn^226(^~clIW%K{-6ES(k7e{;{+fSZ9|MwL$ zc@lgLUoexW#TPR<7QUFtvGB!Aj)gB~ax8o?lVjnF#H1Ye$j5d;@=4}+{Lz&;9{)Va z9FKp+!yJ!)?aCaFe;2|WkAFXTwj7_)$pACS7bjt+%;Z?Y3NtyDX@Hp=%e2i*j%As} zOpaw)%uJ4D8^cVFW!s5mk`Fq^&t$|Tp8=Ij@)=Ocu6!0;GRx<{B|GzZkjXTk1(|2% z&gaag94(s{fYYbk=jp?0dApk3_vb*r`}fs9fFM zZb7p~Ne#{_gb+y*VnujKMo=ObSi`m~`~#~95LktOU=;xZtDpuZC`6M?x$uvxR1wl& zgdm9MU|1kGZG(oGdxzBAKceQ|0X3&agVq#9vcW7sG|d78Q?d-(>K{l`Vhn)OiX@qE;vYs6|1g^Phf$&kXuebtIYC5+NbHH&pb^I2aWtm7 zU~64MGD007j_Lq$R0oKoIzSvH%g6)B$S5+p@my1l2_Ds^6f;&t4}|MN+TJR_M&Cb@ zO8-bI{UfRLkEB!)nZJmXAfmg$fp0tT&ET@O_npwHy8U?Ig1B<{E!}<}andPYc$n&0 zG5I5%l>L$~f?4PJ*1zHTlKt|SF7|6#r$Z&rm+Y74Gn0;?${0_V?3N>&NXI}W&z9_# zBb!IZUCEIrOLmY`oJPk@CC`=Y6Q^jJTq~EIk}r;I5$zlB9OtKrYPqG^x zoJn>=_DOcbgEPr)$Uez#cyK1!4cRBz4G+#FyCM4|yWzo^WH)4=WH&rGlkA4W0PLLebRAR*{T zhyX~y0g(scAY@nVX+ax7PDW7WArQ>`>qRJX8LfmQgj$h%IJPKiL9Apzh9i^Y^1-5C z7q=oX39|gmj>_at71TAYPDraVxl4s{VqFqgncSrkx-4k8$edQ`om!bZ2~kx%K4cMU zO)8nZquw#K0yeqw6KtvQVSIQU%xb>7BF@A z>jOEGso_GA(xJB$NzIOWehx~;v_IsaiL(~*&p*)qN`>g-?c(L%ul3W(O*Ok+E@ty) zQ}-e+YC0AC0r#OnOv24G1L_JN0~#1U1~f2y3}|5Z&K*$6fF3z~V+K^71fX(Q1b^uN zKn9c{-aDWS@!kQI4CuZAl?>>QpD`IwhWOL~l?>?F-sxS~^ZF<3`7+}f_IR1`WPd;A z!(~2OW;~DiXqiuz8PAhgfAYC!DT6|ho*X87=%P-&ZRqtojqPeOwlCtep95+8?pQxmBL+j3sSaxp|of}D4 zXxbH;b%n~LzN4OhY5w&&yLS0`QQl0~n^ifxUr$%%@$21D82(0K#&B(J}aD5H1U#V_vSr@C;7 z?v1>QUsq__6`DN@ZJ|{oFumTwvfe(-R3X&MgVplp@p@BzDyJW+a(+`kmoiDkOA_;J zaW`E*t{&!(^`l&v2cM_wt;E@C3;y+Tbu)dxd|cEpOY!pG^H(>s)or<1Lk4Q>5|eK{ zsYj(_bDcfON#i!SS!(!sGAscIJ8pB`e5|hT8U|hx&Yo|tH?!Mv4N}By?`?7?8k=oK z-Xy4)1Ray4WD>PZ(wRwjGl_O4#m^)cnlw$5Hfu6bO}4s@TY2x>F)gNBKU`H$W0G0% zVr-v3F6ZU6x|x?PZ#)J+X>vR6%JN})KU?3`B<4bAxmI~BQxysKDl1rKg`QN zpE5^k_gZ}$>$l5~f32%6*VFRTHX5z1G?B^MzyEyob}~HoeVEPHW#9bQX=#W1&FZng z;jgbj0;{z1U|@<^Upa$D5X`V@8mXP9My)p5QX=Ya^v{32`TalBcfY*3`h8;cgMezc zq7g+?iQvR;h2uo+<^-fAq3LNv#&~)XYa9;r#Manx^w^3<6iqSoBvzj|dNi6IkY0yo zsu_2RXDYLXKT6vOuB5XW%7e}-Z05Ioz4V~2$i*y&Q1My9LGk?kIBBbvG>wlj;qLAG1{87LhV zF6PicQkE{JtK1RP9&IC!z2n01}T#$=*snUphw+^rY{QC z#Gbx!ur}H$huI38vQlO%(3Rs>zE9nVrY{QC%wE*sU^QnI4)c{cvR0J&3UuYT+3r&} zqUno*wXl~TI9SbTg2Rku&i@r<#sXbAZh-sLjcEF!PI0BZC_}+&w9_t!;@a-m1y*Hi zi-WaK-H4_y3RZ2e>jq)%H0@bk50CMC+nZL&M>$mLvcF{MPKEE4qF^kye_aja*!~R|5_nF2165`#j zfBWst>uIZy?05RxUoZX- LI7!}8w)+480){Eh literal 0 HcmV?d00001 diff --git a/research/stage-zero-commutation-audit/verify.py b/research/stage-zero-commutation-audit/verify.py new file mode 100644 index 0000000000..1749504ab7 --- /dev/null +++ b/research/stage-zero-commutation-audit/verify.py @@ -0,0 +1,255 @@ +#!/usr/bin/env python3 +"""Exact caller-bound Gaussian commutation; no predecessor code is executed. + +Prepared for mihir-s-05 with substantial OpenAI Codex assistance. Apache-2.0. +The mathematical operators and port data are credited in README.md. +""" +from collections import Counter +from copy import deepcopy +from hashlib import sha1, sha256 +import argparse +import gzip +import json +from pathlib import Path + +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' +COVER = 'research/kappa-rebuild/controller/P3-NATIVE-COVER.json.gz' +CANONICAL = 'research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz' + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + + +def authenticate(): + manifest = read(HERE / 'SOURCES.json') + count = 0 + for row in manifest['files']: + if row['usage'] != 'input': + continue + path = ROOT / row['path'] + need(path.resolve().is_relative_to(ROOT), 'Input escaped repository') + raw = path.read_bytes() + need(sha256(raw).hexdigest() == row['sha256'], 'Changed source: ' + row['path']) + need(sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == row['git_blob'], + 'Changed source Git blob: ' + row['path']) + count += 1 + for row in manifest['retained_external_artifacts']: + raw = (HERE / row['local_path']).read_bytes() + if row['local_path'].endswith('.gz'): + raw = gzip.decompress(raw) + need(sha256(raw).hexdigest() == row['sha256'], 'Changed retained artifact') + need(sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == row['git_blob'], + 'Changed retained artifact Git blob') + count += 1 + return count + + +# A translation-invariant operator is its convolution kernel in Q(i)[F_2^9]. +# Store Gaussian integer numerators and one common power-of-two denominator. +def normalized(entries, exponent): + entries = {x: z for x, z in entries.items() if z != (0, 0)} + while exponent and all(a % 2 == b % 2 == 0 for a, b in entries.values()): + entries = {x: (a // 2, b // 2) for x, (a, b) in entries.items()} + exponent -= 1 + return entries, exponent + + +def compose(left, right): + a, da = left + b, db = right + result = {} + for x, (ar, ai) in a.items(): + for y, (br, bi) in b.items(): + r, i = result.get(x ^ y, (0, 0)) + result[x ^ y] = r + ar * br - ai * bi, i + ar * bi + ai * br + return normalized(result, da + db) + + +def gaussian(q, sign=1): + need(0 < q < 512 and sign in (-1, 1), 'Nonzero nine-axis signed Gaussian') + return {0: (1, sign), q: (1, -sign)}, 1 + + +def gaussian_product(axes): + result = ({0: (1, 0)}, 0) + for axis in axes: + result = compose(gaussian(axis), result) + return result + + +def translate(kernel, shift): + entries, exponent = kernel + return {x ^ shift: z for x, z in entries.items()}, exponent + + +def conjugate(kernel): + entries, exponent = kernel + return {x: (a, -b) for x, (a, b) in entries.items()}, exponent + + +def character_on_column(kernel, axis): + """Z_axis applied to this zero-input column; deliberately not convolution.""" + entries, exponent = kernel + return {x: (-a, -b) if (axis & x).bit_count() % 2 else (a, b) + for x, (a, b) in entries.items()}, exponent + + +def first_difference(left, right): + a, da = left + b, db = right + common = max(da, db) + for x in sorted(a.keys() | b.keys()): + ar, ai = a.get(x, (0, 0)) + br, bi = b.get(x, (0, 0)) + delta = ((ar << (common-da)) - (br << (common-db)), + (ai << (common-da)) - (bi << (common-db))) + if delta != (0, 0): + return {'output_address': x, 'numerator_real_imag': list(delta), + 'denominator_power_of_two': common} + return None + + +def span(axes): + values = {0} + for axis in axes: + values |= {x ^ axis for x in tuple(values)} + return values + + +def validate_port(recipe, canonical): + port, q = recipe['port'], recipe['q'] + child = recipe['idle_children'][0] + basis = child['orthogonal_axes'][:8] + shift = child['translation_after'] + need(canonical['ports'][port] == q, 'Port normal differs between native and phase data') + need(canonical['frames'][canonical['start'][port]] == [q], 'Native X entrance line') + need(canonical['start'][112+port] == 0, 'Native Y entrance identity') + need(canonical['final'][port] == 1 and len(canonical['frames'][1]) == 9, + 'Native X full exit') + need(q.bit_count() % 2 == 1 and len(basis) == 8, 'Odd query and eight complementary axes') + need(all(0 < x < 512 for x in basis) and 0 <= shift < 512, 'Nine-axis support') + need(all((x & y).bit_count() % 2 == int(i == j) + for i, x in enumerate([q] + basis) for j, y in enumerate([q] + basis)), + 'Actual query and complement form an orthonormal basis') + need(span(basis) == span(canonical['frames'][canonical['final'][112+port]]), + 'Native Y exit is the same complementary space') + need(child['orthogonal_axes'][8:] == [1 << i for i in range(9, 17)] and child['rank'] == 16, + 'Removing D1 from the actual initial idle leaves these eight old axes') + return q, basis, shift + + +def check_initial_contacts(cover): + contacts = [r for r in cover['main_contacts'] if r['stage'] == 0] + need([r['port'] for r in contacts] == list(range(112)), 'All 112 initial caller contacts') + identity = [1 << i for i in range(73)] + for row in contacts: + need(row['pair'] == 0 and row['direction'] == 'forward' and row['common_spectator_frame'] == [], + 'Source initial forward call') + need(set(row['maps']) == {'entry_X', 'entry_Y', 'exit_X', 'exit_Y'}, 'Four boundary maps') + for rec in row['maps'].values(): + need(rec['owner_columns'] == rec['inverse_owner_columns'] == identity, + 'Stage-zero coordinate map must be the identity') + need(rec['physical_shift'] == rec['inverse_physical_shift'] == rec['global_phase_Z4'] == 0, + 'Stage-zero contact has no omitted affine or global phase') + return 4 * len(contacts) + + +def rejected(action): + try: + action() + except ValueError: + return True + return False + + +def run(): + source_count = authenticate() + phases, canonical, cover = read(ROOT / PHASES), read(ROOT / CANONICAL), read(ROOT / COVER) + word = read(HERE / 'pr4440-COMPLEX-CONTROLLER.json.gz') + need(len(phases['recipes']) == 112 and phases['m'] == 73, 'Actual phase packet') + need([r['port'] for r in phases['recipes']] == list(range(112)), 'Ordered port census') + need(word['pairs'] == 17 and word['ambient_rank'] == 153, 'Pinned p17 caller') + calls = [r for r in word['physical_events'] if r[0] in ('LOCAL', 'QUERY_SHEAR')] + need(calls[0] == ['LOCAL', 0, 0, False] and [r[1] for r in calls] == list(range(35)), + 'Exactly one initial call, followed by all 34 ordered stages') + need(sum(r[0] == 'LOCAL' for r in calls) == 19 and sum(r[0] == 'QUERY_SHEAR' for r in calls) == 16, + 'Actual full/thin call partition') + contacts = check_initial_contacts(cover) + f9 = gaussian_product([1 << i for i in range(9)]) + weights, shift_weights = Counter(), Counter() + omitted, wrong_inverse, noncommuting = [], [], [] + counts = 0 + example = None + for recipe in phases['recipes']: + q, basis, shift = validate_port(recipe, canonical) + positive, inverse = gaussian(q), gaussian(q, -1) + d0 = compose(f9, inverse) + repaired = translate(gaussian_product(basis), shift) + need(d0 == repaired, 'Exact D0 = translation times eight positive Gaussians') + need(len(d0[0]) == 256 and all(256*(a*a+b*b) == 1 << (2*d0[1]) for a, b in d0[0].values()), + 'Every D0 column has 256 entries of squared modulus 1/256') + for d, g, f in ((d0, positive, f9), (conjugate(d0), conjugate(positive), conjugate(f9))): + need(compose(d, g) == compose(g, d) == f, 'All-column physical commutation, both conjugate orientations') + counts += 512 + # Independent evaluation of every Fourier character binds the source + # rank-16 idle's old part and its translation without a phase-polynomial helper. + for xi in range(512): + intended = (xi.bit_count() - ((xi & q).bit_count() % 2)) % 4 + supplied = (sum((xi & b).bit_count() % 2 for b in basis) + + 2*((xi & shift).bit_count() % 2)) % 4 + need(intended == supplied, 'Literal Fourier-character equality including phase') + omitted.append(first_difference(d0, gaussian_product(basis))) + wrong_inverse.append(first_difference(d0, compose(f9, positive))) + # Put a nonconstant character in front of F9. This leaves the abelian + # convolution algebra, and its D0 really fails to commute with Q. + axis = q & -q + left = character_on_column(f9, axis) # (Z F9 Q^-1) Q delta_0 + right = compose(positive, character_on_column(d0, axis)) + noncommuting.append(first_difference(left, right)) + weights[q.bit_count()] += 1 + shift_weights[shift.bit_count()] += 1 + if example is None: + example = {'port': recipe['port'], 'q': q, 'complement': basis, 'translation': shift, + 'omitted_translation_witness': omitted[-1], 'noncommuting_character_witness': noncommuting[-1]} + need(all(omitted) and all(wrong_inverse) and all(noncommuting), 'Every semantic control must expose a nonzero coefficient') + bad_port = deepcopy(phases['recipes'][0]); bad_port['q'] = phases['recipes'][1]['q'] + need(rejected(lambda: validate_port(bad_port, canonical)), 'Wrong port normal rejected') + bad_cover = deepcopy(cover) + bad_cover['main_contacts'][0]['maps']['entry_X']['physical_shift'] ^= 1 + need(rejected(lambda: check_initial_contacts(bad_cover)), 'Wrong initial coordinate translation rejected') + return {'status': 'PASS_STAGE_ZERO_GAUSSIAN_COMMUTATION', 'source_files_authenticated': source_count, + 'ports': 112, 'initial_boundary_maps': contacts, 'p17_full_calls': 19, 'p17_thin_calls': 16, + 'query_hamming_weights': {str(k): v for k, v in sorted(weights.items())}, + 'translation_hamming_weights': {str(k): v for k, v in sorted(shift_weights.items())}, + 'commutator_coefficients_checked_both_orientations': counts, + 'fourier_characters_checked': 112*512, 'rank_eight_support_per_column': 256, + 'controls': {'omitted_translation': len(omitted), 'wrong_Q_inverse': len(wrong_inverse), + 'noncommuting_character': len(noncommuting), 'wrong_port': 1, 'wrong_initial_map': 1}, + 'first_port': example, 'all_column_reason': 'Equality of convolution kernels proves every translated basis column.', + 'all_f_reason': 'The written tensor-product composition lemma applies for every positive integer f.', + 'scope': 'Source-specified complex caller commutation and stage-zero phase normalization; not native supplier admission or a new kappa.'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true', help='authoring only: save the deterministic result') + args = parser.parse_args() + result = run() + if args.write: + (HERE / 'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True)+'\n', encoding='utf-8', newline='\n') + else: + need(result == read(HERE / 'RESULT.json'), 'Changed expected result') + print(json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main()