diff --git a/research/norm6-streaming-features/PROOF.md b/research/norm6-streaming-features/PROOF.md new file mode 100644 index 0000000000..2b347c4c6d --- /dev/null +++ b/research/norm6-streaming-features/PROOF.md @@ -0,0 +1,361 @@ +# Streaming norm-six features without a transform table + +Krzysztof Wojt, with substantial OpenAI Codex assistance and bounded Luna +support. Apache-2.0. This is a scoped algebraic proof, not a physical supplier +or a new multiplication exponent. + +## Premises and new statement + +Let `G` be the exact integral Gram matrix supplied by Cinna Davis's #2222, +retained at `research/norm6-dyadic-decoder/sources/P48p-GRAM.json`. Its dimension +is `d=48`. Positive definiteness, the norm-six lattice interpretation and the +49-bit norm-one chart are cited geometric premises. They are not re-audited. +Put `q(x)=x^T G x` and `D=Z[1/2]`. The predecessor's kernel is + +``` +K(x,y) = ((x^T G y)^3 - 4*x^T G y)/192, q(x)=q(y)=6. +``` + +Nick Petalas's #5084 already proves that at most 19,600 dyadic factor pairs +exist, by applying David Ganz / Dugongue's integer-column rank factorization +to the entire finite kernel matrix. Concurrent JoyboyBrian #5132, head +`08572fdb060e73ecc4cb09a024611039881185f4`, independently makes that result +constructive with a sparse transform descriptor and target accumulator array. +It is credited for the public constructibility result; we do not claim another +first closure of that gap. + +The new statement is a different evaluation contract: emit all feature pairs +in one pass with only four length-d owned vectors, no per-feature transform +table and no target accumulator array. Including both borrowed input vectors +and 32 scalar/counter/record slots gives `6d+32=320` live integer slots, +in addition to the `d^2=2304` immutable Gram entries. Outputs must be consumed +and released one at a time. The proof below derives a two-coordinate pivot, +local coefficient formulas, their complete preprocessing bounds and the +stream contract. Source features remain integral; streamed target coefficients +have common denominator 256. The 19,600-term and 960,400 algebraic support +bounds are inherited, not newly improved values. + +## The integer-valued feature module + +Set `f(u)=(u^3-u)/3`, an integer for every integer `u`. Write `v=Gy`. Use the +following #2222 feature pairs `phi_j(x), psi_j(v)` in this order: + +| Kind | Source phi | Integral target psi | Count | +|---|---|---|---:| +| f | f(x_i) | v_i^3 | d | +| l | x_i | (v_i^3-4v_i)/3 | d | +| s | x_i^2 x_j, i != j | v_i^2 v_j | d(d-1) | +| t | x_i x_j x_k, i < j < k | 2v_i v_j v_k | C(d,3) | + +These are linearly independent polynomials over Q: their cubic leading +monomials are distinct, followed by the independent linear features. Their +formal D-span is therefore free. The cited multinomial identity is + +``` +sum_j phi_j(x) psi_j(v) = ((x dot v)^3 - 4*x dot v)/3. +``` + +The total feature count is `N0=C(d+2,3)+d=19648`. Divisions by three define +integer-valued coefficient preprocessing, as in #2222; they are not authorized +dyadic scalar gates on arbitrary runtime data. + +For each coordinate define the relation polynomial + +``` +r_i(x) = x_i (q(x)-6)/2 = sum_j R[i,j] phi_j(x). +``` + +Even diagonal entries of G make every R entry integral. With `h_i=G[i,i]/2`, +the nonzero candidates in row i are exactly + +``` +R[i,f_i] = 3 h_i, +R[i,l_i] = h_i-3, +R[i,s_(j,i)] = h_j (j != i), +R[i,s_(i,j)] = G[i,j] (j != i), +R[i,t_{i,j,k}] = G[j,k] (i,j,k distinct). +``` + +Here a t subscript is sorted. In particular the leading square term satisfies +`h_i*x_i^3 = 3h_i*f(x_i)+h_i*x_i`; dropping that linear correction would give +the wrong relation. Every `r_i` vanishes on `q(x)=6`. + +## A dyadic-unit minor + +Use zero-based indices `a=0`, `b=4`. The pinned matrix has + +``` +G[{a,b},{a,b}] = [[6,-1],[-1,6]]. +``` + +Remove the two s features `x_a^2*x_b`, `x_b^2*x_a`, and all `d-2` t features +`x_a*x_b*x_i` for `i` outside `{a,b}`. Call their index set P and all retained +indices F. Order the relation rows `a,b,other i`, and the pivot columns as +those two s features followed by the t features. Direct substitution gives + +``` +R_P = [ B T ], B = [-1 3], T[:,i] = [G[i,b]], + [ 0 -I ] [ 3 -1] [G[i,a]] + +B^-1 = (1/8) [1 3; 3 1]. +``` + +Thus `det(R_P)=(-8)*(-1)^(d-2)`, exactly `-8` for d=48. This is a unit in D. +All 48 relations are independent and generate a direct summand of the formal +D-feature module: projection to the pivot coordinates restricts to the +invertible map R_P on their row span. In particular the relation submodule +is saturated over D. No full-shell matrix rank computation or unproved odd +pivot inversion is used. + +The shell relation gives + +``` +phi_P = -R_P^-1 R_F phi_F, +K(x,y) = (1/64) sum_(j in F) phi_j(x) (psi_j(v) - (R^T lambda)_j), +lambda = R_P^-T psi_P(v). +``` + +There are `N0-d=C(d+2,3)=19600` retained feature slots. Some coefficients or +features may vanish on particular points; exact full-shell rank and term +minimality are not asserted. + +## Explicit coefficients and the off-shell identity + +For an arbitrary integral vector v, the above solve is the following formula: + +``` +mu_a = v_a^2*v_b + 3*v_b^2*v_a, +mu_b = 3*v_a^2*v_b + v_b^2*v_a, +mu_i = G[i,b]*mu_a + G[i,a]*mu_b - 16*v_a*v_b*v_i (i != a,b), +c_j = 8*psi_j(v) - sum_i R[i,j]*mu_i. +``` + +Here `mu=8*lambda` is integral. Each pivot c_j is identically zero. Every +retained pair is **phi_j(x), c_j(Gy)/512**, and all runtime coefficients are +dyadic. The exact identity, valid even off the shell, is + +``` +sum_j phi_j(x)*c_j(v)/512 + = ((x dot v)^3 - 4*x dot v)/192 + - (mu dot x)*(q(x)-6)/1024. +``` + +It follows by subtracting `(1/512) sum_i mu_i*r_i` from the uncompressed +identity. This proves the desired kernel for every integral norm-six source +x and every integral target y, without enumerating either set. Both x and y +must have norm six for the uniform bounds in the next section. Changing the +shell condition changes the displayed defect; it cannot simply be omitted. + +## Coefficient and source-value bounds + +The actual pinned Gram has `6 <= G[i,i] <= 10` and `|G[i,j]| <= 5` off the +diagonal. Every R column has at most three entries and l1 norm at most 15: +the f bound is 15, l bound 2, s bound 10, and t bound 15. + +Put `M=max(1,max_i |v_i|)`. Every original target has magnitude at most +`2 M^3`, including `|(v_i^3-4v_i)/3| <= (M^3+4M)/3 <= 2M^3`. +The explicit formulas give + +``` +|mu_a|, |mu_b| <= 4 M^3, +|mu_i| <= 5*4 M^3 + 5*4 M^3 + 16 M^3 = 56 M^3, +|c_j| <= 8*2 M^3 + 15*56 M^3 = 856 M^3. +``` + +For a norm-six target y, Cauchy-Schwarz in the positive definite G inner +product gives `|v_i|^2=|_G|^2 <= 6G[i,i] <= 60`. Since v_i is integral, +`M <= 7`. Consequently + +``` +|c_j| <= 856*7^3 = 293608 < 2^19, +|c_j/512| <= 36701/64 < 574. +``` + +This is a uniform bound over the entire shell, not a maximum found among +sampled vectors. Denominator 512 is a common upper bound, not a sharpness claim. + +For source coordinates the dual Cauchy-Schwarz bound is +`|x_i|^2 <= 6*(G^-1)[i,i]`. The verifier computes G^-1 over Q and checks all +2,304 entries of `G G^-1=I` by exact multiplication. Its generated receipt +records `Dmax=max_i (G^-1)[i,i]=172` and `X=floor(sqrt(6Dmax))=32`. Therefore every +retained source feature is integral and has magnitude at most `X^3`: this +is immediate for linear/mixed cubic features and follows from +`|f(u)| <= (|u|^3+|u|)/3 <= X^3` when `|u| <= X` and `X>=1`. +In particular their magnitude is at most 32,768. Positive definiteness is the +cited premise behind both Cauchy-Schwarz uses. + +## Reference preprocessing bound + +These counts concern integer arithmetic to compute label-dependent constants. +They are not ADD counts, bit complexity or a paid fixed-tape implementation. +Integers are exact, and each exact division by three is separately charged. + +For one source, precompute d squares and d cubes; form all retained s features +with one more multiplication each and all retained t features with two each. +Compute the d f values with one subtraction and one exact division by three. +The total is + +``` +d(d-1)+2*C(d,3)+2 multiplications, +d subtractions and d exact divisions by three. +``` + +For one target, first compute `v=Gy` using at most d^2 multiplications and +d(d-1) additions. Compute all N0 original targets using at most four +multiplications and two additions per feature, and d exact divisions by +three. Reuse the two pivot s targets and the d-2 pivot t targets to compute +mu: at most `3d-4` multiplications and `2d-2` additions. For each of the +`N=C(d+2,3)` retained columns, forming `8*psi_j - sum_i R[i,j]*mu_i` uses at +most four multiplications and three additions. Encode the denominator 512 +once. Thus a simple evaluator has the conservative upper bounds + +``` +target multiplications <= d^2 + 8N + 7d - 4, +target additions <= d^2 + 5N + 3d - 2, +target exact divisions by three = d. +``` + +At d=48 these are 36,850 source multiplications and 48 source subtractions; +at most 159,436 target multiplications and 100,446 target additions; and 48 +exact divisions by three on each side. Precomputing/storing the sparse R +and enumerating the features also takes O(d^3) integer entries/operations. +All these per-label bounds are independent of the number of shell points. +The reference implementation favors transparent formulas; the counts describe +the explicit reuse schedule just given, not an instrumented Python instruction +count. A primitive integer operation is not being priced as unit bit cost. + +## The streaming contract + +The previous reference formulas describe a full feature vector, but need not +materialize it. For integers u,w, `u*w*(u+3*w)` and `u*w*(3*u+w)` are even: +if either factor is even this is immediate, and otherwise both parenthesized +sums are even. Hence every mu_i above is even. Put `nu=mu/2`, so + +``` +nu_a = v_a*v_b*(v_a+3*v_b)/2, +nu_b = v_a*v_b*(3*v_a+v_b)/2, +nu_i = G[i,b]*nu_a + G[i,a]*nu_b - 8*v_a*v_b*v_i. +``` + +Each retained target numerator `e_j=c_j/2` is computed locally: + +| Feature | Numerator e_j; final coefficient is e_j/256 | +|---|---| +| f_i | 4v_i^3 - 3h_i nu_i | +| l_i | 4(v_i^3-4v_i)/3 - (h_i-3)nu_i | +| s_(i,j) | 4v_i^2 v_j - G[i,j]nu_i - h_i nu_j | +| t_(i,j,k) | 8v_i v_j v_k - G[j,k]nu_i - G[i,k]nu_j - G[i,j]nu_k | + +These use at most three entries of one R column, obtained directly from G. +Do not construct R. Traverse f, l, s, t in the lexicographic order specified +above, skipping the 48 pivots, and emit `(key, phi_j(x), e_j(Gy))`. Each retained +key occurs once. The parity reduction is a common-denominator bound, not an +optimality claim or the main contribution. + +**Ownership and lifetime.** G and both integer coordinate vectors x,y are +borrowed, read-only inputs. The caller must keep them immutable for the whole +iterator lifetime; the implementation does not snapshot or police concurrent +mutation. Each output record belongs to the consumer, which must release it +before requesting the next to use the stated bound. Retained outputs and any +physical data on which coefficients will act are additional caller storage. +There is no assertion that every physical decoder consumer can obey this +contract. Early close releases the iterator's state. + +The evaluator owns four length-d vectors: v, nu, x-coordinate squares and +v-coordinate squares. It stores no feature keys, R rows, transform edges or +target accumulation vector. Its remaining state is a fixed number of scalars: +dimension/pivots, three loop indices, Gram-dot accumulator, pivot product and +two pivot numerators, h, current source and target, and the one emitted record. +Allowing 32 scalar/counter/record slots covers those values and temporary +arithmetic results in a sequential register implementation. Therefore + +``` +owned vector slots = 4d, +borrowed source/target coordinate slots = 2d, +scalar/counter/one-record slots <= 32, +live slots excluding the immutable Gram <= 6d+32 = 320, +immutable Gram slots = d^2 = 2304, +combined total <= d^2+6d+32 = 2624. +``` + +These are slots of the stated indexed-integer algorithm, not a claim that +CPython represents every object in one machine word. There is no per-feature +immutable descriptor or descriptor-generation phase. Gram access, loop +generation and emitted-record transport are charged below as indexed work, +but no physical tape placement or time/space hierarchy theorem follows. + +For comparison, [#5132's stated evaluator bounds](https://github.com/CrocSwap/integer-mult-bounds/blob/08572fdb060e73ecc4cb09a024611039881185f4/research/norm6-constructive-feature-evaluation/PROOF.md) +allocate 19,712 target slots, 64 source slots, and 245,884 immutable descriptor +slots including the Gram. The new contract removes the target accumulator and +transform tables instead of merely shrinking their coefficients. This compares +two explicit upper allocations, not a lower bound on every implementation of +the concurrent construction. The feature bases differ, so their coefficient +arrays must not be substituted without the corresponding source features. + +## Streaming work and intermediate widths + +Computing v uses d^2 products and d(d-1) additions. Computing nu from the +shared product `p=v_a*v_b` uses at most `4d-3` products, `2d-2` additions and +two exact divisions by two. The two square arrays use 2d products. Each +emitted pair needs at most eight products and three additions/subtractions: +the t case has two source products, six target products and three subtractions; +the f/l/s cases use no more. Only the f-source and l-target need an exact +division by three. Public h_i values are obtained by halving a Gram diagonal +at most 3d times. Thus with `N=C(d+2,3)` the combined source/target stream uses + +``` +multiplications <= d^2+6d-3+8N = 159389, +additions/subtractions <= d^2+d-2+3N = 61150, +exact feature divisions by three = 2d = 96, +exact pivot divisions by two = 2, +public diagonal halvings <= 3d = 144. +``` + +The counts permit integer multiplication by constants rather than treating it +as free. They bound one explicit schedule; optimal arithmetic cost is not +claimed. Validating the fixed Gram/preconditions is a separate O(d^2) setup +check. A conservative indexed read/write bound for setup plus evaluation is +`128N+32d^2=2582528`: fewer than 64 indexed accesses suffice per attempted +feature (including skipped pivots and diagonal s indices), N+2d<=2N, and +32d^2 covers Gram, vector setup and validation. Comparisons/loop control can likewise be +charged a constant per attempted feature. Random-access integer operations +remain a model, not free physical routing. + +Every intermediate integer in this preprocessing fits 19 signed bits at the +actual shell. Indeed X,Y<=32 and V<=7. Ordered Gram-dot prefixes have magnitude +at most `480Y<=15360`; the final v bound is used only after the dot product +finishes. Source squares/cubes and the `u^3-u` prefix have magnitude at most +32800. Pivot products/numerators are bounded by 49 and 1372. The nu partial +accumulations and final values have magnitude at most `28*7^3=9604`. +Each target numerator, including every displayed left-to-right prefix, has +magnitude at most + +``` +4*2*7^3 + 15*28*7^3 = 146804 < 2^18. +``` + +In the l case the pre-division numerator `v_i^3-4v_i` has magnitude at most +371. Indices, counters and denominator metadata are smaller. Thus no large +canceling Gram prefix is incorrectly priced with the final V bound. The +resulting source feature bound is 32768 and common target scale is 256. + +An optional exact consumer may accumulate `sum phi_j e_j` as records arrive, +using one additional integer slot. All partial sums have magnitude at most +`19600*32768*146804 = 94285280051200 < 2^47`, so a signed 48-bit accumulator +suffices in that abstract consumer. The final exact value is K after division +by 256. This consumer is a diagnostic for the feature identity; it does not +implement a variable-data native decoder or change the cost of obtaining labels. + +## What is not proved + +No exact rank, minimal denominator, optimal coefficient bound, full-shell +factor table or physical source/target schedule is supplied. The binary chart +still bounds every factor support's binary pairing rank by 49, so the inherited +algebraic separate-copy upper bill remains `49*19600=960400`. This bound does +not price source access, arbitrary dirty state, frames, ownership, restoration, +native operations, precision, tape movement, the recursive compiler or the +outer multiplication construction. Those obligations remain open. + +The exact executable checks corroborate the formula and source binding. They +are not independent human review or formal proof-kernel acceptance. The written +identity, rather than finite samples, supplies the full-shell conclusion. diff --git a/research/norm6-streaming-features/README.md b/research/norm6-streaming-features/README.md new file mode 100644 index 0000000000..94f52dc23e --- /dev/null +++ b/research/norm6-streaming-features/README.md @@ -0,0 +1,164 @@ +# Stream norm-six features without a transform table + +**Scoped streaming construction; no new kappa.** Emit all 19,600 norm-six +feature pairs with at most **320 live integer slots**, including both input +vectors, plus **2,304 Gram entries**. There is no per-feature transform table +or target accumulator array. A consumer must release each output before the +next; retaining outputs requires additional storage. + +| Quantity | Bound | +|---|---:| +| Emitted factor pairs | 19,600 | +| Owned vector slots | 192 | +| Borrowed x/y input slots | 96 | +| Scalar/counter/current-record allowance | 32 | +| Per-feature descriptor / target accumulator slots | 0 / 0 | +| Immutable Gram slots | 2,304 | +| Common target denominator, not asserted minimal | 256 | +| Uniform target numerator magnitude | 146,804 | +| Uniform source feature magnitude | 32,768 | + +The term count and algebraic support upper bill `49*19600=960400` are inherited +from Nick Petalas's [#5084](https://github.com/CrocSwap/integer-mult-bounds/pull/5084). +Concurrent JoyboyBrian [#5132](https://github.com/CrocSwap/integer-mult-bounds/pull/5132) +publicly supplied an explicit construction during this investigation and +receives credit for closing that gap. Its stated allocations are 19,712 target +slots, 64 source slots and 245,884 immutable descriptor slots including G. +The new delta is a one-pass stream with O(d) live workspace and only the O(d^2) +Gram as fixed data. This compares explicit upper allocations, not an optimal +space lower bound. The feature bases differ and must not be interchanged. + +## Construction and exact boundary + +The kernel is `K(x,y)=((x^T G y)^3-4*x^T G y)/192` on `x^T G x=y^T G y=6`. +A two-coordinate Gram block `[[6,-1],[-1,6]]` gives a dyadic-unit pivot of +determinant -8 for the 48 shell relations. It removes two square-linear +features and 46 distinct-index cubics. Parity gives integral coefficients +over the common scale 256. + +[streaming.py](streaming.py) contains the table-free iterator. It owns exactly +four length-d vectors, generates feature keys by nested loops, and forms each +coefficient from at most three local relation entries. [PROOF.md](PROOF.md) +proves the identity, ownership/lifetime contract, operation counts and bounds +on all intermediate integers. Borrowed G,x,y must remain immutable throughout +iteration; the implementation preserves them but does not snapshot or police +concurrent mutation. Outputs retained by the caller are outside the 320 slots. + +The combined stream uses at most 159,389 integer multiplications and 61,150 +additions/subtractions, with 96 exact divisions by three, two pivot halvings +and at most 144 public Gram-diagonal halvings. All preprocessing intermediates +fit 19 signed bits on the actual norm-six shell. The counts include the Gram +dot-product prefixes, rather than pricing them by their smaller final values. +Divisions define precomputed integer-valued label features, as in #2222; they +are not dyadic scalar gates on arbitrary runtime data. This is an indexed +integer model, not a Python heap measurement or a physical tape tariff. + +The optional exact pair-kernel consumer needs one additional 48-bit accumulator. +It checks the feature identity; a variable-data physical decoder is not supplied. +The expansion decision is to stop at the specified stream contract. The changed +scope does not claim the historical card's whole-supplier/five-percent gate. + +## Evidence and reproduction + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/norm6-streaming-features +python3.12 -I -B -W error research/norm6-streaming-features/verify.py +python3.12 -I -O -B -W error research/norm6-streaming-features/verify.py +python3.12 -B scripts/check_research_commit.py --package research/norm6-streaming-features --check-source-history +``` + +Expected direct marker: `PASS_NORM6_STREAMING_FEATURES`; the registered runner +also prints `PASS_REGISTERED_RESEARCH_PACKAGE`. `verify.py --emit-result` +generates the deterministic source-bound receipt on stdout; normal verification +writes nothing and compares it to [RESULT.json](RESULT.json), including JSON types. + +New-result evidence: + +- An independently implemented literal polynomial-convolution oracle checks + all 48 relations, with 43,056 coefficient comparisons. It multiplies + polynomials and expands ordered Gram pairs rather than copying the + constructor's coefficient formulas. +- The exact -8 minor and all 2,304 entries of `R_P^T Q=8I` check the full pivot + solve for arbitrary target values. Full polynomial comparisons cover 3,275 + small-dimensional targets and five actual 48-dimensional targets. +- All **3,449,600 emitted coordinates** in **176 complete streams** agree with + the materialized reference already checked by the independent oracle. + Borrowed-input preservation, order, completion, early close and the four + owned vectors are checked. Static inspection supplies the algorithmic + storage proof; sampled Python frame inventories are only corroboration. +- The 44 actual-Gram norm-six vectors are a diagnostic set, not a full-shell + enumeration. A nonzero off-shell defect is tested. Exact multiplication of + G by its computed inverse establishes maximum inverse diagonal 172 and the + source-coordinate bound 32 under the cited positive-definiteness premise. +- Thirteen mathematical/input/stream corruptions reject. Normal and optimized + execution retain all checks. The reference implementation and its full + feature/relation arrays occur only in verification, never in the stream. + +The proof supplies universal coverage; finite tests alone do not. The official +export includes the sole live input, the Gram JSON, and direct replay needs +neither Git nor any predecessor executable. Local publication/export evidence +and hosted CI are reported separately in the PR. + +## Sources, coordination and credit + +Scientific base: `20a1e31bc6009b9b3f4d084bbaadc6350e34fcba`, priority revision 7. +[SOURCES.json](SOURCES.json) pins exact base blobs and SHA256 hashes. The +catalogue, selected record and predecessor proofs are provenance; only the +Gram JSON is a live external input. No frozen source is edited or copied. + +- Cinna Davis / 1337isnot1337, [#2222](https://github.com/CrocSwap/integer-mult-bounds/pull/2222), + `82cf756186c0fc2c542fcd06e486c575d97ffc5c`: kernel, integral-valued features, + P48p Gram and 49-bit chart. +- Nick Petalas, [#5084](https://github.com/CrocSwap/integer-mult-bounds/pull/5084), + `9d7f7805d147028fe5f0174e267ee05b73703f0b`: dyadic existence bound and handoff. +- JoyboyBrian, [#5132](https://github.com/CrocSwap/integer-mult-bounds/pull/5132), + `08572fdb060e73ecc4cb09a024611039881185f4`: concurrent explicit construction + and its transform/target-array resource bounds. Its proof supplies comparison + context; its code is neither imported nor replayed. +- DreamingOfClouds, [#2244](https://github.com/CrocSwap/integer-mult-bounds/pull/2244), + `8ef6fa81403973d3cacaf865bdabe9797a6c34a0`: rational shell-rank perspective. +- David Ganz / Dugongue, [#4494](https://github.com/CrocSwap/integer-mult-bounds/pull/4494), + `ad31d9fdf000d4ca98dd911afe489a45d2ea4f74`: the dyadic factorization lemma + used by #5084; the explicit pivot does not need that general lemma. + +Nebe/Sloane and the retained Leech/Niemeier geometry and kernel lineage retain +credit. Classical elimination and Cauchy-Schwarz are not new techniques. + +The [canonical investigation #5127](https://github.com/CrocSwap/integer-mult-bounds/discussions/5127) +retains the initial claim and the [scope change](https://github.com/CrocSwap/integer-mult-bounds/discussions/5127#discussioncomment-19143848). +The first snapshot covered 310 open PRs, 4,266 Discussion records and 6,884 +tracked notes. The later 10:23–10:24 UTC refresh covered 315 PRs and 4,284 +Discussion records and found #5132. Its claim had appeared between the +preceding live read and ours. Before publication we narrowed the contribution +to the different memory contract; we do not claim another first resolution of +the original constructibility question. Final freshness is recorded in TASK.json. +Arbitrary diffs, unpublished work and subsequent activity are outside snapshot +coverage. The original account's reflection, Schur, Pauli, association, fanout, +frame and A5 work is excluded. + +Prepared by Krzysztof Wojt with substantial OpenAI Codex assistance. Bounded +Luna support covered overlap inventory, the independently written polynomial +oracle, and arithmetic/storage review; the primary agent reviewed and +integrated it. Apache-2.0. Independent human and proof-kernel acceptance are +unclaimed. + +## Limitations + +Positive definiteness, lattice geometry and the binary chart remain cited +premises. No full-shell table, exact rank, term/space optimality, minimum +denominator or superior total arithmetic cost is claimed. Source acquisition, +physical variable-data side programs, frames, owners, dirty restoration, +precision, tape movement, compiler/recursive and outer admission remain +unknown. Unknown costs are not zero. No selected frontier is changed. + +## Open next questions + +Can one chronological physical source/target contract consume the stream +without retaining a cubic-size output array and with a favorable full invoice? +Start with one actual kernel invocation, check its data lifetime/order and +charge acquisition, preparation, frames, owners, dirty restoration, precision +and tape placement. The explicit generator removes the transform-table and +target-array requirement of this abstract interface; a physical caller and +its complete cost are still missing. See [TASK.json](TASK.json). diff --git a/research/norm6-streaming-features/RESULT.json b/research/norm6-streaming-features/RESULT.json new file mode 100644 index 0000000000..d617bb739d --- /dev/null +++ b/research/norm6-streaming-features/RESULT.json @@ -0,0 +1,95 @@ +{ + "actual_shell_fixture_count": 44, + "actual_shell_pairs": 176, + "dimension": 48, + "evaluation_budget": { + "retained_features": 19600, + "source_exact_divisions_by_3": 48, + "source_multiplications": 36850, + "source_subtractions": 48, + "target_additions_upper": 100446, + "target_common_denominator": 512, + "target_exact_divisions_by_3": 48, + "target_multiplications_upper": 159436 + }, + "global_target_numerator_bound": 293608, + "gram_sha256": "e25d51a0a9cdbc897d5db39fb698aa9bbc2f4ce29e8d7add2a44bae8f086add2", + "max_fixture_numerator": 3114, + "max_inverse_diagonal": "172", + "observed_owned_stream_vector_slots": 192, + "offshell_defect_times_3": 4320, + "original_features": 19648, + "package_sha256": { + "PROOF.md": "4d7c62c92bd636261ae4d64e83c1d274729f6bb46d323d4a70592e471db35673", + "README.md": "01cbce4bc286c5edd0a93440cc4634b9d10ebad8ae605941dfa6df10093d462b", + "SOURCES.json": "5aeaaf10528a59fc4022377875d59973b182845b34cebd68285de5e1cf9d9b85", + "TASK.json": "3cf1e8cdc52794b470349eaf9ee40bd553f3caaa4073987c2b3e055546e184ae", + "VERIFY.json": "b5add8380735ceb1fa827412e1154d186215d73fa7d838aec20cf7c1b367c36e", + "compression.py": "94974ecf6c0ff4b17e4057f8f6f5895f7dae37f2f37099ff438354bebeade096", + "oracle.py": "a7ddab8365229da02cbce8341f0ae8eacf8722ac1a0ea16a774546c76d5a734a", + "streaming.py": "4f888ec22eebcf702c6a3b4e9718ed5e9496782872e0c2f7b24b5b79e4f43c53", + "verify.py": "087dd7beb3216478d5635f493d8db2b9ffa7b6cfed7049678c748b8ad9cb7b8b" + }, + "pivot_determinant": -8, + "pivot_inverse_entries_checked": 2304, + "polynomial_oracle": [ + 9176, + 19312, + 18573, + 9176, + 19453 + ], + "rejected_controls": [ + "wrong f coefficient", + "wrong shell constant", + "corrupted retained feature", + "wrong elimination multiplier", + "omitted final factor eight", + "wrong pivot sign", + "asymmetric Gram", + "odd Gram diagonal", + "short target", + "boolean coordinate", + "repeated pivot", + "omitted first stream record", + "corrupted stream target" + ], + "relation_column_l1_max": 15, + "relation_oracle": [ + 48, + 43056 + ], + "removed_features": 48, + "retained_features": 19600, + "schema": "norm6-streaming-features/v1", + "scope": "Written shell identity plus exact finite corroboration; no physical tariff or new kappa.", + "small_all_polynomial_targets": 3275, + "source_coordinate_bound": 32, + "source_feature_bound": 32768, + "status": "PASS_NORM6_STREAMING_FEATURES", + "stream_budget": { + "additions_subtractions_upper": 61150, + "borrowed_source_target_slots": 96, + "combined_live_plus_gram_slots_upper": 2624, + "combined_live_slots_upper": 320, + "common_target_denominator": 256, + "emitted_pairs": 19600, + "feature_exact_divisions_by_3": 96, + "immutable_gram_slots": 2304, + "indexed_reads_writes_upper": 2582528, + "multiplications_upper": 159389, + "multiplier_exact_divisions_by_2": 2, + "owned_vector_slots": 192, + "per_feature_descriptor_slots": 0, + "public_diagonal_halvings_upper": 144, + "scalar_counter_record_slots_upper": 32, + "target_accumulator_array_slots": 0 + }, + "stream_pair_accumulator_absolute_bound": 94285280051200, + "stream_pair_accumulator_signed_bits": 48, + "stream_preprocessing_signed_bits": 19, + "stream_target_denominator": 256, + "stream_target_numerator_bound": 146804, + "streamed_coordinates_checked": 3449600, + "target_denominator": 512 +} diff --git a/research/norm6-streaming-features/SOURCES.json b/research/norm6-streaming-features/SOURCES.json new file mode 100644 index 0000000000..c9f982ac2e --- /dev/null +++ b/research/norm6-streaming-features/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "20a1e31bc6009b9b3f4d084bbaadc6350e34fcba", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/norm6-dyadic-compression/README.md", + "usage": "provenance", + "git_blob": "69cd696606105c1e660b2379f148361b77d4899f", + "sha256": "00d6143d9f54c51b7f0a628d108900612c3631f22cf5289c33bd81842e09031c" + }, + { + "path": "research/norm6-dyadic-decoder/PROOF.md", + "usage": "provenance", + "git_blob": "25fc7d52b5c28b7575cb0878a36955c542c2af13", + "sha256": "10400041efc16ec3aa34cbe945aed13c353377981ffadc746136c9c928d50951" + }, + { + "path": "research/norm6-dyadic-decoder/sources/P48p-GRAM.json", + "usage": "input", + "git_blob": "872dff9406881d567882d70882408eaa1e1f8f6c", + "sha256": "e25d51a0a9cdbc897d5db39fb698aa9bbc2f4ce29e8d7add2a44bae8f086add2" + } + ] +} diff --git a/research/norm6-streaming-features/TASK.json b/research/norm6-streaming-features/TASK.json new file mode 100644 index 0000000000..429822adc1 --- /dev/null +++ b/research/norm6-streaming-features/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "20a1e31bc6009b9b3f4d084bbaadc6350e34fcba", + "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": "Emit all 19600 norm-six feature pairs once without a transform descriptor or target accumulator array, with 6d+32 live indexed-integer slots plus d^2 Gram data and complete preprocessing bounds.", + "scope_change_reason": "The original constructibility question was independently completed by concurrent JoyboyBrian PR #5132. The public scope update narrows this contribution to a different streaming memory/consumer-lifetime contract, using a two-coordinate pivot and locally generated coefficients.", + "bottleneck_link": "Remove cubic-size coefficient-transform and target-accumulation storage from an explicit label-preprocessing interface. The consumer must release each record; retained outputs and physical decoder data remain additional costs. Term/support bounds are inherited, not improved.", + "budget_minutes": 240, + "stop_rule": "Stop at the independently corroborated streaming interface; do not duplicate PR #5132 constructibility, tune coefficients as a separate result or begin physical integration.", + "outcome": "completed", + "evidence": "Written stream identity and storage proof; independent polynomial oracle, all 2304 pivot-inverse entries, 3275 small target polynomials, five full-dimensional target polynomials, 3449600 emitted coordinates in 176 complete streams, exact source bound and 13 rejecting controls. No human/formal acceptance or physical admission.", + "author": "Krzysztof Wojt, with substantial OpenAI Codex assistance and bounded Luna support", + "ai_assistance": "Substantial OpenAI Codex assistance; bounded Luna support for read-only overlap inventory, independent polynomial oracle and arithmetic review. Primary reviewed and integrated all work.", + "open_questions": [ + { + "question": "Can one chronological physical source/target contract consume the stream without retaining a cubic-size output array and with a favorable total invoice?", + "why_it_matters": "The bounded coefficient stream does not price physical source acquisition, frames, owners, variable data, restoration, precision or tape placement.", + "first_step": "Bind one actual kernel invocation, check its ordering/lifetime against one-at-a-time consumption, and price both boundaries including all retained outputs.", + "blocked_by": "A source-bound physical caller and its complete cost invoice are absent." + } + ], + "coordination": { + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5127", + "claim_time_utc": "2026-10-23T10:05:00Z", + "expiry_utc": "2026-10-23T12:15:00Z", + "entry_coverage": { + "open_prs": 310, + "discussion_records": 4266, + "tracked_notes": 6884, + "limitations": "Arbitrary diffs and unpublished work are not exhaustively covered." + }, + "scope_update": { + "utc": "2026-10-23T10:31:00Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5127#discussioncomment-19143848", + "concurrent_pr": 5132, + "concurrent_head": "08572fdb060e73ecc4cb09a024611039881185f4", + "new_contract": "One-pass coefficient stream, no cubic-size transform descriptor or accumulator array; fixed Gram plus linear live workspace." + }, + "prepublication_refresh": { + "open_prs": 303, + "open_prs_fetched_at_utc": "2026-10-23T10:44:01.626421+00:00", + "discussion_records": 4290, + "discussions_fetched_at_utc": "2026-10-23T10:45:03.757128+00:00", + "local_notes": 6886, + "upstream_main": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "guidance_and_selected_frontier": "Unchanged from scientific base 20a1e31bc6009b9b3f4d084bbaadc6350e34fcba.", + "concurrent_pr_state": "PR #5132 merged at 2026-10-23T10:40:44Z; head unchanged from scope update; credited constructibility is not this contribution.", + "result": "No competing claim for the descriptor-free one-pass memory contract was found. All current author claims on reflection rounding, Schur minima and A5 were excluded.", + "limitations": "Title/body and indexed-note coverage is complete at these fetch times; arbitrary diffs, all reply trees and unpublished work are not exhaustively covered." + } + } +} diff --git a/research/norm6-streaming-features/VERIFY.json b/research/norm6-streaming-features/VERIFY.json new file mode 100644 index 0000000000..defb5dd765 --- /dev/null +++ b/research/norm6-streaming-features/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/norm6-dyadic-decoder/sources/P48p-GRAM.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete streaming output, ownership/order and resource bounds; exact inverse-map and independent polynomial certificates; rejecting semantic controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete mathematical and receipt checks with Python assertions disabled" + } + ] +} diff --git a/research/norm6-streaming-features/compression.py b/research/norm6-streaming-features/compression.py new file mode 100644 index 0000000000..8c01594573 --- /dev/null +++ b/research/norm6-streaming-features/compression.py @@ -0,0 +1,164 @@ +"""Explicit dyadic shell-feature elimination, not a physical decoder. + +Krzysztof Wojt with substantial OpenAI Codex assistance. Apache-2.0. +The uncompressed integer-valued feature identity is Cinna Davis's PR2222. +""" + +from itertools import combinations +from math import comb + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate_gram(gram, a=0, b=4): + d = len(gram) + require(2 <= d <= 48, "dimension must be between 2 and 48") + require(type(a) is int and type(b) is int and 0 <= a < b < d, + "invalid pivot indices") + require(all(len(row) == d for row in gram), "Gram must be square") + require(all(type(value) is int for row in gram for value in row), + "Gram entries must be integers") + require(all(gram[i][j] == gram[j][i] for i in range(d) for j in range(d)), + "Gram must be symmetric") + require(all(gram[i][i] % 2 == 0 for i in range(d)), "Gram must be even") + require((gram[a][a], gram[a][b], gram[b][b]) == (6, -1, 6), + "required pivot block is [[6,-1],[-1,6]]") + return d + + +def feature_keys(d): + require(type(d) is int and 2 <= d <= 48, "invalid feature dimension") + return ([('f', i) for i in range(d)] + [('l', i) for i in range(d)] + + [('s', i, j) for i in range(d) for j in range(d) if i != j] + + [('t', *triple) for triple in combinations(range(d), 3)]) + + +def shell_relations(gram, a=0, b=4): + """Rows R with R phi = x_i (x^T G x - 6)/2, in sparse form.""" + d = validate_gram(gram, a, b) + features = feature_keys(d) + positions = {key: j for j, key in enumerate(features)} + rows = [dict() for _ in range(d)] + + def put(row, key, value): + if value: + rows[row][positions[key]] = value + + for i in range(d): + put(i, ('f', i), 3 * (gram[i][i] // 2)) + put(i, ('l', i), gram[i][i] // 2 - 3) + for j in range(d): + if i != j: + put(i, ('s', j, i), gram[j][j] // 2) + put(i, ('s', i, j), gram[i][j]) + for j, k in combinations((j for j in range(d) if j != i), 2): + put(i, ('t', *sorted((i, j, k))), gram[j][k]) + pivots = [positions[('s', a, b)], positions[('s', b, a)]] + pivots += [positions[('t', *sorted((i, a, b)))] + for i in range(d) if i not in (a, b)] + return features, rows, pivots + + +def integer_vector(values, d, name): + require(len(values) == d and all(type(v) is int for v in values), + name + " must have exactly d integer coordinates") + + +def source_values(x, features): + d = sum(key[0] == 'f' for key in features) + integer_vector(x, d, "source") + values = [] + for key in features: + kind, *indices = key + if kind == 'f': + u = x[indices[0]] + values.append((u**3 - u) // 3) + elif kind == 'l': + values.append(x[indices[0]]) + elif kind == 's': + i, j = indices + values.append(x[i] * x[i] * x[j]) + else: + i, j, k = indices + values.append(x[i] * x[j] * x[k]) + return values + + +def old_target(v, features): + """Integral psi; phi dot psi = ((x dot v)^3 - 4 x dot v)/3.""" + d = sum(key[0] == 'f' for key in features) + integer_vector(v, d, "dual target") + values = [] + for key in features: + kind, *indices = key + if kind == 'f': + values.append(v[indices[0]]**3) + elif kind == 'l': + u = v[indices[0]] + values.append((u**3 - 4*u) // 3) + elif kind == 's': + i, j = indices + values.append(v[i] * v[i] * v[j]) + else: + i, j, k = indices + values.append(2 * v[i] * v[j] * v[k]) + return values + + +def elimination_multipliers(gram, pivot_values, a=0, b=4): + """mu=8 R_P^-T pivot_values, valid for arbitrary integral pivot targets.""" + d = validate_gram(gram, a, b) + integer_vector(pivot_values, d, "pivot target") + mu = [0]*d + mu[a] = pivot_values[0] + 3*pivot_values[1] + mu[b] = 3*pivot_values[0] + pivot_values[1] + for position, i in enumerate((i for i in range(d) if i not in (a, b)), 2): + mu[i] = gram[i][b]*mu[a] + gram[i][a]*mu[b] - 8*pivot_values[position] + return mu + + +def compress_target(gram, v, a=0, b=4, prepared=None): + """Integer numerators/512 and mu, with d eliminated positions zero. + + No shell is enumerated. Only source points must have norm six for the + identity; v may be any integer vector. For the kernel set v=G*y. + """ + d = validate_gram(gram, a, b) + integer_vector(v, d, "dual target") + features, rows, pivots = prepared or shell_relations(gram, a, b) + old = old_target(v, features) + mu = elimination_multipliers(gram, [old[j] for j in pivots], a, b) + numerators = [8*value for value in old] + for multiplier, row in zip(mu, rows): + for j, coefficient in row.items(): + numerators[j] -= multiplier*coefficient + require(all(numerators[j] == 0 for j in pivots), "pivot cancellation failed") + return numerators, mu + + +def gram_times(gram, x): + integer_vector(x, len(gram), "lattice target") + return [sum(g*t for g, t in zip(row, x)) for row in gram] + + +def quadratic(gram, x): + return sum(u*v for u, v in zip(x, gram_times(gram, x))) + + +def evaluation_budget(d): + """Conservative integer-preprocessing counts, not native scalar tariffs.""" + require(type(d) is int and 2 <= d <= 48, "invalid budget dimension") + n = comb(d+2, 3) + return { + 'retained_features': n, + 'source_multiplications': d*(d-1) + 2*comb(d, 3) + 2, + 'source_subtractions': d, + 'source_exact_divisions_by_3': d, + 'target_multiplications_upper': d*d + 8*n + 7*d - 4, + 'target_additions_upper': d*d + 5*n + 3*d - 2, + 'target_exact_divisions_by_3': d, + 'target_common_denominator': 512, + } diff --git a/research/norm6-streaming-features/oracle.py b/research/norm6-streaming-features/oracle.py new file mode 100644 index 0000000000..3377e3e9ba --- /dev/null +++ b/research/norm6-streaming-features/oracle.py @@ -0,0 +1,375 @@ +"""Independent exact polynomial oracles for norm-six symbolic compression. + +This module deliberately has no imports from the research package. Polynomials +are dictionaries from sorted variable-index tuples to integer coefficients; +the empty tuple denotes the constant monomial. + +Prepared for Krzysztof Wojt by a bounded Luna supporting agent, with primary +OpenAI Codex review and integration. Apache-2.0. +""" + +from __future__ import annotations + +from time import perf_counter + + +Polynomial = dict[tuple[int, ...], int] + + +def _fail(message: str) -> None: + raise ValueError(message) + + +def _is_int(value: object) -> bool: + return type(value) is int + + +def _validate_matrix(matrix: object) -> tuple[int, list[list[int]]]: + if type(matrix) not in (list, tuple): + _fail("G must be a list or tuple of rows") + rows = list(matrix) + dimension = len(rows) + if dimension == 0: + _fail("G must have positive dimension") + checked: list[list[int]] = [] + for index, row in enumerate(rows): + if type(row) not in (list, tuple) or len(row) != dimension: + _fail(f"G row {index} must have length {dimension}") + checked_row: list[int] = [] + for column, value in enumerate(row): + if not _is_int(value): + _fail(f"G[{index}][{column}] must be an integer") + checked_row.append(value) + checked.append(checked_row) + for i in range(dimension): + if checked[i][i] % 2: + _fail(f"G diagonal entry {i} must be even") + for j in range(i + 1, dimension): + if checked[i][j] != checked[j][i]: + _fail(f"G must be symmetric at ({i}, {j})") + return dimension, checked + + +def _validate_features(features: object, dimension: int) -> list[tuple[object, ...]]: + if type(features) is not list: + _fail("features must be a list") + checked: list[tuple[object, ...]] = [] + seen: set[tuple[object, ...]] = set() + for position, feature in enumerate(features): + if type(feature) is not tuple or not feature: + _fail(f"feature {position} must be a nonempty tuple") + kind = feature[0] + if type(kind) is not str: + _fail(f"feature {position} kind must be a string") + expected_length = {"f": 2, "l": 2, "s": 3, "t": 4}.get(kind) + if expected_length is None or len(feature) != expected_length: + _fail(f"feature {position} has an invalid kind or tuple length") + indices = feature[1:] + if any(not _is_int(index) for index in indices): + _fail(f"feature {position} indices must be integers") + if any(index < 0 or index >= dimension for index in indices): + _fail(f"feature {position} index is outside dimension {dimension}") + if kind == "s" and feature[1] == feature[2]: + _fail(f"feature {position} requires distinct s indices") + if kind == "t" and not (feature[1] < feature[2] < feature[3]): + _fail(f"feature {position} requires strictly increasing t indices") + if feature in seen: + _fail(f"duplicate feature at position {position}") + seen.add(feature) + checked.append(feature) + return checked + + +def _validate_integer_vector(value: object, length: int, name: str) -> list[int]: + if type(value) is not list or len(value) != length: + _fail(f"{name} must be a list of length {length}") + result: list[int] = [] + for index, item in enumerate(value): + if not _is_int(item): + _fail(f"{name}[{index}] must be an integer") + result.append(item) + return result + + +def _add_term(poly: Polynomial, monomial: tuple[int, ...], coefficient: int) -> None: + if not coefficient: + return + value = poly.get(monomial, 0) + coefficient + if value: + poly[monomial] = value + else: + poly.pop(monomial, None) + + +def _add_scaled(target: Polynomial, source: Polynomial, scale: int) -> None: + for monomial, coefficient in source.items(): + _add_term(target, monomial, scale * coefficient) + + +def _scale(poly: Polynomial, scale: int) -> Polynomial: + result: Polynomial = {} + _add_scaled(result, poly, scale) + return result + + +def _add(poly_a: Polynomial, poly_b: Polynomial) -> Polynomial: + result = dict(poly_a) + _add_scaled(result, poly_b, 1) + return result + + +def _subtract(poly_a: Polynomial, poly_b: Polynomial) -> Polynomial: + result = dict(poly_a) + _add_scaled(result, poly_b, -1) + return result + + +def _multiply(poly_a: Polynomial, poly_b: Polynomial) -> Polynomial: + """Multiply by literal monomial-pair convolution, then collect terms.""" + result: Polynomial = {} + for monomial_a, coefficient_a in poly_a.items(): + for monomial_b, coefficient_b in poly_b.items(): + monomial = tuple(sorted(monomial_a + monomial_b)) + _add_term(result, monomial, coefficient_a * coefficient_b) + return result + + +def _half(poly: Polynomial, context: str) -> Polynomial: + result: Polynomial = {} + for monomial, coefficient in poly.items(): + if coefficient % 2: + _fail(f"{context} has an odd coefficient at monomial {monomial}") + half = coefficient // 2 + if half: + result[monomial] = half + return result + + +def _feature_threefold(feature: tuple[object, ...]) -> Polynomial: + """Return the integer polynomial 3*phi for one declared feature.""" + kind = feature[0] + if kind == "f": + index = feature[1] + return {(index, index, index): 1, (index,): -1} + if kind == "l": + return {(feature[1],): 3} + if kind == "s": + return {tuple(sorted((feature[1], feature[1], feature[2]))): 3} + if kind == "t": + return {tuple(sorted(feature[1:])): 3} + _fail("internal error: unvalidated feature kind") + + +def _quadratic_minus_six(matrix: list[list[int]]) -> Polynomial: + """Expand x^T G x by all ordered index pairs, then subtract six.""" + dimension = len(matrix) + result: Polynomial = {} + for i in range(dimension): + for j in range(dimension): + _add_term(result, tuple(sorted((i, j))), matrix[i][j]) + _add_term(result, (), -6) + return result + + +def _linear_form(coefficients: list[int]) -> Polynomial: + result: Polynomial = {} + for index, coefficient in enumerate(coefficients): + _add_term(result, (index,), coefficient) + return result + + +def _monomial_comparison_count(left: Polynomial, right: Polynomial) -> int: + return len(left.keys() | right.keys()) + + +def _compare_exact(left: Polynomial, right: Polynomial, context: str) -> int: + comparisons = _monomial_comparison_count(left, right) + if left != right: + monomial = next( + monomial + for monomial in sorted(left.keys() | right.keys()) + if left.get(monomial, 0) != right.get(monomial, 0) + ) + _fail( + f"{context} mismatch at monomial {monomial}: " + f"left={left.get(monomial, 0)}, right={right.get(monomial, 0)}" + ) + return comparisons + + +def audit_relations( + G: list[list[int]], + features: list[tuple[object, ...]], + relation_rows: list[dict[int, int]], +) -> tuple[int, int]: + """Check every relation against literal 3*x_i*(x^T G x - 6)/2. + + Returns ``(number_of_rows, number_of_monomial_comparisons)``. A comparison + is one monomial key in the union of the two collected row polynomials. + Every input violation or polynomial mismatch raises ``ValueError``. + """ + dimension, matrix = _validate_matrix(G) + checked_features = _validate_features(features, dimension) + if type(relation_rows) is not list or len(relation_rows) != dimension: + _fail(f"relation_rows must be a list of length {dimension}") + feature_polynomials = [_feature_threefold(feature) for feature in checked_features] + quadratic = _quadratic_minus_six(matrix) + total_comparisons = 0 + for row_index, row in enumerate(relation_rows): + if type(row) is not dict: + _fail(f"relation row {row_index} must be a dict") + left: Polynomial = {} + for feature_index, coefficient in row.items(): + if not _is_int(feature_index) or feature_index < 0 or feature_index >= len(checked_features): + _fail(f"relation row {row_index} has an invalid feature index") + if not _is_int(coefficient): + _fail(f"relation row {row_index} coefficient must be an integer") + _add_scaled(left, feature_polynomials[feature_index], coefficient) + + variable = {(row_index,): 1} + literal_numerator = _scale(_multiply(variable, quadratic), 3) + right = _half(literal_numerator, f"relation row {row_index} right-hand side") + total_comparisons += _compare_exact( + left, right, f"relation row {row_index}" + ) + return dimension, total_comparisons + + +def audit_compression( + G: list[list[int]], + v: list[int], + features: list[tuple[object, ...]], + compressed8: list[int], + mu: list[int], +) -> int: + """Check the exact compressed polynomial identity over every source x. + + ``compressed8`` is indexed by the complete feature list; eliminated + features are represented by zero coefficients. Returns the number of + monomial comparisons. Any input violation or mismatch raises ``ValueError``. + """ + dimension, matrix = _validate_matrix(G) + checked_features = _validate_features(features, dimension) + checked_v = _validate_integer_vector(v, dimension, "v") + checked_mu = _validate_integer_vector(mu, dimension, "mu") + checked_compressed = _validate_integer_vector( + compressed8, len(checked_features), "compressed8" + ) + + feature_polynomials = [_feature_threefold(feature) for feature in checked_features] + left: Polynomial = {} + for coefficient, feature_poly in zip(checked_compressed, feature_polynomials): + _add_scaled(left, feature_poly, coefficient) + + linear_v = _linear_form(checked_v) + linear_v_cubed = _multiply(_multiply(linear_v, linear_v), linear_v) + first_rhs_term = _scale( + _subtract(linear_v_cubed, _scale(linear_v, 4)), 8 + ) + + linear_mu = _linear_form(checked_mu) + quadratic = _quadratic_minus_six(matrix) + correction_product = _multiply(linear_mu, quadratic) + correction_term = _scale( + _half(correction_product, "compression correction term"), 3 + ) + right = _subtract(first_rhs_term, correction_term) + return _compare_exact(left, right, "compression identity") + + +def _selfcheck() -> float: + start = perf_counter() + features: list[tuple[object, ...]] = [ + ("f", 0), ("f", 1), ("f", 2), + ("l", 0), ("l", 1), ("l", 2), + ("s", 0, 1), ("s", 0, 2), ("s", 1, 0), + ("s", 1, 2), ("s", 2, 0), ("s", 2, 1), + ("t", 0, 1, 2), + ] + feature_index = {feature: index for index, feature in enumerate(features)} + matrix = [ + [6, 1, 2], + [1, 6, 3], + [2, 3, 6], + ] + rows = [ + { + feature_index[("f", 0)]: 9, + feature_index[("s", 0, 1)]: 1, + feature_index[("s", 0, 2)]: 2, + feature_index[("s", 1, 0)]: 3, + feature_index[("s", 2, 0)]: 3, + feature_index[("t", 0, 1, 2)]: 3, + }, + { + feature_index[("f", 1)]: 9, + feature_index[("s", 0, 1)]: 3, + feature_index[("s", 1, 0)]: 1, + feature_index[("s", 1, 2)]: 3, + feature_index[("s", 2, 1)]: 3, + feature_index[("t", 0, 1, 2)]: 2, + }, + { + feature_index[("f", 2)]: 9, + feature_index[("s", 0, 2)]: 3, + feature_index[("s", 1, 2)]: 3, + feature_index[("s", 2, 0)]: 2, + feature_index[("s", 2, 1)]: 3, + feature_index[("t", 0, 1, 2)]: 1, + }, + ] + row_count, relation_comparisons = audit_relations(matrix, features, rows) + if row_count != 3 or relation_comparisons != 21: + _fail("relation selfcheck returned unexpected counts") + + compressed = [0] * len(features) + compressed[feature_index[("f", 0)]] = 46 + compressed[feature_index[("s", 0, 1)]] = -2 + compressed[feature_index[("s", 0, 2)]] = -4 + compressed[feature_index[("s", 1, 0)]] = -6 + compressed[feature_index[("s", 2, 0)]] = -6 + compressed[feature_index[("t", 0, 1, 2)]] = -6 + compression_comparisons = audit_compression( + matrix, [2, 0, 0], features, compressed, [2, 0, 0] + ) + if compression_comparisons != 7: + _fail("compression selfcheck returned unexpected comparison count") + + bad_rows = [dict(row) for row in rows] + bad_rows[0][feature_index[("f", 0)]] -= 1 + try: + audit_relations(matrix, features, bad_rows) + except ValueError: + pass + else: + _fail("relation corruption control was accepted") + + bad_compressed = list(compressed) + bad_compressed[feature_index[("s", 0, 1)]] -= 1 + try: + audit_compression(matrix, [2, 0, 0], features, bad_compressed, [2, 0, 0]) + except ValueError: + pass + else: + _fail("compression corruption control was accepted") + + try: + audit_relations([[6, 0], [1, 6]], [("f", 0)], [{0: 9}, {}]) + except ValueError: + pass + else: + _fail("invalid-matrix control was accepted") + + try: + audit_compression([[6]], [2], [([], 0)], [0], [0]) + except ValueError: + pass + else: + _fail("invalid-feature-type control was accepted") + + return perf_counter() - start + + +if __name__ == "__main__": + elapsed = _selfcheck() + print(f"PASS_NORM6_SYMBOLIC_POLYNOMIAL_ORACLE elapsed_s={elapsed:.6f}") diff --git a/research/norm6-streaming-features/streaming.py b/research/norm6-streaming-features/streaming.py new file mode 100644 index 0000000000..e84c16f414 --- /dev/null +++ b/research/norm6-streaming-features/streaming.py @@ -0,0 +1,95 @@ +"""One-pass norm-six feature pairs without a feature/transform table. + +Krzysztof Wojt with substantial OpenAI Codex assistance. Apache-2.0. +The caller borrows G,x,y read-only, consumes each emitted record, and releases +it before requesting the next. Retaining outputs is additional caller storage. +The caller must keep all three inputs immutable for the iterator's lifetime. +No physical/native gate or tape tariff is implied by integer-array slots. +""" + +from math import comb +from compression import integer_vector, require, validate_gram + +DENOMINATOR = 256 + + +def feature_stream(gram, x, y, a=0, b=4): + """Yield (feature_key, integer_source, integer_target_numerator). + + Sum source*numerator/256 gives K for integral q(x)=q(y)=6. The iterator + itself does not enforce the shell precondition or buffer emitted records. + Its only owned arrays are v, nu, xsq, vsq, each of length d. There is no + feature list, relation matrix, transform descriptor or output accumulator. + """ + d = validate_gram(gram, a, b) + integer_vector(x, d, 'source') + integer_vector(y, d, 'target') + v = [0]*d + for i in range(d): + total = gram[i][0]*y[0] + for j in range(1, d): + total += gram[i][j]*y[j] + v[i] = total + nu = [0]*d + p = v[a]*v[b] + numerator_a = p*(v[a]+3*v[b]) + numerator_b = p*(3*v[a]+v[b]) + require(numerator_a % 2 == numerator_b % 2 == 0, 'integer parity identity') + nu[a], nu[b] = numerator_a//2, numerator_b//2 + for i in range(d): + if i != a and i != b: + nu[i] = gram[i][b]*nu[a] + gram[i][a]*nu[b] - 8*p*v[i] + xsq = [u*u for u in x] + vsq = [u*u for u in v] + + for i in range(d): + h = gram[i][i]//2 + source = (xsq[i]*x[i]-x[i])//3 + target = 4*vsq[i]*v[i] - 3*h*nu[i] + yield ('f', i), source, target + for i in range(d): + h = gram[i][i]//2 + target = 4*((vsq[i]*v[i]-4*v[i])//3) - (h-3)*nu[i] + yield ('l', i), x[i], target + for i in range(d): + h = gram[i][i]//2 + for j in range(d): + if i == j or (i == a and j == b) or (i == b and j == a): + continue + source = xsq[i]*x[j] + target = 4*vsq[i]*v[j] - gram[i][j]*nu[i] - h*nu[j] + yield ('s', i, j), source, target + for i in range(d): + for j in range(i+1, d): + for k in range(j+1, d): + if ((i == a or j == a or k == a) + and (i == b or j == b or k == b)): + continue + source = x[i]*x[j]*x[k] + target = (8*v[i]*v[j]*v[k] - gram[j][k]*nu[i] + - gram[i][k]*nu[j] - gram[i][j]*nu[k]) + yield ('t', i, j, k), source, target + + +def stream_budget(d): + """Fixed indexed-integer algorithm bounds, not Python heap measurements.""" + require(type(d) is int and 2 <= d <= 48, 'invalid budget dimension') + n = comb(d+2, 3) + return { + 'emitted_pairs': n, + 'immutable_gram_slots': d*d, + 'per_feature_descriptor_slots': 0, + 'target_accumulator_array_slots': 0, + 'owned_vector_slots': 4*d, + 'borrowed_source_target_slots': 2*d, + 'scalar_counter_record_slots_upper': 32, + 'combined_live_slots_upper': 6*d+32, + 'combined_live_plus_gram_slots_upper': d*d+6*d+32, + 'multiplications_upper': d*d+6*d-3+8*n, + 'additions_subtractions_upper': d*d+d-2+3*n, + 'feature_exact_divisions_by_3': 2*d, + 'multiplier_exact_divisions_by_2': 2, + 'public_diagonal_halvings_upper': 3*d, + 'indexed_reads_writes_upper': 128*n+32*d*d, + 'common_target_denominator': DENOMINATOR, + } diff --git a/research/norm6-streaming-features/verify.py b/research/norm6-streaming-features/verify.py new file mode 100644 index 0000000000..2b006e1bae --- /dev/null +++ b/research/norm6-streaming-features/verify.py @@ -0,0 +1,321 @@ +#!/usr/bin/env python3 +"""Exact new-result verification; no predecessor executable is imported. + +Krzysztof Wojt with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +from fractions import Fraction +import hashlib +from itertools import product +import json +from math import isqrt +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from compression import (compress_target, elimination_multipliers, evaluation_budget, gram_times, + quadratic, require, shell_relations, + source_values, validate_gram) +from oracle import audit_compression, audit_relations +from streaming import DENOMINATOR, feature_stream, stream_budget + +GRAM_PATH = 'research/norm6-dyadic-decoder/sources/P48p-GRAM.json' + + +def determinant(matrix): + """Fraction-free Bareiss; independent of the explicit pivot inverse.""" + a = [list(row) for row in matrix] + n = len(a) + sign, previous = 1, 1 + for k in range(n-1): + pivot = next((i for i in range(k, n) if a[i][k]), None) + if pivot is None: + return 0 + if pivot != k: + a[pivot], a[k] = a[k], a[pivot] + sign = -sign + current = a[k][k] + for i in range(k+1, n): + for j in range(k+1, n): + value = a[i][j]*current - a[i][k]*a[k][j] + require(value % previous == 0, 'Bareiss exact divisibility') + a[i][j] = value // previous + a[i][k] = 0 + previous = current + return sign*a[-1][-1] + + +def inverse(matrix): + """Exact rational elimination, used only for source-coordinate bounds.""" + n = len(matrix) + a = [[Fraction(v) for v in row] + [Fraction(i == j) for j in range(n)] + for i, row in enumerate(matrix)] + for k in range(n): + p = next(i for i in range(k, n) if a[i][k]) + a[k], a[p] = a[p], a[k] + scale = a[k][k] + a[k] = [v/scale for v in a[k]] + for i in range(n): + if i != k and a[i][k]: + scale = a[i][k] + a[i] = [u-scale*v for u, v in zip(a[i], a[k])] + return [row[n:] for row in a] + + +def rejected(function, label): + try: + function() + except (ValueError, TypeError): + return label + raise ValueError('control did not reject: '+label) + + +def check_stream(gram, x, y, features, pivots, numerators, iterator=None): + """Materialized reference is verifier-only, never part of the stream.""" + expected_source = source_values(x, features) + positions = {key: i for i, key in enumerate(features)} + pivot_set = set(pivots) + expected_keys = [key for i, key in enumerate(features) if i not in pivot_set] + frozen = (tuple(map(tuple, gram)), tuple(x), tuple(y)) + production_iterator = iterator is None + iterator = feature_stream(gram, x, y) if production_iterator else iterator + count, total, owned_slots_max = 0, 0, 0 + for key, source, target in iterator: + require(count < len(expected_keys) and key == expected_keys[count], 'stream order/count') + j = positions[key] + require(type(source) is int and type(target) is int, 'stream integer types') + require(source == expected_source[j] and 2*target == numerators[j], 'stream feature mismatch') + require(abs(source) <= 32768 and abs(target) <= 146804, 'stream global values') + if production_iterator and count % 1024 == 0: + frame = iterator.gi_frame.f_locals + owned = {name: len(value) for name, value in frame.items() + if isinstance(value, list) and name not in ('gram', 'x', 'y')} + require(owned == {name: len(gram) for name in ('v', 'nu', 'xsq', 'vsq')}, + 'unexpected owned stream array') + owned_slots_max = max(owned_slots_max, sum(owned.values())) + require(all(abs(value) < 2**18 for value in frame.values() + if type(value) is int), 'stream scalar prefix width') + total += source*target + count += 1 + require(count == len(expected_keys), 'incomplete stream') + if production_iterator: + require(iterator.gi_frame is None, 'completed stream retains frame') + require(frozen == (tuple(map(tuple, gram)), tuple(x), tuple(y)), 'borrowed inputs mutated') + v = gram_times(gram, y) + t = sum(u*w for u, w in zip(x, v)) + require(3*total == 4*(t**3-4*t), 'stream kernel consumer') + require(abs(total) <= 19600*32768*146804, 'stream accumulator bound') + return count, owned_slots_max + + +def run(): + gram_bytes = (ROOT/GRAM_PATH).read_bytes() + gram = json.loads(gram_bytes) + require(len(gram) == 48, 'actual source dimension') + validate_gram(gram) + require(max(max(row) for row in gram) == 10, 'actual maximum entry') + require(max(abs(gram[i][j]) for i in range(48) for j in range(48) + if i != j) == 5, 'actual maximum off-diagonal') + prepared = shell_relations(gram) + features, rows, pivots = prepared + require(len(features) == 19648 and len(set(pivots)) == 48, 'feature counts') + order = [0, 4] + [i for i in range(48) if i not in (0, 4)] + minor = [[rows[i].get(j, 0) for j in pivots] for i in order] + minor_det = determinant(minor) + require(minor_det == -8, 'actual dyadic-unit minor') + relation_evidence = list(audit_relations(gram, features, rows)) + # Check the whole inverse map, not just its action at selected targets. + for k in range(48): + basis = [int(j == k) for j in range(48)] + mu_basis = elimination_multipliers(gram, basis) + for j, feature in enumerate(pivots): + require(sum(rows[i].get(feature, 0)*mu_basis[i] for i in range(48)) + == 8*(j == k), 'entire pivot inverse map') + + column_l1 = [0]*len(features) + for row in rows: + for j, value in row.items(): + column_l1[j] += abs(value) + require(max(column_l1) <= 15, 'relation column norm bound') + + # Exact multiplication checks the dual bound's inverse. Positive + # definiteness remains a cited geometric premise, not a replay target. + dual = inverse(gram) + for i in range(48): + for j in range(48): + require(sum(gram[i][k]*dual[k][j] for k in range(48)) == (i == j), + 'inverse identity') + max_inverse_diagonal = max(dual[i][i] for i in range(48)) + require(max_inverse_diagonal.denominator == 1, 'integral dual diagonal') + coordinate_bound = isqrt(6*max_inverse_diagonal.numerator) + + # A complete small coefficient cube, not the complete P48p shell. + shell = [] + for prefix in product(range(-2, 3), repeat=4): + x = list(prefix) + [0]*44 + if quadratic(gram, x) == 6: + shell.append(x) + for i in range(48): + if gram[i][i] == 6: + x = [int(j == i) for j in range(48)] + shell.extend((x, [-v for v in x])) + shell = [list(x) for x in sorted(set(map(tuple, shell)))] + require(len(shell) >= 20, 'nonempty actual-shell diagnostics') + target_indices = sorted(set([0, len(shell)//3, len(shell)//2, len(shell)-1])) + pairs = 0 + streamed_coordinates = 0 + owned_stream_slots = 0 + polynomial_checks = [] + max_fixture_numerator = 0 + for index in target_indices: + y = shell[index] + v = gram_times(gram, y) + numerators, mu = compress_target(gram, v, prepared=prepared) + require(max(map(abs, v)) <= 7, 'dual-coordinate Cauchy bound') + require(max(map(abs, numerators)) <= 293608, 'global numerator bound') + max_fixture_numerator = max(max_fixture_numerator, max(map(abs, numerators))) + polynomial_checks.append(audit_compression(gram, v, features, numerators, mu)) + for x in shell: + value = sum(u*w for u, w in zip(source_values(x, features), numerators)) + t = sum(u*w for u, w in zip(x, v)) + require(3*value == 8*(t**3-4*t), 'literal compressed kernel') + count, slots = check_stream(gram, x, y, features, pivots, numerators) + streamed_coordinates += count + owned_stream_slots = max(owned_stream_slots, slots) + pairs += 1 + + # Arbitrary targets and an off-shell source discriminate the precise + # shell identity from an incorrect global polynomial identity. + arbitrary_v = [((i*7+3) % 11)-5 for i in range(48)] + coefficients, mu = compress_target(gram, arbitrary_v, prepared=prepared) + polynomial_checks.append(audit_compression(gram, arbitrary_v, features, coefficients, mu)) + offshell = [2] + [0]*47 + lhs = sum(c*f for c, f in zip(coefficients, source_values(offshell, features))) + t = sum(u*v for u, v in zip(offshell, arbitrary_v)) + defect3 = 3*lhs - 8*(t**3-4*t) + expected3 = -3*sum(u*x for u, x in zip(mu, offshell))*(quadratic(gram, offshell)-6)//2 + require(defect3 == expected3 and defect3 != 0, 'nonzero off-shell defect') + + small_pairs = 0 + for d in (2, 3, 5): + small = [[6 if i == j else (-1 if {i, j} == {0, 1} else 0) + for j in range(d)] for i in range(d)] + prep = shell_relations(small, 0, 1) + sf, sr, sp = prep + audit_relations(small, sf, sr) + for v in product(range(-2, 3), repeat=d): + c, m = compress_target(small, list(v), 0, 1, prep) + audit_compression(small, list(v), sf, c, m) + require(all(c[j] == 0 for j in sp), 'small pivot cancellation') + small_pairs += 1 + + controls = [] + bad = [dict(row) for row in rows] + bad[0][0] += 1 + controls.append(rejected(lambda: audit_relations(gram, features, bad), 'wrong f coefficient')) + bad = [dict(row) for row in rows] + bad[0][len(gram)] = 1 + controls.append(rejected(lambda: audit_relations(gram, features, bad), 'wrong shell constant')) + changed = list(coefficients) + changed[0] += 1 + controls.append(rejected(lambda: audit_compression(gram, arbitrary_v, features, changed, mu), + 'corrupted retained feature')) + changed_mu = list(mu) + changed_mu[0] += 1 + controls.append(rejected(lambda: audit_compression(gram, arbitrary_v, features, coefficients, changed_mu), + 'wrong elimination multiplier')) + controls.append(rejected(lambda: audit_compression(gram, arbitrary_v, features, + [8*c for c in coefficients], mu), 'omitted final factor eight')) + bad_gram = [list(row) for row in gram] + bad_gram[0][4] = bad_gram[4][0] = 1 + controls.append(rejected(lambda: shell_relations(bad_gram), 'wrong pivot sign')) + bad_gram = [list(row) for row in gram] + bad_gram[0][1] += 1 + controls.append(rejected(lambda: shell_relations(bad_gram), 'asymmetric Gram')) + bad_gram = [list(row) for row in gram] + bad_gram[1][1] += 1 + controls.append(rejected(lambda: shell_relations(bad_gram), 'odd Gram diagonal')) + controls.append(rejected(lambda: compress_target(gram, [0]*47), 'short target')) + controls.append(rejected(lambda: compress_target(gram, [True]+[0]*47), 'boolean coordinate')) + controls.append(rejected(lambda: shell_relations(gram, 0, 0), 'repeated pivot')) + + y = shell[0] + c, _ = compress_target(gram, gram_times(gram, y), prepared=prepared) + early = feature_stream(gram, shell[0], y) + next(early) + early.close() + require(early.gi_frame is None, 'early close retains stream frame') + omitted = feature_stream(gram, shell[0], y) + next(omitted) + controls.append(rejected(lambda: check_stream(gram, shell[0], y, features, pivots, c, omitted), + 'omitted first stream record')) + omitted.close() + def wrong_coefficient(): + first = True + for key, source, target in feature_stream(gram, shell[0], y): + yield key, source, target+1 if first else target + first = False + changed_stream = wrong_coefficient() + controls.append(rejected(lambda: check_stream(gram, shell[0], y, features, pivots, c, changed_stream), + 'corrupted stream target')) + changed_stream.close() + + bindings = {} + for name in ('compression.py', 'streaming.py', 'oracle.py', 'verify.py', 'PROOF.md', 'README.md', + 'TASK.json', 'SOURCES.json', 'VERIFY.json'): + bindings[name] = hashlib.sha256((HERE/name).read_bytes()).hexdigest() + return { + 'schema': 'norm6-streaming-features/v1', + 'status': 'PASS_NORM6_STREAMING_FEATURES', + 'gram_sha256': hashlib.sha256(gram_bytes).hexdigest(), + 'package_sha256': bindings, + 'dimension': 48, 'original_features': len(features), 'removed_features': len(pivots), + 'retained_features': len(features)-len(pivots), 'pivot_determinant': minor_det, + 'relation_column_l1_max': max(column_l1), 'relation_oracle': relation_evidence, + 'pivot_inverse_entries_checked': 48*48, + 'polynomial_oracle': polynomial_checks, + 'actual_shell_fixture_count': len(shell), 'actual_shell_pairs': pairs, + 'small_all_polynomial_targets': small_pairs, + 'max_fixture_numerator': max_fixture_numerator, + 'target_denominator': 512, 'global_target_numerator_bound': 293608, + 'max_inverse_diagonal': str(max_inverse_diagonal), + 'source_coordinate_bound': coordinate_bound, + 'source_feature_bound': coordinate_bound**3, + 'streamed_coordinates_checked': streamed_coordinates, + 'observed_owned_stream_vector_slots': owned_stream_slots, + 'stream_target_denominator': DENOMINATOR, + 'stream_target_numerator_bound': 146804, + 'stream_preprocessing_signed_bits': 19, + 'stream_pair_accumulator_signed_bits': 48, + 'stream_pair_accumulator_absolute_bound': 19600*32768*146804, + 'stream_budget': stream_budget(48), + 'offshell_defect_times_3': defect3, + 'rejected_controls': controls, 'evaluation_budget': evaluation_budget(48), + 'scope': 'Written shell identity plus exact finite corroboration; no physical tariff or new kappa.', + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit-result', action='store_true', help='generate receipt on stdout') + args = parser.parse_args() + result = run() + if args.emit_result: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + expected_path = HERE/'RESULT.json' + require(expected_path.stat().st_size < 65536, 'receipt size limit') + expected = json.loads(expected_path.read_text(encoding='utf-8')) + require(json.dumps(expected, sort_keys=True) == json.dumps(result, sort_keys=True), + 'generated receipt mismatch') + print(result['status'], 'features=19600 denominator=256 live_slots=320', + 'pairs='+str(result['actual_shell_pairs']), + 'polynomial_targets='+str(result['small_all_polynomial_targets']), + 'controls='+str(len(result['rejected_controls']))) + + +if __name__ == '__main__': + main()