diff --git a/research/native-coarse-grid-residue-codec/NOTICE b/research/native-coarse-grid-residue-codec/NOTICE new file mode 100644 index 0000000000..2d5bb70ae5 --- /dev/null +++ b/research/native-coarse-grid-residue-codec/NOTICE @@ -0,0 +1,43 @@ +Ali Romman with substantial OpenAI Codex assistance. No subagents. +New work is Apache-2.0. All consumed source files remain unchanged. + +DreamingOfClouds supplies the selected PR6030 word and its retained P104 +lineage. Cinna Davis (@1337isnot1337), PR4088 and PR2226, supplies the consumed +native compiler/coordinate representations. Retain the native/compiler work +of icekylinx, DreamingOfClouds, vendor531, Rohan Arun and earlier contributors. +https://github.com/CrocSwap/integer-mult-bounds/pull/6030 +https://github.com/CrocSwap/integer-mult-bounds/pull/4088 +https://github.com/CrocSwap/integer-mult-bounds/pull/2226 + +Dugongue's PR5815 supplies the Gaussian Smith construction and tensor schedule. +Ali Romman's PR5821 supplies its executed reference and image-information +proofs. Nick Petalas's PR5880 supplies a different modular-overwrite clean-bit +minimum and attaining full-state permutation. The present code is a changed- +grid stochastic quotient codec, not a new Smith decomposition or an extension +of that physical permutation result. +https://github.com/CrocSwap/integer-mult-bounds/pull/5815 +https://github.com/CrocSwap/integer-mult-bounds/pull/5821 +https://github.com/CrocSwap/integer-mult-bounds/pull/5880 + +PR6499 supplies the complete selected scalar-record grid interface. PR6506 +supplies its Boolean scalar layer. PR6532 supplies the prior selected same-grid +unbiased native construction and its relative-error limit. No caller error +constant is transferred to this new quantizer without a proof. +https://github.com/CrocSwap/integer-mult-bounds/pull/6499 +https://github.com/CrocSwap/integer-mult-bounds/pull/6506 +https://github.com/CrocSwap/integer-mult-bounds/pull/6532 + +Nick Petalas's PR6438 supplies the optimal unbiased reversible ensemble +question. His PR6418 and zxv's PR6066 retain adaptive-seed and scalar residue +credit. PR6068 supplies the finite-fair-bit denominator obstruction. Adjacent- +grid stochastic rounding, lattice quotients and counting arguments are +classical. No global literature priority is claimed. +https://github.com/CrocSwap/integer-mult-bounds/pull/6438 +https://github.com/CrocSwap/integer-mult-bounds/pull/6418 +https://github.com/CrocSwap/integer-mult-bounds/pull/6066 +https://github.com/CrocSwap/integer-mult-bounds/pull/6068 + +The earlier Gaussian/native/precision lineage includes Tekalign, JoyboyBrian, +Arham Tahir, Adam Gall, ywz65 and all notices in the cited predecessor chains. +The new contribution is the explicit coarsening codec, its source bindings, +the stated information and sampling optima, and its full direct invoice. diff --git a/research/native-coarse-grid-residue-codec/PROOF.md b/research/native-coarse-grid-residue-codec/PROOF.md new file mode 100644 index 0000000000..1f07baed7f --- /dev/null +++ b/research/native-coarse-grid-residue-codec/PROOF.md @@ -0,0 +1,233 @@ +# Unbiased native coarsening with an exact residue codec + +This result gives a numerical interface and an information-preserving codec. +It does not give a new kappa, a finite-state reversible circuit or a tape bill. +The retained-information optimum is for the full fine input grid. Correlations +in an actual caller can reduce that information; no caller storage optimum is +claimed. + +## Contract and source + +Let A=L C_r R be a serialized Gaussian native child on 512 complex coordinates. +L and R are Gaussian-unit signed permutations, including their global phases. +The central pair is C=[[1+i,1-i],[1-i,1+i]]/2. At tensor width f>=1, put +N=512^f, a=r*f, d=ceil(a/2), and use the tensor L,R with a active C axes. +Below, A denotes this complete tensor operator. Choose integer k>=d and m=2^k. +Input x is any vector in Z[i]^N, stored in units h/m for h>0. Output q is in +Z[i]^N, stored in units h. One fresh uniform integer u in [0,2^(k+d)) serves +every real and imaginary coordinate of the call. The seed stays unchanged. + +The selected PR6030 word has 3453 MOVE events, 2886 distinct directed frame +edges, and 1001 frames used by those edges. All endpoint frame checks pass. +An independent 18-bit matrix inverse/composition and finite-span pass agrees +with every B block and the complete rank census. +The rank census is 2219,457,496,100,163,11,6,1 for ranks 1 through 8. The +unchanged Clifford compiler and separate coordinate oracle agree on all 512 +columns of the first event of each rank. The new interpreter also checks all +4096 columns. It does not instantiate every one of the 2886 edge recipes. +The universal argument applies to any supplied L C_r R recipe in this class. + +Source pins are in SOURCES.json. The selected word and the retained native +implementations are unchanged. The native/global compiler and all-size supplier +premises are not discharged by these representative checks. + +## One common seed gives the minimum unbiased mean squared error + +Each entry of C^tensor a has an integer Gaussian numerator over 2^d. Products +of a factors 1+i or 1-i are divisible by 2^floor(a/2). Gaussian monomials +preserve this property. Thus n=2^d A x is an integer Gaussian vector. +Set D=2^(k+d), and round each real component by + +```text +q_j = floor((n_j+u)/D). +``` + +Write n_j=D*b_j+t_j with 0<=t_j=0 gives Var(Z)>=t*(D-t)/D^2. Summing over real coordinates +proves that this quantizer attains the least possible mean squared error among +ALL unbiased grid-valued outputs at each input. Reversibility is not required +for this lower bound. Some outcomes are the farther adjacent integer; no +minimum deterministic-error claim is made. + +A unit input column has a real or imaginary numerator equal to +1 or -1 after +the common reduction to denominator 2^d. Gaussian monomials preserve that +property. Its required mean is +1/D or -1/D. An integer-valued sampler using +a fixed b fair bits has a mean equal to an integer divided by 2^b. It needs +b>=k+d, even without the minimum-error condition. The common seed attains this +minimum fixed fair-bit count. This is not a minimum entropy or expected variable-length +sampling theorem. Reuse of the same seed in a later adaptive call is not +authorized by the conditional proof. The inverse uses the retained seed for +exact decoding; it is not a new stochastic call. + +## The coarse-period lattice and its explicit Gaussian digits + +Because k>=d, B=m*A^-1 is integral over Z[i]. The quantizer Q_u satisfies + +```text +Q_u(x+B*z) = Q_u(x)+z for every z in Z[i]^N. +``` + +Put pi=1+i and H=[[1,i],[i,1]]. Then C^-1=pi^-1 H. The integral unimodular +matrices U=[[1,0],[-i,1]] and V=[[1,-i],[0,1]] satisfy U H V=diag(1,2). +Tensor them over the a active axes. The source R maps the period lattice +B Z[i]^N to m*C^(-tensor a) Z[i]^N, since L^-1 preserves Z[i]^N. Applying U +maps it to a diagonal Gaussian lattice with coordinate ideals + +```text +(pi^e_j), e_j = 2*k-a+2*weight(active bits of address j). +``` + +Indeed m*pi^-a*2^weight is a Gaussian unit times pi^e_j. Every e_j is +nonnegative. Their sum is 2*k*N because each active address bit is one at +exactly half the coordinates. Thus + +```text +Z[i]^N / B Z[i]^N is isomorphic to product_j Z[i]/(pi^e_j), +number of cosets = 2^(2*k*N). +``` + +These Gaussian Smith methods are prior work, including +[PR5815](https://github.com/CrocSwap/integer-mult-bounds/pull/5815), its +[executed form](https://github.com/CrocSwap/integer-mult-bounds/pull/5821), and +the distinct modular-overwrite capacity in +[PR5880](https://github.com/CrocSwap/integer-mult-bounds/pull/5880). +The new use here is the quantizer's coarse-period quotient, its exact codec, +the minimum unbiased law and the actual selected native bindings. + +Each Gaussian remainder has exactly e_j binary pi-adic digits. For z=A+iB, +take digit b=(A+B) mod 2, subtract b and divide by pi. The quotient is +((A-b+B)/2)+i*((B-A+b)/2), with exact integer halves. Repeat e_j times. +The e_j bits give one representative of every coset modulo pi^e_j. Reverse +Horner evaluation with pi reconstructs the representative. The implementation +packs all digits into exactly 2*k*N bits; byte containers use ceiling(bits/8) +bytes with required zero padding. At N=512^f there is no padding. + +## Exact two-sided codec and sharp retained information + +Encode x by taking the digits of U R x and returning (Q_u(x),digits). Decode +the digits to a representative x0 by applying U^-1 and R^-1. Then set + +```text +z = q-Q_u(x0), +x = x0+B*z. +``` + +The translation identity proves Q_u(x)=q. The added B*z leaves the digits +unchanged. Conversely, any original x differs from its representative by a +unique B*z, so this formula recovers it exactly. For every fixed u, this is +a bijection between the fine-grid integer input representation and all pairs +(coarse integer output, 2*k*N-bit residue label). Every coarse output has +exactly 2^(2*k*N) fine-grid preimages. + +An injective implementation that retains the seed and coarse output therefore +needs at least 2*k*N bits of additional information. An arbitrary finite dirty +bank with Q possible initial values cannot reduce this bound: the preimage +slice has 2^(2*k*N)*Q states and the output side has at most 2^b*Q states. +The codec attains b=2*k*N. This is a retained-label capacity result on the +advertised full input lattice. It is NOT an initially clean hardware-register +minimum, a full-state permutation on identical finite registers, or a lower +bound on correlated inputs reached by the complete selected caller. + +The label cannot be erased from q and u alone. The inverse needs it. Any +physical uncompute, reuse, ownership or erasure schedule must still be paid. +The mathematical conversion between two representations does not silently +provide such a circuit. + +## Selected grid interface and its boundary + +At f=1 every selected MOVE rank is at most 8. Thus k=5 is sufficient. A call +accepts the h/32 grid and returns the h grid, matching the grid ratio in +[PR6499](https://github.com/CrocSwap/integer-mult-bounds/pull/6499) and +[PR6506](https://github.com/CrocSwap/integer-mult-bounds/pull/6506). Each full-grid +codec retains 5120 bits. Its seed has 5+ceil(r/2) bits, hence 6 through 9 for +the selected ranks. Allocating one such residue slot for each of the 3453 +MOVE events uses 17,679,360 bits; separate fresh seeds use 21,683 bits. +These are uncompressed slot counts for that proposed interface, not joint +entropy lower bounds or a complete multiplication invoice. + +This is only a grid match. The stochastic error contract is new; the scalar +predecessors' completed error budgets are not imported as proved consequences. +Whole-word restoration and caller probability bounds remain open. At tensor +width f, k>=ceil(r*f/2) is required for the stated integral-period codec. +Fixed k=5 does not cover all widths. For the rank-eight class, k>=4*f is +required. A larger fine grid can represent the scalar inputs but has a larger +full-grid residue code; its cost must not be omitted. + +The condition is exact for integral inclusion m*A^-1 Z[i]^N subset Z[i]^N: +a unit column has a primitive component over 2^d. If k=1, a sufficient signed +temporary width is W=w+4*a+2*k+12. One raw native stage enlarges a component +by at most four. A triangular stage enlarges it by at most two. A pi^e digit +representative has magnitude below 3*2^(e/2), and e<=2*k+a. These bounds give +an x0 component bound 2^(k+ceil(a/2)+a+2); the coarse q0, direct inverse and +final scale fit W. The width is sufficient, not optimal. Addresses need +O(f+log(k+1)) bits. The displayed algorithm thus uses +O((a+k+f)*N*(w+a+k+f)) indexed bit work and O(N*(w+a+k)) data storage, plus +the 2*k*N retained bits. At most six live Gaussian fields are needed during +decoding, including its coarse input, with separate precision/route tables. + +This ordinary integer reference does not provide a reversible gate circuit, +fixed multitape routing, physical clean storage, sampler access, entropy +recovery, an accelerated recursive tariff or a complete caller. It does not +imply additivity, native-graph flatness or dirty compensation after intervening +arithmetic. All five selected assumptions and the frontier remain unchanged. + +## Verification scope + +The finite checks enumerate 25,184 complete quotient endpoints and 16 retained- +bit collisions, compare 36 small tensors to a separate dense coefficient oracle, +and run 432 small seed round trips. The source checks include 4096 columns in +each of two interpreters, 128 signed source round trips, 64 arbitrary coarse/ +residue endpoints and exact means/variances for all 1920 relevant seeds. +A full 262,144-coordinate tensor uses a 524,288-bit label and all four seeds; +its exact mean squared error is 326311/4, below N/2. Eleven semantic/domain +controls and three source corruption controls are retained. These finite checks +corroborate the all-size proof. Independent human and proof-kernel acceptance, +all selected native instances and a complete selected cold replay are unrun. diff --git a/research/native-coarse-grid-residue-codec/README.md b/research/native-coarse-grid-residue-codec/README.md new file mode 100644 index 0000000000..2d192cd0b4 --- /dev/null +++ b/research/native-coarse-grid-residue-codec/README.md @@ -0,0 +1,89 @@ +# Unbiased native coarsening with an exact residue codec + +A Gaussian native child can now accept a fine grid and return an unbiased +coarse-grid output while retaining exactly the information needed for inversion. +For N=512^f, a=r*f active axes and grid ratio 2^k with k>=ceil(a/2), the codec +uses 2*k*N retained bits and one fresh uniform seed of k+ceil(a/2) bits. It +attains the minimum possible unbiased mean squared error at every input. The +retained information and fixed fair-bit count are sharp in the stated classes. + +The [proof](PROOF.md), [executable codec](codec.py), [generated receipt](RESULT.json) +and [source pins](SOURCES.json) give the contracts and limits. This is a +numerical interface and representation codec, not a new kappa or a finite-state +reversible circuit. Its storage optimum concerns the full fine input grid; +actual caller correlations can reduce the required information. + +## Selected source binding + +The selected PR6030 word has 3453 MOVE events, with ranks 1 through 8. The +complete frame ledger and rank census pass; an independent binary matrix and +finite-span pass checks every B block and the full census. The unchanged native compiler, +independent coordinate oracle and new interpreter check all 512 columns for +the first event of each rank. The other 2878 distinct edge recipes are not +instantiated by this package. The theorem applies to any supplied L C_r R +recipe in the stated class. + +At width one, k=5 accepts the h/32 grid and returns the h grid used by the +PR6499/PR6506 scalar interfaces. A full-grid record uses 5120 retained bits and +6–9 fresh seed bits. One record slot for each MOVE uses 17,679,360 retained +bits and 21,683 separate fresh seed bits. These are proposed uncompressed +slots, not a complete invoice or joint storage lower bound. At larger widths +k must satisfy ceil(r*f/2); fixed k=5 is not an all-width result. + +## Verification + +The checks enumerate 25,184 complete quotient endpoints, 16 retained-bit +witnesses, 36 independent dense tensor cases and 432 small seed round trips. +Source checks include all 4096 representative columns in each of two +interpreters, 128 signed native round trips, 64 arbitrary residue endpoints +and exact means/variances for all 1920 seeds. All four seeds of a complete +262,144-coordinate tensor input pass with a 524,288-bit residue code. +Eleven semantic/domain controls and three source corruption controls pass. + +Use CPython 3.12 and NumPy 2.3.4: + +```sh +python3.12 -B scripts/research_package.py --package research/native-coarse-grid-residue-codec +``` + +The registered commands use isolated, warning-strict normal and optimized +modes. The unchanged source compiler/oracle run in a normal subprocess with +assertions enabled in both modes. Expected markers are +`PASS_NATIVE_COARSE_GRID_RESIDUE_CODEC` and `PASS_REGISTERED_RESEARCH_PACKAGE`. + +## Complete scope + +The proof gives the direct native, triangular, monomial, digit, arithmetic, +copy, width and buffer bills. It includes every encode/decode pass. The +O((a+k+f)*N*(w+a+k+f)) indexed bit-work bound is not an accelerated recursive +supplier or a fixed multitape schedule. Exact input recovery requires the +residue and seed. It does not justify free erasure, additivity, native-graph +consistency or cleanup after intervening arithmetic. + +All five selected assumptions remain. The scalar predecessors' completed error +constants are not imported into this changed stochastic contract. Sampling, +physical seed access, residue lifetimes, reversible bit circuits, full caller +probability/restoration and outer admission remain open. A selected cold replay, +all native instances, predecessor full suites, independent human acceptance and +proof-kernel review were not run. See the PR for publication and hosted status. + +## Open next questions + +The next step is a complete caller join with a paid residue and randomness +schedule. First bind its error budget and every retained record lifetime to +the source rank census. The higher tensor precision requirement and physical +routing/circuit costs are blockers. No next scope is reserved. + +## Credit and overlap + +Ali Romman with substantial OpenAI Codex assistance; no subagents. [NOTICE](NOTICE) +credits the Gaussian Smith, modular capacity, stochastic sampling, scalar-grid, +selected word and native compiler predecessors. Those sources are unchanged. +The new contribution combines the explicit coarse-period quotient codec, +pointwise stochastic optimum, exact capacity/sampling statements and selected +source bindings. Classical factors and prior results are not counted again. + +Canonical main: 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, +selected PR6030. Public open/closed PR and Discussion metadata was refreshed +before the claim; related coarsening, Smith, unbiased, mixed-grid and entrance +work was inspected. Arbitrary diffs and unpublished work remain coverage limits. diff --git a/research/native-coarse-grid-residue-codec/RESULT.json b/research/native-coarse-grid-residue-codec/RESULT.json new file mode 100644 index 0000000000..f7b35e4245 --- /dev/null +++ b/research/native-coarse-grid-residue-codec/RESULT.json @@ -0,0 +1,812 @@ +{ + "source": { + "word_events": 22803, + "move_events": 3453, + "rank_counts": { + "1": 2219, + "2": 457, + "3": 496, + "4": 100, + "5": 163, + "6": 11, + "7": 6, + "8": 1 + }, + "distinct_edges": 2886, + "source_frames": 1001, + "independent_binary_census": true, + "all_endpoint_frames_checked": true, + "assertions_enabled": true, + "width_one_k5_residue_bits_per_move": 5120, + "width_one_k5_uncompressed_residue_slots": 17679360, + "width_one_k5_fixed_seed_bits": 21683, + "representatives": [ + { + "rank": 1, + "event_index": 9896, + "event": [ + "MOVE", + 236, + 3, + 7, + false + ], + "recipe": { + "rank": 1, + "left": { + "matrix_rows": [ + 3, + 4, + 9, + 16, + 1, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "phase": 0 + }, + "right": { + "matrix_rows": [ + 21, + 17, + 2, + 20, + 8, + 32, + 64, + 128, + 256 + ], + "offset": 1, + "quadratic_rows": [ + 5, + 0, + 5, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "linear_Z4": [ + 3, + 0, + 3, + 0, + 2, + 0, + 0, + 0, + 0 + ], + "phase": 1 + } + }, + "oracle_exponent": 1, + "oracle_columns": 512 + }, + { + "rank": 2, + "event_index": 9934, + "event": [ + "MOVE", + 76, + 3, + 252, + false + ], + "recipe": { + "rank": 2, + "left": { + "matrix_rows": [ + 5, + 8, + 17, + 33, + 64, + 1, + 130, + 258, + 2 + ], + "offset": 0, + "quadratic_rows": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "linear_Z4": [ + 3, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "phase": 0 + }, + "right": { + "matrix_rows": [ + 13, + 448, + 33, + 2, + 36, + 40, + 16, + 320, + 384 + ], + "offset": 2, + "quadratic_rows": [ + 45, + 0, + 45, + 45, + 0, + 13, + 192, + 192, + 0 + ], + "linear_Z4": [ + 1, + 0, + 1, + 1, + 0, + 2, + 3, + 3, + 2 + ], + "phase": 1 + } + }, + "oracle_exponent": 2, + "oracle_columns": 512 + }, + { + "rank": 3, + "event_index": 12854, + "event": [ + "MOVE", + 464, + 3, + 298, + false + ], + "recipe": { + "rank": 3, + "left": { + "matrix_rows": [ + 10, + 21, + 39, + 6, + 67, + 131, + 1, + 259, + 3 + ], + "offset": 0, + "quadratic_rows": [ + 2, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "linear_Z4": [ + 2, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "phase": 0 + }, + "right": { + "matrix_rows": [ + 438, + 437, + 334, + 321, + 266, + 76, + 272, + 288, + 384 + ], + "offset": 7, + "quadratic_rows": [ + 245, + 496, + 261, + 0, + 259, + 259, + 3, + 259, + 438 + ], + "linear_Z4": [ + 3, + 2, + 1, + 2, + 2, + 2, + 2, + 2, + 3 + ], + "phase": 3 + } + }, + "oracle_exponent": 3, + "oracle_columns": 512 + }, + { + "rank": 4, + "event_index": 12725, + "event": [ + "MOVE", + 63, + 288, + 267, + false + ], + "recipe": { + "rank": 4, + "left": { + "matrix_rows": [ + 17, + 37, + 4, + 66, + 136, + 7, + 13, + 261, + 5 + ], + "offset": 0, + "quadratic_rows": [ + 15, + 7, + 15, + 13, + 0, + 0, + 0, + 0, + 0 + ], + "linear_Z4": [ + 3, + 3, + 3, + 3, + 0, + 0, + 0, + 0, + 0 + ], + "phase": 0 + }, + "right": { + "matrix_rows": [ + 107, + 264, + 366, + 272, + 256, + 266, + 288, + 320, + 384 + ], + "offset": 254, + "quadratic_rows": [ + 362, + 13, + 362, + 47, + 64, + 13, + 21, + 0, + 261 + ], + "linear_Z4": [ + 2, + 2, + 2, + 1, + 0, + 0, + 0, + 0, + 3 + ], + "phase": 3 + } + }, + "oracle_exponent": 12, + "oracle_columns": 512 + }, + { + "rank": 5, + "event_index": 12422, + "event": [ + "MOVE", + 106, + 1090, + 127, + false + ], + "recipe": { + "rank": 5, + "left": { + "matrix_rows": [ + 33, + 66, + 132, + 8, + 16, + 13, + 11, + 265, + 9 + ], + "offset": 0, + "quadratic_rows": [ + 6, + 11, + 13, + 6, + 0, + 0, + 0, + 0, + 0 + ], + "linear_Z4": [ + 2, + 3, + 3, + 2, + 2, + 0, + 0, + 0, + 0 + ], + "phase": 0 + }, + "right": { + "matrix_rows": [ + 417, + 418, + 324, + 168, + 16, + 256, + 480, + 352, + 320 + ], + "offset": 371, + "quadratic_rows": [ + 160, + 64, + 32, + 160, + 0, + 13, + 66, + 137, + 0 + ], + "linear_Z4": [ + 0, + 0, + 0, + 0, + 2, + 2, + 1, + 1, + 0 + ], + "phase": 0 + } + }, + "oracle_exponent": 13, + "oracle_columns": 512 + }, + { + "rank": 6, + "event_index": 13458, + "event": [ + "MOVE", + 770, + 549, + 593, + true + ], + "recipe": { + "rank": 6, + "left": { + "matrix_rows": [ + 69, + 3, + 128, + 257, + 8, + 4, + 5, + 16, + 32 + ], + "offset": 0, + "quadratic_rows": [ + 3, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "linear_Z4": [ + 3, + 2, + 2, + 2, + 2, + 2, + 0, + 0, + 0 + ], + "phase": 0 + }, + "right": { + "matrix_rows": [ + 105, + 2, + 35, + 16, + 128, + 256, + 67, + 6, + 104 + ], + "offset": 4, + "quadratic_rows": [ + 8, + 98, + 0, + 9, + 0, + 2, + 2, + 0, + 0 + ], + "linear_Z4": [ + 0, + 1, + 0, + 1, + 2, + 0, + 2, + 2, + 2 + ], + "phase": 3 + } + }, + "oracle_exponent": 8, + "oracle_columns": 512 + }, + { + "rank": 7, + "event_index": 15656, + "event": [ + "MOVE", + 455, + 3, + 925, + false + ], + "recipe": { + "rank": 7, + "left": { + "matrix_rows": [ + 254, + 365, + 7, + 11, + 17, + 2, + 35, + 67, + 3 + ], + "offset": 0, + "quadratic_rows": [ + 18, + 17, + 16, + 16, + 127, + 16, + 16, + 0, + 0 + ], + "linear_Z4": [ + 2, + 2, + 2, + 2, + 3, + 2, + 2, + 0, + 0 + ], + "phase": 0 + }, + "right": { + "matrix_rows": [ + 50, + 49, + 55, + 59, + 461, + 115, + 179, + 477, + 494 + ], + "offset": 111, + "quadratic_rows": [ + 236, + 274, + 461, + 461, + 258, + 257, + 461, + 461, + 254 + ], + "linear_Z4": [ + 0, + 3, + 3, + 3, + 0, + 0, + 3, + 3, + 0 + ], + "phase": 2 + } + }, + "oracle_exponent": 7, + "oracle_columns": 512 + }, + { + "rank": 8, + "event_index": 15619, + "event": [ + "MOVE", + 115, + 3, + 189, + false + ], + "recipe": { + "rank": 8, + "left": { + "matrix_rows": [ + 1, + 2, + 4, + 8, + 288, + 48, + 16, + 64, + 128 + ], + "offset": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 48, + 48, + 0, + 0, + 0 + ], + "linear_Z4": [ + 2, + 2, + 2, + 2, + 3, + 3, + 2, + 2, + 0 + ], + "phase": 0 + }, + "right": { + "matrix_rows": [ + 1, + 2, + 4, + 8, + 96, + 80, + 128, + 256, + 112 + ], + "offset": 207, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 48, + 48, + 0, + 0, + 0 + ], + "linear_Z4": [ + 2, + 2, + 2, + 2, + 1, + 3, + 0, + 2, + 2 + ], + "phase": 2 + } + }, + "oracle_exponent": 8, + "oracle_columns": 512 + } + ] + }, + "finite": { + "complete_quotient_endpoints": 25184, + "retained_bit_witnesses": 16, + "dense_tensor_fixtures": 36, + "small_seed_roundtrips": 432 + }, + "native": { + "new_interpreter_columns": 4096, + "signed_native_roundtrips": 128, + "arbitrary_source_endpoints": 64, + "native_seed_executions": 1920, + "native_moments": [ + { + "rank": 1, + "seeds": 64, + "variance": "52877/512" + }, + { + "rank": 2, + "seeds": 64, + "variance": "55677/512" + }, + { + "rank": 3, + "seeds": 128, + "variance": "53829/512" + }, + { + "rank": 4, + "seeds": 128, + "variance": "51629/512" + }, + { + "rank": 5, + "seeds": 256, + "variance": "50633/512" + }, + { + "rank": 6, + "seeds": 256, + "variance": "52401/512" + }, + { + "rank": 7, + "seeds": 512, + "variance": "51833/512" + }, + { + "rank": 8, + "seeds": 512, + "variance": "50883/512" + } + ], + "tensor_coordinates": 262144, + "tensor_residue_bits": 524288, + "tensor_seed_roundtrips": 4, + "tensor_moments": { + "seeds": 4, + "variance": "326311/4" + }, + "tensor_output_sha256": "fc816391772d1a8b8bcbd890d0992849f996aa99f0caf1c3a3dbda4b1fe3ffa9" + }, + "controls": { + "semantic_and_domain_controls": 11 + }, + "source_corruption_controls": 3 +} diff --git a/research/native-coarse-grid-residue-codec/SOURCES.json b/research/native-coarse-grid-residue-codec/SOURCES.json new file mode 100644 index 0000000000..dc4e6683f6 --- /dev/null +++ b/research/native-coarse-grid-residue-codec/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + }, + { + "path": "research/staged544-mixed-fourth-entry/native/vendor/native/new/code/borrow/bw_gauss.py", + "usage": "input", + "git_blob": "1ff29dfb244e2114de8e586a450ae9fb70308d58", + "sha256": "0884b14d6d77cde419a3c773ad9b21d0d18de1e6e20e6b6d5add458ed32ba4cb" + }, + { + "path": "research/staged544-mixed-fourth-entry/native/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ] +} diff --git a/research/native-coarse-grid-residue-codec/TASK.json b/research/native-coarse-grid-residue-codec/TASK.json new file mode 100644 index 0000000000..c314ba3c66 --- /dev/null +++ b/research/native-coarse-grid-residue-codec/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct an unbiased Gaussian native coarse-grid interface with an exact optimal residue codec, bind the selected MOVE rank census and representatives, and give the complete direct invoice.", + "scope_change_reason": "The selected scalar records need a native return on a coarser grid. A same-grid bijection does not supply that interface. The new codec retains the required input information explicitly.", + "bottleneck_link": "Native all-column and precision/tape admission need a finite-grid implementation with charged information retention. This supplies the scoped native numerical/codec contract, not a full caller or funded supplier.", + "budget_minutes": 90, + "stop_rule": "Stop at one verified codec with a universal proof, exact source bindings, complete resource bounds and failed-premise controls.", + "outcome": "completed", + "evidence": "PROOF.md and generated RESULT.json. Exact quotient endpoints, independent dense and source oracles, all-seed moments, source census, arbitrary residue endpoints, full tensor return and semantic/source controls.", + "author": "Ali Romman", + "ai_assistance": "Ali Romman with substantial OpenAI Codex assistance. No subagents.", + "open_questions": [ + { + "question": "Can a full selected caller use this coarse-grid law with a paid retained-information schedule?", + "why_it_matters": "The native grid interface is supplied, but whole-word probability, physical randomness, residue lifetime and all-width cost are not.", + "first_step": "Bind a complete caller error budget and residue ownership/lifetime ledger to the source rank census.", + "blocked_by": "Fixed five-bit input reserves do not cover all tensor widths under this codec; physical routing, sampler, reversible circuits and recursive tariffs remain open." + } + ] +} diff --git a/research/native-coarse-grid-residue-codec/VERIFY.json b/research/native-coarse-grid-residue-codec/VERIFY.json new file mode 100644 index 0000000000..171019514d --- /dev/null +++ b/research/native-coarse-grid-residue-codec/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.3.4" + ], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/staged544-mixed-fourth-entry/native/vendor/native/new/code/borrow/bw_gauss.py", + "research/staged544-mixed-fourth-entry/native/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Exact quotient codec and inverse; pointwise unbiased moments; selected rank census and all columns of each representative; dense oracle, full tensor, domain and corruption controls. Source assertions run unchanged in a normal subprocess." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Exact quotient codec and inverse; pointwise unbiased moments; selected rank census and all columns of each representative; dense oracle, full tensor, domain and corruption controls. Source assertions run unchanged in a normal subprocess." + } + ] +} diff --git a/research/native-coarse-grid-residue-codec/codec.py b/research/native-coarse-grid-residue-codec/codec.py new file mode 100644 index 0000000000..808dfc1573 --- /dev/null +++ b/research/native-coarse-grid-residue-codec/codec.py @@ -0,0 +1,154 @@ +"""Quantize an exact Gaussian child and retain its input lattice coset.""" + + +def phase(z, p): + a, b = z + p %= 4 + if p == 0: + return a, b + if p == 1: + return -b, a + if p == 2: + return -a, -b + return b, -a + + +def route(rec, h): + if rec is None: + return list(range(1 << h)), [0] * (1 << h) + dest, phases = [], [] + for x in range(1 << h): + dest.append(sum(((row & x).bit_count() % 2) << j + for j, row in enumerate(rec["matrix_rows"])) ^ rec["offset"]) + p = rec["phase"] + for j in range(h): + if x >> j & 1: + p += rec["linear_Z4"][j] + p += 2 * (((rec["quadratic_rows"][j] >> (j + 1)) + & (x >> (j + 1))).bit_count() % 2) + phases.append(p % 4) + if sorted(dest) != list(range(1 << h)): + raise ValueError("route must be a permutation") + return dest, phases + + +class Codec: + def __init__(self, recipe, h, f, k): + r = recipe["rank"] + if any(type(v) is not int for v in (r, h, f, k)) or not (h >= 1 and f >= 1 and 0 <= r <= h): + raise ValueError("invalid native dimensions") + self.h, self.f, self.k = h, f, k + self.axes = [h * j + t for j in range(f) for t in range(r)] + self.a = len(self.axes) + self.d = (self.a + 1) // 2 + if k < self.d: + raise ValueError("coarse inverse is not integral at this grid ratio") + self.n = 1 << (h * f) + self.seed_bits = k + self.d + self.seed_count = 1 << self.seed_bits + self.bits = 2 * k * self.n + self.widths = [2 * k - self.a + 2 * sum((j >> b) & 1 for b in self.axes) + for j in range(self.n)] + if min(self.widths) < 0 or sum(self.widths) != self.bits: + raise ArithmeticError("incorrect quotient digit widths") + self.left, self.right = route(recipe["left"], h), route(recipe.get("right"), h) + + def check(self, values, seed): + if type(seed) is not int or not 0 <= seed < self.seed_count: + raise ValueError("invalid uniform seed") + if len(values) != self.n or any(len(z) != 2 or any(type(v) is not int for v in z) for z in values): + raise ValueError("invalid Gaussian integer field") + + def mono(self, values, routing, inverse=False): + out = [None] * self.n + dest, phases = routing + mask = (1 << self.h) - 1 + for src in range(self.n): + digits, dst, p = src, 0, 0 + for axis in range(self.f): + digit = digits & mask + digits >>= self.h + dst |= dest[digit] << (self.h * axis) + p += phases[digit] + if inverse: + out[src] = phase(values[dst], -p) + else: + out[dst] = phase(values[src], p) + return out + + def exact(self, values, inverse=False): + """Return integer numerators over the common denominator 2**d.""" + out = self.mono(values, self.left if inverse else self.right, inverse) + for axis in self.axes: + stride = 1 << axis + for start in range(0, self.n, 2 * stride): + for low in range(stride): + p, q = start + low, start + stride + low + a, b = out[p] + c, d = out[q] + first = (a - b + c + d, a + b - c + d) + second = (a + b + c - d, -a + b + c + d) + out[p], out[q] = (second, first) if inverse else (first, second) + out = self.mono(out, self.right if inverse else self.left, inverse) + divisor = 1 << (self.a // 2) + if any(a % divisor or b % divisor for a, b in out): + raise ArithmeticError("Gaussian tensor numerator is not divisible") + return [(a // divisor, b // divisor) for a, b in out] + + def triangular(self, values, inverse=False): + out = list(values) + for axis in reversed(self.axes) if inverse else self.axes: + stride = 1 << axis + for start in range(0, self.n, 2 * stride): + for low in range(stride): + p, q = start + low, start + stride + low + a, b = out[p] + c, d = out[q] + out[q] = (c - b, d + a) if inverse else (c + b, d - a) + return out + + def residue(self, values): + transformed = self.triangular(self.mono(values, self.right)) + packed = bytearray((self.bits + 7) // 8) + offset = 0 + for (a, b), width in zip(transformed, self.widths): + for _ in range(width): + digit = (a + b) % 2 + packed[offset // 8] |= digit << (offset % 8) + a -= digit + a, b = (a + b) // 2, (b - a) // 2 + offset += 1 + return bytes(packed) + + def representative(self, packed): + if not isinstance(packed, bytes) or len(packed) != (self.bits + 7) // 8: + raise ValueError("invalid residue byte count") + if self.bits % 8 and packed[-1] >> (self.bits % 8): + raise ValueError("nonzero residue padding") + values = [] + offset = 0 + for width in self.widths: + a = b = 0 + for bit in reversed(range(offset, offset + width)): + digit = (packed[bit // 8] >> (bit % 8)) & 1 + a, b = a - b + digit, a + b + values.append((a, b)) + offset += width + return self.mono(self.triangular(values, True), self.right, True) + + def rounded(self, values, seed): + self.check(values, seed) + return [((a + seed) // self.seed_count, (b + seed) // self.seed_count) + for a, b in self.exact(values)] + + def encode(self, values, seed): + return self.rounded(values, seed), self.residue(values) + + def restore(self, coarse, packed, seed): + self.check(coarse, seed) + x0 = self.representative(packed) + q0 = self.rounded(x0, seed) + diff = [(a - c, b - d) for (a, b), (c, d) in zip(coarse, q0)] + period = self.exact(diff, True) + shift = self.k - self.d + return [(a + (c << shift), b + (d << shift)) for (a, b), (c, d) in zip(x0, period)] diff --git a/research/native-coarse-grid-residue-codec/produce.py b/research/native-coarse-grid-residue-codec/produce.py new file mode 100644 index 0000000000..c65a682b9a --- /dev/null +++ b/research/native-coarse-grid-residue-codec/produce.py @@ -0,0 +1,139 @@ +"""Bind every selected MOVE rank and check one full operator of each rank.""" + +import gzip +import hashlib +import json +import sys +from collections import Counter +from pathlib import Path + +import numpy as np + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, label): + if not ok: + raise ValueError(label) + + +def binary_inverse(columns): + n = len(columns) + rows = [sum(((columns[j] >> i) & 1) << j for j in range(n)) | (1 << (n + i)) + for i in range(n)] + for col in range(n): + pivot = next(j for j in range(col, n) if rows[j] >> col & 1) + rows[col], rows[pivot] = rows[pivot], rows[col] + for j in range(n): + if j != col and rows[j] >> col & 1: + rows[j] ^= rows[col] + need([v & ((1 << n) - 1) for v in rows] == [1 << j for j in range(n)], + "independent binary inverse") + return [sum(((rows[j] >> (n + i)) & 1) << j for j in range(n)) for i in range(n)] + + +def binary_apply(columns, value): + out = 0 + while value: + bit = value & -value + out ^= columns[bit.bit_length() - 1] + value ^= bit + return out + + +def main(): + need(__debug__, "source assertions must remain enabled") + for item in json.loads((HERE / "SOURCES.json").read_text())["files"]: + if item["usage"] == "input": + need(hashlib.sha256((ROOT / item["path"]).read_bytes()).hexdigest() == item["sha256"], + "source bytes changed: " + item["path"]) + word = json.loads(gzip.decompress((ROOT / "research/p104-helper470-twin-rung-removal/WORD.json.gz").read_bytes())) + source = ROOT / "research/staged544-mixed-fourth-entry/native/vendor/native/new/code/borrow" + sys.path.insert(0, str(source)) + sys.path.insert(0, str(source / "vendor/clifford")) + import bw_gauss + from clifford_exact import canonical_frame, lower_child, rank + + charts, edges, edge_columns, representatives, counts = {}, {}, {}, {}, Counter() + current = dict(enumerate(word["initial"])) + for j, e in enumerate(word["program"]): + op, field = e[:2] + if op == "INIT": + need(field not in current, "INIT field already live") + current[field] = e[2] + elif op == "CLEAR": + need(current.pop(field) == e[2], "CLEAR frame") + elif op == "ADD": + need(current[field] == current[e[2]] == e[4], "ADD frames") + elif op == "SCALE": + need(current[field] == e[3], "SCALE frame") + elif op == "COPY": + need(current[field] == current[e[2]] == e[4], "COPY frames") + elif op == "MOVE": + old, new = e[2:4] + need(current[field] == old, "MOVE input frame") + current[field] = new + for t in (old, new): + if t not in charts: + charts[t] = canonical_frame(9, word["frames"][t]) + key = old, new + if key not in edges: + operator = charts[old].adjoint().then(charts[new]) + r = rank([x for x, z, p in operator.tab[9:]]) + edges[key] = r + edge_columns[key] = [x for x, z, p in operator.tab[9:]] + if r not in representatives: + recipe, compiled = lower_child(operator) + need(recipe["rank"] == r, "compiler rank agrees") + representatives[r] = (j, e, recipe, compiled) + counts[edges[key]] += 1 + else: + raise ValueError("unknown source opcode") + need(current == dict(enumerate(word["final"])), "all source endpoint frames") + need(sum(counts.values()) == 3453 and len(word["program"]) == 22803, "selected event inventory") + # A second pass uses 18-bit matrices and finite spans, without Pauli composition. + columns = {j: [x | (z << 9) for x, z, p in chart.tab] for j, chart in charts.items()} + inverses = {j: binary_inverse(cols) for j, cols in columns.items()} + other_counts = Counter() + for e in (event for event in word["program"] if event[0] == "MOVE"): + old, new = e[2:4] + b = [binary_apply(columns[new], col) & 511 for col in inverses[old][9:]] + need(b == edge_columns[old, new], "all independently composed B columns") + span = {0} + for col in b: + span |= {x ^ col for x in span} + other_counts[len(span).bit_length() - 1] += 1 + need(other_counts == counts, "independent complete MOVE rank census") + arrays, selected = {}, [] + for r, (j, e, recipe, compiled) in sorted(representatives.items()): + real, imag, exponent = bw_gauss.frame( + bw_gauss.frame(bw_gauss.eye(9), word["frames"][e[2]], 9, -1), + word["frames"][e[3]], 9, + ) + need(exponent <= 18 and np.max(np.abs(real)) <= 1 << 18 and np.max(np.abs(imag)) <= 1 << 18, + "small exact oracle integer range") + for col in range(512): + values, exp = compiled.zero_state(col) + need(all(a * (1 << exponent) == int(real[row, col]) * (1 << exp) and + b * (1 << exponent) == int(imag[row, col]) * (1 << exp) + for row, (a, b) in enumerate(values)), "full source columns") + arrays[f"r{r}_real"], arrays[f"r{r}_imag"] = real, imag + selected.append({"rank": r, "event_index": j, "event": e, "recipe": recipe, + "oracle_exponent": exponent, "oracle_columns": 512}) + out = Path(sys.argv[1]) + np.savez(out / "oracle.npz", **arrays) + result = {"word_events": len(word["program"]), "move_events": sum(counts.values()), + "rank_counts": {str(r): count for r, count in sorted(counts.items())}, + "distinct_edges": len(edges), "source_frames": len(charts), + "independent_binary_census": True, + "all_endpoint_frames_checked": True, "assertions_enabled": __debug__, + "width_one_k5_residue_bits_per_move": 5120, + "width_one_k5_uncompressed_residue_slots": 5120 * sum(counts.values()), + "width_one_k5_fixed_seed_bits": sum((5 + (r + 1) // 2) * count for r, count in counts.items()), + "representatives": selected} + (out / "source.json").write_text(json.dumps(result, indent=2) + "\n") + + +if __name__ == "__main__": + main() diff --git a/research/native-coarse-grid-residue-codec/verify.py b/research/native-coarse-grid-residue-codec/verify.py new file mode 100644 index 0000000000..119052b1cb --- /dev/null +++ b/research/native-coarse-grid-residue-codec/verify.py @@ -0,0 +1,267 @@ +"""Check quotient endpoints, exact native columns and stochastic moments.""" + +import hashlib +import itertools +import json +import subprocess +import sys +import tempfile +from fractions import Fraction +from pathlib import Path + +import numpy as np + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from codec import Codec + + +def need(ok, label): + if not ok: + raise ValueError(label) + + +def check_source(data, expected): + need(hashlib.sha256(data).hexdigest() == expected, "source bytes") + + +def gauss_mul(x, y): + a, b = x + c, d = y + return a * c - b * d, a * d + b * c + + +def direct_tensor(values, axes, inverse=False): + """Use a dense product of scalar coefficients, not butterfly stages.""" + mask = sum(1 << b for b in axes) + out = [] + for row in range(len(values)): + sr = si = 0 + for col, value in enumerate(values): + if (row ^ col) & ~mask: + continue + coefficient = (1, 0) + for axis in axes: + same = ((row ^ col) >> axis & 1) == 0 + sign = (1 if same else -1) * (-1 if inverse else 1) + coefficient = gauss_mul(coefficient, (1, sign)) + a, b = gauss_mul(coefficient, value) + sr, si = sr + a, si + b + out.append((Fraction(sr, 1 << len(axes)), Fraction(si, 1 << len(axes)))) + return out + + +def exact_moments(c, values, numerators): + sums = [[0, 0] for _ in values] + squares = 0 + d = c.seed_count + for seed in range(d): + # This loop checks the actual public quantizer for every seed. + result = c.rounded(values, seed) + for j, (out, raw) in enumerate(zip(result, numerators)): + for component in (0, 1): + sums[j][component] += out[component] + squares += (d * out[component] - raw[component]) ** 2 + need([tuple(z) for z in sums] == numerators, "all-seed exact mean") + variance_numerator = sum((v % d) * (d - v % d) for z in numerators for v in z) + need(squares == d * variance_numerator, "exact pointwise minimum second moment") + need(variance_numerator * 2 <= c.n * d * d, "native variance upper bound") + return {"seeds": d, "variance": str(Fraction(variance_numerator, d * d))} + + +def finite_quotients(): + count = collisions = 0 + for h, r, k in ((1, 0, 1), (1, 1, 1), (2, 2, 1)): + c = Codec({"rank": r, "left": None, "right": None}, h, 1, k) + if c.n == 2: + outputs = [list(zip(v[::2], v[1::2])) for v in itertools.product((-1, 0, 1), repeat=4)] + else: + outputs = [[(0, 0)] * c.n] + for j in range(2 * c.n): + for sign in (-1, 1): + out = [[0, 0] for _ in range(c.n)] + out[j // 2][j % 2] = sign + outputs.append([tuple(z) for z in out]) + for seed in range(c.seed_count): + seen = set() + for label in range(1 << c.bits): + packed = label.to_bytes((c.bits + 7) // 8, "little") + for index, q in enumerate(outputs): + x = c.restore(q, packed, seed) + actual, residue = c.encode(x, seed) + need(actual == q and residue == packed, "arbitrary coarse/label endpoint") + if index == 0: + seen.add(tuple(x)) + count += 1 + need(len(seen) == 1 << c.bits, "every residue labels a distinct input at one output") + zero = bytes((c.bits + 7) // 8) + first = c.restore([(0, 0)] * c.n, zero, 0) + for bit in range(c.bits): + packed = (1 << bit).to_bytes(len(zero), "little") + x = c.restore([(0, 0)] * c.n, packed, 0) + need(x != first and c.rounded(x, 0) == c.rounded(first, 0), "each retained bit can matter") + collisions += 1 + fixtures = stages = 0 + for h, r, f in ((1, 1, 1), (1, 1, 2), (1, 1, 3), (2, 1, 2), (2, 2, 2), (3, 2, 1)): + a = r * f + for k in ((a + 1) // 2, (a + 1) // 2 + 1): + c = Codec({"rank": r, "left": None, "right": None}, h, f, k) + for t in range(3): + x = [((j * 13 + t) % 9 - 4, (j * j + 2 * t) % 11 - 5) for j in range(c.n)] + oracle = direct_tensor(x, c.axes) + actual = c.exact(x) + need([(Fraction(a, 1 << c.d), Fraction(b, 1 << c.d)) for a, b in actual] == oracle, + "dense tensor oracle") + inverse = c.exact(actual, True) + need(inverse == [(a << (2 * c.d), b << (2 * c.d)) for a, b in x], "exact tensor inverse") + moments = exact_moments(c, x, actual) + for seed in range(c.seed_count): + q, packed = c.encode(x, seed) + need(c.restore(q, packed, seed) == x, "small tensor data return") + stages += 1 + fixtures += 1 + return {"complete_quotient_endpoints": count, "retained_bit_witnesses": collisions, + "dense_tensor_fixtures": fixtures, "small_seed_roundtrips": stages} + + +def oracle_vector(real, imag, values, exponent, d): + out = [] + for rr, ii in zip(real, imag): + a = sum(int(r) * x - int(i) * y for r, i, (x, y) in zip(rr, ii, values)) + b = sum(int(r) * y + int(i) * x for r, i, (x, y) in zip(rr, ii, values)) + scale = 1 << max(exponent - d, 0) + if exponent >= d: + need(a % scale == b % scale == 0, "source oracle numerator reduction") + out.append((a // scale, b // scale)) + else: + out.append((a << (d - exponent), b << (d - exponent))) + return out + + +def source_checks(source, arrays): + columns = returns = endpoints = seeds = 0 + moment_records = [] + first = None + for item in source["representatives"]: + r = item["rank"] + c = Codec(item["recipe"], 9, 1, 5) + real, imag = arrays[f"r{r}_real"], arrays[f"r{r}_imag"] + exp = item["oracle_exponent"] + for col in range(512): + x = [(0, 0)] * 512 + x[col] = (1, 0) + actual = c.exact(x) + need(all(a * (1 << exp) == int(real[row, col]) * (1 << c.d) and + b * (1 << exp) == int(imag[row, col]) * (1 << c.d) + for row, (a, b) in enumerate(actual)), "new interpreter source columns") + if col == 0: + need(any(abs(v) == 1 for z in actual for v in z), "primitive seed-denominator witness") + columns += 1 + for t, bits in enumerate((0, 8, 64, 257)): + x = [(((j * 13 + t) % 17 - 8) << bits, + ((j * j + 3 * t) % 19 - 9) << max(bits - 1, 0)) for j in range(512)] + actual = c.exact(x) + need(actual == oracle_vector(real, imag, x, exp, c.d), "signed dense source oracle") + for seed in (0, 1, c.seed_count // 2, c.seed_count - 1): + q, packed = c.encode(x, seed) + need(len(packed) == 640 and c.restore(q, packed, seed) == x, "actual native changed-grid return") + returns += 1 + if t == 0: + record = exact_moments(c, x, actual) + seeds += record["seeds"] + moment_records.append({"rank": r, **record}) + for byte in (0, 85, 170, 255): + packed = bytes([byte]) * 640 + q = [((j % 7) - 3, (j % 5) - 2) for j in range(512)] + for seed in (0, c.seed_count - 1): + x = c.restore(q, packed, seed) + need(c.encode(x, seed) == (q, packed), "full source arbitrary output/residue endpoint") + endpoints += 1 + if r == 1: + first = item["recipe"] + need(first is not None, "selected rank-one source exists") + c = Codec(first, 9, 2, 1) + # A complete tensor field, with a coarse/fine ratio of two. + x = [((j % 5) - 2, (j % 7) - 3) for j in range(c.n)] + actual = c.exact(x) + tensor = exact_moments(c, x, actual) + digest = hashlib.sha256() + for seed in range(c.seed_count): + q, packed = c.encode(x, seed) + need(c.restore(q, packed, seed) == x, "full 512**2 changed-grid inverse") + digest.update(packed) + digest.update(json.dumps(q, separators=(",", ":")).encode()) + return {"new_interpreter_columns": columns, "signed_native_roundtrips": returns, + "arbitrary_source_endpoints": endpoints, "native_seed_executions": seeds, + "native_moments": moment_records, "tensor_coordinates": c.n, + "tensor_residue_bits": c.bits, "tensor_seed_roundtrips": c.seed_count, + "tensor_moments": tensor, "tensor_output_sha256": digest.hexdigest()} + + +def controls(source, arrays): + small = Codec({"rank": 1, "left": None, "right": None}, 1, 1, 1) + q = [(0, 0), (0, 0)] + a = small.restore(q, b"\x00", 0) + b = small.restore(q, b"\x01", 0) + need(a != b and small.rounded(a, 0) == small.rounded(b, 0), "coarse output alone loses information") + need(small.restore(q, b"\x01", small.seed_count - 1) != b, "wrong retained seed") + for action in (lambda: Codec({"rank": 1, "left": None, "right": None}, 1, 1, 0), + lambda: small.restore(q, b"\x10", 0), + lambda: small.restore(q, b"", 0), + lambda: small.rounded(q, True), + lambda: small.rounded(q, small.seed_count)): + try: + action() + except ValueError: + pass + else: + raise ValueError("invalid grid, residue or seed accepted") + period = direct_tensor([(1, 0), (0, 0)], (0,), True) + need(any(v.denominator != 1 for z in period for v in z), "k=0 inverse-period integrality witness") + d = small.seed_count + need(sum(small.rounded([(1, 0), (0, 0)], u)[0][0] for u in range(0, d, 2)) == 0, + "one fewer fair bit can bias a primitive fraction") + need(small.rounded([(-1, 0), (0, 0)], 0)[0][0] == -1 and int(Fraction(-1, d)) == 0, + "signed floor is not truncation") + item = source["representatives"][0] + bad = json.loads(json.dumps(item["recipe"])) + bad["left"]["phase"] = (bad["left"]["phase"] + 1) % 4 + c = Codec(bad, 9, 1, 5) + x = [(1, 0)] + [(0, 0)] * 511 + actual = c.exact(x) + real, imag = arrays['r1_real'], arrays['r1_imag'] + expected = oracle_vector(real, imag, x, item["oracle_exponent"], c.d) + need(actual != expected, "changed native global phase rejected by the source oracle") + return {"semantic_and_domain_controls": 11} + + +def main(): + files = [x for x in json.loads((HERE / "SOURCES.json").read_text())["files"] if x["usage"] == "input"] + for item in files: + data = (ROOT / item["path"]).read_bytes() + check_source(data, item["sha256"]) + try: + check_source(data + b"!", item["sha256"]) + except ValueError: + pass + else: + raise ValueError("changed source bytes were accepted") + with tempfile.TemporaryDirectory(prefix="native-coarse-grid-") as tmp: + subprocess.run([sys.executable, "-I", "-W", "error", "-B", str(HERE / "produce.py"), tmp], + check=True, capture_output=True, text=True, timeout=240) + source = json.loads((Path(tmp) / "source.json").read_text()) + with np.load(Path(tmp) / "oracle.npz") as archive: + arrays = {k: archive[k] for k in archive.files} + result = {"source": source, "finite": finite_quotients(), "native": source_checks(source, arrays), + "controls": controls(source, arrays), "source_corruption_controls": len(files)} + if "--write-result" in sys.argv: + (HERE / "RESULT.json").write_text(json.dumps(result, indent=2) + "\n") + else: + need(result == json.loads((HERE / "RESULT.json").read_text()), "committed result differs") + print("PASS_NATIVE_COARSE_GRID_RESIDUE_CODEC") + print(json.dumps({k: v for k, v in result.items() if k != "source"}, sort_keys=True)) + + +if __name__ == "__main__": + main()