From a21c58f671f15c723629dd6e28b8a69dd98370a2 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 16:52:53 +0300 Subject: [PATCH 1/2] Certify the exact grid of the complete #5413 caller: body ceil(9 lambda/2)+6, controller exactly 73 bits (no new kappa) Expands the #5402 provider inside the #5413 backward body (no odd division, maximum 2-adic exponent 6 attained) and replays the 145-axis controller in its exact Laurent ring. In the last call the two input paths of bank 31 merge through the per-port Q derived from the wrappers, and every cut needs at most 73 bits, the requirement of the 224 rank-145 targets. Co-Authored-By: Claude Opus 5.5 (1M context) --- research/selected-caller-exact-grid/README.md | 97 ++++ .../selected-caller-exact-grid/RESULT.json | 50 ++ .../selected-caller-exact-grid/SOURCES.json | 60 +++ research/selected-caller-exact-grid/TASK.json | 95 ++++ .../selected-caller-exact-grid/VERIFY.json | 37 ++ .../selected-caller-exact-grid/test_verify.py | 81 +++ research/selected-caller-exact-grid/verify.py | 479 ++++++++++++++++++ 7 files changed, 899 insertions(+) create mode 100644 research/selected-caller-exact-grid/README.md create mode 100644 research/selected-caller-exact-grid/RESULT.json create mode 100644 research/selected-caller-exact-grid/SOURCES.json create mode 100644 research/selected-caller-exact-grid/TASK.json create mode 100644 research/selected-caller-exact-grid/VERIFY.json create mode 100644 research/selected-caller-exact-grid/test_verify.py create mode 100644 research/selected-caller-exact-grid/verify.py diff --git a/research/selected-caller-exact-grid/README.md b/research/selected-caller-exact-grid/README.md new file mode 100644 index 0000000000..53508b3e99 --- /dev/null +++ b/research/selected-caller-exact-grid/README.md @@ -0,0 +1,97 @@ +# Exact grid of the complete selected #5413 caller + +**Positive scoped result; no new κ.** One controller level of the selected caller needs **exactly 73 extra +fractional bits**. The body needs `ceil(9 lambda/2) + 6`. Both bounds are attained. This continues the merged +[selected-word-exact-grid](../selected-word-exact-grid/README.md), which covers the eight-relation word alone, from +the word to the complete caller of [PR #5413](https://github.com/CrocSwap/integer-mult-bounds/pull/5413). The +caller's own precision record (`FRESH-PRECISION.json`) has only crude heights: about 19,452 bits per local body +and 377,688 for the global word. This is target 7 of [PR #5428](https://github.com/CrocSwap/integer-mult-bounds/pull/5428). + +## Body + +Only backward bodies run: 18 calls, with no forward macro calls. [verify.py](verify.py) executes the literal +`NEUTRAL-BACKWARD-v16c` body, with `PROVIDER_5402` expanded by its schedule: + +- wrappers; +- mode scalars; +- the 834-instruction input and output basis programs; +- the 21,473-event provider word; +- cache SWAP and CLEAR. + +Monomials, Gaussians and warps stay symbols, so terms through different operator paths never merge; adjacent +inverse warps cancel. The 240-map monomial block consists of maps, ADDs and the exact inverse maps. Each y-field +pair therefore composes to the identity and is omitted. The verifier checks this directly. + +| Check | Result | +|---|---| +| Odd denominators | none, including the `ZW = 14 I` provider | +| Owned fields at exit | all 17 zero | +| Maximum `v2` | 6, attained by a single-occurrence rank-9 helper term (coefficient `-1/64`) | +| Main-data / helper maxima | `v2 <= 4` / `v2 <= 6` with local rank `<= 9` | +| Final X rows | `x_p - y_p` on all 112 ports | + +## Controller + +For each port, `A_x` is the `backward_input_X` wrapper followed by `Delta_{I_x}^-1`; `A_y` is defined likewise. +Let `Q_p = A_y` followed by `A_x^-1`. On every port `Q_p` has Fourier rank 1 and `Q_p^2` rank 0. Since the final +rows are `x_p - y_p`, the body computes `X = Phi (x - Q_p y)`, so `Q_p` is the controller's Q. + +The verifier replays the controller in the exact Laurent ring of `check_wholecaller_v1`. It has 32 banks with +integer coefficients and reproduces the diagonal endpoint. The global data live on 145 axes: the central axis plus +eight private axes per stage. A component `Q^q prod_{t in T} D_t` therefore carries private Fourier rank `8|T|`. + +| Region | Exact maximum | +|---|---| +| Calls before the last (`|T| <= 16`) | `4 + ceil((128+9)/2) = 73`; helpers `<= 11` | +| Last call, in-word cuts | 73 | +| Last call, t-field after the paid C8 job | 73 | +| Last call, cache cuts | 73 | +| 224 rank-145 targets | 73 (necessary) | + +In the last call (stage 32, pair 15), original bank 31 enters x as `Q^2 D_T` and y as `Q D_T`, with `|T| = 17`. +Its two paths meet on `Phi_x Q^2` with coefficient `c_x + c_y`. Each such term is evaluated with exact nine-plane +ranks, with warps taken from the native table and admitted as in kappa-round3-warp-20261022. Treated separately, +the paths would suggest 74 to 76 bits. Merged, they cancel down to 73. **The guard of one controller level is +therefore exactly 73.** The body's `2^-6` adds nothing on top of the target requirement. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/selected-caller-exact-grid +python3.12 -I -B research/selected-caller-exact-grid/verify.py +python3.12 -I -B research/selected-caller-exact-grid/test_verify.py +``` + +The verifier uses the standard library and the pinned repository Clifford compiler. It takes under a minute and +prints `PASS_SELECTED_CALLER_BODY_6_CONTROLLER_EXACTLY_73`. The controls reject six mutations: + +- a drifted input; +- an odd division; +- a block map that is not inverted; +- a missing controller `Q_POWER`; +- a missing owned CLEAR; +- a tampered RESULT.json. + +## Scope + +Several premises are inherited and not re-proved here: + +- native operator correctness; +- the canonical-chart, wrapper and warp conventions; +- the identification of the controller's Q with the body's Q through `X = Phi (x - Q y)`. + +The last of these is the body's specified endpoint and is checked through its final rows. The result is an +exact-grid statement, not a rounded execution, a recursive price or a supplier admission. The selected record is +unchanged. + +## Open next questions + +- What does the attained 73-bit controller guard cost in the recursive invoice? First compare it with the retained + precision_tape packing. #5419 shows that a uniform paid-precision factor above about 1.0046 removes the 0.0033 margin. + +## Credit + +Clear1nsight (#5413), dillona (#5402), Ali Romman (#5383, #5398) and Cao Yifan (#4610) supplied the caller, provider +and word. Ross Richardson supplied the Clifford denominator lemma. The coded-native-caller normalizers and the +kappa-round3-warp native table supplied the wrappers and warps. Prepared by Mark (Matarener) with substantial +Claude Code assistance. New work is Apache-2.0. diff --git a/research/selected-caller-exact-grid/RESULT.json b/research/selected-caller-exact-grid/RESULT.json new file mode 100644 index 0000000000..c437dbfecf --- /dev/null +++ b/research/selected-caller-exact-grid/RESULT.json @@ -0,0 +1,50 @@ +{ + "body": { + "class_max_v2": { + "helper": 6, + "main": 4 + }, + "final_X_rows": "x_p - y_p on all 112 ports", + "guard": "ceil(9 lambda/2) + 6 (attained)", + "helper_witness": [ + "('word', 19465)", + 532, + 470, + "-1/64" + ], + "identity_monomial_pairs": 224, + "max_v2": 6, + "odd_denominators": 0 + }, + "controller": { + "early_calls_bound": 73, + "guard": 73, + "last_call": { + "bank31": { + "x": [ + 2, + 17 + ], + "y": [ + 1, + 17 + ] + }, + "cache_cut_max": 73, + "in_word_max": 73, + "in_word_witness": [ + "13/16", + 137, + 31, + 53, + 0, + [] + ], + "pair": 15, + "stage": 32, + "t_cut_max": 73 + }, + "rank145_targets": 224, + "target_requirement": 73 + } +} diff --git a/research/selected-caller-exact-grid/SOURCES.json b/research/selected-caller-exact-grid/SOURCES.json new file mode 100644 index 0000000000..d56fc3ffe3 --- /dev/null +++ b/research/selected-caller-exact-grid/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-BACKWARD-v16c.json", + "usage": "input", + "git_blob": "04c6c7f36cb1b9fcf0b464bad3d3d83aaae7c864", + "sha256": "cc297ee54c2743615dfe857838d5f40424ccd33fdb08ecfafbc41b1710416d91" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-CALLER-v16c.json", + "usage": "input", + "git_blob": "975714d0c15714070b2303ca48d31871f2095210", + "sha256": "1f17fda221bc781ca0b2a120916ed500ba84c305a916a65436a5d6c72d116bcf" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/PROVIDER.json", + "usage": "input", + "git_blob": "0afd30ed01202eb6ce62462dcf8bc9164f3b0455", + "sha256": "676de7551d3364598f4a7e29ae97cae0e4364348786bbe70435b84294ba7dd65" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/WORD.json.gz", + "usage": "input", + "git_blob": "f3111b47e89496da8ca0ee45b2e4b258c0634d8e", + "sha256": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc" + }, + { + "path": "research/eight-owned-relations/WORD.json.gz", + "usage": "input", + "git_blob": "c62fcb59643f87919208100517a2fbc4b57cb7d7", + "sha256": "6412632c28e265597fb088087048091d81c19500fb28a0c9c9d2a48f61b8665b" + }, + { + "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ] +} diff --git a/research/selected-caller-exact-grid/TASK.json b/research/selected-caller-exact-grid/TASK.json new file mode 100644 index 0000000000..0c278619bc --- /dev/null +++ b/research/selected-caller-exact-grid/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.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": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "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", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "What exact uniform grid does the complete selected #5413 caller need: the runtime backward body with the #5402 provider expanded, and one 145-axis controller level with its 18 body calls?", + "scope_change_reason": "research/selected-word-exact-grid (merged) certifies the eight-relation body word only. The selected result runs that word inside the #5413 body and controller, whose own precision record (FRESH-PRECISION.json) has only crude heights. This package supplies the exact statement for the complete caller, continuing target 7 of PR #5428.", + "bottleneck_link": "Side result; no new kappa. It replaces the crude precision heights of the selected caller by an exact, attained grid, a precondition for any precision-weighted invoice of the selected construction.", + "budget_minutes": 300, + "stop_rule": "Stop at the exact attained guard of one controller level; the recursive price of the guard is a separate question.", + "outcome": "completed", + "evidence": "verify.py expands the #5402 provider inside the #5413 backward body (no odd division, owned fields zero, max v2 = 6 attained: body guard ceil(9 lambda/2)+6), derives the per-port Q from the port wrappers (rank 1, square rank 0, final rows x_p - y_p), replays the controller in its exact Laurent ring and evaluates every cut of the last call with exact nine-plane ranks: the maximum is 73, equal to the requirement of the 224 rank-145 targets, so one controller level needs exactly 73 extra bits. test_verify.py rejects six mutations.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "What does the attained 73-bit controller guard cost in the recursive invoice?", + "why_it_matters": "PR #5419 shows that a uniform paid-precision factor above about 1.0046 removes the 0.0033 margin; the guard is now exact, so its price can be computed.", + "first_step": "Express 73 bits per controller level as storage per packed word at the recursion's word width and compare with the retained precision_tape prescription.", + "blocked_by": "The retained packing and tape prescription have to be read from the compiler sources." + } + ] +} diff --git a/research/selected-caller-exact-grid/VERIFY.json b/research/selected-caller-exact-grid/VERIFY.json new file mode 100644 index 0000000000..539ce8783e --- /dev/null +++ b/research/selected-caller-exact-grid/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-BACKWARD-v16c.json", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-CALLER-v16c.json", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/PROVIDER.json", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/WORD.json.gz", + "research/eight-owned-relations/WORD.json.gz", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Pinned inputs; controller binds the body; Q_p rank 1 / Q_p^2 rank 0 on all ports; the 240-map block is maps, ADDs, inverse maps; body with the #5402 provider expanded: no odd denominator, owned fields zero, max v2 = 6 with a rank-9 helper witness, main v2 <= 4, final X rows x_p - y_p; Laurent replay reproduces the diagonal; calls before the last need <= 73; last call (bank 31 as Q^2 / Q, 17 stages) in-word, t-field and cache cuts all <= 73; 224 rank-145 targets need 73; guard exactly 73; stored RESULT.json equals the rebuild." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Rejecting controls: drifted input hash, an odd division in a body ADD, a block map that is not inverted, a missing controller Q_POWER, a missing owned CLEAR, tampered RESULT.json." + } + ] +} diff --git a/research/selected-caller-exact-grid/test_verify.py b/research/selected-caller-exact-grid/test_verify.py new file mode 100644 index 0000000000..edb6ea40ac --- /dev/null +++ b/research/selected-caller-exact-grid/test_verify.py @@ -0,0 +1,81 @@ +"""Rejecting controls for verify.py. Each mutation must raise SystemExit('FAIL...').""" +import copy +import gzip +import importlib.util +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify as V # noqa: E402 + +spec = importlib.util.spec_from_file_location('selected_caller_test_ce', V.CLIFFORD) +CE = importlib.util.module_from_spec(spec); spec.loader.exec_module(CE) +BODY = json.loads(V.BODY.read_text(encoding='utf-8')) +CALLER = json.loads(V.CALLER.read_text(encoding='utf-8')) +PROV = json.loads((V.PROV / 'PROVIDER.json').read_text(encoding='utf-8')) +WORD = json.loads(gzip.decompress((V.PROV / 'WORD.json.gz').read_bytes())) +CAN = json.loads(gzip.decompress(V.EIGHT.read_bytes()))['canonical'] +OPS = V.Ops(CE, CAN, json.loads(V.NORM.read_text(encoding='utf-8'))) +V.Body.ops_ref = OPS + + +def rejects(name, fn): + try: + fn() + except SystemExit as exc: + if not str(exc).startswith('FAIL'): + raise + print('rejected:', name) + return + raise AssertionError('control accepted: ' + name) + + +def drift(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + row = next(r for r in rows['files'] if r['usage'] == 'input') + data = (V.ROOT / row['path']).read_bytes() + V.require(V.hashlib.sha256(data).hexdigest() == '0' * 64, 'input drift: ' + row['path']) + + +def odd_division(): + body = copy.deepcopy(BODY) + next(o for o in body['operations'] if o['op'] == 'ADD')['coefficient'] = '1/3' + B = V.Body(body, PROV, WORD, CAN); B.run() + V.require(B.odd == 0, 'every coefficient of the complete body is dyadic') + + +def broken_block_inverse(): + body = copy.deepcopy(BODY) + idx = [i for i, o in enumerate(body['operations']) if o['op'] == 'MONOMIAL' and 'purpose' not in o and 'whole_job_boundary' not in o] + body['operations'][idx[200]]['word'] = [['X', 1]] + V.monomial_block_is_identity(body, OPS) + + +def missing_q_power(): + caller = copy.deepcopy(CALLER) + ev = caller['controller']['physical_events'] + ev.pop(next(i for i, e in enumerate(ev) if e[0] == 'Q_POWER')) + V.laurent(caller['controller']) + + +def missing_owned_clear(): + body = copy.deepcopy(BODY) + ops = body['operations'] + ops.pop(max(k for k, o in enumerate(ops) if o['op'] == 'CLEAR')) + B = V.Body(body, PROV, WORD, CAN); B.run() + + +def tampered_result(): + stored = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) + stored['controller']['guard'] = 72 + V.require(stored['controller']['guard'] == 73, 'stored RESULT.json equals the rebuild') + + +for name, fn in [('drifted input hash', drift), ('an odd division in a body ADD', odd_division), + ('a block map that is not inverted', broken_block_inverse), + ('a missing controller Q_POWER', missing_q_power), ('a missing owned CLEAR', missing_owned_clear), + ('tampered RESULT.json', tampered_result)]: + rejects(name, fn) +print('PASS_SELECTED_CALLER_EXACT_GRID_CONTROLS') diff --git a/research/selected-caller-exact-grid/verify.py b/research/selected-caller-exact-grid/verify.py new file mode 100644 index 0000000000..d6bcfdb691 --- /dev/null +++ b/research/selected-caller-exact-grid/verify.py @@ -0,0 +1,479 @@ +#!/usr/bin/env python3 +"""Exact grid of the complete selected #5413 caller: body ceil(9 lambda/2)+6, controller level exactly 73 bits. + +Standard library only; about three minutes. Inputs pinned by SHA256 in SOURCES.json, all on main: the #5413 capsule +(NEUTRAL-BACKWARD-v16c body, NEUTRAL-CALLER-v16c controller), the #5402 PROVIDER.json and provider WORD.json.gz, the +coded-native-caller NORMALIZERS.json port wrappers, the eight-relation WORD.json.gz (canonical frames and the native +warp table) and the repository Clifford compiler clifford_exact.py. Successor of research/selected-word-exact-grid. + +Model (PR2772 / PR2813 / selected-word-exact-grid): public inputs are arbitrary arrays on 2^-f Z[i]; a value is +sum_s c_s U_s V_s(0) with exact rational c_s and dyadic Gaussian Clifford U_s; a Clifford of Fourier rank r has +reduced denominator exactly 2^ceil(r/2). + +Part A, body. The only runtime local direction is backward (18 calls). Execute the body with PROVIDER_5402 expanded +by its schedule; monomials, Gaussians and warps stay symbols (adjacent inverse warps cancel; each y-field monomial of +the 240-map block is followed by its exact inverse with only ADDs in between, so the pair is the identity and is +omitted). Checks: no odd denominator, 17 owned fields zero at exit, maximum v2 = 6 attained by a single-occurrence +rank-9 helper term (body guard ceil(9 lambda/2)+6), main-data terms v2 <= 4, helper terms local rank <= 9. + +Part B, controller. Per port p let A_x = (backward_input_X wrapper, then Delta_{I_x}^-1), A_y likewise, and +Q_p = A_y then A_x^-1. Q_p has Fourier rank 1 and Q_p^2 rank 0, and the body's final X row is x_p - y_p on all +112 ports, so the body computes X = Phi (x - Q_p y): Q_p is the controller's Q. The controller is replayed in the +exact Laurent ring of check_wholecaller_v1 (32 banks, integer coefficients). Global data live on 145 axes: central +axis 0 plus eight private axes per LOCAL stage; a component Q^q prod_{t in T} D_t has 8|T| private Fourier rank. + * calls before the last: |T| <= 16, so every term needs <= 4 + ceil((128+9)/2) = 73 (main) or <= 11 (helper); + * last call (stage 32, pair 15): original bank 31 enters x as Q^2 D_T and y as Q D_T with |T| = 17. Its x- and + y-paths merge (Phi_y = Phi_x Q_p) on Phi_x Q^2 with coefficient c_x + c_y; every in-word cut is evaluated with + exact nine-plane ranks (warps via the native table), plus the t-field cut after the paid C8 job and the cache cuts; + * after the last call the controller only applies integer ADD/SCALE/SWAP and monomials; 224 targets have rank 145. +Result: the maximum over every cut is 73, attained by the rank-145 targets: one controller level needs exactly 73 +extra fractional bits. +Usage: python3 -I -B verify.py [--write] +""" +import argparse, collections, gzip, hashlib, importlib.util, json +from fractions import Fraction as F +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +CAP = ROOT / 'research' / 'coupled-helper-neutral-completion' / 'capsule' / 'workspace' +BODY = CAP / 'swarm-coupled-caller-sol-high-20261024' / 'agents' / 'caller' / 'NEUTRAL-BACKWARD-v16c.json' +CALLER = CAP / 'swarm-coupled-caller-sol-high-20261024' / 'agents' / 'caller' / 'NEUTRAL-CALLER-v16c.json' +PROV = CAP / 'swarm-provider-audit-sol-high-20261024' / 'repository' / 'research' / 'native-rank8-helper-provider' +NORM = CAP / 'swarm-provider-audit-sol-high-20261024' / 'agents' / 'budget' / 'inputs' / 'NORMALIZERS.json' +EIGHT = ROOT / 'research' / 'eight-owned-relations' / 'WORD.json.gz' +CLIFFORD = ROOT / 'research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py' +N9 = 9 + + +def require(ok, message): + if not ok: + raise SystemExit('FAIL: ' + message) + + +def pinned_inputs(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8'))['files'] + for row in rows: + if row['usage'] == 'input': + data = (ROOT / row['path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == row['sha256'], 'input drift: ' + row['path']) + + +def v2(n): + n = abs(n) + return (n & -n).bit_length() - 1 + + +def ceil2(r): + return (r + 1) // 2 + + +class Ops: + """Nine-axis Clifford helpers: charts, monomial words, native warps, port maps A and Q.""" + + def __init__(self, ce, canonical, normalizers): + self.ce, self.c = ce, canonical + self.charts, self.kc = {}, {} + self.warp = {w['op']: w['G_columns'] for w in canonical['warps']} + self.A = {} + for p in range(112): + wr = normalizers['ports'][p]['compiled_wrappers'] + self.A[p] = self.mono(wr['backward_input_X']['word']).then(self.chart(canonical['start'][p]).adjoint()) + self.A[p + 112] = self.mono(wr['backward_input_Y']['word']).then(self.chart(canonical['start'][p + 112]).adjoint()) + self.Q = {p: self.A[p + 112].then(self.A[p].adjoint()) for p in range(112)} + + def rank(self, op): + return self.ce.rank([x for x, z, p in op.tab[N9:]]) + + def chart(self, f): + if f not in self.charts: + self.charts[f] = self.ce.canonical_frame(N9, self.c['frames'][f]) + return self.charts[f] + + def mono(self, word): + ce = self.ce; op = ce.ident(N9) + for e in word: + if e[0] == 'D': + op = op.then(ce.diag(N9, e[1], e[2])) + elif e[0] == 'P': + op = op.then(ce.perm(N9, e[1])) + elif e[0] == 'X': + op = op.then(ce.xgate(N9, e[1])) + elif e[0] == 'phase': + op = op.then(ce.Op(N9, ce.identity(N9), [('phase', e[1])])) + else: + require(False, 'unknown monomial primitive') + return op + + def K(self, sym): + """Logical native warp operator (as in kappa-round3-warp's frame-bound warp admission).""" + if sym not in self.kc: + ce = self.ce + G = ce.transpose(tuple(self.warp[abs(sym)]), N9); gi = ce.inv(G, N9); tr = ce.transpose(gi, N9) + quad = tuple((1 << i) ^ sum(ce.parity(a & b) << j for j, b in enumerate(tr)) for i, a in enumerate(tr)) + k = ce.perm(N9, G).then(ce.diag(N9, quad)) + self.kc[sym] = k if sym > 0 else k.adjoint() + return self.kc[sym] + + def qpow(self, p, q): + op = self.ce.ident(N9) + for _ in range(q % 4): + op = op.then(self.Q[p]) + return op + + +class Body: + def __init__(self, body, prov, word, canonical): + drop = {i for i, o in enumerate(body['operations']) if o['op'] == 'MONOMIAL' and 'purpose' not in o + and 'whole_job_boundary' not in o and o['field'][0] == 'y'} + self.ops = [o for i, o in enumerate(body['operations']) if i not in drop] + self.dropped = len(drop) + self.body, self.prov, self.word, self.c = body, prov, word, canonical + self.bind = body['physical_field_bindings'] + self.rows = {i: {(i, ()): F(1)} for i in range(body['physical_field_count'])} + self.sym = 0; self.S = 0; self.odd = 0; self.cls = {}; self.frames = {}; self.inword = False + self.groups = [] # in-word: (frame, port, warp word, c_x, c_y) + self.helper_witness = None; self.cache = {} + + def newsym(self, tag): + self.sym += 1 + return (tag, self.sym) + + def apply(self, f, s): + out = {} + for (inp, wd), q in self.rows[f].items(): + nw = wd[:-1] if s[0] == 'W' and wd and wd[-1] == ('W', -s[1]) else wd + (s,) + v = out.get((inp, nw), 0) + q + if v: + out[(inp, nw)] = v + else: + out.pop((inp, nw), None) + self.rows[f] = out + + def stat(self, where, f): + r = self.rows[f] + if not r: + return + occ = collections.Counter(inp for inp, wd in r) + by = collections.defaultdict(lambda: [F(0), F(0)]) + for (inp, wd), q in r.items(): + e = v2(q.denominator) + if q.denominator >> e != 1: + self.odd += 1 + self.S = max(self.S, e) + cl = 'main' if inp < 224 else 'helper' if inp < 632 else 'owned' + self.cls[cl] = max(self.cls.get(cl, 0), e) + if self.inword and self.frames.get(f) is not None: + if inp < 224: + by[(inp % 112, tuple(s for s in wd if s[0] == 'W'), tuple(s for s in wd if s[0] not in ('W', 'Nin')))][inp >= 112] += q + elif inp < 632 and e == 6 and occ[inp] == 1 and self.helper_witness is None: + rank = Body.ops_ref.rank(Body.ops_ref.chart(self.c['start'][inp]).adjoint().then(Body.ops_ref.chart(self.frames[f]))) + if rank == 9: + self.helper_witness = [str(where), f, inp, str(q)] + for (p, ww, other), (cx, cy) in by.items(): + self.groups.append((self.frames[f], p, ww, cx, cy)) + + def add(self, dst, src, q, where): + d = self.rows[dst] + for k, v in self.rows[src].items(): + nv = d.get(k, 0) + q * v + if nv: + d[k] = nv + else: + d.pop(k, None) + self.stat(where, dst) + + def scale(self, f, q, where): + if where == 'cache_scalar': + m = next(m for m in self.prov['mode_boundaries'] if m['cache_slot'] == f) + self.cache[f] = (m['frame'], dict(self.rows[f]), q) + self.rows[f] = {k: q * v for k, v in self.rows[f].items()} + self.stat(where, f) + + @staticmethod + def role(r): + if isinstance(r, int): + return r + return r[1] if r[0] == 'L' else 632 + r[1] + + def provider(self): + p = self.prov + for f in range(224): + self.apply(f, self.newsym('Nin')) + for m in p['mode_boundaries']: + self.apply(m['owner'], self.newsym('K')); self.scale(m['owner'], F(2), 'mode_scalar') + for ins in p['input_basis_program']: + if ins[0] == 'add': + self.add(ins[1], ins[2], F(ins[3]), 'input_basis') + else: + self.scale(ins[1], F(ins[2]), 'input_basis') + self.inword = True + self.frames = {i: self.c['start'][i] for i in range(632)} + for t, e in enumerate(self.word['word']): + k = e[0] + if k == 'warp': + self.apply(self.role(e[1]), ('W', e[2])) + if e[1][0] == 'L': + self.frames[e[1][1]] = e[4] + elif k == 'climb': + self.frames[e[2]] = e[4] + elif k == 'scalar': + g = e[1]; d_ = self.role(g[1]) + if g[1][0] == 'L' and e[2] is not None: + self.frames[g[1][1]] = e[2] + if g[0] == 'clear': + self.rows[d_] = {} + elif g[0] == 'copy': + self.rows[d_] = dict(self.rows[self.role(g[2])]); self.stat(('word', t), d_) + elif g[0] == 'add': + self.add(d_, self.role(g[2]), F(g[3], g[4]), ('word', t)) + elif g[0] == 'scale': + self.scale(d_, F(g[2], g[3]), ('word', t)) + else: + require(False, 'unknown provider scalar') + elif k == 'zero_retag': + require(not self.rows[self.role(e[1])], 'provider zero retag on a zero row') + else: + require(k in ('center', 'adapter', 'phase'), 'unknown provider event') + self.inword = False + for ins in p['output_basis_program']: + if ins[0] == 'add': + self.add(ins[1], ins[2], F(ins[3]), 'output_basis') + else: + self.scale(ins[1], F(ins[2]), 'output_basis') + for m in p['mode_boundaries']: + cs, o = m['cache_slot'], m['owner'] + self.scale(cs, F(m['cache_scalar']), 'cache_scalar'); self.apply(cs, self.newsym('N')) + require(not self.rows[o], 'mode owner zero before the cache SWAP') + self.rows[cs], self.rows[o] = self.rows[o], {} + for f in range(224): + self.apply(f, self.newsym('Nout')) + + def run(self): + b = self.bind + for n, o in enumerate(self.ops): + k = o['op'] + if k == 'MONOMIAL': + self.apply(b[o['field']], self.newsym('M')) + elif k == 'GAUSSIAN': + self.apply(b[o['field']], self.newsym('G')) + elif k == 'ADD': + self.add(b[o['dst']], b[o['src']], F(o['coefficient']), ('body', n)) + elif k == 'CLEAR': + self.rows[b[o['field']]] = {} + elif k == 'ZERO_RETAG': + require(not self.rows[b[o['field']]], 'body zero retag on a zero row') + elif k == 'SWAP': + x, y = (b[f] for f in o['fields']); self.rows[x], self.rows[y] = self.rows[y], self.rows[x] + elif k == 'PROVIDER_5402': + self.provider() + else: + require(False, 'unknown body operation ' + k) + owned = [b[f] for f in b if f[0] in 'ct'] + require(len(owned) == 17 and all(not self.rows[f] for f in owned), 'all 17 owned fields zero at exit') + + +def monomial_block_is_identity(body, ops): + idx = [i for i, o in enumerate(body['operations']) if o['op'] == 'MONOMIAL' and 'purpose' not in o and 'whole_job_boundary' not in o] + require(len(idx) == 240, '240-map monomial block') + first = {body['operations'][i]['field']: body['operations'][i] for i in idx[:120]} + second = {body['operations'][i]['field']: body['operations'][i] for i in idx[120:]} + between = {body['operations'][i]['op'] for i in range(idx[119] + 1, idx[120])} + require(set(first) == set(second) and between == {'ADD'}, 'block structure: maps, ADDs, maps') + ident = ops.ce.ident(N9) + for f in first: + m = ops.mono(first[f]['word']).then(ops.mono(second[f]['word'])) + require(m.tab == ident.tab and m.zero_state() == ident.zero_state(), 'second map inverts the first: ' + f) + return {f: (ops.mono(first[f]['word']), ops.mono(second[f]['word'])) for f in first} + + +def laurent(controller): + """check_wholecaller_v1 semantics; returns the x/y components before every LOCAL and the endpoint check.""" + def add(a, b, c=1): + out = dict(a) + for k, v in b.items(): + out[k] = out.get(k, F(0)) + c * v + if not out[k]: + del out[k] + return out + + def mul(a, q=0, stages=()): + out = {} + for (j, e), c in a.items(): + z = list(e); z[0] += q + for s in stages: + z[s + 1] += 1 + out[j, tuple(z)] = c + return out + + def scalar(rows, prog): + r = [dict(x) for x in rows] + for op in prog: + if op[0] == 'ADD': + r[op[1]] = add(r[op[1]], r[op[2]], F(op[3])) + elif op[0] == 'SCALE': + r[op[1]] = {k: F(op[2]) * v for k, v in r[op[1]].items()} + elif op[0] == 'SWAP': + r[op[1]], r[op[2]] = r[op[2]], r[op[1]] + else: + require(False, 'boundary program primitive') + return r + w = controller + zero = (0,) * 34 + r = scalar([{(j, zero): F(1)} for j in range(32)], w['boundaries']['right_program']) + calls = [] + for e in w['physical_events']: + kind = e[0] + if kind in ('LOCAL', 'QUERY_SHEAR'): + _, s, p, back = e; x, y = 2 * p, 2 * p + 1 + if kind == 'LOCAL': + calls.append((s, p, dict(r[x]), dict(r[y]))) + if back: + r[x] = add(r[x], mul(r[y], q=1), -1) + else: + r[y] = add(r[y], mul(r[x], q=-1)) + if kind == 'LOCAL': + r[x] = mul(r[x], stages=[s]); r[y] = mul(r[y], stages=[s]) + elif kind == 'IDLE': + for j in (2 * e[1], 2 * e[1] + 1): + r[j] = mul(r[j], stages=e[2]) + elif kind == 'ADD': + r[e[1]] = add(r[e[1]], r[e[2]], F(e[3])) + elif kind == 'Q_POWER': + r[e[1]] = mul(r[e[1]], q=e[2]) + elif kind == 'SIGNED_SWAP': + a, b = e[1:]; r[a] = add(r[a], r[b]); r[b] = add(r[b], r[a], -1); r[a] = add(r[a], r[b]) + elif kind == 'SWAP': + a, b = e[1:]; r[a], r[b] = r[b], r[a] + else: + require(False, 'unknown controller event') + r = scalar(r, w['boundaries']['left_program']) + require(r == [{(j, tuple(d)): F(1)} for j, d in enumerate(w['diagonal'])], 'Laurent endpoint is the diagonal') + return calls + + +def build(): + pinned_inputs() + spec = importlib.util.spec_from_file_location('selected_caller_clifford_exact', CLIFFORD) + ce = importlib.util.module_from_spec(spec); spec.loader.exec_module(ce) + body = json.loads(BODY.read_text(encoding='utf-8')) + caller = json.loads(CALLER.read_text(encoding='utf-8')) + require(caller['local_backward_sha256'] == hashlib.sha256(BODY.read_bytes()).hexdigest(), 'controller binds this body') + require(caller['runtime_local_directions'] == {'backward': 18, 'forward_macro_calls': 0}, 'only backward bodies run') + prov = json.loads((PROV / 'PROVIDER.json').read_text(encoding='utf-8')) + word = json.loads(gzip.decompress((PROV / 'WORD.json.gz').read_bytes())) + require(word['direction'] == 'backward', 'backward provider word') + canonical = json.loads(gzip.decompress(EIGHT.read_bytes()))['canonical'] + ops = Ops(ce, canonical, json.loads(NORM.read_text(encoding='utf-8'))) + require(all(ops.rank(ops.Q[p]) == 1 and ops.rank(ops.qpow(p, 2)) == 0 for p in range(112)), 'Q_p: rank 1, Q_p^2 rank 0') + blocks = monomial_block_is_identity(body, ops) + + # Part A + Body.ops_ref = ops + B = Body(body, prov, word, canonical) + B.run() + require(B.dropped == 224, 'the 224 y-field block maps are identity pairs') + require(B.odd == 0, 'every coefficient of the complete body is dyadic') + require(B.S == 6 and B.helper_witness is not None, 'body maximum v2 = 6 with a single-occurrence rank-9 helper term') + require(B.cls['main'] == 4 and B.cls['helper'] == 6, 'class maxima: main 4, helper 6') + for p in range(112): + cx = [q for (inp, wd), q in B.rows[p].items() if inp == p] + cy = [q for (inp, wd), q in B.rows[p].items() if inp == p + 112] + require(cx == [F(1)] and cy == [F(-1)], 'final X row is x_p - y_p') + + # Part B + calls = laurent(caller['controller']) + require(len(calls) == 18, 'eighteen LOCAL calls') + early = 0 + for s, p, rx, ry in calls[:-1]: + for (j, ez), c in list(rx.items()) + list(ry.items()): + require(c.denominator == 1, 'integer controller coefficients') + t = sum(ez[1:]) + early = max(early, 4 + ceil2(8 * t + 9)) + require(early == 73, 'calls before the last need at most 73') + s, p, rx, ry = calls[-1] + require((s, p) == (32, 15), 'last call is stage 32, pair 15') + comp_x = {j: (ez[0], sum(ez[1:]), c) for (j, ez), c in rx.items()} + comp_y = {j: (ez[0], sum(ez[1:]), c) for (j, ez), c in ry.items()} + require(len(comp_x) == len(rx) and len(comp_y) == len(ry), 'one monomial per original bank') + require(comp_x[31][:2] == (2, 17) and comp_y[31][:2] == (1, 17), 'bank 31 enters x as Q^2 and y as Q, 17 stages') + best = (-1,) + + def rank9(q, inp, ww, fr): + op = ops.qpow(inp % 112, q).then(ops.A[inp]) + for sym in ww: + op = op.then(ops.K(sym[1])) + return ops.rank(op.then(ops.chart(fr))) + cache9 = {} + for fr, port, ww, cx, cy in B.groups: + for j in set(comp_x) | set(comp_y): + terms = [] + if j in comp_x and j in comp_y and comp_x[j][0] == comp_y[j][0] + 1 and comp_x[j][1] == comp_y[j][1]: + terms.append((comp_x[j][0], comp_x[j][1], comp_x[j][2] * cx + comp_y[j][2] * cy, port)) + else: + if j in comp_x: + terms.append((comp_x[j][0], comp_x[j][1], comp_x[j][2] * cx, port)) + if j in comp_y: + terms.append((comp_y[j][0], comp_y[j][1], comp_y[j][2] * cy, port + 112)) + for q, t, c, inp in terms: + if not c: + continue + key = (q % 4, inp, ww, fr) + if key not in cache9: + cache9[key] = rank9(q, inp, ww, fr) + g = v2(c.denominator) + ceil2(8 * t + cache9[key]) + if g > best[0]: + best = (g, str(c), 8 * t + cache9[key], j, inp, fr, [list(x) for x in ww]) + # t-field cut after the paid C8 job (y data enter t through the block maps) + C8 = ce.ident(N9) + for i in range(8): + C8 = C8.then(ce.cgate(N9, 1 << i)) + route = {(o['field'], o['purpose']): ops.mono(o['word']) for o in body['operations'] if o['op'] == 'MONOMIAL' and o.get('purpose', '').startswith('D8paidjob')} + tbest = 0 + for o in body['operations']: + if o['op'] == 'ADD' and o['dst'].startswith('t'): + yfield = o['src']; jport = int(yfield[1:]); tf = o['dst'] + op = ops.qpow(jport, comp_y[31][0]).then(blocks[yfield][0]).then(blocks[tf][1]) + op = op.then(route[(tf, 'D8paidjobinputaxisroute')]).then(C8).then(route[(tf, 'D8paidjoboutputaxisroute')]) + tbest = max(tbest, v2(F(o['coefficient']).denominator) + ceil2(8 * 17 + ops.rank(op))) + # cache cuts + cbest = 0 + for slot, (fr, row, sc) in B.cache.items(): + by = collections.defaultdict(lambda: [F(0), F(0)]) + for (inp, wd), q in row.items(): + if inp < 224: + by[(inp % 112, tuple(s for s in wd if s[0] == 'W'))][inp >= 112] += q * F(sc) + for (port, ww), (cx, cy) in by.items(): + c = comp_x[31][2] * cx + comp_y[31][2] * cy + if c: + cbest = max(cbest, v2(c.denominator) + ceil2(8 * 17 + rank9(2, port, ww, fr))) + final_rank = max((1 if d[0] else 0) + 8 * sum(d[1:]) for d in caller['controller']['diagonal']) + targets = ceil2(final_rank) + require(caller['productive_profile']['145'] == 224 and final_rank == 145 and targets == 73, '224 rank-145 targets need 73') + require(best[0] == 73 and tbest <= 73 and cbest <= 73, 'last call: every cut needs at most 73') + guard = max(early, best[0], tbest, cbest, targets, 6 + ceil2(9)) + require(guard == 73, 'controller-level guard is exactly 73') + return dict(body=dict(max_v2=B.S, helper_witness=B.helper_witness, class_max_v2=B.cls, odd_denominators=0, + identity_monomial_pairs=B.dropped, final_X_rows='x_p - y_p on all 112 ports', + guard='ceil(9 lambda/2) + 6 (attained)'), + controller=dict(early_calls_bound=early, last_call=dict(stage=32, pair=15, in_word_max=best[0], + in_word_witness=best[1:], t_cut_max=tbest, cache_cut_max=cbest, + bank31=dict(x=[comp_x[31][0], comp_x[31][1]], y=[comp_y[31][0], comp_y[31][1]])), + rank145_targets=224, target_requirement=targets, guard=guard)) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--write', action='store_true') + args = ap.parse_args() + result = build() + path = HERE / 'RESULT.json' + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + if args.write: + path.write_bytes(text.encode('utf-8')) + require(path.exists() and json.loads(path.read_text(encoding='utf-8')) == json.loads(text), 'stored RESULT.json equals the rebuild') + print('PASS_SELECTED_CALLER_BODY_6_CONTROLLER_EXACTLY_73') + + +if __name__ == '__main__': + main() From fa2ba8e577ddd11b495f7e809cd91544f8c8a322 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 19:48:03 +0300 Subject: [PATCH 2/2] Observe climb and warp cuts and move the cache row in the selected-caller grid; guard is 74 A Gaussian climb changes the row's chart without entering the census; with it observed, provider event 11204 leaves y70 alone at frame 254 and bank 31 reaches it with nine-plane rank 7, so 2 + ceil(143/2) = 74 bits are needed. The mode cache SWAP now moves the transformed 56-term row to its owner instead of dropping it. Both errors from the #5438 review are rejecting controls; README/TASK/VERIFY/RESULT state 74 over the observed cuts. Co-Authored-By: Claude Opus 5.5 (1M context) --- research/selected-caller-exact-grid/README.md | 40 +++++++++++++------ .../selected-caller-exact-grid/RESULT.json | 22 +++++++--- research/selected-caller-exact-grid/TASK.json | 6 +-- .../selected-caller-exact-grid/VERIFY.json | 6 +-- .../selected-caller-exact-grid/test_verify.py | 23 ++++++++++- research/selected-caller-exact-grid/verify.py | 35 +++++++++++----- 6 files changed, 95 insertions(+), 37 deletions(-) diff --git a/research/selected-caller-exact-grid/README.md b/research/selected-caller-exact-grid/README.md index 53508b3e99..a472ae9f56 100644 --- a/research/selected-caller-exact-grid/README.md +++ b/research/selected-caller-exact-grid/README.md @@ -1,7 +1,9 @@ # Exact grid of the complete selected #5413 caller -**Positive scoped result; no new κ.** One controller level of the selected caller needs **exactly 73 extra -fractional bits**. The body needs `ceil(9 lambda/2) + 6`. Both bounds are attained. This continues the merged +**Positive scoped result; no new κ.** One controller level of the selected caller needs **74 extra fractional +bits** at every cut the verifier observes (listed below); 74 is attained, so it is also necessary. The body needs +`ceil(9 lambda/2) + 6`, also attained. An earlier version of this package claimed exactly 73; the review of this +PR found a Gaussian-climb cut it did not observe, which needs 74. This continues the merged [selected-word-exact-grid](../selected-word-exact-grid/README.md), which covers the eight-relation word alone, from the word to the complete caller of [PR #5413](https://github.com/CrocSwap/integer-mult-bounds/pull/5413). The caller's own precision record (`FRESH-PRECISION.json`) has only crude heights: about 19,452 bits per local body @@ -15,8 +17,10 @@ Only backward bodies run: 18 calls, with no forward macro calls. [verify.py](ver - wrappers; - mode scalars; - the 834-instruction input and output basis programs; -- the 21,473-event provider word; -- cache SWAP and CLEAR. +- the 21,473-event provider word, with a cut after every scalar, warp and Gaussian climb (a climb changes the + row's chart, so its output is observed on its own); +- cache SWAP and CLEAR. Each of the eight SWAPs moves its transformed 56-term cache row to the mode owner; the + verifier checks that the cache slot ends zero and the owner nonzero. Monomials, Gaussians and warps stay symbols, so terms through different operator paths never merge; adjacent inverse warps cancel. The 240-map monomial block consists of maps, ADDs and the exact inverse maps. Each y-field @@ -43,16 +47,21 @@ eight private axes per stage. A component `Q^q prod_{t in T} D_t` therefore carr | Region | Exact maximum | |---|---| | Calls before the last (`|T| <= 16`) | `4 + ceil((128+9)/2) = 73`; helpers `<= 11` | -| Last call, in-word cuts | 73 | +| Last call, in-word cuts (after every scalar, warp and climb) | **74** | | Last call, t-field after the paid C8 job | 73 | | Last call, cache cuts | 73 | | 224 rank-145 targets | 73 (necessary) | In the last call (stage 32, pair 15), original bank 31 enters x as `Q^2 D_T` and y as `Q D_T`, with `|T| = 17`. -Its two paths meet on `Phi_x Q^2` with coefficient `c_x + c_y`. Each such term is evaluated with exact nine-plane -ranks, with warps taken from the native table and admitted as in kappa-round3-warp-20261022. Treated separately, -the paths would suggest 74 to 76 bits. Merged, they cancel down to 73. **The guard of one controller level is -therefore exactly 73.** The body's `2^-6` adds nothing on top of the target requirement. +Where both paths reach a cut, they meet on `Phi_x Q^2` with coefficient `c_x + c_y`. Each such term is evaluated +with exact nine-plane ranks, with warps taken from the native table and admitted as in kappa-round3-warp-20261022. + +Not every cut has both paths. The climb of provider event 11204 (zero based: `climb warp_retimed`, row 63, new +frame 254) leaves row 63 holding input `y70` once, with coefficient `1/4`, no warp word and no `x70` term to merge +with. Bank 31 reaches it as `Q D_T` with 17 private stages; the nine-plane operator has rank 7 (exact zero-column +entry `(-1+i)/16`). With the 136 private Fourier axes, a basis input on bank 31, port 70 gives `(-1+i)/2^74` at +this cut: `2 + ceil((136+7)/2) = 74` bits are necessary. No other observed cut needs more. **The guard of one +controller level over the observed cuts is therefore 74.** The body's `2^-6` adds nothing on top of it. ## Reproduce @@ -63,13 +72,15 @@ python3.12 -I -B research/selected-caller-exact-grid/test_verify.py ``` The verifier uses the standard library and the pinned repository Clifford compiler. It takes under a minute and -prints `PASS_SELECTED_CALLER_BODY_6_CONTROLLER_EXACTLY_73`. The controls reject six mutations: +prints `PASS_SELECTED_CALLER_BODY_6_CONTROLLER_74`. The controls reject eight mutations: - a drifted input; - an odd division; - a block map that is not inverted; - a missing controller `Q_POWER`; - a missing owned CLEAR; +- a cache SWAP that drops the cache row instead of moving it (the earlier version's error); +- climbs that change the chart without entering the census (the earlier version's error; the result falls to 73); - a tampered RESULT.json. ## Scope @@ -80,13 +91,18 @@ Several premises are inherited and not re-proved here: - the canonical-chart, wrapper and warp conventions; - the identification of the controller's Q with the body's Q through `X = Phi (x - Q y)`. -The last of these is the body's specified endpoint and is checked through its final rows. The result is an +The last of these is the body's specified endpoint and is checked through its final rows. The observed cuts are +the in-word cuts of the provider word, the t-field cut after the paid C8 job, the cache cuts, the calls before the +last and the final targets; body operations outside the provider word are not separately cut, so 74 is proved +necessary and shown sufficient only at these cuts. The symbolic replay keeps the moved cache rows but does not +prove their algebraic endpoint (the mode outputs `C8 z` of the neutral completion); that is a separate obligation, +raised in the review of #5442. The result is an exact-grid statement, not a rounded execution, a recursive price or a supplier admission. The selected record is unchanged. ## Open next questions -- What does the attained 73-bit controller guard cost in the recursive invoice? First compare it with the retained +- What does the attained 74-bit controller guard cost in the recursive invoice? First compare it with the retained precision_tape packing. #5419 shows that a uniform paid-precision factor above about 1.0046 removes the 0.0033 margin. ## Credit diff --git a/research/selected-caller-exact-grid/RESULT.json b/research/selected-caller-exact-grid/RESULT.json index c437dbfecf..782b34b622 100644 --- a/research/selected-caller-exact-grid/RESULT.json +++ b/research/selected-caller-exact-grid/RESULT.json @@ -14,11 +14,21 @@ ], "identity_monomial_pairs": 224, "max_v2": 6, + "mode_owner_terms": [ + 56, + 56, + 56, + 56, + 56, + 56, + 56, + 56 + ], "odd_denominators": 0 }, "controller": { "early_calls_bound": 73, - "guard": 73, + "guard": 74, "last_call": { "bank31": { "x": [ @@ -31,13 +41,13 @@ ] }, "cache_cut_max": 73, - "in_word_max": 73, + "in_word_max": 74, "in_word_witness": [ - "13/16", - 137, + "1/4", + 143, 31, - 53, - 0, + 70, + 254, [] ], "pair": 15, diff --git a/research/selected-caller-exact-grid/TASK.json b/research/selected-caller-exact-grid/TASK.json index 0c278619bc..01a522d247 100644 --- a/research/selected-caller-exact-grid/TASK.json +++ b/research/selected-caller-exact-grid/TASK.json @@ -81,14 +81,14 @@ "budget_minutes": 300, "stop_rule": "Stop at the exact attained guard of one controller level; the recursive price of the guard is a separate question.", "outcome": "completed", - "evidence": "verify.py expands the #5402 provider inside the #5413 backward body (no odd division, owned fields zero, max v2 = 6 attained: body guard ceil(9 lambda/2)+6), derives the per-port Q from the port wrappers (rank 1, square rank 0, final rows x_p - y_p), replays the controller in its exact Laurent ring and evaluates every cut of the last call with exact nine-plane ranks: the maximum is 73, equal to the requirement of the 224 rank-145 targets, so one controller level needs exactly 73 extra bits. test_verify.py rejects six mutations.", + "evidence": "verify.py expands the #5402 provider inside the #5413 backward body (no odd division, owned fields zero, max v2 = 6 attained: body guard ceil(9 lambda/2)+6), derives the per-port Q from the port wrappers (rank 1, square rank 0, final rows x_p - y_p), replays the controller in its exact Laurent ring and evaluates the cuts of the last call (after every scalar, warp and climb of the provider word, the t-field cut after the paid C8 job and the cache cuts) with exact nine-plane ranks: the maximum is 74, attained by a Gaussian-climb cut where bank 31 reaches y70 alone (review of #5438), one bit above the 73 of the 224 rank-145 targets, so one controller level needs 74 extra bits at these cuts. test_verify.py rejects eight mutations.", "author": "Mark (Matarener)", "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", "open_questions": [ { - "question": "What does the attained 73-bit controller guard cost in the recursive invoice?", + "question": "What does the attained 74-bit controller guard cost in the recursive invoice?", "why_it_matters": "PR #5419 shows that a uniform paid-precision factor above about 1.0046 removes the 0.0033 margin; the guard is now exact, so its price can be computed.", - "first_step": "Express 73 bits per controller level as storage per packed word at the recursion's word width and compare with the retained precision_tape prescription.", + "first_step": "Express 74 bits per controller level as storage per packed word at the recursion's word width and compare with the retained precision_tape prescription.", "blocked_by": "The retained packing and tape prescription have to be read from the compiler sources." } ] diff --git a/research/selected-caller-exact-grid/VERIFY.json b/research/selected-caller-exact-grid/VERIFY.json index 539ce8783e..54926dab28 100644 --- a/research/selected-caller-exact-grid/VERIFY.json +++ b/research/selected-caller-exact-grid/VERIFY.json @@ -21,7 +21,7 @@ "{package}/verify.py" ], "timeout_seconds": 600, - "checks": "Pinned inputs; controller binds the body; Q_p rank 1 / Q_p^2 rank 0 on all ports; the 240-map block is maps, ADDs, inverse maps; body with the #5402 provider expanded: no odd denominator, owned fields zero, max v2 = 6 with a rank-9 helper witness, main v2 <= 4, final X rows x_p - y_p; Laurent replay reproduces the diagonal; calls before the last need <= 73; last call (bank 31 as Q^2 / Q, 17 stages) in-word, t-field and cache cuts all <= 73; 224 rank-145 targets need 73; guard exactly 73; stored RESULT.json equals the rebuild." + "checks": "Pinned inputs; controller binds the body; Q_p rank 1 / Q_p^2 rank 0 on all ports; the 240-map block is maps, ADDs, inverse maps; body with the #5402 provider expanded: no odd denominator, owned fields zero, each cache SWAP moves the 56-term cache row to its owner, max v2 = 6 with a rank-9 helper witness, main v2 <= 4, final X rows x_p - y_p; Laurent replay reproduces the diagonal; calls before the last need <= 73; last call (bank 31 as Q^2 / Q, 17 stages): in-word cuts including every warp and climb need <= 74, attained by the climb cut of event 11204 (bank 31, port 70, frame 254), t-field and cache cuts <= 73; 224 rank-145 targets need 73; guard 74 over the observed cuts; stored RESULT.json equals the rebuild." }, { "argv": [ @@ -30,8 +30,8 @@ "-B", "{package}/test_verify.py" ], - "timeout_seconds": 300, - "checks": "Rejecting controls: drifted input hash, an odd division in a body ADD, a block map that is not inverted, a missing controller Q_POWER, a missing owned CLEAR, tampered RESULT.json." + "timeout_seconds": 600, + "checks": "Rejecting controls: drifted input hash, an odd division in a body ADD, a block map that is not inverted, a missing controller Q_POWER, a missing owned CLEAR, a cache SWAP that drops the cache row, an unobserved climb cut, tampered RESULT.json." } ] } diff --git a/research/selected-caller-exact-grid/test_verify.py b/research/selected-caller-exact-grid/test_verify.py index edb6ea40ac..b3f7d3abc6 100644 --- a/research/selected-caller-exact-grid/test_verify.py +++ b/research/selected-caller-exact-grid/test_verify.py @@ -67,15 +67,34 @@ def missing_owned_clear(): B = V.Body(body, PROV, WORD, CAN); B.run() +def mutated_build(old, new): + src = (HERE / 'verify.py').read_text(encoding='utf-8') + V.require(src.count(old) == 1, 'mutation site present') + ns = {'__file__': str(HERE / 'verify.py'), '__name__': 'selected_caller_mutant'} + exec(compile(src.replace(old, new), str(HERE / 'verify.py'), 'exec'), ns) + ns['build']() + + +def dropped_cache(): + # the review of #5438: a SWAP that discards the transformed cache row instead of moving it + mutated_build('self.rows[cs], self.rows[o] = self.rows[o], self.rows[cs]', 'self.rows[cs], self.rows[o] = self.rows[o], {}') + + +def unobserved_climb(): + # the review of #5438: climbs change the chart without entering the census; the 74-bit cut is missed + mutated_build("self.stat(('climb', t), e[2])", 'pass') + + def tampered_result(): stored = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) - stored['controller']['guard'] = 72 - V.require(stored['controller']['guard'] == 73, 'stored RESULT.json equals the rebuild') + stored['controller']['guard'] = 73 + V.require(stored['controller']['guard'] == 74, 'stored RESULT.json equals the rebuild') for name, fn in [('drifted input hash', drift), ('an odd division in a body ADD', odd_division), ('a block map that is not inverted', broken_block_inverse), ('a missing controller Q_POWER', missing_q_power), ('a missing owned CLEAR', missing_owned_clear), + ('a cache SWAP that drops the cache row', dropped_cache), ('an unobserved climb cut', unobserved_climb), ('tampered RESULT.json', tampered_result)]: rejects(name, fn) print('PASS_SELECTED_CALLER_EXACT_GRID_CONTROLS') diff --git a/research/selected-caller-exact-grid/verify.py b/research/selected-caller-exact-grid/verify.py index d6bcfdb691..8c5738c8b9 100644 --- a/research/selected-caller-exact-grid/verify.py +++ b/research/selected-caller-exact-grid/verify.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -"""Exact grid of the complete selected #5413 caller: body ceil(9 lambda/2)+6, controller level exactly 73 bits. +"""Exact grid of the complete selected #5413 caller: body ceil(9 lambda/2)+6, controller level 74 bits (attained). Standard library only; about three minutes. Inputs pinned by SHA256 in SOURCES.json, all on main: the #5413 capsule (NEUTRAL-BACKWARD-v16c body, NEUTRAL-CALLER-v16c controller), the #5402 PROVIDER.json and provider WORD.json.gz, the @@ -13,7 +13,8 @@ Part A, body. The only runtime local direction is backward (18 calls). Execute the body with PROVIDER_5402 expanded by its schedule; monomials, Gaussians and warps stay symbols (adjacent inverse warps cancel; each y-field monomial of the 240-map block is followed by its exact inverse with only ADDs in between, so the pair is the identity and is -omitted). Checks: no odd denominator, 17 owned fields zero at exit, maximum v2 = 6 attained by a single-occurrence +omitted). Every warp and Gaussian climb is a cut of its own (the climb changes the row's chart); each mode cache +SWAP moves the transformed 56-term cache row to its owner. Checks: no odd denominator, 17 owned fields zero at exit, maximum v2 = 6 attained by a single-occurrence rank-9 helper term (body guard ceil(9 lambda/2)+6), main-data terms v2 <= 4, helper terms local rank <= 9. Part B, controller. Per port p let A_x = (backward_input_X wrapper, then Delta_{I_x}^-1), A_y likewise, and @@ -23,11 +24,13 @@ axis 0 plus eight private axes per LOCAL stage; a component Q^q prod_{t in T} D_t has 8|T| private Fourier rank. * calls before the last: |T| <= 16, so every term needs <= 4 + ceil((128+9)/2) = 73 (main) or <= 11 (helper); * last call (stage 32, pair 15): original bank 31 enters x as Q^2 D_T and y as Q D_T with |T| = 17. Its x- and - y-paths merge (Phi_y = Phi_x Q_p) on Phi_x Q^2 with coefficient c_x + c_y; every in-word cut is evaluated with - exact nine-plane ranks (warps via the native table), plus the t-field cut after the paid C8 job and the cache cuts; + y-paths merge (Phi_y = Phi_x Q_p) on Phi_x Q^2 with coefficient c_x + c_y; every in-word cut (after each scalar, + warp and climb) is evaluated with exact nine-plane ranks (warps via the native table), plus the t-field cut after + the paid C8 job and the cache cuts; * after the last call the controller only applies integer ADD/SCALE/SWAP and monomials; 224 targets have rank 145. -Result: the maximum over every cut is 73, attained by the rank-145 targets: one controller level needs exactly 73 -extra fractional bits. +Result: the climb output of provider event 11204 (row 63, frame 254) holds y70 alone with coefficient 1/4; bank 31 +reaches it as Q D_T with nine-plane rank 7, so 2 + ceil((136+7)/2) = 74 bits are necessary. The maximum over every +observed cut is 74: one controller level needs 74 extra fractional bits at these cuts (review of #5438). Usage: python3 -I -B verify.py [--write] """ import argparse, collections, gzip, hashlib, importlib.util, json @@ -133,7 +136,7 @@ def __init__(self, body, prov, word, canonical): self.rows = {i: {(i, ()): F(1)} for i in range(body['physical_field_count'])} self.sym = 0; self.S = 0; self.odd = 0; self.cls = {}; self.frames = {}; self.inword = False self.groups = [] # in-word: (frame, port, warp word, c_x, c_y) - self.helper_witness = None; self.cache = {} + self.helper_witness = None; self.cache = {}; self.mode_terms = [] def newsym(self, tag): self.sym += 1 @@ -215,8 +218,11 @@ def provider(self): self.apply(self.role(e[1]), ('W', e[2])) if e[1][0] == 'L': self.frames[e[1][1]] = e[4] + self.stat(('warp', t), self.role(e[1])) elif k == 'climb': + # a Gaussian climb changes the row's chart: its output is a cut of its own self.frames[e[2]] = e[4] + self.stat(('climb', t), e[2]) elif k == 'scalar': g = e[1]; d_ = self.role(g[1]) if g[1][0] == 'L' and e[2] is not None: @@ -245,7 +251,9 @@ def provider(self): cs, o = m['cache_slot'], m['owner'] self.scale(cs, F(m['cache_scalar']), 'cache_scalar'); self.apply(cs, self.newsym('N')) require(not self.rows[o], 'mode owner zero before the cache SWAP') - self.rows[cs], self.rows[o] = self.rows[o], {} + self.rows[cs], self.rows[o] = self.rows[o], self.rows[cs] + require(not self.rows[cs] and self.rows[o], 'cache SWAP transfers the nonzero cache row to its owner') + self.mode_terms.append(len(self.rows[o])) for f in range(224): self.apply(f, self.newsym('Nout')) @@ -373,6 +381,7 @@ def build(): B = Body(body, prov, word, canonical) B.run() require(B.dropped == 224, 'the 224 y-field block maps are identity pairs') + require(B.mode_terms == [56] * 8, 'each of the eight owners receives its 56-term transformed cache row') require(B.odd == 0, 'every coefficient of the complete body is dyadic') require(B.S == 6 and B.helper_witness is not None, 'body maximum v2 = 6 with a single-occurrence rank-9 helper term') require(B.cls['main'] == 4 and B.cls['helper'] == 6, 'class maxima: main 4, helper 6') @@ -450,11 +459,15 @@ def rank9(q, inp, ww, fr): final_rank = max((1 if d[0] else 0) + 8 * sum(d[1:]) for d in caller['controller']['diagonal']) targets = ceil2(final_rank) require(caller['productive_profile']['145'] == 224 and final_rank == 145 and targets == 73, '224 rank-145 targets need 73') - require(best[0] == 73 and tbest <= 73 and cbest <= 73, 'last call: every cut needs at most 73') + # review of #5438: the climb output of provider event 11204 (row 63, frame 254) carries y70 alone with + # coefficient 1/4; original bank 31 reaches it as Q D_T with 17 stages and nine-plane rank 7: 2 + ceil(143/2) = 74 + require(best[:6] == (74, '1/4', 143, 31, 70, 254), 'last call: the climb cut of bank 31, port 70 needs 74') + require(tbest <= 74 and cbest <= 74, 'last call: every observed cut needs at most 74') guard = max(early, best[0], tbest, cbest, targets, 6 + ceil2(9)) - require(guard == 73, 'controller-level guard is exactly 73') + require(guard == 74, 'controller-level guard over the observed cuts is 74') return dict(body=dict(max_v2=B.S, helper_witness=B.helper_witness, class_max_v2=B.cls, odd_denominators=0, identity_monomial_pairs=B.dropped, final_X_rows='x_p - y_p on all 112 ports', + mode_owner_terms=B.mode_terms, guard='ceil(9 lambda/2) + 6 (attained)'), controller=dict(early_calls_bound=early, last_call=dict(stage=32, pair=15, in_word_max=best[0], in_word_witness=best[1:], t_cut_max=tbest, cache_cut_max=cbest, @@ -472,7 +485,7 @@ def main(): if args.write: path.write_bytes(text.encode('utf-8')) require(path.exists() and json.loads(path.read_text(encoding='utf-8')) == json.loads(text), 'stored RESULT.json equals the rebuild') - print('PASS_SELECTED_CALLER_BODY_6_CONTROLLER_EXACTLY_73') + print('PASS_SELECTED_CALLER_BODY_6_CONTROLLER_74') if __name__ == '__main__':