diff --git a/research/selected-sigma-chart-binding/README.md b/research/selected-sigma-chart-binding/README.md new file mode 100644 index 0000000000..883503aaf0 --- /dev/null +++ b/research/selected-sigma-chart-binding/README.md @@ -0,0 +1,235 @@ +# Selected1094 binary chart certificates: complete dictionary and reference binding + +This is an independent **finite certificate/application audit**, not a new Lean +proof, physical supplier, cost saving or multiplication exponent. + +The selected1094 replay has **10,002 distinct 73-dimensional helper charts** in +`ACTUAL-SIGMAS.json.gz`. Every chart has a recovered five-array certificate in +the exact grammar of James Chang's [PR1879](https://github.com/CrocSwap/integer-mult-bounds/pull/1879), +consumed by the dictionary adapter of [PR1927](https://github.com/CrocSwap/integer-mult-bounds/pull/1927). +Those packages prove generic implications but explicitly do not supply a +selected-instance census or the auxiliary certificates. This package supplies +those witnesses and independently checks their mathematical premises, original +content keys and **all 69,120 helper references across 144 calls**. + +No predecessor executable is imported. In particular, a Python check of the +premises is **not** reported as execution of Lean's `certifyEntry` or fresh +kernel acceptance. The original generic theorems retain their own trust base. + +## Exact result and artifacts + +- [WITNESSES.json.gz](WITNESSES.json.gz) contains one complete five-array witness + per original dictionary key. Its decompressed payload, rather than gzip + container bytes, is the replay identity. +- [RESULT.json](RESULT.json) records all source/member digests, counts, the + reference multiplicities and explicit failure controls. Normal replay reads + this receipt and never overwrites it. +- [recover.py](recover.py) reconstructs certificates from the raw matrices only. + It does not read the original port bases, route recipes or formal checker. +- [verify.py](verify.py) does not import the recovery algorithm. It checks the + certificates and independently computes inverses by augmented-row + Gauss-Jordan elimination over F2. +- [SELECTION.json](SELECTION.json) preserves the complete original chooser + output: seed `e059d89919a0078380ea43f90a32a2f6`, track + `independent-verification`, selected card `formal-interface-lemma`. + +All 10,002 certificates have `a = u`; 6,612 updates have Hamming weight four +and 3,390 have weight eight. Thus these are even-weight orthogonal +transvections followed by the explicitly witnessed coordinate permutation. +The checker also compares each elimination inverse with the matrix transpose; +this extra selected-instance fact is not assumed from the word “orthogonal.” + +Coverage is **53,300,658 binary coefficient entries**, represented exactly by +730,146 packed columns, and **1,460,292 basis-vector compositions** across the +two inverse directions. Each check is over exact Python integers, with no +random test vectors, floating-point tolerance, or sampled address set. + +The raw source is the selected archive +`research/community-frontier1094-audit/selected-replay.tar.gz`, SHA256 +`f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6`. +This is **not** the similarly named historical R492 evidence under +`gauge44-slots-t16/evidence/global/`, which contains only 7,870 charts. +The selected archive's dictionary has payload SHA256 +`2cad2187e792fe7c879084a23f15577730ce27e82ff0c341885935c8adffc58f`. + +## Precise mathematical contract and direction + +For dimension n, write the source matrix as columns `A_j` in F2^n, least +significant bit first. The five arrays, in order, are: + +1. forward permutation `p`; +2. inverse permutation `p_inverse`; +3. original packed columns `A_j`; +4. update bits `u_i`; +5. coefficient bits `a_i`. + +Each array has length n. Indices are below n, columns below `2^n`, and bits +are 0 or 1. The checks require both permutation round trips, original column +identity, `a·u = 0`, and, for **every** j, + +``` +A_j = e_(p(j)) + a_(p(j)) u. +``` + +The coefficient index is `p(j)`, not j. With `P e_j = e_(p(j))` and +`T x = x + u(a·x)`, this is `A = T P`. Since `a·u=0`, characteristic two gives +`T(Tx)=x`; hence **`A^-1 = P^-1 T`**, not `T P^-1`. The independent checker +reconstructs the inverse by row elimination and verifies both compositions on +all n basis vectors. Linearity then proves both identities on every one of +the `2^73` addresses for these fixed matrices; no exhaustive-address execution +is claimed. + +For any payload function f, the stated logical pullback convention is +`f -> (x -> f(Ax))`; its inverse is `f -> (x -> f(A^-1 x))`. This derives +logical cancellation. It does not select the direction of an external physical +executor or establish in-place memory safety. The receipt contains an actual +selected chart and axis where the wrong inverse order gives a different vector. + +These are precisely the finite scalar obligations behind +`CheckedBinaryChart.Checks`, `ParsedBinaryChartCertificate.certify_sound`, and +`JsonPackedColumnDictionary.certifyEntry_sound` at the immutable heads in +[SOURCES.json](SOURCES.json). The witness's complete five-array value can be +passed as `certificateJson` to that adapter with `n=73` and JSON depth fuel 3. +A full call to the pinned Lean interpreter remains a separate kernel replay, +not an implicit consequence of this Python implementation. + +## Independent recovery and source/reference closure + +For a non-permutation matrix, choose any nonunit column v. In a factorization +`A = (I+u a^T)P`, that column must be `e_i+u`, so one of the n values `v+e_i` +is the update. For each candidate, the producer constructs the bipartite +column-to-coordinate possibilities and finds a matching. The matching gives +p and a; the producer retains only `a·u=0`. The verifier accepts a witness by +the equations above, not by trusting the search or its completeness. Every +selected chart is accepted, so no negative classification theorem is needed. + +The source dictionary is populated only by helper roles. The independent +reference pass reads the selected template, phase axes and provider ports: + +1. For an odd non-full port q, let z be its first zero coordinate among 0..8 + and put `u=q+e_z`. Apply `x -> x+u(u·x)` to the coordinate basis with + coordinates 0 and z exchanged. This reconstructs the source idle basis. +2. Decode each original helper route (`[3, child, offset]` at width nine or + `[4, child, offset, width, spectators]` otherwise), preserving all ordered + spectator coordinates. Pending child axes identify the first `width` + columns; spectators complete the first nine; the remaining basis coordinates + follow in order. +3. Recompute the SHA256 of the compact ordered decimal column list. Compare + the full list with the dictionary entry, not merely its hash. +4. Require all 144×480 role triples exactly once, every dictionary key referenced, + no missing entries, and the exact ordered occurrence stream hash from + `HOSTED.json`. Its digest is + `e9d95a4a108476a0971d19c8815e1cb747e3b28214b44c92500fdd9647f9bf6d`. + +This covers the dictionary's complete helper domain. It **does not** turn the +32,256 data-owner rows, private centre allocations or idle remainder operations +into claims about this helper-only dictionary. The emitter's route convention +is pinned and credited; its native replay and placement/chronology admission +are not rerun or replaced. + +## Controls and reproduction + +Use CPython 3.12, standard library only, from the repository root: + +```sh +uv run --python 3.12 --no-project python -I -O -B research/selected-sigma-chart-binding/verify.py +uv run --python 3.12 --no-project python -B scripts/research_package.py --package research/selected-sigma-chart-binding +``` + +The registered replay runs the direct verifier and eight focused test groups. +The verifier has two positive controls and nineteen semantic rejection +controls: malformed numeric/shape/index fields; a nonzero `a·u`; singular +elimination; wrong permutation direction and inverse table; coefficient and +source-column changes; content-key drift; duplicate JSON keys; missing and +orphan live entries; and a changed spectator axis. The wrong-inverse-order +example is an additional explicit separation witness. + +The focused tests independently enumerate every 3×3 binary matrix and all +permutation/transvection factors, compare the producer to that separate oracle, +and test exact inverses on every 3-bit input. They also check the coefficient +index convention, numeric/duplicate policies, compression invariance, source +pin drift, and all odd non-full nine-bit port bases. These are controls for the +implementation; the selected result still checks all 10,002 actual matrices. + +To independently regenerate the complete auxiliary witness file, without +replacing committed evidence: + +```sh +uv run --python 3.12 --no-project python -B research/selected-sigma-chart-binding/recover.py --output /tmp/selected-sigma-witnesses-new.json.gz +``` + +The producer refuses an existing destination. Compare decompressed canonical +JSON, not gzip headers. A receipt may likewise be written only to an absent +path with `verify.py --write-receipt NEW_PATH`. + +Observed final local verification on **CPython3.12.12, Clang21.1.4, +macOS27.0.1 arm64**: + +```text +PASS_SELECTED_SIGMA_CHART_BINDING charts=10002 dimension=73 helper_roles=69120 controls=19 no_new_lean_build no_new_kappa +Ran 8 tests in 0.247s +OK +PASS_REGISTERED_RESEARCH_PACKAGE research/selected-sigma-chart-binding outcome=completed +``` + +The direct optimized receipt-producing replay took14.46seconds; the registered +verifier-plus-tests took14.85seconds in this environment. These are observations, +not timing acceptance gates. The first metadata launch stopped before running +commands because `outcome` was descriptive text rather than the required enum; +after changing it to `completed`, the complete registered replay above passed. + +## Scope, provenance and credit + +Base main: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. The selected exponent +`836330098538459/500000000000000000` and every paid profile remain unchanged. +This is a refined, not rerolled, chooser assignment; [TASK.json](TASK.json) +records the working example, changed scope, budget, falsification and next steps. +The public claim is in +[round-two Discussion1929](https://github.com/CrocSwap/integer-mult-bounds/discussions/1929#discussioncomment-18925867). + +Credit **James Chang** for the generic PR1879/1927 Lean certificate and actual +JSON adapter; **Rohan Arun** for selected PR1094; **Jeremy Kothe** for the T16 +emitter and helper chart construction; **Hao Yan** and the PR484/507/514 +lineage for the retained geometry; and the Lean/Mathlib contributors. PR1831's +source-reviewed route-to-owner census is adjacent work, not a result claimed +again here. The existing emitter/auditor already reconstructs actual sigmas; +our new contribution is separately recovered **formal-interface-format +certificates**, their complete selected binding, independent elimination, and +portable semantic controls. No priority is claimed for the charts, source +construction, orthogonal port formula, or generic rank-one identity. + +Prepared for Adam Gall with substantial **OpenAI Codex GPT-6 Astra** assistance +in research, code and documentation. Apache-2.0. No independent human review +or unseen CI result is claimed. + +### Limitations + +- No Lean executable was found by `command -v lean`, and no cached toolchain + was found in the searched `/tmp/*lean*/`, `~/.elan/toolchains/` or + `~/.cache/*lean*/` locations. No Lean installation, kernel build or axiom + replay was performed. The Python policy is deliberately stricter than the + Lean JSON AST policy for lexical numbers: booleans, floating values and + exponent notation are rejected here. The actual source uses integer arrays. +- This is not a verified JSON byte parser. Python's parser and exact integer + arithmetic remain in this audit's trust base. Duplicate keys fail explicitly; + all consumed archive/source bytes are pinned. The SHA keys are checked, + unlike the generic dictionary adapter, which treats keys only as selectors. +- Complex phases, affine translations, physical executor direction/allocation, + dirty-state execution, whole-call hosting, complete precision/tape invoices, + and all-size multiplication/analytic transfer are not certified. No charge + is waived or declared free. + +## Open next questions + +1. **Can the pinned Lean `certifyEntry` replay accept every supplied five-array + witness?** This would replace the remaining semantic-translation boundary + with actual kernel/interpreter evidence. First materialize the immutable + PR1879/1831/1927 source closure and feed these integer-only JSON values at + dimension73/fuel3, with the same malformed controls. The blocker here is + the absent Lean4.21/Mathlib308445d7 runtime, not missing certificate data. +2. **Which physical executor realizes the derived address pullback and its + inverse for every helper occurrence?** This would connect logical charts to + the implementation. First pin one complete executor and compare its gather + direction and spectator treatment with the receipt's wrong-order witness. + Physical allocation, chart direction, phases and priced memory access are + still separate obligations; this audit supplies no such admission. diff --git a/research/selected-sigma-chart-binding/RESULT.json b/research/selected-sigma-chart-binding/RESULT.json new file mode 100644 index 0000000000..b1ea9d28e6 --- /dev/null +++ b/research/selected-sigma-chart-binding/RESULT.json @@ -0,0 +1,174 @@ +{ + "archive_sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "charts": { + "charts": 10002, + "coefficient_entries": 53300658, + "dimension": 73, + "elimination_inverses": 10002, + "orthogonal_charts": 10002, + "symmetric_transvections": 10002, + "two_sided_basis_compositions": 1460292, + "update_weight_histogram": { + "4": 6612, + "8": 3390 + } + }, + "controls": { + "positive_cases": [ + "identity-3", + "noncommuting-permutation-transvection-3" + ], + "rejected": [ + "boolean-column", + "float-column", + "negative-column", + "out-of-range-column", + "forward-out-of-range", + "bad-update-bit", + "bad-coefficient-bit", + "dictionary-certificate-mismatch", + "inverse-table-mutation", + "coefficient-mutation", + "permutation-direction-reversal", + "extra-certificate-field", + "nonorthogonal-transvection-form", + "singular-elimination", + "duplicate-json-key", + "wrong-content-key", + "missing-live-chart", + "orphan-dictionary-entry", + "changed-spectator-axis" + ], + "wrong_inverse_order_witness": { + "correct_inverse_column": 2128, + "input_axis": 0, + "key": "0008043bb33954fa69e0a93740f44f5a254d1bfb23f1f7b80484527f4d6bf224", + "wrong_order_column": 32 + } + }, + "members": { + "hosted": { + "bytes_sha256": "1ea853d02e3d3377f03761909bf1825bde48431e9e2258303c57c78be12a4b95", + "member": "candidate/strict/global/hosted/HOSTED.json", + "payload_bytes": 2139, + "payload_sha256": "1ea853d02e3d3377f03761909bf1825bde48431e9e2258303c57c78be12a4b95" + }, + "phases": { + "bytes_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "member": "candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json", + "payload_bytes": 814141, + "payload_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "sigmas": { + "bytes_sha256": "f12383eb2691fe33cc9f0525ccb5f6429db6d7bbf0eec76e97f50e752f943dd9", + "member": "candidate/strict/global/hosted/ACTUAL-SIGMAS.json.gz", + "payload_bytes": 9769015, + "payload_sha256": "2cad2187e792fe7c879084a23f15577730ce27e82ff0c341885935c8adffc58f" + }, + "template": { + "bytes_sha256": "2acf02b418078e37090495c601fe550448751d4f35912757b13a1f778efc7760", + "member": "candidate/strict/global/hosted/GLOBAL-TEMPLATE.json.gz", + "payload_bytes": 14139930, + "payload_sha256": "9c4c51425251389ee9a747c465814cd07c64812c15b7aeef704dad7d65395a74" + } + }, + "references": { + "calls": 144, + "first_occurrence": [ + 0, + 0, + 0, + 13006, + "64f754f81e8c82bf94848cd5ad9ec4df0a99aaf0e649819badd6b02434a82498" + ], + "helper_roles": 69120, + "last_occurrence": [ + 8, + 15, + 479, + 13684, + "e0d787884772072e729d0a7fc0b4aa5cd8b5251ae92dc1f912996f0b006209ca" + ], + "missing_entries": 0, + "ordered_sigma_stream_sha256": "e9d95a4a108476a0971d19c8815e1cb747e3b28214b44c92500fdd9647f9bf6d", + "reference_multiplicity_histogram": { + "1": 2257, + "10": 260, + "11": 238, + "12": 207, + "13": 161, + "14": 110, + "15": 96, + "16": 99, + "17": 97, + "18": 85, + "19": 72, + "2": 1737, + "20": 85, + "21": 54, + "22": 27, + "23": 12, + "24": 4, + "25": 13, + "26": 12, + "27": 5, + "28": 55, + "29": 54, + "3": 934, + "30": 111, + "31": 37, + "32": 114, + "33": 12, + "34": 11, + "35": 9, + "36": 12, + "37": 7, + "38": 10, + "39": 1, + "4": 790, + "40": 4, + "41": 6, + "42": 5, + "43": 10, + "44": 9, + "45": 6, + "46": 6, + "47": 7, + "48": 6, + "49": 3, + "5": 536, + "50": 3, + "51": 2, + "52": 4, + "53": 11, + "54": 4, + "55": 10, + "56": 2, + "57": 2, + "58": 7, + "59": 4, + "6": 484, + "60": 5, + "61": 2, + "62": 4, + "63": 3, + "64": 1, + "65": 1, + "7": 363, + "8": 355, + "9": 349 + }, + "unique_references": 10002, + "unreferenced_entries": 0, + "width_histogram": { + "4": 8064, + "5": 4608, + "7": 4320, + "8": 17568, + "9": 34560 + } + }, + "scope": "Exact selected binary-column certificate and helper-reference audit; no Lean build, physical executor, paid-cost or kappa claim.", + "status": "PASS_SELECTED_SIGMA_CHART_BINDING", + "witness_payload_sha256": "1fb840863c3ff869a488d93a4789eabcf56ca3211031fc158aeac14608c318de" +} diff --git a/research/selected-sigma-chart-binding/SELECTION.json b/research/selected-sigma-chart-binding/SELECTION.json new file mode 100644 index 0000000000..cd7da1b679 --- /dev/null +++ b/research/selected-sigma-chart-binding/SELECTION.json @@ -0,0 +1,60 @@ +{ + "seed": "e059d89919a0078380ea43f90a32a2f6", + "track": "independent-verification", + "suggestions": [ + { + "task_id": "formal-interface-lemma", + "scope_key": "e3ffea67887eeb4c396c", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "method": "Audit a formal theorem-to-certificate binding independently.", + "starting_points": ["certificates/selected-result.json", "research/hyperplane-end-lean/PROOF.md"], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": ["python3", "-B", "scripts/research_baseline.py"], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": ["Narrow to one formal lemma or one theorem-to-certificate binding."], + "scope_change_triggers": ["Formalizing already-covered arithmetic and claiming the full multiplication theorem."], + "overlap_terms": ["hyperplane end", "formal interface", "Lean binding"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "independent-moment", + "scope_key": "c191650c0fa8d2fa514e", + "question": "Can one selected pricing or assembly claim be checked by a genuinely independent exact implementation?", + "method": "Implement certified moment inequalities through a different exact enclosure method.", + "starting_points": ["certificates/selected-result.json"], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls.", + "first_step": { + "command": ["python3", "-B", "scripts/research_baseline.py"], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Recompute one small part of the ledger or one certified enclosure using an independent implementation.", + "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."], + "overlap_terms": ["independent moment", "rank histogram", "exact enclosure"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "catalog_assessed_on": "2026-10-13", + "priority_revision": 3, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/selected-sigma-chart-binding/SOURCES.json b/research/selected-sigma-chart-binding/SOURCES.json new file mode 100644 index 0000000000..148447a20f --- /dev/null +++ b/research/selected-sigma-chart-binding/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/community-frontier1094-audit/REPLAY.json", + "usage": "input", + "git_blob": "2cfb7fffa7cd78f418be16c13224c3206b6d0183", + "sha256": "ce0678fa7abaab221de74baeace0c6696d5ea23a36719a58cff230215a06aae7" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/gauge44-slots-t16/code/emit_allcold.py", + "usage": "input", + "git_blob": "28a08a79da911d8f0e16f4bf8df47c580fb6b255", + "sha256": "354367e1fd6185a67b04f4268bcae4d502e47b18cb2131e247f5bcab5b3a769e" + } + ], + "theorem_references": [ + { + "pr": 1879, + "head": "981afe759f7dd206188b1c1a62250c6425bcd76a", + "path": "research/lean-parsed-binary-chart-chain/sources/CheckedBinaryChart.lean", + "declarations": ["Checks", "sourceLinear_eq_checked", "inverse_source", "source_inverse"], + "usage": "Immutable semantic reference, not imported or freshly compiled" + }, + { + "pr": 1879, + "head": "981afe759f7dd206188b1c1a62250c6425bcd76a", + "path": "research/lean-parsed-binary-chart-chain/sources/ParsedBinaryChartCertificate.lean", + "declarations": ["witnessValue", "decodeFields", "certify_sound"], + "usage": "Immutable five-array grammar reference, not imported or freshly compiled" + }, + { + "pr": 1927, + "head": "a5838afac3a2d69d802c2440cbfa7d160ca0b218", + "path": "research/lean-actual-json-format-adapters/sources/JsonPackedColumnDictionary.lean", + "declarations": ["certifyEntry", "certifyEntry_sound", "arbitrary_payload_cancellation"], + "usage": "Immutable selected dictionary adapter reference, not imported or freshly compiled" + } + ], + "overlap": { + "open_prs_fetched_at": "2026-10-14T14:27:47.108625Z", + "open_pr_records": 584, + "discussions_fetched_at": "2026-10-14T14:29:09.251198Z", + "discussion_records": 565, + "complete_pagination": true, + "terms": ["ACTUAL-SIGMAS", "JsonPackedColumnDictionary", "permutation transvection", "binary chart"], + "nearest_results": [1879, 1927], + "distinction": "Both predecessors explicitly leave actual selected dictionary success and the auxiliary witnesses open. PR1831 instead binds owner/route tables and has a separate source-reviewed route transcription census.", + "targeted_live_head_check": "2026-10-14T14:29Z: PR1879, PR1927 and PR1831 remained OPEN at the exact heads above", + "retained_predecessor_check": "Exact ACTUAL-SIGMAS, JsonPackedColumnDictionary, CheckedBinaryChart and permutation/transvection searches over all retained research READMEs, TASK files and the PR ledger returned no prior certificate application package. The existing emitter and native sigma audit are explicitly credited.", + "limitation": "Cached metadata plus targeted live reads and retained notes, not arbitrary diff/code completeness or proof of novelty." + } +} diff --git a/research/selected-sigma-chart-binding/TASK.json b/research/selected-sigma-chart-binding/TASK.json new file mode 100644 index 0000000000..5866eee304 --- /dev/null +++ b/research/selected-sigma-chart-binding/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently recover and check the permutation-plus-transvection five-array certificates for every 73-dimensional ACTUAL-SIGMAS entry in the selected1094 replay, including source-key and referencing closure; characterize any matrices outside this sufficient certificate class.", + "scope_change_reason": "The selected moment and retained HPE pair audits are already covered. PR1879 and PR1927 supply generic formal chart checks but explicitly leave selected artifact success and the auxiliary witnesses uninstantiated. This refines the emitted theorem-to-certificate audit method to that concrete missing application.", + "bottleneck_link": "Closes or precisely bounds the selected binary address-chart certificate gap. This is verification evidence, not a new supplier or exponent saving; all physical, phase, precision, hosting, restoration and runtime charges remain outside this finite audit.", + "budget_minutes": 120, + "stop_rule": "One complete finite census of the selected dictionary. Recover candidates from a nonunit column and all 73 possible output axes; require an exact permutation matching, orthogonality and all coefficients. If any chart is outside the class, prove the finite candidate obstruction rather than weaken the class. No searches over other suppliers.", + "outcome": "completed", + "evidence": "RESULT.json and WITNESSES.json.gz: direct optimized CPython3.12 verification passed with10002 charts,69120 helper roles and19 rejection controls. Every inverse independently computed by elimination. Required working example passed. Registered package replay and environment are recorded in the README.", + "author": "Adam Gall with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex GPT-6 Astra assistance in research, implementation and documentation; no independent human review claimed.", + "open_questions": [ + { + "question": "Can the exact pinned Lean certifyEntry accept all supplied five-array witnesses?", + "why_it_matters": "Removes the remaining Python-to-formal-checker translation boundary for these selected inputs.", + "first_step": "Materialize PR1879/1831/1927 sources, load the supplied integer-only witnesses at n73 and fuel3, and execute the actual checker with the same malformed controls.", + "blocked_by": "Lean4.21/Mathlib308445d7 is absent from this worker; no fresh kernel or interpreter acceptance is claimed." + }, + { + "question": "Which complete physical executor realizes the derived chart pullback at every helper occurrence?", + "why_it_matters": "Logical binary address cancellation alone does not establish physical direction, allocation, phase or priced execution.", + "first_step": "Pin one executor and compare its gather convention and spectators with the source-bound wrong-inverse-order example in RESULT.json.", + "blocked_by": "Physical execution, complex phases, allocation, memory access and complete costs remain separate suppliers." + } + ], + "selection_seed": "e059d89919a0078380ea43f90a32a2f6", + "selection_scope_key": "e3ffea67887eeb4c396c", + "method_domain": "All selected archive ACTUAL-SIGMAS entries, dimension73 over F2; exact integer bit operations, independent elimination, exact coefficient comparison; no floating point.", + "optimistic_full_cost_budget": "No construction change, so no saving or free physical operations are claimed. Selected kappa and every paid profile remain unchanged.", + "success_evidence": "Every dictionary entry and live reference classified, every admitted five-array witness independently checked, both matrix inverse identities, semantic negative controls, registered Python3.12 replay.", + "falsification": "Any source/key/reference mismatch, wrong dimension, singular chart, invalid coefficient/permutation, or incomplete candidate coverage rejects the claimed selected binding.", + "predecessors": [ + {"pr":1879,"head":"981afe759f7dd206188b1c1a62250c6425bcd76a","credit":"James Chang, generic parsed binary chart certificate"}, + {"pr":1927,"head":"a5838afac3a2d69d802c2440cbfa7d160ca0b218","credit":"James Chang, actual JSON dictionary adapter"}, + {"pr":1831,"head":"542f914ca0e5df4026341d08c84385cb1a71cfdf","credit":"James Chang, parsed route-to-owner binding; distinct source-reviewed table census"}, + {"pr":1094,"credit":"Rohan Arun, selected rare-pattern owner overlay; Jeremy Kothe T16 emitter and inherited Hao Yan geometry"} + ] +} diff --git a/research/selected-sigma-chart-binding/VERIFY.json b/research/selected-sigma-chart-binding/VERIFY.json new file mode 100644 index 0000000000..a47b8ecd26 --- /dev/null +++ b/research/selected-sigma-chart-binding/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/REPLAY.json", + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/gauge44-slots-t16/code/emit_allcold.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "All 10002 exact five-array certificates, independent elimination and both inverse laws, all 69120 original helper references, source keys, full closure and 19 rejection controls" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Eight semantic test groups: exhaustive 3D independent recovery oracle and inverses, ordered content keys, JSON/numeric boundary, coefficient index, compression, source drift and all odd non-full port bases" + } + ] +} diff --git a/research/selected-sigma-chart-binding/WITNESSES.json.gz b/research/selected-sigma-chart-binding/WITNESSES.json.gz new file mode 100644 index 0000000000..2306489971 Binary files /dev/null and b/research/selected-sigma-chart-binding/WITNESSES.json.gz differ diff --git a/research/selected-sigma-chart-binding/recover.py b/research/selected-sigma-chart-binding/recover.py new file mode 100755 index 0000000000..6f49996f1d --- /dev/null +++ b/research/selected-sigma-chart-binding/recover.py @@ -0,0 +1,93 @@ +#!/usr/bin/env python3 +"""Recover PR1879 five-array witnesses from the selected raw dictionary only. + +This producer is deliberately not imported by verify.py. No source port basis, +provider recipe or predecessor checker is used to find a factorization. +Prepared for Adam Gall with OpenAI Codex assistance. Apache-2.0. +""" +from __future__ import annotations + +import argparse +import gzip +from pathlib import Path + +from verify import canonical, load_inputs, require + + +def unit_index(value: int) -> int | None: + return value.bit_length() - 1 if value > 0 and value & (value - 1) == 0 else None + + +def recover(columns: list[int]) -> list[list[int]]: + """Find A=(I+u*a^T)P, with a.u=0, using only the packed columns. + + If A is not a permutation, any nonunit column v must be e_i+u. Thus + v+e_i, i=0..n-1, contains every possible u. Each proposed u gives a + bipartite matching problem between columns and coordinate units. A + successful matching explicitly determines P and a. The final checker, + not this search, is the acceptance oracle. + """ + n = len(columns) + anchor = next((v for v in columns if unit_index(v) is None), None) + candidates = [0] if anchor is None else [anchor ^ (1 << i) for i in range(n)] + for update in candidates: + options = [] + for column in columns: + choices = [] + index = unit_index(column) + if index is not None: + choices.append((index, 0)) + index = unit_index(column ^ update) + if index is not None and update: + choices.append((index, 1)) + if not choices: + break + options.append(choices) + if len(options) != n: + continue + owner = [-1] * n + chosen = [None] * n + + def augment(column: int, seen: set[int]) -> bool: + for index, coefficient in options[column]: + if index in seen: + continue + seen.add(index) + if owner[index] < 0 or augment(owner[index], seen): + owner[index] = column + chosen[column] = (index, coefficient) + return True + return False + + if not all(augment(column, set()) for column in range(n)): + continue + forward = [item[0] for item in chosen] + coefficients = sum(item[1] << item[0] for item in chosen) + if (update & coefficients).bit_count() % 2: + continue + backward = [0] * n + for column, index in enumerate(forward): + backward[index] = column + return [forward, backward, columns, + [(update >> i) & 1 for i in range(n)], + [(coefficients >> i) & 1 for i in range(n)]] + raise ValueError("no recovered permutation/transvection certificate; no singularity claim") + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, required=True, + help="New .json.gz file; existing outputs are refused") + args = parser.parse_args() + require(not args.output.exists(), "refusing to replace an existing witness") + values, _ = load_inputs() + entries = {key: recover(columns) for key, columns in sorted(values["sigmas"].items())} + witness = {"format": "pr1879-five-array-chart-witnesses-v1", "dimension": 73, "entries": entries} + payload = canonical(witness) + with args.output.open("xb") as output: + output.write(gzip.compress(payload, mtime=0)) + print(f"RECOVERED_SELECTED_SIGMA_WITNESSES charts={len(entries)} dimension=73 payload_bytes={len(payload)}") + + +if __name__ == "__main__": + main() diff --git a/research/selected-sigma-chart-binding/test_verify.py b/research/selected-sigma-chart-binding/test_verify.py new file mode 100644 index 0000000000..8258dedbcf --- /dev/null +++ b/research/selected-sigma-chart-binding/test_verify.py @@ -0,0 +1,118 @@ +"""Focused exact controls, not a new selected-supplier admission. + +Prepared for Adam Gall with OpenAI Codex assistance. Apache-2.0. +""" +import gzip +import itertools +from pathlib import Path +import tempfile +import unittest +from unittest.mock import patch + +import recover +import verify + + +class ChartTests(unittest.TestCase): + def test_elimination_all_three_dimensional_matrices(self): + invertible = 0 + for columns in itertools.product(range(8), repeat=3): + columns = list(columns) + images = [verify.apply_columns(columns, x) for x in range(8)] + if len(set(images)) < 8: + with self.assertRaises(verify.Rejected): + verify.elimination_inverse(columns) + else: + inverse = verify.elimination_inverse(columns) + invertible += 1 + for x in range(8): + self.assertEqual(verify.apply_columns(inverse, images[x]), x) + self.assertEqual(verify.apply_columns(columns, verify.apply_columns(inverse, x)), x) + self.assertEqual(invertible, 168) + + def test_recovery_against_exhaustive_independent_factor_oracle(self): + # Enumerate factors, rather than using the producer's anchor or matching. + expected = set() + for permutation in itertools.permutations(range(3)): + for update, coefficients in itertools.product(range(8), repeat=2): + if (update & coefficients).bit_count() % 2: + continue + columns = [] + for j in range(3): + basis = [int(i == permutation[j]) for i in range(3)] + value = sum(basis[i] * ((coefficients >> i) & 1) for i in range(3)) % 2 + columns.append(sum((basis[i] ^ (value * ((update >> i) & 1))) << i for i in range(3))) + expected.add(tuple(columns)) + accepted = set() + for columns in itertools.product(range(8), repeat=3): + try: + witness = recover.recover(list(columns)) + except ValueError: + self.assertNotIn(columns, expected) + else: + verify.check_certificate(list(columns), witness, 3) + accepted.add(columns) + self.assertEqual(accepted, expected) + self.assertLess(len(expected), 168) + self.assertGreater(len(expected), 6) + + def test_dictionary_key_binds_order(self): + identity = [1 << i for i in range(verify.N)] + key = verify.digest(verify.canonical(identity)) + entries = {key: recover.recover(identity)} + witnesses = {"format": "pr1879-five-array-chart-witnesses-v1", "dimension": verify.N, "entries": entries} + self.assertEqual(verify.check_dictionary({key: identity}, witnesses)["charts"], 1) + identity[0], identity[1] = identity[1], identity[0] + entries[key] = recover.recover(identity) + with self.assertRaisesRegex(verify.Rejected, "content key"): + verify.check_dictionary({key: identity}, witnesses) + + def test_json_duplicate_and_numeric_policies(self): + with self.assertRaises(verify.Rejected): + verify.decode(b'{"k":0,"k":1}') + with self.assertRaises(verify.Rejected): + verify.decode(b'{"k":NaN}') + for raw in (b"[true]", b"[1.0]", b"[1e0]", b"[-1]", b"[2]"): + with self.assertRaises(verify.Rejected): + verify.vector(verify.decode(raw), 1, 2, "bit") + self.assertEqual(verify.vector(verify.decode(b"[1]"), 1, 2, "bit"), [1]) + + def test_column_coefficient_is_after_permutation(self): + witness = [[1, 2, 0], [2, 0, 1], [1, 4, 2], [1, 1, 0], [1, 1, 0]] + verify.check_certificate(witness[2], witness, 3) + wrongly_indexed = [(1 << witness[0][j]) ^ (3 if witness[4][j] else 0) for j in range(3)] + witness[2] = wrongly_indexed + with self.assertRaisesRegex(verify.Rejected, "coefficient"): + verify.check_certificate(wrongly_indexed, witness, 3) + + def test_compression_headers_are_not_mathematical_identity(self): + value = {"entries": {"k": [[0], [0], [1], [0], [0]]}} + raw = verify.canonical(value) + a, b = gzip.compress(raw, mtime=0), gzip.compress(raw, mtime=1) + self.assertNotEqual(a, b) + self.assertEqual(verify.canonical(verify.decode(gzip.decompress(a))), + verify.canonical(verify.decode(gzip.decompress(b)))) + + def test_source_drift_is_rejected_before_archive_read(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + path = root / "research/community-frontier1094-audit/REPLAY.json" + path.parent.mkdir(parents=True) + path.write_text("{}\n") + with patch.object(verify, "ROOT", root): + with self.assertRaisesRegex(verify.Rejected, "changed source"): + verify.load_inputs() + + def test_all_odd_nonfull_ports_have_exact_orthogonal_bases(self): + for q in range(511): + if q.bit_count() % 2 == 0: + continue + columns = verify.port_basis(q) + inverse = verify.elimination_inverse(columns) + transpose = [sum(((column >> i) & 1) << j for j, column in enumerate(columns)) + for i in range(verify.N)] + self.assertEqual(inverse, transpose) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/selected-sigma-chart-binding/verify.py b/research/selected-sigma-chart-binding/verify.py new file mode 100755 index 0000000000..982969594a --- /dev/null +++ b/research/selected-sigma-chart-binding/verify.py @@ -0,0 +1,381 @@ +#!/usr/bin/env python3 +"""Exact selected1094 binary-chart binding; no supplier or Lean runtime imports. + +Prepared for Adam Gall with substantial OpenAI Codex assistance. Apache-2.0. +The independent checker consumes witnesses; recover.py is not imported. +""" +from __future__ import annotations + +import argparse +from collections import Counter +import copy +import gzip +import hashlib +import json +from pathlib import Path +import tarfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +ARCHIVE = "research/community-frontier1094-audit/selected-replay.tar.gz" +MEMBERS = { + "sigmas": "candidate/strict/global/hosted/ACTUAL-SIGMAS.json.gz", + "template": "candidate/strict/global/hosted/GLOBAL-TEMPLATE.json.gz", + "hosted": "candidate/strict/global/hosted/HOSTED.json", + "phases": "candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json", +} +N = 73 + + +class Rejected(ValueError): + """An exact source, shape, or mathematical obligation failed.""" + + +def require(ok: bool, message: str) -> None: + if not ok: + raise Rejected(message) + + +def digest(data: bytes) -> str: + return hashlib.sha256(data).hexdigest() + + +def canonical(value: object) -> bytes: + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def no_duplicates(items: list[tuple[str, object]]) -> dict: + result = {} + for key, value in items: + require(key not in result, "duplicate JSON object key") + result[key] = value + return result + + +def decode(data: bytes) -> object: + return json.loads(data, object_pairs_hook=no_duplicates, + parse_constant=lambda _: (_ for _ in ()).throw(Rejected("nonfinite JSON"))) + + +def nat(value: object, bound: int, name: str) -> int: + require(type(value) is int and 0 <= value < bound, f"invalid {name}") + return value + + +def vector(value: object, n: int, bound: int, name: str) -> list[int]: + require(type(value) is list and len(value) == n, f"invalid {name} length") + return [nat(x, bound, name) for x in value] + + +def load_inputs() -> tuple[dict, dict]: + sources = decode((PACKAGE / "SOURCES.json").read_bytes()) + for source in sources["files"]: + if source["usage"] == "input": + require(digest((ROOT / source["path"]).read_bytes()) == source["sha256"], + f"changed source: {source['path']}") + values, hashes = {}, {} + with tarfile.open(ROOT / ARCHIVE, "r:gz") as archive: + names = Counter(member.name for member in archive.getmembers()) + for label, name in MEMBERS.items(): + require(names[name] == 1, "archive member missing or duplicated") + member = archive.extractfile(name) + require(member is not None, "archive member is not a file") + raw = member.read() + payload = gzip.decompress(raw) if name.endswith(".gz") else raw + values[label] = decode(payload) + hashes[label] = {"member": name, "bytes_sha256": digest(raw), + "payload_sha256": digest(payload), "payload_bytes": len(payload)} + values["replay"] = decode((ROOT / "research/community-frontier1094-audit/REPLAY.json").read_bytes()) + require(hashes["template"]["payload_sha256"] == values["hosted"]["template_sha256"], + "template/hosted binding") + require(hashes["phases"]["bytes_sha256"] == + values["hosted"]["source_artifacts"]["work/complex-nine-native/DATA-PHASES.json"], + "phase/hosted binding") + require(hashes["phases"]["bytes_sha256"] == values["template"]["exact_data_phase_recipe_sha256"], + "phase/template binding") + return values, hashes + + +def apply_columns(columns: list[int], value: int) -> int: + result = 0 + while value: + bit = value & -value + result ^= columns[bit.bit_length() - 1] + value ^= bit + return result + + +def elimination_inverse(columns: list[int]) -> list[int]: + """Gauss-Jordan on augmented rows, independent of the chart factorization.""" + n = len(columns) + rows = [sum(((column >> i) & 1) << j for j, column in enumerate(columns)) | + (1 << (n + i)) for i in range(n)] + for j in range(n): + pivot = next((i for i in range(j, n) if (rows[i] >> j) & 1), None) + require(pivot is not None, "singular column operator") + rows[j], rows[pivot] = rows[pivot], rows[j] + for i in range(n): + if i != j and (rows[i] >> j) & 1: + rows[i] ^= rows[j] + require(all((row & ((1 << n) - 1)) == 1 << i for i, row in enumerate(rows)), + "elimination did not reach identity") + return [sum(((row >> (n + j)) & 1) << i for i, row in enumerate(rows)) for j in range(n)] + + +def check_certificate(columns: object, certificate: object, n: int) -> tuple[list[int], int, int]: + """Check PR1879's exact five-array obligations, then independent inverses. + + Column j is e_(p[j]) + a[p[j]] u; the coefficient is NOT a[j]. + A = (I + u a^T) P. Thus A^-1 = P^-1 (I + u a^T). + """ + cols = vector(columns, n, 1 << n, "dictionary columns") + require(type(certificate) is list and len(certificate) == 5, "five-array certificate shape") + p = vector(certificate[0], n, n, "forward indices") + backward = vector(certificate[1], n, n, "inverse indices") + witnessed = vector(certificate[2], n, 1 << n, "certificate columns") + ubits = vector(certificate[3], n, 2, "update bits") + abits = vector(certificate[4], n, 2, "coefficient bits") + require(cols == witnessed, "dictionary/certificate columns mismatch") + require(all(backward[p[j]] == j and p[backward[j]] == j for j in range(n)), + "permutation round trip") + u = sum(bit << i for i, bit in enumerate(ubits)) + a = sum(bit << i for i, bit in enumerate(abits)) + require((u & a).bit_count() % 2 == 0, "nonzero form on update") + require(all(cols[j] == ((1 << p[j]) ^ (u if abits[p[j]] else 0)) for j in range(n)), + "serialized coefficient mismatch") + inverse = elimination_inverse(cols) + p_inverse = [1 << i for i in backward] + for j in range(n): + expected = apply_columns(p_inverse, (1 << j) ^ (u if abits[j] else 0)) + require(inverse[j] == expected, "factor inverse differs from elimination") + require(apply_columns(cols, inverse[j]) == 1 << j, "source after inverse") + require(apply_columns(inverse, cols[j]) == 1 << j, "inverse after source") + return inverse, u, a + + +def check_dictionary(sigmas: object, witnesses: object) -> dict: + require(type(sigmas) is dict and type(witnesses) is dict, "dictionary shape") + require(witnesses.get("format") == "pr1879-five-array-chart-witnesses-v1", "witness format") + require(type(witnesses.get("dimension")) is int and witnesses["dimension"] == N, "witness dimension") + entries = witnesses.get("entries") + require(type(entries) is dict and set(entries) == set(sigmas), "witness key coverage") + weights = Counter() + symmetric = 0 + for key in sorted(sigmas): + columns = vector(sigmas[key], N, 1 << N, "dictionary columns") + require(key == digest(canonical(columns)), "dictionary content key mismatch") + inverse, u, a = check_certificate(columns, entries[key], N) + transpose = [sum(((column >> i) & 1) << j for j, column in enumerate(columns)) for i in range(N)] + require(inverse == transpose, "selected chart is not orthogonal") + weights[u.bit_count()] += 1 + symmetric += u == a + return {"charts": len(sigmas), "dimension": N, + "coefficient_entries": len(sigmas) * N * N, + "two_sided_basis_compositions": 2 * len(sigmas) * N, + "elimination_inverses": len(sigmas), "orthogonal_charts": len(sigmas), + "symmetric_transvections": symmetric, + "update_weight_histogram": {str(k): v for k, v in sorted(weights.items())}} + + +def port_basis(q: int) -> list[int]: + """Apply the written rank-one port reflection to coordinate units. + + This is the source's idle chart convention, not a physical executor model. + """ + nat(q, 512, "port label") + require(q != 511 and q.bit_count() % 2 == 1, "port requires odd non-full label") + z = next(i for i in range(9) if not ((q >> i) & 1)) + u = q ^ (1 << z) + axes = [1 << i for i in range(N)] + axes[0], axes[z] = axes[z], axes[0] + return [x ^ (u if (x & u).bit_count() % 2 else 0) for x in axes] + + +def check_references(values: dict) -> dict: + """Bind every helper occurrence to the complete actual dictionary. + + Data-owner routes and private/idle charts are NOT claimed to be dictionary + entries. The emitter populates ACTUAL-SIGMAS only from the 480 helper roles. + """ + sigmas, template, phases, hosted = (values[k] for k in ("sigmas", "template", "phases", "hosted")) + require(template["m"] == N and template["live"] == 14336, "selected dimensions") + calls = template["calls"] + require(type(calls) is list and len(calls) == 144, "selected call count") + require(len(phases["recipes"]) == 112, "phase recipe port coverage") + providers = template["local_providers"] + references, widths, role_keys, occurrences = Counter(), Counter(), set(), [] + stream = hashlib.sha256() + for time, call in enumerate(calls): + stage = nat(call["stage"], 9, "stage") + replica = nat(call["replica"], 16, "replica") + require(call["time"] == time, "call chronological index") + require(call["provider_id"] in providers, "missing provider") + provider = providers[call["provider_id"]] + require((provider["v"], provider["h"], provider["R"]) == (112, 9, 480), "provider dimensions") + require(len(call["owners"]) == 704 and len(provider["widths"]) == 480, "complete owner rows") + for helper, owner in enumerate(call["owners"][224:]): + require(type(owner) is list and len(owner) == 2, "owner pair shape") + family = nat(owner[0], 14336, "family") + route = owner[1] + require(type(route) is list and len(route) in (3, 5), "helper route shape") + typ = nat(route[0], 5, "route tag") + require(typ in (3, 4), "nonhelper route in helper rows") + require(len(route) == (3 if typ == 3 else 5), "route tag/shape mismatch") + offset = nat(route[2], N, "offset") + width = nat(provider["widths"][helper], 10, "helper width") + require(width > 0 and (width == 9) == (typ == 3), "helper width/route tag") + port = family % 112 + q = provider["ports"][port] + recipe = phases["recipes"][port] + require(recipe["port"] == port and recipe["q"] == q, "port/phase correspondence") + child = nat(route[1], len(recipe["idle_children"]), "child") + basis = port_basis(q) + pending = recipe["idle_children"][child]["orthogonal_axes"] + require(offset + width <= len(pending), "pending slice outside child") + axes = pending[offset:offset + width] + lookup = {axis: i for i, axis in enumerate(basis)} + require(all(axis in lookup for axis in axes), "pending axis outside basis") + active = [lookup[axis] for axis in axes] + free = [j for j in range(N) if j not in active] + spectators = free[:9 - width] + if typ == 4: + require(type(route[3]) is int and route[3] == width, "serialized helper width") + supplied = vector(route[4], 9 - width, N, "spectators") + require(supplied == spectators, "spectator order mismatch") + order = active + spectators + free[9 - width:] + require(sorted(order) == list(range(N)), "route is not a coordinate permutation") + columns = [basis[j] for j in order] + key = digest(canonical(columns)) + require(key in sigmas and sigmas[key] == columns, "referenced chart absent or different") + role = (stage, replica, helper) + require(role not in role_keys, "duplicate helper occurrence") + role_keys.add(role) + references[key] += 1 + widths[width] += 1 + record = [stage, replica, helper, family, key] + stream.update(canonical(record) + b"\n") + occurrences.append(record) + require(role_keys == {(s, r, h) for s in range(9) for r in range(16) for h in range(480)}, + "incomplete selected role domain") + require(set(references) == set(sigmas), "unreferenced dictionary entry") + require(stream.hexdigest() == hosted["sigma_stream_sha256"], "ordered occurrence digest mismatch") + require(len(sigmas) == hosted["unique_actual_73column_sigmas"] == values["replay"]["actual_73_axis_charts"], + "selected chart count binding") + require(len(occurrences) == hosted["hosted_residuals"] == values["replay"]["roles"], "selected role count binding") + return {"calls": len(calls), "helper_roles": len(occurrences), "unique_references": len(references), + "unreferenced_entries": 0, "missing_entries": 0, + "ordered_sigma_stream_sha256": stream.hexdigest(), + "width_histogram": {str(k): v for k, v in sorted(widths.items())}, + "reference_multiplicity_histogram": {str(k): v for k, v in sorted(Counter(references.values()).items())}, + "first_occurrence": occurrences[0], "last_occurrence": occurrences[-1]} + + +def controls(values: dict, witnesses: dict) -> dict: + rejected = [] + + def reject(name, action): + try: + action() + except Rejected: + rejected.append(name) + else: + raise Rejected(f"negative control accepted: {name}") + + identity = [list(range(3)), list(range(3)), [1, 2, 4], [0, 0, 0], [0, 0, 0]] + check_certificate([1, 2, 4], identity, 3) + # A three-cycle ensures reversal/direction controls are not involution-blind. + example = [[1, 2, 0], [2, 0, 1], [1, 4, 2], [1, 1, 0], [1, 1, 0]] + check_certificate(example[2], example, 3) + key = next(k for k in sorted(values["sigmas"]) + if witnesses["entries"][k][0] != witnesses["entries"][k][1]) + original = witnesses["entries"][key] + for name, field, index, replacement in [ + ("boolean-column", 2, 0, True), ("float-column", 2, 0, 1.0), + ("negative-column", 2, 0, -1), ("out-of-range-column", 2, 0, 1 << N), + ("forward-out-of-range", 0, 0, N), ("bad-update-bit", 3, 0, 2), + ("bad-coefficient-bit", 4, 0, 2), + ("dictionary-certificate-mismatch", 2, 0, original[2][0] ^ 1), + ("inverse-table-mutation", 1, 0, (original[1][0] + 1) % N), + ("coefficient-mutation", 4, 0, 1 - original[4][0]), + ]: + bad = copy.deepcopy(original) + bad[field][index] = replacement + reject(name, lambda bad=bad: check_certificate(values["sigmas"][key], bad, N)) + bad = copy.deepcopy(original) + bad[0], bad[1] = bad[1], bad[0] + reject("permutation-direction-reversal", lambda: check_certificate(values["sigmas"][key], bad, N)) + reject("extra-certificate-field", lambda: check_certificate(values["sigmas"][key], original + [[]], N)) + singular = [[0, 1, 2], [0, 1, 2], [0, 2, 4], [1, 0, 0], [1, 0, 0]] + reject("nonorthogonal-transvection-form", lambda: check_certificate(singular[2], singular, 3)) + reject("singular-elimination", lambda: elimination_inverse([1, 1, 4])) + reject("duplicate-json-key", lambda: decode(b'{"x":1,"x":2}')) + # A simultaneous change of both source and witness cannot preserve the content key. + fake = {key: list(values["sigmas"][key])} + fake[key][0] ^= 1 + reject("wrong-content-key", lambda: check_dictionary(fake, { + "format": witnesses["format"], "dimension": N, "entries": {key: original}})) + reduced = dict(values) + reduced["sigmas"] = dict(values["sigmas"]) + del reduced["sigmas"][values["first_reference_key"]] + reject("missing-live-chart", lambda: check_references(reduced)) + extra = dict(values) + extra["sigmas"] = dict(values["sigmas"]) + extra["sigmas"]["unreferenced"] = list(range(N)) + reject("orphan-dictionary-entry", lambda: check_references(extra)) + altered = dict(values) + altered["template"] = copy.deepcopy(values["template"]) + route = next(row[1] for row in altered["template"]["calls"][0]["owners"][224:] if row[1][0] == 4) + route[4][0] = (route[4][0] + 1) % N + reject("changed-spectator-axis", lambda: check_references(altered)) + # Show that moving the permutation to the wrong side changes an actual map. + direction_witness = None + for candidate_key in sorted(values["sigmas"]): + candidate = witnesses["entries"][candidate_key] + u = sum(bit << i for i, bit in enumerate(candidate[3])) + a = sum(bit << i for i, bit in enumerate(candidate[4])) + inverse = elimination_inverse(candidate[2]) + for j in range(N): + permuted = 1 << candidate[1][j] + wrong = permuted ^ (u if (permuted & a).bit_count() % 2 else 0) + if inverse[j] != wrong: + direction_witness = {"key": candidate_key, "input_axis": j, + "correct_inverse_column": inverse[j], "wrong_order_column": wrong} + break + if direction_witness: + break + require(direction_witness is not None, "no actual wrong-order separating witness") + return {"positive_cases": ["identity-3", "noncommuting-permutation-transvection-3"], + "rejected": rejected, "wrong_inverse_order_witness": direction_witness} + + +def run() -> dict: + values, hashes = load_inputs() + raw = gzip.decompress((PACKAGE / "WITNESSES.json.gz").read_bytes()) + witnesses = decode(raw) + chart_report = check_dictionary(values["sigmas"], witnesses) + references = check_references(values) + values["first_reference_key"] = references["first_occurrence"][-1] + return {"status": "PASS_SELECTED_SIGMA_CHART_BINDING", "archive_sha256": digest((ROOT / ARCHIVE).read_bytes()), + "members": hashes, "witness_payload_sha256": digest(canonical(witnesses)), + "charts": chart_report, "references": references, "controls": controls(values, witnesses), + "scope": "Exact selected binary-column certificate and helper-reference audit; no Lean build, physical executor, paid-cost or kappa claim."} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path, help="Write a new receipt; refuses an existing file") + args = parser.parse_args() + result = run() + if args.write_receipt: + with args.write_receipt.open("x") as output: + output.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + expected = decode((PACKAGE / "RESULT.json").read_bytes()) + require(canonical(result) == canonical(expected), "receipt differs from exact replay") + print(f"PASS_SELECTED_SIGMA_CHART_BINDING charts={result['charts']['charts']} " + f"dimension={N} helper_roles={result['references']['helper_roles']} " + f"controls={len(result['controls']['rejected'])} no_new_lean_build no_new_kappa") + + +if __name__ == "__main__": + main()