From 1998c8990031081b71d75c62dea9049236dcfdec Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 19:07:59 +1100 Subject: [PATCH 1/4] Bind one selected Toom candidate to its exact dirty-input interface --- research/selected-toom3-typed-block/PROOF.md | 176 +++++++++++++ research/selected-toom3-typed-block/README.md | 86 +++++++ .../selected-toom3-typed-block/RESULT.json | 154 ++++++++++++ .../selected-toom3-typed-block/SOURCES.json | 30 +++ research/selected-toom3-typed-block/TASK.json | 72 ++++++ .../selected-toom3-typed-block/VERIFY.json | 33 +++ research/selected-toom3-typed-block/verify.py | 235 ++++++++++++++++++ 7 files changed, 786 insertions(+) create mode 100644 research/selected-toom3-typed-block/PROOF.md create mode 100644 research/selected-toom3-typed-block/README.md create mode 100644 research/selected-toom3-typed-block/RESULT.json create mode 100644 research/selected-toom3-typed-block/SOURCES.json create mode 100644 research/selected-toom3-typed-block/TASK.json create mode 100644 research/selected-toom3-typed-block/VERIFY.json create mode 100644 research/selected-toom3-typed-block/verify.py diff --git a/research/selected-toom3-typed-block/PROOF.md b/research/selected-toom3-typed-block/PROOF.md new file mode 100644 index 0000000000..680cecfa34 --- /dev/null +++ b/research/selected-toom3-typed-block/PROOF.md @@ -0,0 +1,176 @@ +# One literal selected block does not have the same-width Toom-only interface + +## Source and exact boundary + +Fix canonical main `20ecf2891d80b5acf18d980b2164fb44ea7faa90` and the +selected #1094 archive pinned in `SOURCES.json`. The question is the next +experiment explicitly left open by Gonzalo Mier's #3974, head +`23bb4de61d629e3f103a65baa7882b34042ab10f`: bind one of its nine-climb windows +to ordinary degree-two Toom coefficient inputs. This is one window, not a +reclassification of all 254 reported windows. + +Use the first forward phase-A group under the earliest-deadline rule adapted +from Josie Elliston's #1817. Its nine `L` registers, in order, are + +`546, 560, 547, 568, 548, 558, 549, 570, 464`. + +The first eight climbs are `(old,new,rank)=(0,4,1)`, where frame 4 is `[459]`; +the last is `(0,5,1)`, where frame 5 is `[75]`. Frame zero is empty. The original +zero-based event indices are `9297,9299,9301,9304,9313,9315,9317,9322,9330`. +Their legal windows meet at skeleton gap 1190; the last event's window starts +at 42, the others at zero. All nine destinations are distinct. Moving the +climbs to that gap changes no event on their own registers and crosses no +phase boundary. This is the inherited local movement model, not a new global +hosting proof. + +Let `W=Q(i)^512`, the nine-bit index space of one physical payload. Write +`Z_j` for the independent unframed coordinates immediately after the entry +adapters, so physical register `j` is `T_start(j) Z_j`. These are **not** raw +initial values: for example register 512 has a residual pre-wrapper. Entry +adapters are invertible; frame coordinates do not impose a zero or clean-data +promise on a productive helper. The selected nine helpers start at frame zero, +have ordinary identity entry adapters, and end at full frame. The scalar +prefix consists of nonzero scales and shears, hence is invertible. A direct +rational replay gives the actual incoming forms at the chosen gap: + +`Z_546,Z_560,Z_547,Z_568,Z_548,Z_558,Z_549,Z_570,Z_464+Z_512`. + +Their coefficient minor on the nine named variables is the identity. Thus +these are nine freely variable W-valued payloads, even when all other entrance +coordinates are fixed. None can be discarded because a helper was called +"cold": that word describes its entrance frame, not a zero value. + +At this boundary the demanded map is the **linear** operator + +`F = diag(T_[459],T_[459],T_[459],T_[459],T_[459],T_[459],T_[459],T_[459],T_[75])`. + +It must overwrite all nine named destinations, preserve every other productive +payload, and return any additional scratch in its required initial state. The +selected event is a frame transform, not an independently named bilinear +product of two coefficient variables. + +## Exact operator reconstruction + +For each of the two transitions the pinned serialized recipe says +`T = L (C_[1] tensor I_256) R`, with R applied first. L and R are monomial +maps with explicit binary permutation, translation, quadratic and Z/4 phases. +The one-axis child is exactly + +`C = ((1+i) I + (1-i) X)/2`. + +The verifier decodes the recipe directly on every basis vector, using Gaussian +integer numerators and a single factor 2. Independently, it evaluates the +retained canonical-frame constructor on all 512 basis vectors for each frame. +All 1,024 columns agree, including global phase. A separate sparse Gram +calculation gives `T* T = I` exactly. Both operators have rank 512, and F has +rank **4,608**. For example + +`T_[459] e_0 = ((1+i)e_0 - (1+i)e_459)/2`, + +`T_[75] e_0 = ((1+i)e_0 - (1+i)e_75)/2`. + +These explicit outputs catch replacing an omitted dirty input by zero. +The implemented checks also reject altered global phase and translation. +The retained constructor is predecessor code, not claimed newly independent; +the direct recipe decoder and Gram certificate are separate implementations. + +## Declared Toom-only substitution contract + +The rejected contract has exactly these restrictions: + +1. Each polynomial has three coefficients in a vector space of dimension 512 + over `Q(i)`. Both triples are produced by affine maps of the nine incoming + payloads. They may have arbitrary fixed coefficients and constants. +2. The usual five Toom evaluation products, interpolation and output decoding + receive data **only through these six coefficient blocks**. The coefficient + multiplication may be any bilinear law; it need not be commutative. +3. The nine final payloads are functions of the coefficient blocks and fixed + constants only. Productive inputs, other registers and scratch may not + supply additional data to that output decoder. + +Restriction 3 is material. Retaining or bypassing original payloads changes +the contract. Five recursive calls in a general circuit do **not** imply this +restriction. No lower bound on arbitrary five-child circuits is claimed. + +**Proposition.** This contract cannot realize the named selected block. + +**Proof.** Its affine encoding `E:W^9 -> W^6` has a nonzero linear kernel of +dimension at least `9*512-6*512=1536`. For any nonzero kernel vector h, +`E(x+h)=E(x)`, so every downstream output is the same at x+h and x. But the +selected F is invertible, hence `F(x+h)-F(x)=F(h)` is nonzero. This contradicts +exact equality on arbitrary dirty inputs. The argument permits nonlinear +interpolation or decoding as long as it receives no extra input data. If one +polynomial is fixed, only three coefficient blocks depend on x and the kernel +has dimension at least **3,072**. Equivalently the possible linear output ranks +are at most **3,072** and **1,536**, respectively, against 4,608. QED. + +**Sharper ordinary-decoder corollary.** If the final decoder is affine linear +and receives only the five product blocks, the possible output differences +lie in the image of a linear map `W^5 -> W^9`, of dimension at most **2,560**. +Thus the usual product-only Toom interpolation/output decoder has an output +deficit of **2,048** dimensions. An additional affine side channel entering +that decoder must have dimension at least 2,048. This corollary has the extra +product-only/affine-decoder restrictions; the more generous six-coefficient +contract above permits direct coefficient reads and still fails. + +If both operands are homogeneous linear encodings, an additional elementary +control applies: the Toom output is homogeneous quadratic, so its value at +2x is four times its value at x. The nonzero selected block doubles instead. +Affine constants remove that degree objection, but do not remove the input +kernel obstruction above. + +Noncommutativity is not the obstruction. Ordinary Toom convolution works over +an associative algebra over the rationals when its indeterminate and +interpolation scalars are central: each ordered term is `A_i B_j`, and no +reversal is used. What is missing here is a typed coefficient embedding of +nine independent payloads, not a scalar identity. + +## What can reopen the route + +Adding an affine side channel of scalar dimension d changes the encoding to +`W^9 -> W^6 x Q(i)^d`. Injectivity then requires **d >= 1536**; with a fixed +factor it requires **d >= 3072**. These are information dimensions, **not** +native operation, child-count, storage, or time lower bounds. Already-retained +productive data could supply such a channel; its exact use and legal costs +must be specified. Wider coefficient spaces, data-dependent non-affine +encoding, a different output contract, or a new coupled recursive primitive +are also outside this proposition. A wider space must be priced at its actual +recursive size, rather than silently counted as the same five children. + +The original block already pays nine rank-one frame children and its named +recipes. There is no completed replacement here. Extra data acquisition, +encoding, scratch, phase/frame conversion, dyadic precision and halving, +interpolation's non-dyadic divisions, native hosting, decoding and restoration +all remain unknown for a changed interface. Unknowns are not zero. In +particular the predecessor's 19 additions and 13 rational scales do not price +those obligations or establish legal native division by three. + +**Expansion decision:** pause the same-width Toom-only substitution on this +actual group. Reopen on one explicit interface carrying the missing data, +with all nine output identities and complete restoration, then price that +module. Do not extrapolate the 254 event count into implemented savings. This +result changes neither the selected paid profile nor either supplier cap, +and establishes zero realized blocks and zero kappa improvement. + +## Constructive comparison: homogeneous lane packing + +The first eight selected maps do have an exact different tensor structure: + +`diag(T_[459],...,T_[459]) = I_8 tensor T_[459]`. + +With index `(lane,x)` encoded as `512*lane+x`, the same canonical frame `[459]` +on twelve bits realizes this identity. The verifier compares its full Pauli +tableau with the nine-bit tableau plus three idle bits, then checks its exact +zero-state vector to fix the global phase. Its Fourier B-block rank is **one**, +with payload dimension **4,096** and eight times the idle extent. This is a +constructive operator equality, not an eight-to-one paid-call conversion. + +The grouping therefore has a precise alternative to Toom, but the rank-one +child must now act on eight times the payload, or a different native operator +must be supplied. No rule identifying that enlarged input with a unit-priced +rank-eight child follows from this identity. #1779's diagonal-product screen +and #1836's joint-shear screen also explicitly leave physical interfaces open; +#1836 is pinned at `0a62e3f1c0ea493ddb83f25b91c5548c87978bcc` for this comparison. +A paid enlarged-payload native call would be the next discriminating module. +This comparison supplies its exact operator and width, without assigning +unproved copy, layout, precision, restoration or supplier costs to zero. diff --git a/research/selected-toom3-typed-block/README.md b/research/selected-toom3-typed-block/README.md new file mode 100644 index 0000000000..cba259cc2e --- /dev/null +++ b/research/selected-toom3-typed-block/README.md @@ -0,0 +1,86 @@ +# A typed boundary test for one selected Toom-3 candidate + +**One actual nine-climb group is an invertible 4,608-dimensional linear map. +It cannot factor through the 3,072-dimensional input boundary of a same-width, +Toom-only coefficient module. No replacement or new kappa is claimed.** + +This answers the first source-binding experiment left by Gonzalo Mier's +[PR #3974](https://github.com/CrocSwap/integer-mult-bounds/pull/3974), head +`23bb4de61d629e3f103a65baa7882b34042ab10f`. It pairs fast bilinear algorithms +with linear-algebraic information bounds and typed reversible interfaces. + +The first forward phase-A group contains registers +`546,560,547,568,548,558,549,570,464`. Eight climb from the empty frame to +`[459]`, one to `[75]`. The actual incoming forms have a nine-by-nine identity +minor, so arbitrary dirty inputs cannot be identified with only three +coefficients per operand. We reconstruct both 512-dimensional Clifford maps +on **all 1,024 basis columns**, including phases and halving, and independently +check their exact Gram matrices. The selected block rank is **4,608**. + +| Explicit coefficient interface | Maximum linear input rank | Deficit | +|---|---:|---:| +| One variable coefficient triple, one fixed factor | 1,536 | 3,072 | +| Two affine variable coefficient triples, decoder may read both | 3,072 | 1,536 | +| Five product blocks, affine output decoder | 2,560 | 2,048 | +| Actual selected nine-payload boundary | 4,608 | 0 | + +The obstruction assumes outputs receive data only through the coefficient +blocks. General circuits may retain original inputs or use bypasses; five +child calls alone do not imply this factorization. The deficits are algebraic +information dimensions, not native cost lower bounds. Wider coefficient +spaces and changed interfaces remain open. Noncommutative Toom convolution +itself remains valid with central interpolation scalars. + +[PROOF.md](PROOF.md) gives the exact contract, source event indices, input +forms, proof, missing obligations and expansion decision. [RESULT.json](RESULT.json) +is regenerated by the bounded verifier. **Zero source blocks are replaced; +selected kappa remains 0.001672660197076918.** + +## Reproduce + +``` +python3 scripts/research_package.py --package research/selected-toom3-typed-block --check-only +python3 scripts/research_package.py --package research/selected-toom3-typed-block +``` + +The two registered runs (normal and optimized Python) bind the selected +archive, reconstruct the first eligible group, derive its input minor, check +all basis columns and exact Gram matrices, compare the result, and exercise +four failure controls. They do not replay the complete selected supplier. +The canonical-frame evaluator is retained predecessor code; the recipe +interpreter and sparse Gram check are new separate implementations. No +independent human or formal-kernel acceptance is claimed. + +## Open next questions + +Can one explicit bypass or wider-coefficient construction preserve the nine +independent dirty payloads while delivering five **legal** children, with +complete frames, precision, output and scratch restoration costs? First write +that interface and verify all nine outputs on basis inputs, then compare the +complete paid profile against the selected supplier. The present Toom-only +contract is paused; another larger event-window census cannot repair it. +The checked alternative `I_8 tensor T_[459]` packs the first eight lanes into +a 4,096-dimensional, twelve-bit payload, but its Fourier rank remains one. +Its larger native call and full invoice remain open. Structured obligations +and the stop rule appear in `TASK.json`. + +## Sources, overlap and credit + +Canonical base is `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision +6. Parent entry overlap checked 679 open PR bodies and rendered active/handoff +Discussions on 2026-10-19; broader closed/private/Discussion coverage remains +partial. Target #3974 was reread at its exact head before this experiment. +This package does not claim novelty from an empty keyword search. + +Credit Gonzalo Mier / #3974 for the Toom screen and explicit missing binding; +Josie Elliston / #1817 for phase-local dependency windows; Jose Manuel +(@jmbarrancoml, as credited in #1779, submitted via 1337isnot1337) for the +diagonal batching screen; Arham Tahir / #1605 for rank-shape budgets; Discussion +#1987 contributors for the Karatsuba antecedent; and the selected #1094, +Clifford compiler, PR514/PR433 and Rohan Arun / Jeremy Kothe / Hao Yan source +lineage. Predecessor attribution is preserved rather than treating archive +retention as scientific acceptance. + +Prepared for Clear1nsight with substantial OpenAI Codex assistance in source +inspection, proof, implementation and exposition. Apache-2.0. Frozen sources +are unchanged. diff --git a/research/selected-toom3-typed-block/RESULT.json b/research/selected-toom3-typed-block/RESULT.json new file mode 100644 index 0000000000..0d1c4031a5 --- /dev/null +++ b/research/selected-toom3-typed-block/RESULT.json @@ -0,0 +1,154 @@ +{ + "actual_input_and_output_rank": 4608, + "controls": [ + "global_phase", + "translation", + "quadratic_scaling", + "omitted_dirty_register" + ], + "five_product_linear_decoder_output_rank_upper": 2560, + "fixed_factor_toom_input_rank_upper": 1536, + "implemented_replacements": 0, + "input_form_coordinates": "post-entry-adapter unframed Z_j; not raw initial payloads", + "input_forms": [ + { + "546": "1" + }, + { + "560": "1" + }, + { + "547": "1" + }, + { + "568": "1" + }, + { + "548": "1" + }, + { + "558": "1" + }, + { + "549": "1" + }, + { + "570": "1" + }, + { + "464": "1", + "512": "1" + } + ], + "kappa_change": 0, + "minimum_extra_input_dimension_two_affine_factors": 1536, + "minimum_extra_output_dimension_five_product_decoder": 2048, + "operators": { + "4": { + "basis_zero_numerator": { + "0": [ + 1, + 1 + ], + "459": [ + -1, + -1 + ] + }, + "column_digest": "ca98c05490e1e296fbd24a690e771c9d699ae3d09a221ee1c96322e1fdfcc20d", + "denominator": 2, + "frame": [ + 459 + ], + "rank": 512 + }, + "5": { + "basis_zero_numerator": { + "0": [ + 1, + 1 + ], + "75": [ + -1, + -1 + ] + }, + "column_digest": "e509530d9c9ea86e448cef60b5339b766805c9f41edbc3df8a86881781dead5c", + "denominator": 2, + "frame": [ + 75 + ], + "rank": 512 + }, + "eight_lane_packing": { + "fourier_rank": 1, + "index_bits": 12, + "paid_profile_delta": "unknown; no admitted larger-payload call", + "payload_dimension": 4096, + "same_rank_payload_multiplier": 8 + } + }, + "original_event_indices_zero_based": [ + 9297, + 9299, + 9301, + 9304, + 9313, + 9315, + 9317, + 9322, + 9330 + ], + "registers": [ + 546, + 560, + 547, + 568, + 548, + 558, + 549, + 570, + 464 + ], + "scope": "one actual forward phase-A group; same-width Toom-only interface", + "skeleton_gap": 1190, + "two_affine_factors_input_rank_upper": 3072, + "windows": [ + [ + 0, + 1190 + ], + [ + 0, + 1191 + ], + [ + 0, + 1192 + ], + [ + 0, + 1194 + ], + [ + 0, + 1202 + ], + [ + 0, + 1203 + ], + [ + 0, + 1204 + ], + [ + 0, + 1208 + ], + [ + 42, + 1215 + ] + ] +} diff --git a/research/selected-toom3-typed-block/SOURCES.json b/research/selected-toom3-typed-block/SOURCES.json new file mode 100644 index 0000000000..de1dd9f136 --- /dev/null +++ b/research/selected-toom3-typed-block/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/complex-multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ] +} diff --git a/research/selected-toom3-typed-block/TASK.json b/research/selected-toom3-typed-block/TASK.json new file mode 100644 index 0000000000..5475f4c04a --- /dev/null +++ b/research/selected-toom3-typed-block/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Bind one literal selected nine-climb event group to its exact linear operator and reject a specified same-width Toom-only coefficient interface by input dimension.", + "scope_change_reason": "PR3974 provides an ordinary convolution identity and candidate event windows but no typed coefficient embedding. This experiment resolves that next boundary obligation on one actual group.", + "bottleneck_link": "Prevent counting hypothetical nine-to-five rank-one savings when the proposed coefficient boundary loses independent dirty payloads; a changed interface must be priced before any kappa extrapolation.", + "budget_minutes": 60, + "stop_rule": "Stop after one exact group, explicit operator, dimension obstruction and bounded controls. Reopen only on an explicit bypass or wider-coefficient interface and complete paid invoice; do not expand the event census.", + "outcome": "negative-result", + "evidence": "1024 exact basis columns and sparse Gram matrices establish actual block rank4608; same-width affine coefficient-only input cap3072, fixed-factor cap1536, and product-only affine output cap2560. Constructive eight-lane packing has width4096 and Fourier rank1. Zero realized replacements; no kappa improvement.", + "author": "Clear1nsight with OpenAI Codex", + "ai_assistance": "Substantial OpenAI Codex assistance for source analysis, mathematical argument, exact verifier, documentation and publication.", + "open_questions": [ + { + "question": "Can a changed Toom interface carry the missing input data and realize all nine outputs with five legal children?", + "why_it_matters": "Only an actual typed replacement with complete paid costs can change the complex supplier profile.", + "first_step": "Specify one bypass or wider coefficient encoding, verify all output identities and arbitrary-dirty restoration, then charge frame, source, scratch, precision and native costs.", + "blocked_by": "No such interface or invoice is supplied; the same-width Toom-only interface loses at least1536 scalar dimensions." + } + ] +} diff --git a/research/selected-toom3-typed-block/VERIFY.json b/research/selected-toom3-typed-block/VERIFY.json new file mode 100644 index 0000000000..39810f6cde --- /dev/null +++ b/research/selected-toom3-typed-block/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/complex-multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/vendor/clifford/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source-bound group, literal input forms,1024basis columns,Gram ranks and four mutation/degree controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same evidence with Python assertions disabled; new acceptance checks remain active." + } + ] +} diff --git a/research/selected-toom3-typed-block/verify.py b/research/selected-toom3-typed-block/verify.py new file mode 100644 index 0000000000..d9a5ee37bd --- /dev/null +++ b/research/selected-toom3-typed-block/verify.py @@ -0,0 +1,235 @@ +#!/usr/bin/env python3 +"""One selected nine-climb block: exact typed map and Toom interface obstruction. +Prepared with substantial OpenAI Codex assistance. Apache-2.0. +Window selection adapts Josie Elliston #1817 and Gonzalo Mier #3974. +""" +import bisect +import collections +import gzip +import hashlib +import importlib.util +import io +import json +import sys +import tarfile +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = 'research/community-frontier1094-audit/selected-replay.tar.gz' +CLIFFORD = 'research/complex-multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/vendor/clifford/clifford_exact.py' +PREFIX = 'candidate/strict/global/base/providers/gauge44/' +REGISTERS = [546, 560, 547, 568, 548, 558, 549, 570, 464] + +def need(ok, message): + if not ok: + raise ValueError(message) + +def sources(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + for row in manifest['files']: + if row['usage'] == 'input': + need(hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], 'input pin: ' + row['path']) + with tarfile.open(fileobj=io.BytesIO((ROOT / ARCHIVE).read_bytes()), mode='r:gz') as tar: + def obj(name): + raw = tar.extractfile(PREFIX + name).read() + return json.loads(gzip.decompress(raw) if name.endswith('.gz') else raw) + return obj('LOCAL-PROGRAMS.json.gz'), obj('CANONICAL-WORD.json.gz'), obj('CLIFFORD-RECIPES.json') + +def touches(e): + if e[0] in ('climb', 'adapter', 'residual_adapter'): + return {('L', e[2])} + if e[0] == 'center': + return {('C', e[1])} + if e[0] == 'scalar': + o = e[1] + return {tuple(o[1])} | ({tuple(o[2])} if o[0] in ('add', 'copy') else set()) + return set() + +def first_group(events): + a = events.index(['phase', 'A']) + 1 + end = next(i for i in range(a, len(events)) if events[i][0] == 'phase') + body = events[a:end] + r1 = lambda e: e[0] == 'climb' and e[5] == 1 + skeleton = [e for e in body if not r1(e)] + positions = collections.defaultdict(list) + for j, e in enumerate(skeleton): + for r in touches(e): + positions[r].append(j) + climbs, gap = [], 0 + for index, e in enumerate(body): + if r1(e): + pos = positions['L', e[2]] + k = bisect.bisect_left(pos, gap) + lo, hi = (pos[k-1]+1 if k else 0), (pos[k] if k < len(pos) else len(skeleton)) + climbs.append((a+index, gap, lo, hi, e)) + else: + gap += 1 + counts = collections.Counter((e[2], lo, hi) for _, _, lo, hi, e in climbs) + for g in range(len(skeleton)+1): + available = [(k, c) for k, c in enumerate(climbs) if c[2] <= g <= c[3] and counts[c[4][2], c[2], c[3]] == 1] + if len(available) >= 9 and any(c[3] == g for _, c in available): + chosen = sorted(available, key=lambda pair: (pair[1][3], pair[0]))[:9] + rows = [c for _, c in chosen] + return a, g, skeleton, rows + raise ValueError('no group') + +def scalar_prefix(events, a, gap, skeleton, group): + # Scalar-coordinate ledger: frame transitions preserve the abstract column. + # All selected group columns are still frame zero; therefore their rows + # here give literal physical input forms in the post-entry-adapter + # unframed coordinates Z_j. In particular Z_512 is not raw initial x_512. + n = 704 + rows = [{i: Q(1)} for i in range(n)] + for e in skeleton[:gap]: + if e[0] != 'scalar': + continue + o = e[1] + need(o[1][0] == 'L', 'no private target before selected group') + t = o[1][1] + if o[0] == 'scale': + q = Q(o[2], o[3]) + need(q != 0, 'invertible scalar scale') + rows[t] = {j: q*v for j, v in rows[t].items()} + elif o[0] == 'add': + need(o[2][0] == 'L', 'productive scalar source') + s, q = o[2][1], Q(o[3], o[4]) + need(s != t, 'invertible shear') + for j, v in list(rows[s].items()): + z = rows[t].get(j, 0) + q*v + if z: rows[t][j] = z + else: rows[t].pop(j, None) + else: + raise ValueError('unexpected prefix scalar') + expected = [{r: Q(1)} for r in REGISTERS] + expected[-1][512] = Q(1) + need([rows[r] for r in REGISTERS] == expected, 'nine literal independent incoming forms') + need([[rows[r].get(c, 0) for c in REGISTERS] for r in REGISTERS] == [[int(i == j) for j in range(9)] for i in range(9)], 'identity dirty-input minor') + return [{str(k): str(v) for k, v in rows[r].items()} for r in REGISTERS] + +def gf_inverse(rows): + n = len(rows) + work = [r | (1 << (n+i)) for i, r in enumerate(rows)] + for j in range(n): + k = next((i for i in range(j, n) if work[i] >> j & 1), None) + need(k is not None, 'invertible binary map') + work[j], work[k] = work[k], work[j] + for i in range(n): + if i != j and work[i] >> j & 1: work[i] ^= work[j] + return [r >> n for r in work] + +def mv(rows, x): + return sum(((r & x).bit_count() & 1) << i for i, r in enumerate(rows)) + +def phase(rec, x): + n = len(rec['matrix_rows']) + return (rec['phase'] + sum(rec['linear_Z4'][i] for i in range(n) if x >> i & 1) + 2*sum(((rec['quadratic_rows'][i] >> (i+1)) & (x >> (i+1))).bit_count() for i in range(n) if x >> i & 1)) % 4 + +def mono(rec, x): + return mv(rec['matrix_rows'], x) ^ rec['offset'], phase(rec, x) + +def rotate(z, p): + a, b = z + return [(a,b),(-b,a),(-a,-b),(b,-a)][p % 4] + +def recipe_column(rec, x): + y, rp = mono(rec['right'], x) + out = {} + for z, coefficient in [(y, (1,1)), (y ^ 1, (1,-1))]: + w, lp = mono(rec['left'], z) + out[w] = rotate(coefficient, rp+lp) + return out # Gaussian integer numerators, common denominator two + +def multiply(a,b): + return (a[0]*b[0]-a[1]*b[1],a[0]*b[1]+a[1]*b[0]) + +def exact_operator(word, recipes): + spec = importlib.util.spec_from_file_location('selected_toom_retained_clifford', ROOT / CLIFFORD) + c = importlib.util.module_from_spec(spec) + sys.modules[spec.name] = c + spec.loader.exec_module(c) + outputs = {} + for frame in (4,5): + rec = next(r for r in recipes['children'] if (r['old'],r['new']) == (0,frame)) + need(rec['rank'] == 1, 'rank-one recipe') + for side in ('left','right'): + gf_inverse(rec[side]['matrix_rows']) + need(len({mono(rec[side],x)[0] for x in range(512)}) == 512, 'monomial permutation') + target = c.canonical_frame(9, tuple(word['frames'][frame])) + columns = [] + for x in range(512): + column = recipe_column(rec,x) + values, den = target.zero_state(x) + expected = {j:(a*(2//(2**den)),b*(2//(2**den))) for j,(a,b) in enumerate(values) if a or b} + need(den == 1, 'one exact halving layer') + need(column == expected, 'literal canonical frame vs independent serialized recipe, all basis vectors') + columns.append(column) + # Sparse Gram is an independent full-rank certificate, not a float rank. + row_to_cols = collections.defaultdict(list) + for x,col in enumerate(columns): + for y,z in col.items(): row_to_cols[y].append((x,z)) + gram = collections.defaultdict(lambda: (0,0)) + for pairs in row_to_cols.values(): + for x,z in pairs: + for y,w in pairs: + product = multiply((z[0],-z[1]),w) + old = gram[x,y] + gram[x,y] = (old[0]+product[0],old[1]+product[1]) + need(all(v == ((4,0) if x == y else (0,0)) for (x,y),v in gram.items()), 'exact unitary Gram') + need(all(gram[x,x] == (4,0) for x in range(512)), '512 independent columns') + digest = hashlib.sha256(json.dumps(columns, sort_keys=True,separators=(',',':')).encode()).hexdigest() + outputs[str(frame)] = {'frame':word['frames'][frame],'rank':512,'column_digest':digest,'basis_zero_numerator':columns[0],'denominator':2} + # Constructive alternative: eight identical maps can be packed on three + # extra lane bits, but this is still rank one on a larger payload. + small = c.canonical_frame(9, (459,)) + packed = c.canonical_frame(12, (459,)) + wanted = tuple(list(small.tab[:9]) + [(1< 6*512 > 3*512, 'Toom input-space strict deficits') + # Homogeneous variable-variable multiplication cannot equal the nonzero + # linear selected block: scaling by two gives factor four, not two. + z=base[0] + need({k:(4*a,4*b) for k,(a,b) in z.items()} != {k:(2*a,2*b) for k,(a,b) in z.items()}, 'quadratic scaling mismatch') + # Explicit naive three-coefficient packing loses dirty register570. + x=[0]*9;x[7]=1 + need(x[:3] == [0,0,0] and x[7] == 1 and base[0] != {}, 'omitted dirty input has nonzero demanded output') + return mutants + ['quadratic_scaling','omitted_dirty_register'] + +def main(): + p,w,r=sources() + need((w['v'],w['R'],w['h']) == (112,480,9), 'selected boundary dimensions') + a,g,s,group=first_group(p['forward']) + events=[row[4] for row in group] + need([e[2] for e in events] == REGISTERS, 'literal first #3974 group') + need(all(lo <= g <= hi for _,_,lo,hi,_ in group), 'common legal gap') + need([e[3:] for e in events] == [[0,4,1]]*8+[[0,5,1]], 'group frames') + need(all(w['start'][q] == 0 and q >= 2*w['v'] for q in REGISTERS), 'cold-entry helpers retain arbitrary dirty payloads') + need(all(not (e[0] == 'residual_adapter' and e[2] in REGISTERS) for e in p['forward'][:a]), 'selected helpers have no hidden entry wrappers') + forms=scalar_prefix(p['forward'],a,g,s,group) + operators=exact_operator(w,r) + result={'scope':'one actual forward phase-A group; same-width Toom-only interface', 'registers':REGISTERS,'original_event_indices_zero_based':[x[0] for x in group], 'skeleton_gap':g,'windows':[[x[2],x[3]] for x in group], 'input_form_coordinates':'post-entry-adapter unframed Z_j; not raw initial payloads', 'input_forms':forms,'operators':operators,'actual_input_and_output_rank':4608,'five_product_linear_decoder_output_rank_upper':2560,'minimum_extra_output_dimension_five_product_decoder':2048,'fixed_factor_toom_input_rank_upper':1536,'two_affine_factors_input_rank_upper':3072,'minimum_extra_input_dimension_two_affine_factors':1536,'controls':controls(w,r),'implemented_replacements':0,'kappa_change':0} + result=json.loads(json.dumps(result)) + expected=json.loads((HERE/'RESULT.json').read_text()) if (HERE/'RESULT.json').exists() else None + if '--write' in sys.argv: (HERE/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else: need(result == expected,'committed result equality') + print('PASS_SELECTED_TOOM3_TYPED_BLOCK basis_columns=1024 actual_rank=4608 affine_toom_input_cap=3072 fixed_factor_cap=1536 controls=4 replacements=0 no_new_kappa') + +if __name__ == '__main__': + main() From 84060b40f2f0ec4ac832fddb33784f066ad1e578 Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 19:11:42 +1100 Subject: [PATCH 2/4] Bind arbitrary-dirty independence to the complete selected entry prefix --- research/selected-toom3-typed-block/PROOF.md | 14 ++++++- .../selected-toom3-typed-block/RESULT.json | 7 ++++ research/selected-toom3-typed-block/verify.py | 40 +++++++++++++++++-- 3 files changed, 56 insertions(+), 5 deletions(-) diff --git a/research/selected-toom3-typed-block/PROOF.md b/research/selected-toom3-typed-block/PROOF.md index 680cecfa34..16ce9d8c20 100644 --- a/research/selected-toom3-typed-block/PROOF.md +++ b/research/selected-toom3-typed-block/PROOF.md @@ -29,8 +29,18 @@ adapters, so physical register `j` is `T_start(j) Z_j`. These are **not** raw initial values: for example register 512 has a residual pre-wrapper. Entry adapters are invertible; frame coordinates do not impose a zero or clean-data promise on a productive helper. The selected nine helpers start at frame zero, -have ordinary identity entry adapters, and end at full frame. The scalar -prefix consists of nonzero scales and shears, hence is invertible. A direct +have ordinary identity entry adapters, and end at full frame. The pinned `INDEPENDENT-LOCAL-REPLAY.json` explicitly declares replay on +"every arbitrary data/helper column", with all 704 input columns and 480 +helpers; this is the selected local replacement contract. The verifier binds +that receipt and independently checks the entire entry prefix consists of +7,344 shears, 56 nonzero scales, 464 typed frame adapters and 240 invertible +monomial residual pre-wrappers. There are no entry clears or copies. The first +1,190 phase-A events before this group are also invertible scalar operations. +Thus the full pre-cut map is invertible on all productive columns, and the +nine payload projection is surjective. This establishes independence from +the actual prefix and its arbitrary-dirty contract, not from an assumed +clean-helper initialization. A globally restricted clean-input caller would +be a different contract; it is not excluded by the dimension argument. A direct rational replay gives the actual incoming forms at the chosen gap: `Z_546,Z_560,Z_547,Z_568,Z_548,Z_558,Z_549,Z_570,Z_464+Z_512`. diff --git a/research/selected-toom3-typed-block/RESULT.json b/research/selected-toom3-typed-block/RESULT.json index 0d1c4031a5..1ef8a04c1f 100644 --- a/research/selected-toom3-typed-block/RESULT.json +++ b/research/selected-toom3-typed-block/RESULT.json @@ -6,6 +6,7 @@ "quadratic_scaling", "omitted_dirty_register" ], + "entry_contract": "every arbitrary data/helper column; exact selected receipt", "five_product_linear_decoder_output_rank_upper": 2560, "fixed_factor_toom_input_rank_upper": 1536, "implemented_replacements": 0, @@ -40,6 +41,12 @@ "512": "1" } ], + "invertible_entry_prefix": { + "frame_adapters": 464, + "residual_pre_wrappers": 240, + "scales": 56, + "shears": 7344 + }, "kappa_change": 0, "minimum_extra_input_dimension_two_affine_factors": 1536, "minimum_extra_output_dimension_five_product_decoder": 2048, diff --git a/research/selected-toom3-typed-block/verify.py b/research/selected-toom3-typed-block/verify.py index d9a5ee37bd..b255bd993e 100644 --- a/research/selected-toom3-typed-block/verify.py +++ b/research/selected-toom3-typed-block/verify.py @@ -35,7 +35,7 @@ def sources(): def obj(name): raw = tar.extractfile(PREFIX + name).read() return json.loads(gzip.decompress(raw) if name.endswith('.gz') else raw) - return obj('LOCAL-PROGRAMS.json.gz'), obj('CANONICAL-WORD.json.gz'), obj('CLIFFORD-RECIPES.json') + return obj('LOCAL-PROGRAMS.json.gz'), obj('CANONICAL-WORD.json.gz'), obj('CLIFFORD-RECIPES.json'), obj('RESIDUAL-ADAPTERS.json'), obj('INDEPENDENT-LOCAL-REPLAY.json') def touches(e): if e[0] in ('climb', 'adapter', 'residual_adapter'): @@ -75,6 +75,38 @@ def first_group(events): return a, g, skeleton, rows raise ValueError('no group') +def entry_contract(events, a, word, residuals, receipt): + need(receipt['local']['forward']['all_exact_columns'] == 704, 'selected receipt binds every incoming column') + need(receipt['helpers'] == 480 and 'every arbitrary data/helper column' in receipt['scope'], 'literal arbitrary-dirty helper contract') + counts=collections.Counter() + for e in events[:a-1]: + tag=e[0] + if tag == 'phase': + continue + if tag == 'scalar': + o=e[1];need(o[1][0] == 'L', 'entry acts on productive columns') + if o[0] == 'add': + need(o[2][0] == 'L' and o[1] != o[2], 'entry invertible shear') + Q(o[3],o[4]);counts['shears']+=1 + elif o[0] == 'scale': + need(Q(o[2],o[3]) != 0, 'entry nonzero scale');counts['scales']+=1 + else: + raise ValueError('entry not invertible scalar operation') + elif tag == 'adapter': + need(e[1] == 'old_to_new' and e[3] == word['start'][e[2]], 'typed entry frame adapter') + counts['frame_adapters']+=1 + elif tag == 'residual_adapter': + need(e[1] == 'pre' and e[3] == word['start'][e[2]], 'typed residual pre-wrapper') + key=str(e[3]) if len(e) == 4 else str(e[3])+':'+str(e[4]) + rec=residuals['recipes'][key]['right'] + gf_inverse(rec['matrix_rows']) + need(len(rec['matrix_rows']) == 9, 'nine-bit monomial wrapper') + counts['residual_pre_wrappers']+=1 + else: + raise ValueError('unexpected entry operation') + need(dict(counts) == {'shears':7344,'scales':56,'frame_adapters':464,'residual_pre_wrappers':240}, 'complete invertible entry prefix') + return dict(counts) + def scalar_prefix(events, a, gap, skeleton, group): # Scalar-coordinate ledger: frame transitions preserve the abstract column. # All selected group columns are still frame zero; therefore their rows @@ -213,9 +245,11 @@ def controls(word,recipes): return mutants + ['quadratic_scaling','omitted_dirty_register'] def main(): - p,w,r=sources() + p,w,r,residuals,receipt=sources() need((w['v'],w['R'],w['h']) == (112,480,9), 'selected boundary dimensions') a,g,s,group=first_group(p['forward']) + entry=entry_contract(p['forward'],a,w,residuals,receipt) + need(all(e[0] == 'scalar' for e in s[:g]), 'first candidate has only invertible scalar prefix') events=[row[4] for row in group] need([e[2] for e in events] == REGISTERS, 'literal first #3974 group') need(all(lo <= g <= hi for _,_,lo,hi,_ in group), 'common legal gap') @@ -224,7 +258,7 @@ def main(): need(all(not (e[0] == 'residual_adapter' and e[2] in REGISTERS) for e in p['forward'][:a]), 'selected helpers have no hidden entry wrappers') forms=scalar_prefix(p['forward'],a,g,s,group) operators=exact_operator(w,r) - result={'scope':'one actual forward phase-A group; same-width Toom-only interface', 'registers':REGISTERS,'original_event_indices_zero_based':[x[0] for x in group], 'skeleton_gap':g,'windows':[[x[2],x[3]] for x in group], 'input_form_coordinates':'post-entry-adapter unframed Z_j; not raw initial payloads', 'input_forms':forms,'operators':operators,'actual_input_and_output_rank':4608,'five_product_linear_decoder_output_rank_upper':2560,'minimum_extra_output_dimension_five_product_decoder':2048,'fixed_factor_toom_input_rank_upper':1536,'two_affine_factors_input_rank_upper':3072,'minimum_extra_input_dimension_two_affine_factors':1536,'controls':controls(w,r),'implemented_replacements':0,'kappa_change':0} + result={'scope':'one actual forward phase-A group; same-width Toom-only interface', 'entry_contract':'every arbitrary data/helper column; exact selected receipt','invertible_entry_prefix':entry,'registers':REGISTERS,'original_event_indices_zero_based':[x[0] for x in group], 'skeleton_gap':g,'windows':[[x[2],x[3]] for x in group], 'input_form_coordinates':'post-entry-adapter unframed Z_j; not raw initial payloads', 'input_forms':forms,'operators':operators,'actual_input_and_output_rank':4608,'five_product_linear_decoder_output_rank_upper':2560,'minimum_extra_output_dimension_five_product_decoder':2048,'fixed_factor_toom_input_rank_upper':1536,'two_affine_factors_input_rank_upper':3072,'minimum_extra_input_dimension_two_affine_factors':1536,'controls':controls(w,r),'implemented_replacements':0,'kappa_change':0} result=json.loads(json.dumps(result)) expected=json.loads((HERE/'RESULT.json').read_text()) if (HERE/'RESULT.json').exists() else None if '--write' in sys.argv: (HERE/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') From e8ed7160e6ce18a13f94a541a9bfbfe1127e9048 Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 19:14:09 +1100 Subject: [PATCH 3/4] Check common frames throughout the literal input-form prefix --- research/selected-toom3-typed-block/PROOF.md | 17 ++++++++++++++--- research/selected-toom3-typed-block/verify.py | 7 +++++-- 2 files changed, 19 insertions(+), 5 deletions(-) diff --git a/research/selected-toom3-typed-block/PROOF.md b/research/selected-toom3-typed-block/PROOF.md index 16ce9d8c20..b94f4b00b4 100644 --- a/research/selected-toom3-typed-block/PROOF.md +++ b/research/selected-toom3-typed-block/PROOF.md @@ -29,7 +29,9 @@ adapters, so physical register `j` is `T_start(j) Z_j`. These are **not** raw initial values: for example register 512 has a residual pre-wrapper. Entry adapters are invertible; frame coordinates do not impose a zero or clean-data promise on a productive helper. The selected nine helpers start at frame zero, -have ordinary identity entry adapters, and end at full frame. The pinned `INDEPENDENT-LOCAL-REPLAY.json` explicitly declares replay on +have ordinary identity entry adapters, and end at full frame. + +The pinned `INDEPENDENT-LOCAL-REPLAY.json` explicitly declares replay on "every arbitrary data/helper column", with all 704 input columns and 480 helpers; this is the selected local replacement contract. The verifier binds that receipt and independently checks the entire entry prefix consists of @@ -40,7 +42,13 @@ Thus the full pre-cut map is invertible on all productive columns, and the nine payload projection is surjective. This establishes independence from the actual prefix and its arbitrary-dirty contract, not from an assumed clean-helper initialization. A globally restricted clean-input caller would -be a different contract; it is not excluded by the dimension argument. A direct +be a different contract; it is not excluded by the dimension argument. + +For the additional input-form receipt, the verifier checks that this first +phase-A prefix contains no climbs or adapters, and every scalar source and +target has the literal common frame recorded by the trace. Thus propagating +plain rational rows in the unframed coordinates is valid. The independent +surjectivity argument above already suffices for the rank obstruction. The rational replay gives the actual incoming forms at the chosen gap: `Z_546,Z_560,Z_547,Z_568,Z_548,Z_558,Z_549,Z_570,Z_464+Z_512`. @@ -86,7 +94,10 @@ the direct recipe decoder and Gram certificate are separate implementations. ## Declared Toom-only substitution contract -The rejected contract has exactly these restrictions: +The rejected contract asks for the formal exact local operator on `W^9`, +not an encoding of a bounded finite set into wider-precision scalar words. +The latter would require its own precision and decoding contract. The +rejected contract has exactly these restrictions: 1. Each polynomial has three coefficients in a vector space of dimension 512 over `Q(i)`. Both triples are produced by affine maps of the nine incoming diff --git a/research/selected-toom3-typed-block/verify.py b/research/selected-toom3-typed-block/verify.py index b255bd993e..1280376cff 100644 --- a/research/selected-toom3-typed-block/verify.py +++ b/research/selected-toom3-typed-block/verify.py @@ -107,7 +107,7 @@ def entry_contract(events, a, word, residuals, receipt): need(dict(counts) == {'shears':7344,'scales':56,'frame_adapters':464,'residual_pre_wrappers':240}, 'complete invertible entry prefix') return dict(counts) -def scalar_prefix(events, a, gap, skeleton, group): +def scalar_prefix(events, a, gap, skeleton, group, word): # Scalar-coordinate ledger: frame transitions preserve the abstract column. # All selected group columns are still frame zero; therefore their rows # here give literal physical input forms in the post-entry-adapter @@ -118,6 +118,9 @@ def scalar_prefix(events, a, gap, skeleton, group): if e[0] != 'scalar': continue o = e[1] + need(word['start'][o[1][1]] == e[2], 'prefix target literal frame matches annotation') + if o[0] == 'add': + need(word['start'][o[2][1]] == e[2], 'prefix source literal frame matches target') need(o[1][0] == 'L', 'no private target before selected group') t = o[1][1] if o[0] == 'scale': @@ -256,7 +259,7 @@ def main(): need([e[3:] for e in events] == [[0,4,1]]*8+[[0,5,1]], 'group frames') need(all(w['start'][q] == 0 and q >= 2*w['v'] for q in REGISTERS), 'cold-entry helpers retain arbitrary dirty payloads') need(all(not (e[0] == 'residual_adapter' and e[2] in REGISTERS) for e in p['forward'][:a]), 'selected helpers have no hidden entry wrappers') - forms=scalar_prefix(p['forward'],a,g,s,group) + forms=scalar_prefix(p['forward'],a,g,s,group,w) operators=exact_operator(w,r) result={'scope':'one actual forward phase-A group; same-width Toom-only interface', 'entry_contract':'every arbitrary data/helper column; exact selected receipt','invertible_entry_prefix':entry,'registers':REGISTERS,'original_event_indices_zero_based':[x[0] for x in group], 'skeleton_gap':g,'windows':[[x[2],x[3]] for x in group], 'input_form_coordinates':'post-entry-adapter unframed Z_j; not raw initial payloads', 'input_forms':forms,'operators':operators,'actual_input_and_output_rank':4608,'five_product_linear_decoder_output_rank_upper':2560,'minimum_extra_output_dimension_five_product_decoder':2048,'fixed_factor_toom_input_rank_upper':1536,'two_affine_factors_input_rank_upper':3072,'minimum_extra_input_dimension_two_affine_factors':1536,'controls':controls(w,r),'implemented_replacements':0,'kappa_change':0} result=json.loads(json.dumps(result)) From 251aba3a98e6eae2e2dd26c954aa0d1b2069cd4c Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 19:25:29 +1100 Subject: [PATCH 4/4] Extend the selected Toom interface obstruction to rational encodings and decoders --- research/selected-toom3-typed-block/PROOF.md | 54 ++++++++++++++++++- research/selected-toom3-typed-block/README.md | 20 +++++-- .../selected-toom3-typed-block/RESULT.json | 8 ++- research/selected-toom3-typed-block/TASK.json | 6 +-- .../selected-toom3-typed-block/VERIFY.json | 2 +- research/selected-toom3-typed-block/verify.py | 24 +++++++-- 6 files changed, 99 insertions(+), 15 deletions(-) diff --git a/research/selected-toom3-typed-block/PROOF.md b/research/selected-toom3-typed-block/PROOF.md index b94f4b00b4..347eac8270 100644 --- a/research/selected-toom3-typed-block/PROOF.md +++ b/research/selected-toom3-typed-block/PROOF.md @@ -146,6 +146,58 @@ interpolation scalars are central: each ordered term is `A_i B_j`, and no reversal is used. What is missing here is a typed coefficient embedding of nine independent payloads, not a scalar identity. +## Larger rational-interface obstruction + +There is a separate extension beyond affine encoders: allow **rational +encoding and rational decoding** over K=Q(i). This does not assume, or imply, +that an arbitrary set-theoretic decoder is rational. + +Let x=(x_1,...,x_N) be algebraically independent over K, N=4608, and let +E=(E_1,...,E_m) be rational functions in K(x). All fixed coefficients and fixed +side information belong to K. If independent other dirty coordinates remain +visible as parameters, adjoin them to the base field and work at the generic +full cut; invertibility of the full prefix keeps the nine selected payloads +algebraically independent over that field. No special zero-valued helper +slice is required, since such a slice could annihilate a denominator. +Suppose D is rational over K, every denominator +of D remains nonzero after substitution E(x), and `D(E(x))=F x` as a generic +rational identity, where F is the exact invertible selected operator. Then + +`K(x)=K(F x) subset K(E_1,...,E_m) subset K(x)`. + +Indeed F inverse recovers each x_j from the coordinates of F x. The fields +are equal, but the middle field has transcendence degree at most m over K, +whereas K(x) has transcendence degree N. Therefore **m >= 4608**. Equivalently, +the chain rule on the generic domain gives `J_D(E) J_E=F`; the left side has +rank at most m and the right side rank 4608. This differential proof uses +characteristic zero and the same generic-denominator condition. + +The two coefficient triples contain m=3072 scalar rational functions. A fixed +operand leaves m=1536. If the decoder receives only the five product blocks, +m=2560, so the product-only deficit is **2048 even for a nonlinear rational +decoder**. Every input-dependent bypass, retained register or side channel +visible to the decoder must be counted in m. Adding d rational side-channel +coordinates thus requires d at least 1536, 3072 or 2048 respectively; these are +information dimensions, not operation/child/native-cost lower bounds. + +Ordinary Toom evaluation and interpolation are rational scalar operations. +Any fixed finite-dimensional bilinear coefficient algebra, including a +noncommutative one with structure constants in K, has polynomial multiplication +in its scalar entries. Variable inversion is rational where the element is a +unit and the corresponding denominator is nonzero. Thus this larger model +covers rational coefficient preparation, those products and rational output +recovery, while leaving nonrational operations, wider coefficient spaces, +finite-set/precision encodings and changed output contracts open. A denominator +vanishing identically on the encoded image does not define an available +rational decoder there. Pointwise injectivity over the countable field K is +not a replacement for the formal generic identity. + +A small verifier fixture demonstrates a legal nonlinear rational change of +coordinates `(x/y,y/z,z)` with exact inverse `(uvw,vw,w)`, and rejects the +lost-scale map `(x/y,y/z)` and the identically undefined decoder denominator +`u-v` under encoding `(x,x)`. These fixtures check boundary failure modes; +the written function-field/chain-rule argument proves the general theorem. + ## What can reopen the route Adding an affine side channel of scalar dimension d changes the encoding to @@ -153,7 +205,7 @@ Adding an affine side channel of scalar dimension d changes the encoding to factor it requires **d >= 3072**. These are information dimensions, **not** native operation, child-count, storage, or time lower bounds. Already-retained productive data could supply such a channel; its exact use and legal costs -must be specified. Wider coefficient spaces, data-dependent non-affine +must be specified. Wider coefficient spaces, nonrational data encoding, a different output contract, or a new coupled recursive primitive are also outside this proposition. A wider space must be priced at its actual recursive size, rather than silently counted as the same five children. diff --git a/research/selected-toom3-typed-block/README.md b/research/selected-toom3-typed-block/README.md index cba259cc2e..ad87055215 100644 --- a/research/selected-toom3-typed-block/README.md +++ b/research/selected-toom3-typed-block/README.md @@ -2,7 +2,9 @@ **One actual nine-climb group is an invertible 4,608-dimensional linear map. It cannot factor through the 3,072-dimensional input boundary of a same-width, -Toom-only coefficient module. No replacement or new kappa is claimed.** +Toom-only coefficient module. The obstruction extends to rational encoders +and rational decoders by transcendence degree. No replacement or new kappa +is claimed.** This answers the first source-binding experiment left by Gonzalo Mier's [PR #3974](https://github.com/CrocSwap/integer-mult-bounds/pull/3974), head @@ -17,13 +19,19 @@ coefficients per operand. We reconstruct both 512-dimensional Clifford maps on **all 1,024 basis columns**, including phases and halving, and independently check their exact Gram matrices. The selected block rank is **4,608**. -| Explicit coefficient interface | Maximum linear input rank | Deficit | +| Explicit coefficient interface | Capacity in scalar dimensions | Deficit | |---|---:|---:| | One variable coefficient triple, one fixed factor | 1,536 | 3,072 | | Two affine variable coefficient triples, decoder may read both | 3,072 | 1,536 | -| Five product blocks, affine output decoder | 2,560 | 2,048 | +| Five product blocks, affine or rational output decoder | 2,560 | 2,048 | | Actual selected nine-payload boundary | 4,608 | 0 | +The rational extension uses `K(x)=K(Fx) subset K(E(x))` and transcendence +degree, or equivalently the generic Jacobian chain rule. Decoder denominators +must remain nonzero after substitution and all input-dependent side data +must be counted. The original affine-encoder result permits an arbitrary +decoder; the rational-encoder extension requires rational decoding. + The obstruction assumes outputs receive data only through the coefficient blocks. General circuits may retain original inputs or use bypasses; five child calls alone do not imply this factorization. The deficits are algebraic @@ -46,7 +54,8 @@ python3 scripts/research_package.py --package research/selected-toom3-typed-bloc The two registered runs (normal and optimized Python) bind the selected archive, reconstruct the first eligible group, derive its input minor, check all basis columns and exact Gram matrices, compare the result, and exercise -four failure controls. They do not replay the complete selected supplier. +six failure controls, including a legal birational-coordinate fixture and +rejected lost-scale/undefined-denominator boundaries. They do not replay the complete selected supplier. The canonical-frame evaluator is retained predecessor code; the recipe interpreter and sparse Gram check are new separate implementations. No independent human or formal-kernel acceptance is claimed. @@ -82,5 +91,6 @@ lineage. Predecessor attribution is preserved rather than treating archive retention as scientific acceptance. Prepared for Clear1nsight with substantial OpenAI Codex assistance in source -inspection, proof, implementation and exposition. Apache-2.0. Frozen sources +inspection, proof, implementation and exposition, with separate same-team mathematical +review of the rational-interface extension. Apache-2.0. Frozen sources are unchanged. diff --git a/research/selected-toom3-typed-block/RESULT.json b/research/selected-toom3-typed-block/RESULT.json index 1ef8a04c1f..0aad756d38 100644 --- a/research/selected-toom3-typed-block/RESULT.json +++ b/research/selected-toom3-typed-block/RESULT.json @@ -4,10 +4,13 @@ "global_phase", "translation", "quadratic_scaling", - "omitted_dirty_register" + "omitted_dirty_register", + "rational_lost_scale", + "rational_undefined_pullback" ], "entry_contract": "every arbitrary data/helper column; exact selected receipt", "five_product_linear_decoder_output_rank_upper": 2560, + "five_product_rational_decoder_transcendence_degree_upper": 2560, "fixed_factor_toom_input_rank_upper": 1536, "implemented_replacements": 0, "input_form_coordinates": "post-entry-adapter unframed Z_j; not raw initial payloads", @@ -117,7 +120,8 @@ 570, 464 ], - "scope": "one actual forward phase-A group; same-width Toom-only interface", + "scope": "one actual forward phase-A group; affine coefficient-only and rational-encoding/rational-decoding Toom-only interfaces", + "six_coefficient_rational_field_transcendence_degree_upper": 3072, "skeleton_gap": 1190, "two_affine_factors_input_rank_upper": 3072, "windows": [ diff --git a/research/selected-toom3-typed-block/TASK.json b/research/selected-toom3-typed-block/TASK.json index 5475f4c04a..38752761ff 100644 --- a/research/selected-toom3-typed-block/TASK.json +++ b/research/selected-toom3-typed-block/TASK.json @@ -52,15 +52,15 @@ ] }, "scope_status": "changed", - "actual_scope": "Bind one literal selected nine-climb event group to its exact linear operator and reject a specified same-width Toom-only coefficient interface by input dimension.", + "actual_scope": "Bind one literal selected nine-climb event group to its exact linear operator and reject a specified same-width Toom-only coefficient interface by input dimension. Extend the interface obstruction from affine encoders to rational encoders with rational decoders by transcendence degree.", "scope_change_reason": "PR3974 provides an ordinary convolution identity and candidate event windows but no typed coefficient embedding. This experiment resolves that next boundary obligation on one actual group.", "bottleneck_link": "Prevent counting hypothetical nine-to-five rank-one savings when the proposed coefficient boundary loses independent dirty payloads; a changed interface must be priced before any kappa extrapolation.", "budget_minutes": 60, "stop_rule": "Stop after one exact group, explicit operator, dimension obstruction and bounded controls. Reopen only on an explicit bypass or wider-coefficient interface and complete paid invoice; do not expand the event census.", "outcome": "negative-result", - "evidence": "1024 exact basis columns and sparse Gram matrices establish actual block rank4608; same-width affine coefficient-only input cap3072, fixed-factor cap1536, and product-only affine output cap2560. Constructive eight-lane packing has width4096 and Fourier rank1. Zero realized replacements; no kappa improvement.", + "evidence": "1024 exact basis columns and sparse Gram matrices establish actual block rank4608; same-width affine coefficient-only input cap3072, fixed-factor cap1536, and product-only affine output cap2560. Constructive eight-lane packing has width4096 and Fourier rank1. Zero realized replacements; no kappa improvement. Generic rational recovery requires4608algebraically independent coordinates;3072coefficient or2560product coordinates cannot suffice without counted side information.", "author": "Clear1nsight with OpenAI Codex", - "ai_assistance": "Substantial OpenAI Codex assistance for source analysis, mathematical argument, exact verifier, documentation and publication.", + "ai_assistance": "Substantial OpenAI Codex assistance for source analysis, mathematical argument, exact verifier, documentation and publication. Separate same-team mathematical review checked the rational-interface strengthening.", "open_questions": [ { "question": "Can a changed Toom interface carry the missing input data and realize all nine outputs with five legal children?", diff --git a/research/selected-toom3-typed-block/VERIFY.json b/research/selected-toom3-typed-block/VERIFY.json index 39810f6cde..951985a89a 100644 --- a/research/selected-toom3-typed-block/VERIFY.json +++ b/research/selected-toom3-typed-block/VERIFY.json @@ -16,7 +16,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Exact source-bound group, literal input forms,1024basis columns,Gram ranks and four mutation/degree controls." + "checks": "Exact source-bound group, literal input forms,1024basis columns,Gram ranks, six failure controls and rational-interface boundary fixtures; general rational obstruction is proved in PROOF.md." }, { "argv": [ diff --git a/research/selected-toom3-typed-block/verify.py b/research/selected-toom3-typed-block/verify.py index 1280376cff..42c189a001 100644 --- a/research/selected-toom3-typed-block/verify.py +++ b/research/selected-toom3-typed-block/verify.py @@ -228,6 +228,24 @@ def exact_operator(word, recipes): outputs['eight_lane_packing'] = {'payload_dimension':4096,'index_bits':12,'fourier_rank':1,'same_rank_payload_multiplier':8,'paid_profile_delta':'unknown; no admitted larger-payload call'} return outputs +def rational_boundary_fixture(): + # Laurent monomials are exact rational functions; exponent addition gives + # exact substitution. This fixture does not prove the general theorem. + encoding = [(1,-1,0),(0,1,-1),(0,0,1)] + inverse = [(1,1,1),(0,1,1),(0,0,1)] + def substitute_monomial(exponents, images): + return tuple(sum(e*image[j] for e,image in zip(exponents,images)) for j in range(3)) + need([substitute_monomial(row,encoding) for row in inverse] == [(1,0,0),(0,1,0),(0,0,1)], 'rational birational positive control') + def ratio_pair(x): return Q(x[0],x[1]),Q(x[1],x[2]) + need(ratio_pair((1,2,3)) == ratio_pair((2,4,6)), 'lost common scale in rational encoding') + need((1,2,3) != (2,4,6), 'distinct required outputs for lost-scale pair') + # Pull back u-v by (u,v)=(x,x). Cancellation is identically zero, + # so 1/(u-v) cannot be used as a generic decoder on that image. + denominator=collections.defaultdict(int) + for coefficient,image in [(1,(1,0,0)),(-1,(1,0,0))]: denominator[image]+=coefficient + need(not any(denominator.values()), 'identically vanishing pulled-back denominator rejected') + return ['rational_lost_scale','rational_undefined_pullback'] + def controls(word,recipes): import copy rec = next(r for r in recipes['children'] if (r['old'],r['new']) == (0,4)) @@ -245,7 +263,7 @@ def controls(word,recipes): # Explicit naive three-coefficient packing loses dirty register570. x=[0]*9;x[7]=1 need(x[:3] == [0,0,0] and x[7] == 1 and base[0] != {}, 'omitted dirty input has nonzero demanded output') - return mutants + ['quadratic_scaling','omitted_dirty_register'] + return mutants + ['quadratic_scaling','omitted_dirty_register'] + rational_boundary_fixture() def main(): p,w,r,residuals,receipt=sources() @@ -261,12 +279,12 @@ def main(): need(all(not (e[0] == 'residual_adapter' and e[2] in REGISTERS) for e in p['forward'][:a]), 'selected helpers have no hidden entry wrappers') forms=scalar_prefix(p['forward'],a,g,s,group,w) operators=exact_operator(w,r) - result={'scope':'one actual forward phase-A group; same-width Toom-only interface', 'entry_contract':'every arbitrary data/helper column; exact selected receipt','invertible_entry_prefix':entry,'registers':REGISTERS,'original_event_indices_zero_based':[x[0] for x in group], 'skeleton_gap':g,'windows':[[x[2],x[3]] for x in group], 'input_form_coordinates':'post-entry-adapter unframed Z_j; not raw initial payloads', 'input_forms':forms,'operators':operators,'actual_input_and_output_rank':4608,'five_product_linear_decoder_output_rank_upper':2560,'minimum_extra_output_dimension_five_product_decoder':2048,'fixed_factor_toom_input_rank_upper':1536,'two_affine_factors_input_rank_upper':3072,'minimum_extra_input_dimension_two_affine_factors':1536,'controls':controls(w,r),'implemented_replacements':0,'kappa_change':0} + result={'scope':'one actual forward phase-A group; affine coefficient-only and rational-encoding/rational-decoding Toom-only interfaces', 'entry_contract':'every arbitrary data/helper column; exact selected receipt','invertible_entry_prefix':entry,'registers':REGISTERS,'original_event_indices_zero_based':[x[0] for x in group], 'skeleton_gap':g,'windows':[[x[2],x[3]] for x in group], 'input_form_coordinates':'post-entry-adapter unframed Z_j; not raw initial payloads', 'input_forms':forms,'operators':operators,'actual_input_and_output_rank':4608,'five_product_rational_decoder_transcendence_degree_upper':2560,'six_coefficient_rational_field_transcendence_degree_upper':3072,'five_product_linear_decoder_output_rank_upper':2560,'minimum_extra_output_dimension_five_product_decoder':2048,'fixed_factor_toom_input_rank_upper':1536,'two_affine_factors_input_rank_upper':3072,'minimum_extra_input_dimension_two_affine_factors':1536,'controls':controls(w,r),'implemented_replacements':0,'kappa_change':0} result=json.loads(json.dumps(result)) expected=json.loads((HERE/'RESULT.json').read_text()) if (HERE/'RESULT.json').exists() else None if '--write' in sys.argv: (HERE/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') else: need(result == expected,'committed result equality') - print('PASS_SELECTED_TOOM3_TYPED_BLOCK basis_columns=1024 actual_rank=4608 affine_toom_input_cap=3072 fixed_factor_cap=1536 controls=4 replacements=0 no_new_kappa') + print('PASS_SELECTED_TOOM3_TYPED_BLOCK basis_columns=1024 actual_rank=4608 affine_toom_input_cap=3072 fixed_factor_cap=1536 controls=6 replacements=0 no_new_kappa') if __name__ == '__main__': main()