From 19eac371b963b5dd4a3bf2902bca6e3e009758a1 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 10:09:43 +0000 Subject: [PATCH] Record that the 40 frame-0 monomials are not #6030 invoice primitives. The charged polynomial from PR #7031 expands to 40 degree-at-least-2 monomials. The selected invoice names primitives by frame-dimension ranks and ordinary opcodes, and those constructors do not read the chart. Thirty-two exponents miss both histograms, including all six degree-4 masks. No kappa change. Co-authored-by: unpaidmoon --- .../PROOF.md | 156 +++++++++ .../README.md | 112 ++++++ .../SOURCES.json | 48 +++ .../TASK.json | 75 ++++ .../VERIFY.json | 41 +++ .../verify.py | 327 ++++++++++++++++++ 6 files changed, 759 insertions(+) create mode 100644 research/p104-frame0-invoice-primitive-names/PROOF.md create mode 100644 research/p104-frame0-invoice-primitive-names/README.md create mode 100644 research/p104-frame0-invoice-primitive-names/SOURCES.json create mode 100644 research/p104-frame0-invoice-primitive-names/TASK.json create mode 100644 research/p104-frame0-invoice-primitive-names/VERIFY.json create mode 100644 research/p104-frame0-invoice-primitive-names/verify.py diff --git a/research/p104-frame0-invoice-primitive-names/PROOF.md b/research/p104-frame0-invoice-primitive-names/PROOF.md new file mode 100644 index 0000000000..5bcc858f6c --- /dev/null +++ b/research/p104-frame0-invoice-primitive-names/PROOF.md @@ -0,0 +1,156 @@ +# The 40 frame-0 monomials are not primitives of the selected invoice + +No new κ. The selected record stays `781451/250000000`. This note answers the +naming step left open by PR #7031: whether the 40 charged monomials can be +named as primitives on the selected #6030 invoice. They cannot, under the +naming rules that invoice actually uses. The missing obligation is one total +map that those rules accept. This is not a comparison with the selected +profile, and it is not a claim that no future contract could name the +monomials. + +## 1. The 40 monomials + +PR #7031 charges the degree-at-least-2 terms of + +```text +(1 + x0)(1 + x1 + x2 + x4)(1 + x5)(1 + x6 + x7) +``` + +in the square-free ring `F_2[x0,...,x7]/(x_i^2 = x_i)`. The four factors use +disjoint variables, so the expansion is the Cartesian product of the summands. +That domain has `2 · 4 · 2 · 3 = 48` elements, every product is distinct, and +there is no cancellation. The degrees are 1, 7, 17, 17, and 6 in degrees 0 +through 4. The eight monomials of degree at most 1 are `1, x0, x1, x2, x4, +x5, x6, x7`. The other 40 are the charged monomials. + +The SHA256 of the 48 sorted exponent integers, joined by commas, is + +```text +26803d29aa3141a357da4aa551195fe6378d3f2e1cba0c4291a4dedbce6ded2a +``` + +which is the normal-form hash recorded by the #7031 verifier at head +`531ecca652dde63c6010cd6097cb55a994367ce7`. This note does not replay that +pull request's hosting census. It takes this polynomial as the charged object. + +An exponent is the integer whose bit `i` is the factor `x_i`. The six +degree-4 exponents are `99, 101, 113, 163, 165, 177`, namely + +```text +x0*x1*x5*x6, x0*x2*x5*x6, x0*x4*x5*x6, +x0*x1*x5*x7, x0*x2*x5*x7, x0*x4*x5*x7. +``` + +## 2. What the selected invoice calls a primitive + +The selected record points at +`research/p104-helper470-twin-rung-removal/RESULT.json`. Its word has schema +`p104-accumulated-block-composition/2`. A recursive primitive on that invoice +is a pair `(side, rank)` produced by one of the following constructors, as +written in `local.py` `replay` and `pricing.py` `assemble`. + +- A `MOVE` from frame `a` to frame `b` has local paid rank `|dim b - dim a|`, + where the dimension is the length of the stored basis. +- A non-main public helper has local target rank `dim(final) - dim(initial)`. +- Eighteen forward `LOCAL` calls repeat both local histograms. +- Fifteen query shears add paid rank `1`, with count `104` each. +- For each idle length `L` in `{7, 8}` and each `j = 1, ..., L`, the assembly + adds paid rank `8(j+1)` and target rank `1 + 8(j+1)`, with count `208`. +- One further target of rank `145` is added with count `208`. + +Replaying every `MOVE` and every non-main helper of the selected word, then +applying this finite formula, reproduces `RESULT.json` `local.paid`, +`local.helpers`, `complete_cost.paid`, and `complete_cost.targets`. The paid +keys are + +```text +1, 2, 3, 4, 5, 6, 7, 8, 16, 24, 32, 40, 48, 56, 64, 72. +``` + +The target keys are + +```text +1, 2, 3, 4, 5, 6, 7, 8, 9, 17, 25, 33, 41, 49, 57, 65, 73, 145. +``` + +The ordinary names on the same word are the opcodes that occur: `ADD`, +`CLEAR`, `COPY`, `INIT`, `MOVE`, and `SCALE`. Each acts on a role index and, +for a scalar event, a dyadic coefficient. The assembly text and the replay +text do not mention a chart variable, a polynomial degree, or a monomial. + +The native routine in `local.py` builds Clifford recipes from frame charts +and ports. It is not replayed here. Its inputs are those frames and ports, +not the 40 exponents, so it does not assign these monomials names either. + +## 3. Readings that still do not name all 40 + +A naming, in the sense asked by #7031, would be a total function from the 40 +exponents to this alphabet that the constructors above determine. The +readings that use only an integer or a string already attached to the +monomial fail. + +**Exponent integer as a histogram key.** Of the 40 exponents, exactly three +are paid keys: `3, 5, 48`. Exactly seven are target keys: `3, 5, 17, 33, 49, +65, 145`. The union has eight exponents, so 32 exponents are keys of neither +side. The two exponents `3` and `5` are keys of both sides, so the integer +does not choose a unique primitive even in the collisions. All six degree-4 +exponents lie in the 32. This is an exhaustive check of a 40-element set +against the two finite key sets. + +**Printed name as an opcode.** None of the 40 strings `x0*x1`, ... equals +`ADD`, `CLEAR`, `COPY`, `INIT`, `MOVE`, or `SCALE`. + +**Exponent integer as a selected port.** The word stores 104 ports, and the +local native check identifies the initial frame of each live line with the +singleton `[port]`. Exactly 14 of the 40 exponents occur in that port list: +`35, 37, 49, 69, 81, 98, 100, 112, 131, 133, 145, 161, 164, 176`. The other +26 do not. This reading does not name all 40. + +**Degree as rank.** The degrees that occur are 2, 3, and 4, and each of those +integers is both a paid key and a target key. That numerical fact is not a +name. Neither constructor reads a degree. Calling these monomials `H_2`, +`H_3`, and `H_4` would be a new tariff. This note does not adopt that tariff +and does not claim that every future contract must reject it. + +## 4. The chart is not the invoice coordinate system + +The same integer can appear in both lists without being the same object. +The hosting word of #7031 uses ports `11, 21, 38, 140`. Their simple-root +labels, with the ninth coordinate set, are `282, 284, 270, 454`. None equals +its port, and none is one of the 40 exponents (every charged exponent is at +most `177`). The invoice frames are vectors in the port-space `F_2^9`. The +monomials are functions of the simple-root coordinates. An exponent that +happens to equal a port, or a frame basis vector, is not that port and not +that vector. + +For the record, 34 of the 40 exponent integers occur somewhere in the stored +frame bases, and the six that do not are exactly the degree-4 exponents. +That census is not a naming: a basis vector is not a primitive of the +invoice, and the two coordinate systems are distinct. + +## 5. The obstruction + +Under the constructors in section 2, the selected invoice does not determine +a total function from these 40 exponents to its primitive alphabet. The +missing obligation is that function, together with a proof that an inherited +constructor, or a stated extension of one, sends each exponent to the image +it names. Until the function exists, these 40 monomials are not primitives +on the selected invoice. + +No profile comparison is made. The other twelve frames are not expanded. +The selected κ is unchanged. This is not a proof that the monomials cannot +be named by a different contract, and it is not a proof that no function +into the alphabet exists. Many functions exist. None is fixed by the +invoice that was asked about. + +## Evidence class + +The expansion is an exhaustive census of a 48-element product, complete +because the factors are disjoint and every combination is enumerated. The +histogram identity is an exhaustive replay of the finite selected word plus +the finite assembly formula, matched to the selected receipt. The three +failed readings are exhaustive checks of the same 40 exponents against +finite sets. The refusal of the degree reading is the observation that the +constructor texts do not read a degree. Together this is a scoped proof and +an exhaustive finite census. It is not a heuristic and not an incomplete +search inside those readings. diff --git a/research/p104-frame0-invoice-primitive-names/README.md b/research/p104-frame0-invoice-primitive-names/README.md new file mode 100644 index 0000000000..1e54f0ff56 --- /dev/null +++ b/research/p104-frame0-invoice-primitive-names/README.md @@ -0,0 +1,112 @@ +# The 40 frame-0 monomials are not selected-invoice primitives + +**No new κ.** The selected frontier stays `781451/250000000`. This package +asks whether the 40 monomials charged by open PR #7031 can be named as +primitives on the selected #6030 invoice. Under that invoice's constructors, +they cannot. The missing map is stated in [PROOF.md](PROOF.md). Naming them +would not by itself be a κ change, and this obstruction is not one either. + +## Result + +The charged polynomial is + +```text +(1 + x0)(1 + x1 + x2 + x4)(1 + x5)(1 + x6 + x7). +``` + +Its 40 degree-at-least-2 monomials are the object #7031 asked to place on +the invoice. A recursive primitive of the selected invoice is a pair +`(side, rank)` built from frame-dimension gaps, eighteen local copies, +fifteen query shears, the idle lengths 7 and 8, and one rank-145 target. +Ordinary names on the same word are the opcodes `ADD`, `CLEAR`, `COPY`, +`INIT`, `MOVE`, and `SCALE`. Those constructors do not read a chart monomial. + +Against that alphabet: + +- 32 of the 40 exponent integers are keys of neither histogram. The six + degree-4 masks `99, 101, 113, 163, 165, 177` are among them. +- The eight integers that do collide are not unique names. Masks `3` and `5` + are both paid keys and target keys. +- No printed monomial equals an opcode. +- 14 exponent integers occur in the selected port list, and 26 do not. +- Degrees 2, 3, and 4 are histogram keys, but the constructors do not set + rank equal to degree. That reading is not adopted. + +The chart is a different coordinate system from the invoice. The simple-root +labels of ports `11, 21, 38, 140` are `282, 284, 270, 454`, not the ports +themselves. An integer collision with a port or a frame vector is not an +identification. + +## Evidence class + +The product expansion is an exhaustive 48-element census. The invoice +histograms are an exhaustive replay of the selected word, matched to +`RESULT.json`. The failed readings are exhaustive checks of the 40 +exponents. The degree reading is refused because the constructor texts do +not mention it. This is a scoped proof together with those censuses. It is +not a heuristic, not a search over arbitrary maps, and not a proof that +another contract could not name the monomials. + +## Scope + +Catalogue card `complex-rank-shape-decoder`, priority revision 8, pinned at +`17469fff78c22941280f04d39dc5a1faee09c840`. The card asks whether a decoder +or coframe change improves the signed moment. Scope is **changed** to the +naming step in open question 3 of +[#7031](https://github.com/CrocSwap/integer-mult-bounds/pull/7031). The +connection to the bottleneck is in [TASK.json](TASK.json): a thirteen-row +comparison with the selected profile is not available until each charged +monomial has a primitive name, and this package stops when that name is +shown to be missing. + +The selected record, `upstream/`, and the #6030 word are inputs, not edits. +Open #7031 already hosted the row and charged the 40 monomials; this package +does not redo that hosting. It does not host frame 1, and it does not ask +whether a sum of letters can use fewer than 40 monomials. + +Overlap searched on 2026-11-10: the open-PR search for this naming returned +only #7031, whose discussion finding +[19514167](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19514167) +leaves the naming open. No fork branch had taken the question. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3 -B research/p104-frame0-invoice-primitive-names/verify.py +python3 -I -O -B research/p104-frame0-invoice-primitive-names/verify.py +python3 -B scripts/research_package.py --package research/p104-frame0-invoice-primitive-names +python3 -B scripts/check_research_commit.py --package research/p104-frame0-invoice-primitive-names --check-source-history +``` + +The verifier prints `PASS_P104_FRAME0_INVOICE_NAMES` with `monomials=40`, +`outside_both_histograms=32`, `degree4_outside=6`, and the unchanged κ. +Failure controls drop the factor `x0`, accept mask `99` as a paid rank, and +replace the 18 local copies by 17. + +Not run: `make frontier6030-verify`, the native Clifford replay, Lean, and +any expansion of frames 1–12. + +## Open next questions + +1. Give a total map from these 40 exponents to the inherited primitive + alphabet that one of the selected constructors determines. The + thirteen-row comparison stays blocked until that map exists. The first + step is to make one constructor read one of these exponents, or to show + that a constructor already does, and then check the image of all 40. + The present constructors read frame dimensions, idle lengths, and a + diagonal popcount only. + +The thirteen-row profile comparison is not opened. Frames 1–12 remain the +separate hosting question already stated by #7031, and a missing name for +these 40 blocks that comparison on its own. + +## Credit + +The 40 monomials and the factored word: unpaidmoon, PR #7031. The selected +invoice and word: DreamingOfClouds, PR #6030, on the PR #5827 verifier chain. +Ports and the odd-graph line map: PR #6933. Prepared by unpaidmoon with +substantial Cursor Grok assistance. New work is Apache-2.0. + +Workflow note: https://github.com/CrocSwap/integer-mult-bounds/discussions/1200 diff --git a/research/p104-frame0-invoice-primitive-names/SOURCES.json b/research/p104-frame0-invoice-primitive-names/SOURCES.json new file mode 100644 index 0000000000..4df2c300f2 --- /dev/null +++ b/research/p104-frame0-invoice-primitive-names/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper470-twin-rung-removal/RESULT.json", + "usage": "input", + "git_blob": "e4a03118d585fb80c9ac932281b528ac394ccc5f", + "sha256": "84fcbe2a0b64307b5703c363408042bdd91555b0419509aa50daa43b3b1924ad" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + }, + { + "path": "research/p104-helper470-twin-rung-removal/pricing.py", + "usage": "input", + "git_blob": "65bb723f8558dc60ff92764db1a43d8bf438aa09", + "sha256": "3c6cf2966ccfe5a5fb6c90f89f46ac224ea455127e35dd34975683c68c36d710" + }, + { + "path": "research/p104-port-window-haemers/data/e8_line_map.json", + "usage": "input", + "git_blob": "19ea2d553aff60e53af50dd9582ab70730e93450", + "sha256": "b37530e8e9b2b3bd5be418d5ed3060a42ceb66e60ed3789f8ee79f29dabde437" + }, + { + "path": "research/p104-unread-path-resynthesis/local.py", + "usage": "input", + "git_blob": "b7be846b10c4c54a4e1558d7b563bc8c3a170223", + "sha256": "7201df8e32f5c99f7403150e8664042322037906088bc754c67293a241368597" + } + ] +} diff --git a/research/p104-frame0-invoice-primitive-names/TASK.json b/research/p104-frame0-invoice-primitive-names/TASK.json new file mode 100644 index 0000000000..ee35096be5 --- /dev/null +++ b/research/p104-frame0-invoice-primitive-names/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Can the 40 degree-at-least-2 monomials of the #7031 frame-0 word be named as primitives on the selected #6030 invoice, under the constructors that invoice uses?", + "scope_change_reason": "The card asks whether a decoder or coframe change improves the full signed moment. Open PR #7031, question 3, asks a prior naming question: place its 40 charged monomials on the selected #6030 invoice before any profile comparison. This package answers only that naming question.", + "bottleneck_link": "A thirteen-row comparison with the selected profile is not available until each charged monomial has a primitive name on the #6030 invoice. The inherited constructors do not assign those names, so the comparison stays blocked and no kappa is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop when each of the 40 monomials has an inherited primitive name, or when the inherited constructors are shown not to determine such a name. Do not compare thirteen rows with the selected profile and do not change kappa.", + "outcome": "negative-result", + "evidence": "PROOF.md and verify.py. The expansion and the three failed readings are exhaustive finite censuses. The invoice histograms are rebuilt from the selected word. The degree reading is refused because the constructor texts do not read a degree. This is a scoped obstruction, not a kappa.", + "author": "unpaidmoon, with substantial Cursor Grok assistance", + "ai_assistance": "Substantial Cursor Grok assistance. No subagents. The selected word, the PR5827 replay rule, and the #7031 polynomial are used as pinned inputs.", + "open_questions": [ + { + "question": "Which total function from these 40 exponents to the inherited (side, rank) alphabet do the selected constructors determine?", + "why_it_matters": "No comparison of thirteen frame rows with the selected profile is available until every charged monomial has one primitive name.", + "first_step": "Make one rank constructor read one of these exponents, or show that a constructor already does, and check the image of all 40.", + "blocked_by": "The present constructors read frame dimensions, idle lengths, query shears, and one diagonal popcount. They do not read a chart monomial." + } + ] +} diff --git a/research/p104-frame0-invoice-primitive-names/VERIFY.json b/research/p104-frame0-invoice-primitive-names/VERIFY.json new file mode 100644 index 0000000000..ee50366022 --- /dev/null +++ b/research/p104-frame0-invoice-primitive-names/VERIFY.json @@ -0,0 +1,41 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "checks": "Charged expansion, rebuilt #6030 histograms, and the failed naming readings, with failure controls.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "checks": "The same naming obstruction under optimization. Checks raise SystemExit rather than using assertions.", + "timeout_seconds": 120 + } + ], + "inputs": [ + "certificates/selected-result.json", + "research/p104-helper470-twin-rung-removal/RESULT.json", + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-helper470-twin-rung-removal/pricing.py", + "research/p104-port-window-haemers/data/e8_line_map.json", + "research/p104-unread-path-resynthesis/local.py" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-frame0-invoice-primitive-names/verify.py b/research/p104-frame0-invoice-primitive-names/verify.py new file mode 100644 index 0000000000..7d004cbcc8 --- /dev/null +++ b/research/p104-frame0-invoice-primitive-names/verify.py @@ -0,0 +1,327 @@ +#!/usr/bin/env python3 +"""Name the 40 frame-0 monomials against the selected #6030 invoice. + +The charged polynomial is the disjoint-variable form recorded by PR #7031. +The selected invoice names a recursive primitive by a ledger side and a +positive rank. Those ranks are rebuilt from the selected word. None of the +inherited constructors reads a chart monomial, and the readings that use only +the monomial's own integers do not place all 40 on a unique primitive. + +Standard library only. Checks raise SystemExit, so python -O still runs them. +No kappa is computed. +""" + +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction +from itertools import combinations, product +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +WORD = ROOT / "research/p104-helper470-twin-rung-removal/WORD.json.gz" +RESULT = ROOT / "research/p104-helper470-twin-rung-removal/RESULT.json" +PRICING = ROOT / "research/p104-helper470-twin-rung-removal/pricing.py" +LOCAL = ROOT / "research/p104-unread-path-resynthesis/local.py" +LINE_MAP = ROOT / "research/p104-port-window-haemers/data/e8_line_map.json" +SELECTED = ROOT / "certificates/selected-result.json" + +ANF_SHA256 = "26803d29aa3141a357da4aa551195fe6378d3f2e1cba0c4291a4dedbce6ded2a" +DEGREE4_OUTSIDE = (99, 101, 113, 163, 165, 177) +HOST_PORTS = (11, 21, 38, 140) +HOST_LABELS = {11: 282, 21: 284, 38: 270, 140: 454} +KAPPA = "781451/250000000" + + +def need(condition, message): + if not condition: + raise SystemExit(message) + + +def expect_fail(function, message): + try: + function() + except SystemExit: + return + raise SystemExit(message) + + +def monomial_name(exponent): + return "*".join("x{0}".format(index) for index in range(8) if exponent >> index & 1) + + +def expand_charged_polynomial(): + """Cartesian product of the four disjoint factors. Size 2*4*2*3 = 48.""" + factors = ( + (0, 1 << 0), + (0, 1 << 1, 1 << 2, 1 << 4), + (0, 1 << 5), + (0, 1 << 6, 1 << 7), + ) + need(len(factors[0]) * len(factors[1]) * len(factors[2]) * len(factors[3]) == 48, + "the charged product is not the 48-element domain") + counts = Counter() + for parts in product(*factors): + mask = 0 + for part in parts: + mask |= part + counts[mask] += 1 + need(max(counts.values()) == 1 and len(counts) == 48, + "disjoint factors cancelled or collided") + exponents = tuple(sorted(counts)) + payload = ",".join(str(exponent) for exponent in exponents) + need(hashlib.sha256(payload.encode()).hexdigest() == ANF_SHA256, + "charged normal form does not match the #7031 hash") + degrees = dict(Counter(exponent.bit_count() for exponent in exponents)) + need(degrees == {0: 1, 1: 7, 2: 17, 3: 17, 4: 6}, + "degree counts changed: {0}".format(degrees)) + new = tuple(exponent for exponent in exponents if exponent.bit_count() >= 2) + need(len(new) == 40, "expected 40 degree-at-least-2 monomials") + need(tuple(exponent for exponent in exponents if exponent.bit_count() <= 1) + == (0, 1, 2, 4, 16, 32, 64, 128), + "the degree-at-most-1 complement changed") + return new + + +def load_json(path): + raw = path.read_bytes() + if path.suffix == ".gz": + raw = gzip.decompress(raw) + return json.loads(raw.decode()) + + +def rebuild_invoice(word): + paid = Counter() + for event in word["program"]: + if event[0] != "MOVE": + continue + _op, _role, source, destination, _private = event + paid[abs(len(word["frames"][destination]) - len(word["frames"][source]))] += 1 + live = set(word["live"]) + main = live | {role + 112 for role in live} + helpers = Counter() + for role in range(word["public"]): + if role not in main: + helpers[len(word["frames"][word["final"][role]]) + - len(word["frames"][word["initial"][role]])] += 1 + targets = Counter({rank: 18 * count for rank, count in helpers.items()}) + full_paid = Counter({rank: 18 * count for rank, count in paid.items()}) + targets[145] += 208 + full_paid[1] += 15 * 104 + for length in (7, 8): + for step in range(1, length + 1): + targets[1 + 8 * (step + 1)] += 208 + full_paid[8 * (step + 1)] += 208 + return paid, helpers, full_paid, targets + + +def integer_keys(histogram): + return {int(rank): count for rank, count in histogram.items()} + + +def simple_basis(): + basis = [ + (1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0), + (-2, 2, 0, 0, 0, 0, 0, 0), + ] + for index in range(1, 6): + vector = [0] * 8 + vector[index] = -2 + vector[index + 1] = 2 + basis.append(tuple(vector)) + return basis + + +def root_dot(left, right): + return sum(entry * other for entry, other in zip(left, right)) // 4 + + +def label_of(root): + basis = simple_basis() + matrix = list(zip(*basis)) + rows = [[Fraction(matrix[row][column]) for column in range(8)] + [Fraction(root[row])] + for row in range(8)] + for column in range(8): + pivot = next(row for row in range(column, 8) if rows[row][column]) + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = 1 / rows[column][column] + rows[column] = [entry * scale for entry in rows[column]] + for row in range(8): + if row != column and rows[row][column]: + factor = rows[row][column] + rows[row] = [rows[row][index] - factor * rows[column][index] + for index in range(9)] + coordinates = [rows[index][8] for index in range(8)] + need(all(entry.denominator == 1 for entry in coordinates), + "simple-root coordinates are not integral") + bits = 0 + for index, value in enumerate(coordinates): + if int(value) & 1: + bits |= 1 << index + return bits | (1 << 8) + + +def classify(monomials, paid_keys, target_keys, opcodes, ports): + rows = [] + for exponent in monomials: + rows.append({ + "exponent": exponent, + "degree": exponent.bit_count(), + "name": monomial_name(exponent), + "paid_key": exponent in paid_keys, + "target_key": exponent in target_keys, + "opcode": monomial_name(exponent) in opcodes, + "port": exponent in ports, + }) + return rows + + +def require_constructors(pricing, local): + needles = ( + "paid[abs(len(w['frames'][b])-len(w['frames'][a]))] += 1", + "second_p[1] += 15*104", + "second_t[145] += 208", + "for length in (7,8):", + "second_p[8*(j+1)] += 208", + "second_t[1+8*(j+1)] += 208", + "second_t = Counter({r:18*n for r,n in local['helpers'].items()})", + "second_p = Counter({r:18*n for r,n in local['paid'].items()})", + ) + for needle in needles: + need(needle in pricing or needle in local, "missing inherited constructor: " + needle) + replay, _separator, _rest = local.partition("def reverse_columns") + need("def replay" in replay, "local replay function missing") + need("x0" not in replay and "degree" not in replay and "monomial" not in replay, + "the local replay reads a chart monomial") + assemble, _separator, _rest = pricing.partition("def run") + need("def assemble" in assemble, "pricing assembly missing") + need("x0" not in assemble and "degree" not in assemble and "monomial" not in assemble, + "the invoice assembly reads a chart monomial") + need("need(w['frames'][w['initial'][r]] == [q], 'Literal central port')" in local, + "literal central-port frame is not the inherited port name") + + +def run_controls(monomials, paid_keys, word): + def dropped_factor(): + factors = ((0,), (0, 1 << 1, 1 << 2, 1 << 4), (0, 1 << 5), (0, 1 << 6, 1 << 7)) + found = set() + for parts in product(*factors): + mask = 0 + for part in parts: + mask |= part + if mask.bit_count() >= 2: + found.add(mask) + need(len(found) == 40, "dropping x0 still leaves 40 monomials") + + expect_fail(dropped_factor, "dropping the x0 factor still charged 40 monomials") + + def degree4_is_paid(): + need(DEGREE4_OUTSIDE[0] in paid_keys, "mask 99 became a paid rank") + + expect_fail(degree4_is_paid, "degree-4 mask 99 was accepted as a paid rank") + + def wrong_local_multiplier(): + paid = Counter() + for event in word["program"]: + if event[0] == "MOVE": + paid[abs(len(word["frames"][event[3]]) - len(word["frames"][event[2]]))] += 1 + forged = Counter({rank: 17 * count for rank, count in paid.items()}) + expected = Counter() + for event in word["program"]: + if event[0] == "MOVE": + expected[abs(len(word["frames"][event[3]]) - len(word["frames"][event[2]]))] += 1 + expected = Counter({rank: 18 * count for rank, count in expected.items()}) + need(forged == expected, "a 17-fold local bill matched the 18-fold bill") + + expect_fail(wrong_local_multiplier, "changing 18 LOCAL copies was not detected") + need(all(monomial_name(exponent) not in {"ADD", "SCALE", "MOVE", "COPY", "INIT", "CLEAR"} + for exponent in monomials), + "a chart monomial was stored as an opcode") + + +def main(): + monomials = expand_charged_polynomial() + word = load_json(WORD) + result = load_json(RESULT) + selected = load_json(SELECTED) + need(word["schema"] == "p104-accumulated-block-composition/2", "unexpected word schema") + need(selected["kappa"] == KAPPA, "selected kappa changed") + need(selected["source_certificate"] == "research/p104-helper470-twin-rung-removal/RESULT.json", + "selected source certificate is not the #6030 result") + need(hashlib.sha256(RESULT.read_bytes()).hexdigest() == selected["source_certificate_sha256"], + "RESULT.json is not the selected source certificate") + local_paid, helpers, full_paid, targets = rebuild_invoice(word) + need(dict(local_paid) == integer_keys(result["local"]["paid"]), + "rebuilt local paid histogram disagrees with RESULT.json") + need(dict(helpers) == integer_keys(result["local"]["helpers"]), + "rebuilt helper histogram disagrees with RESULT.json") + need(dict(full_paid) == integer_keys(result["complete_cost"]["paid"]), + "rebuilt paid invoice disagrees with RESULT.json") + need(dict(targets) == integer_keys(result["complete_cost"]["targets"]), + "rebuilt target invoice disagrees with RESULT.json") + opcodes = {event[0] for event in word["program"]} + need(opcodes == {"ADD", "CLEAR", "COPY", "INIT", "MOVE", "SCALE"}, + "ordinary opcode alphabet changed: {0}".format(sorted(opcodes))) + require_constructors(PRICING.read_text(encoding="utf-8"), LOCAL.read_text(encoding="utf-8")) + + paid_keys = set(full_paid) + target_keys = set(targets) + ports = set(word["ports"]) + need(len(ports) == 104, "the selected word does not carry 104 ports") + rows = classify(monomials, paid_keys, target_keys, opcodes, ports) + paid_hits = [row["exponent"] for row in rows if row["paid_key"]] + target_hits = [row["exponent"] for row in rows if row["target_key"]] + either = [row["exponent"] for row in rows if row["paid_key"] or row["target_key"]] + both = [row["exponent"] for row in rows if row["paid_key"] and row["target_key"]] + port_hits = [row["exponent"] for row in rows if row["port"]] + opcode_hits = [row["name"] for row in rows if row["opcode"]] + need(paid_hits == [3, 5, 48], "paid-key collisions changed: {0}".format(paid_hits)) + need(target_hits == [3, 5, 17, 33, 49, 65, 145], + "target-key collisions changed: {0}".format(target_hits)) + need(both == [3, 5], "two-sided collisions changed") + need(len(either) == 8 and len(rows) - len(either) == 32, "histogram coverage changed") + degree4 = tuple(row["exponent"] for row in rows if row["degree"] == 4) + need(degree4 == DEGREE4_OUTSIDE, "degree-4 masks changed") + need(all(exponent not in paid_keys and exponent not in target_keys + for exponent in DEGREE4_OUTSIDE), + "a degree-4 mask became a histogram key") + need(opcode_hits == [], "an opcode reading named a monomial") + need(port_hits == [35, 37, 49, 69, 81, 98, 100, 112, 131, 133, 145, 161, 164, 176], + "port-integer collisions changed") + need(len(port_hits) == 14, "port reading unexpectedly named every monomial") + frame_vectors = {vector for frame in word["frames"] for vector in frame} + frame_hits = [row["exponent"] for row in rows if row["exponent"] in frame_vectors] + need(len(frame_hits) == 34, "frame-vector integer collisions changed") + need(tuple(exponent for exponent in DEGREE4_OUTSIDE if exponent not in frame_vectors) + == DEGREE4_OUTSIDE, + "a degree-4 exponent occurred as a frame vector") + + line_map = load_json(LINE_MAP) + roots = {vector: tuple(root) for vector, root in zip(line_map["vectors"], line_map["roots2"])} + labels = {} + for port in HOST_PORTS: + labels[port] = label_of(roots[port]) + need(labels == HOST_LABELS, "simple-root labels of the hosting ports changed: {0}".format(labels)) + need(all(label not in set(monomials) and label != port for port, label in labels.items()), + "a hosting-port label collapsed onto its port or onto a charged mask") + # The eight simple-root coordinates are not the nine port-space bits. + basis_dots = [root_dot(left, right) & 1 + for left, right in combinations(simple_basis(), 2)] + need(any(basis_dots), "the simple-root chart was treated as an orthonormal port basis") + + run_controls(monomials, paid_keys, word) + print( + "PASS_P104_FRAME0_INVOICE_NAMES monomials=40 outside_both_histograms=32 " + "degree4_outside=6 paid_collisions=3 target_collisions=7 opcode_hits=0 " + "port_collisions=14 kappa={0}".format(KAPPA) + ) + for row in rows: + print("MONOMIAL {exponent} deg={degree} {name} paid_key={paid_key} " + "target_key={target_key} port_integer={port}".format(**row)) + + +if __name__ == "__main__": + main()