diff --git a/research/selected-toom3-typed-block/PROOF.md b/research/selected-toom3-typed-block/PROOF.md new file mode 100644 index 0000000000..347eac8270 --- /dev/null +++ b/research/selected-toom3-typed-block/PROOF.md @@ -0,0 +1,249 @@ +# 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 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. + +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`. + +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 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 + 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. + +## 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 +`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, 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. + +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..ad87055215 --- /dev/null +++ b/research/selected-toom3-typed-block/README.md @@ -0,0 +1,96 @@ +# 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. 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 +`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 | 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 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 +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 +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. + +## 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, 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 new file mode 100644 index 0000000000..0aad756d38 --- /dev/null +++ b/research/selected-toom3-typed-block/RESULT.json @@ -0,0 +1,165 @@ +{ + "actual_input_and_output_rank": 4608, + "controls": [ + "global_phase", + "translation", + "quadratic_scaling", + "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", + "input_forms": [ + { + "546": "1" + }, + { + "560": "1" + }, + { + "547": "1" + }, + { + "568": "1" + }, + { + "548": "1" + }, + { + "558": "1" + }, + { + "549": "1" + }, + { + "570": "1" + }, + { + "464": "1", + "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, + "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; 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": [ + [ + 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..38752761ff --- /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. 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. 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. 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?", + "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..951985a89a --- /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, six failure controls and rational-interface boundary fixtures; general rational obstruction is proved in PROOF.md." + }, + { + "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..42c189a001 --- /dev/null +++ b/research/selected-toom3-typed-block/verify.py @@ -0,0 +1,290 @@ +#!/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'), obj('RESIDUAL-ADAPTERS.json'), obj('INDEPENDENT-LOCAL-REPLAY.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 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, 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 + # 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(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': + 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'] + rational_boundary_fixture() + +def main(): + 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') + 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,w) + operators=exact_operator(w,r) + 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=6 replacements=0 no_new_kappa') + +if __name__ == '__main__': + main()