From 362b20bc934500bc503e850059f0d34daa5dcae3 Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Fri, 6 Nov 2026 12:24:41 +0800 Subject: [PATCH] Restore phase covariance in sharp four-axis Gaussian rounding Construct and certify a minimal-period odd lattice map. Bind its exact inverse to retained two-/three-call ports and save two fractional bits at four axes. Preserve explicit fourth-power counterexample and complete scoped cost limits. Prepared for @CubeJerry with substantial OpenAI Codex assistance. --- .../CALLER-SOURCES.json | 23 + .../four-axis-phase-covariant-grid/CALLER.md | 104 +++++ .../CERTIFICATE.json | 1 + .../four-axis-phase-covariant-grid/NOTICE.md | 44 ++ .../four-axis-phase-covariant-grid/PROOF.md | 404 +++++++++++++++++ .../four-axis-phase-covariant-grid/README.md | 201 +++++++++ .../SOURCES.json | 81 ++++ .../four-axis-phase-covariant-grid/TASK.json | 96 ++++ .../VERIFY.json | 55 +++ .../four-axis-phase-covariant-grid/caller.py | 115 +++++ .../construction.py | 107 +++++ .../inputs/retained_ports.py | 26 ++ .../inputs/retained_rounded.py | 123 ++++++ .../four-axis-phase-covariant-grid/kernel.py | 45 ++ .../four-axis-phase-covariant-grid/verify.py | 413 ++++++++++++++++++ .../verify_caller.py | 140 ++++++ 16 files changed, 1978 insertions(+) create mode 100644 research/four-axis-phase-covariant-grid/CALLER-SOURCES.json create mode 100644 research/four-axis-phase-covariant-grid/CALLER.md create mode 100644 research/four-axis-phase-covariant-grid/CERTIFICATE.json create mode 100644 research/four-axis-phase-covariant-grid/NOTICE.md create mode 100644 research/four-axis-phase-covariant-grid/PROOF.md create mode 100644 research/four-axis-phase-covariant-grid/README.md create mode 100644 research/four-axis-phase-covariant-grid/SOURCES.json create mode 100644 research/four-axis-phase-covariant-grid/TASK.json create mode 100644 research/four-axis-phase-covariant-grid/VERIFY.json create mode 100644 research/four-axis-phase-covariant-grid/caller.py create mode 100644 research/four-axis-phase-covariant-grid/construction.py create mode 100644 research/four-axis-phase-covariant-grid/inputs/retained_ports.py create mode 100644 research/four-axis-phase-covariant-grid/inputs/retained_rounded.py create mode 100644 research/four-axis-phase-covariant-grid/kernel.py create mode 100644 research/four-axis-phase-covariant-grid/verify.py create mode 100644 research/four-axis-phase-covariant-grid/verify_caller.py diff --git a/research/four-axis-phase-covariant-grid/CALLER-SOURCES.json b/research/four-axis-phase-covariant-grid/CALLER-SOURCES.json new file mode 100644 index 0000000000..5da4d32c57 --- /dev/null +++ b/research/four-axis-phase-covariant-grid/CALLER-SOURCES.json @@ -0,0 +1,23 @@ +{ + "repository": "aliromman/integer-mult-bounds", + "pull_request": "CrocSwap/integer-mult-bounds#6509", + "commit": "a4173e810c4d34a1d13b9745af123ad0ec6cfed5", + "files": [ + { + "local_path": "inputs/retained_ports.py", + "module": "retained_ports", + "path": "research/conservative-gaussian-rounding/ports.py", + "size": 1012, + "sha256": "8460457aaafeaedf3b7fb287c0d61b049fb2595e8993ba3fc8695d8f9c9b830d", + "git_blob": "a9d5d0268ff6872536edadf159f79448aa30197a" + }, + { + "local_path": "inputs/retained_rounded.py", + "module": "retained_rounded", + "path": "research/conservative-gaussian-rounding/inputs/rounded.py", + "size": 4348, + "sha256": "f320d180bdcd65d28102eb34a26b3ab5287b39d8d00bb4734019060d174d47c9", + "git_blob": "8ae18373f2f5b0d33a7f0d1d6a591489f81401f1" + } + ] +} diff --git a/research/four-axis-phase-covariant-grid/CALLER.md b/research/four-axis-phase-covariant-grid/CALLER.md new file mode 100644 index 0000000000..1a21359612 --- /dev/null +++ b/research/four-axis-phase-covariant-grid/CALLER.md @@ -0,0 +1,104 @@ +# Four-axis retained-port binding + +This binds the phase-covariant four-axis result to two exact retained port +programs. No complete multiplication improvement is claimed. + +## Exact model and boundary + +Use the exact two-/three-call retained port bodies in +CrocSwap/integer-mult-bounds#6509, head +`a4173e810c4d34a1d13b9745af123ad0ec6cfed5`, package +`research/conservative-gaussian-rounding`, by Ali Romman. Its retained +`inputs/rounded.py` originates with JoyboyBrian's #5485, and the underlying +port algebra comes from #4743. Pin and credit these sources in the final +package. This claim is only for `f=4`, hence `N=4096`, and axes zero and two. + +The four active bits are `3*j+axis`, `0<=j<4`. Fixing all eight spectator +bits gives 256 disjoint fibers of length16. Apply the new block map F to +each fiber, or its literal inverse in a reverse call. Its ideal matrix on +that fiber is exactly the fourfold native Gaussian tensor, with entries +`-i^(4-popcount(r xor s))/4`. This coefficient formula is independently +used by the port oracle; the implemented factorization is `-D*(W/4)*D`. + +All retained monomials and triangular mixes are exact maps of the Gaussian +integer grid and have their displayed literal inverses. Therefore reversing +the port body with the true inverse block map restores both arbitrary dirty +banks exactly. Both composition orders are covered. No `F^2=J`, `F^4=I`, +additivity or commutation of independently rounded layers is required. + +## Coordinate precision and finite words + +The finite certificate verifies `|e_j|<=3` and `|f_j|<=5`, where +`f=-W e/4` is the inverse correction. Applying the real map independently +to real and imaginary components, with quarter phases, proves pointwise +complex-coordinate errors at most `3*sqrt(2)*h/4` forward and +`5*sqrt(2)*h/4` inverse. Both are strictly below `2*h`. These are universal +claims conditional on the finite table predicates, not extrapolations from +the port fixtures. In particular `g=q+1` suffices for a call tolerance +`2^-q`, replacing the predecessor's four-axis `g=q+3`. + +Retain the predecessor's source-ordered call requests: + +| Direction | q at f=4 | New g | Old g | +|---|---|---|---| +| Two calls forward | P+7 | P+8 | P+10 | +| Three calls forward | P+9 | P+10 | P+12 | +| Two calls reverse | P+4 | P+5 | P+7 | +| Three calls reverse | P+6 | P+7 | P+9 | + +The new call meets exactly the same actual-input premise used by those +budgets, so the complete port coordinate error is at most `2^-P`. +This leaves initial quantization charged separately, as in the predecessor. +It does not optimize the external requests q. An independent direct check +is possible: the native infinity norm is4 and the mixing matrix P+2Q has +infinity norm at most3. For a uniform completed-call error epsilon, the +two-/three-call forward error multipliers are13 and53, and the reverse +multipliers are1 and5. These constants also imply the displayed budgets. + +For source coordinate magnitude at most `2^H`, retain the source entry +bound `U=2^(H+12)` and signed width `w=H+g+19`. In a block call, each real +input component is bounded by `M=2^g U`. Every fast Walsh intermediate is +bounded by `16M`; the final corrected numerator is bounded by `16M+5`. +For H,g>=0 this is at most `2^(H+g+16)+5 < 2^(H+g+18)`, the positive +w-bit limit. Quarter phases and exact shifts are also safe. The retained +monomial/mix width argument is unchanged, as the actual-input error +premise still holds. Thus both fractional precision and signed word width +can be lowered by two relative to that retained request, with its large +headroom margin left intact. A different tape representation may have a +different bill; this is not a lower bound on all implementations. + +## Direct accounting + +One complex block executes two real 16-point fast Walsh transforms:128 +full-word sums/differences in total, followed by32 correction additions +and32 exact quarter shifts. The finite residue calculation uses only +three-bit residues, but is still payable, as are table access, phase/sign +operations, source reads, writes and word checks. A fixed 2048-entry scan +is an explicit bounded implementation of table access if constant-time +indexed lookup is not available; no physical tape speedup is inferred. +Each native call executes256 blocks, including all-zero blocks. A k-call +port executes `256k` blocks, `40960k` full-word block additions and +`8192k` exact quarter shifts, plus the unchanged retained monomial/mix +work. In particular the retained mixes cost4N real additions and2N left +shifts, and there are four/six monomial passes for two/three-call ports. + +The implementation can load32 words, perform the two transforms in place, +apply offsets and store the result, then clear all owned scratch. Tables +and quotient/control storage are finite constants. Such scratch work costs +O(w) per block, and source/index/control work is also paid. This proves a +finite direct reference interface only. No accelerated recursive tariff, +fixed multitape placement, compiler-stock estimate, outer admission or new +kappa is established. + +## Verification distinction + +The independent caller oracle uses native coefficients rather than the +Walsh factorization. Exact scaled integers represent all ideal intermediates; +the common scale64 suffices for three calls. It verifies both composition +orders, global Gaussian phase covariance, every actual paid input cut, +all spectator-fiber sums, exact operation totals and complete-port error. +Separate boundary fixtures use the new g and width. Negative controls cover +aliasing, unsupported f, overflow, forward replay substituted for an inverse, +and a wrong native axis that remains reversible but has the wrong operator. +These finite fixtures corroborate the algebraic interface proof. They do +not certify a complete multiplication supplier or graph consistency. diff --git a/research/four-axis-phase-covariant-grid/CERTIFICATE.json b/research/four-axis-phase-covariant-grid/CERTIFICATE.json new file mode 100644 index 0000000000..7456dbcf47 --- /dev/null +++ b/research/four-axis-phase-covariant-grid/CERTIFICATE.json @@ -0,0 +1 @@ +{"schema_version":1,"moduli":[8,4,4,4,4],"rows":[[[0,0,0,0,1],[0,0,0,0,0,0,0,0,-2,-2,2,-2,-2,-2,2,-2]],[[0,0,0,1,0],[0,0,0,0,-2,-2,-2,-2,0,0,0,0,2,2,-2,-2]],[[0,0,0,1,1],[0,0,0,0,2,-2,2,-2,-2,-2,2,2,0,0,0,0]],[[0,0,0,1,2],[0,0,0,0,-2,-2,-2,-2,0,0,0,0,2,2,-2,-2]],[[0,0,0,1,3],[0,0,0,0,2,-2,2,2,2,-2,2,2,0,0,0,0]],[[0,0,0,2,1],[0,0,0,0,0,0,0,0,-2,-2,2,-2,-2,-2,2,-2]],[[0,0,1,0,0],[0,0,-2,2,0,0,2,-2,0,0,-2,2,0,0,-2,2]],[[0,0,1,0,1],[0,0,2,-2,0,0,2,2,-2,-2,0,0,2,-2,0,0]],[[0,0,1,0,2],[0,0,2,-2,0,0,-2,-2,0,0,2,2,0,0,2,-2]],[[0,0,1,0,3],[0,0,2,-2,0,0,2,2,-2,-2,0,0,2,-2,0,0]],[[0,0,1,1,0],[0,0,2,-2,-2,2,0,0,0,0,-2,-2,2,2,0,0]],[[0,0,1,1,1],[0,0,-2,-2,2,-2,0,0,-2,2,0,0,0,0,-2,-2]],[[0,0,1,1,2],[0,0,2,-2,-2,2,0,0,0,0,-2,-2,2,2,0,0]],[[0,0,1,1,3],[0,0,-2,-2,2,-2,0,0,-2,2,0,0,0,0,-2,-2]],[[0,0,1,2,0],[0,0,-2,2,0,0,2,-2,0,0,-2,2,0,0,-2,2]],[[0,0,1,2,1],[0,0,2,-2,0,0,-2,-2,-2,2,0,0,2,2,0,0]],[[0,0,1,2,2],[0,0,-2,2,0,0,2,-2,0,0,-2,2,0,0,-2,2]],[[0,0,1,2,3],[0,0,2,-2,0,0,-2,2,2,2,0,0,2,2,0,0]],[[0,0,1,3,0],[0,0,2,-2,2,2,0,0,0,0,-2,2,2,2,0,0]],[[0,0,1,3,1],[0,0,-2,-2,2,-2,0,0,-2,2,0,0,0,0,-2,-2]],[[0,0,1,3,2],[0,0,2,-2,2,2,0,0,0,0,-2,2,2,2,0,0]],[[0,0,1,3,3],[0,0,-2,-2,2,-2,0,0,-2,2,0,0,0,0,-2,-2]],[[0,0,2,0,1],[0,0,0,0,0,0,0,0,-2,-2,-2,-2,2,2,-2,-2]],[[0,0,2,1,0],[0,0,0,0,-2,-2,-2,-2,0,0,0,0,2,-2,2,-2]],[[0,0,2,1,1],[0,0,0,0,-2,-2,2,2,2,-2,2,-2,0,0,0,0]],[[0,0,2,1,2],[0,0,0,0,-2,-2,-2,-2,0,0,0,0,2,-2,2,-2]],[[0,0,2,1,3],[0,0,0,0,-2,-2,2,-2,-2,-2,2,-2,0,0,0,0]],[[0,0,2,2,1],[0,0,0,0,0,0,0,0,2,2,-2,-2,2,2,2,2]],[[0,1,0,0,0],[0,-2,0,-2,0,2,0,-2,0,2,0,-2,0,2,0,2]],[[0,1,0,0,1],[0,-2,0,2,0,-2,0,-2,-2,0,2,0,-2,0,-2,0]],[[0,1,0,0,2],[0,-2,0,-2,0,2,0,-2,0,2,0,-2,0,2,0,2]],[[0,1,0,0,3],[0,-2,0,-2,0,2,0,2,2,0,-2,0,2,0,-2,0]],[[0,1,0,1,0],[0,-2,0,-2,-2,0,2,0,0,2,0,-2,-2,0,-2,0]],[[0,1,0,1,1],[0,2,0,2,-2,0,-2,0,-2,0,-2,0,0,-2,0,-2]],[[0,1,0,1,2],[0,-2,0,-2,2,0,2,0,0,-2,0,2,2,0,-2,0]],[[0,1,0,1,3],[0,2,0,2,-2,0,-2,0,-2,0,-2,0,0,-2,0,-2]],[[0,1,0,2,0],[0,-2,0,-2,0,-2,0,-2,0,2,0,2,0,-2,0,-2]],[[0,1,0,2,1],[0,-2,0,2,0,-2,0,-2,-2,0,2,0,-2,0,-2,0]],[[0,1,0,2,2],[0,-2,0,-2,0,-2,0,-2,0,2,0,2,0,-2,0,-2]],[[0,1,0,2,3],[0,-2,0,-2,0,2,0,2,2,0,-2,0,2,0,-2,0]],[[0,1,0,3,0],[0,-2,0,-2,-2,0,2,0,0,2,0,-2,-2,0,-2,0]],[[0,1,0,3,1],[0,2,0,2,-2,0,-2,0,-2,0,-2,0,0,-2,0,-2]],[[0,1,0,3,2],[0,-2,0,-2,-2,0,2,0,0,-2,0,-2,2,0,-2,0]],[[0,1,0,3,3],[0,2,0,2,-2,0,-2,0,-2,0,-2,0,0,-2,0,-2]],[[0,1,1,0,0],[0,-2,-2,0,0,2,-2,0,0,2,-2,0,0,-2,-2,0]],[[0,1,1,0,1],[0,-2,2,0,0,-2,-2,0,-2,0,0,-2,2,0,0,-2]],[[0,1,1,0,2],[0,-2,-2,0,0,2,-2,0,0,2,-2,0,0,-2,-2,0]],[[0,1,1,0,3],[0,-2,2,0,0,-2,-2,0,-2,0,0,-2,2,0,0,-2]],[[0,1,1,1,0],[0,-2,2,0,2,0,0,2,0,-2,-2,0,2,0,0,-2]],[[0,1,1,1,1],[0,2,-2,0,-2,0,0,-2,-2,0,0,-2,0,-2,2,0]],[[0,1,1,1,2],[0,-2,2,0,2,0,0,2,0,-2,-2,0,2,0,0,-2]],[[0,1,1,1,3],[0,-2,-2,0,2,0,0,2,2,0,0,-2,0,-2,2,0]],[[0,1,1,2,0],[0,-2,2,0,0,-2,2,0,0,-2,2,0,0,2,-2,0]],[[0,1,1,2,1],[0,-2,2,0,0,-2,-2,0,-2,0,0,-2,2,0,0,-2]],[[0,1,1,2,2],[0,-2,2,0,0,-2,2,0,0,-2,2,0,0,2,-2,0]],[[0,1,1,2,3],[0,-2,2,0,0,-2,-2,0,-2,0,0,-2,2,0,0,-2]],[[0,1,1,3,0],[0,-2,2,0,2,0,0,2,0,-2,-2,0,2,0,0,-2]],[[0,1,1,3,1],[0,-2,-2,0,2,0,0,-2,-2,0,0,-2,0,-2,2,0]],[[0,1,1,3,2],[0,2,2,0,-2,0,0,2,0,2,2,0,-2,0,0,2]],[[0,1,1,3,3],[0,-2,-2,0,2,0,0,2,2,0,0,-2,0,-2,2,0]],[[0,1,2,0,0],[0,-2,0,2,0,-2,0,2,0,2,0,-2,0,-2,0,2]],[[0,1,2,0,1],[0,2,0,2,0,-2,0,2,2,0,2,0,-2,0,2,0]],[[0,1,2,0,2],[0,-2,0,2,0,-2,0,2,0,2,0,-2,0,-2,0,2]],[[0,1,2,0,3],[0,2,0,-2,0,2,0,-2,-2,0,-2,0,2,0,2,0]],[[0,1,2,1,0],[0,-2,0,-2,-2,0,2,0,0,2,0,-2,-2,0,-2,0]],[[0,1,2,1,1],[0,2,0,-2,-2,0,-2,0,2,0,2,0,0,2,0,-2]],[[0,1,2,1,2],[0,-2,0,-2,2,0,2,0,0,-2,0,2,2,0,-2,0]],[[0,1,2,1,3],[0,2,0,-2,-2,0,-2,0,2,0,2,0,0,2,0,-2]],[[0,1,2,2,0],[0,-2,0,-2,0,2,0,-2,0,2,0,2,0,-2,0,2]],[[0,1,2,2,1],[0,2,0,2,0,-2,0,2,2,0,2,0,-2,0,2,0]],[[0,1,2,2,2],[0,-2,0,-2,0,2,0,-2,0,2,0,2,0,-2,0,2]],[[0,1,2,2,3],[0,2,0,-2,0,2,0,-2,-2,0,-2,0,2,0,2,0]],[[0,1,2,3,0],[0,-2,0,-2,-2,0,2,0,0,2,0,-2,-2,0,-2,0]],[[0,1,2,3,1],[0,-2,0,2,2,0,2,0,2,0,-2,0,0,2,0,2]],[[0,1,2,3,2],[0,-2,0,-2,-2,0,2,0,0,-2,0,-2,2,0,-2,0]],[[0,1,2,3,3],[0,-2,0,2,2,0,2,0,2,0,-2,0,0,2,0,2]],[[0,1,3,0,0],[0,2,2,0,0,-2,2,0,0,-2,2,0,0,2,2,0]],[[0,1,3,0,1],[0,-2,2,0,0,-2,-2,0,-2,0,0,-2,2,0,0,-2]],[[0,1,3,0,2],[0,2,2,0,0,-2,2,0,0,-2,2,0,0,2,2,0]],[[0,1,3,0,3],[0,-2,2,0,0,-2,-2,0,-2,0,0,-2,2,0,0,-2]],[[0,1,3,1,0],[0,-2,-2,0,2,0,0,-2,0,2,-2,0,2,0,0,2]],[[0,1,3,1,1],[0,2,2,0,2,0,0,-2,-2,0,0,2,0,2,2,0]],[[0,1,3,1,2],[0,-2,-2,0,2,0,0,-2,0,2,-2,0,2,0,0,2]],[[0,1,3,1,3],[0,-2,2,0,2,0,0,2,2,0,0,-2,0,2,2,0]],[[0,1,3,2,0],[0,2,-2,0,0,-2,2,0,0,-2,2,0,0,-2,2,0]],[[0,1,3,2,1],[0,-2,2,0,0,-2,-2,0,-2,0,0,-2,2,0,0,-2]],[[0,1,3,2,2],[0,2,-2,0,0,-2,2,0,0,-2,2,0,0,-2,2,0]],[[0,1,3,2,3],[0,-2,2,0,0,-2,-2,0,-2,0,0,-2,2,0,0,-2]],[[0,1,3,3,0],[0,-2,2,0,-2,0,0,-2,0,-2,2,0,2,0,0,2]],[[0,1,3,3,1],[0,-2,2,0,-2,0,0,-2,2,0,0,-2,0,2,2,0]],[[0,1,3,3,2],[0,-2,2,0,-2,0,0,-2,0,-2,2,0,2,0,0,2]],[[0,1,3,3,3],[0,-2,2,0,-2,0,0,-2,2,0,0,-2,0,2,2,0]],[[0,2,0,0,1],[0,0,0,0,0,0,0,0,2,-2,2,2,2,-2,2,2]],[[0,2,0,1,0],[0,0,0,0,-2,-2,2,-2,0,0,0,0,2,-2,2,2]],[[0,2,0,1,1],[0,0,0,0,2,-2,2,-2,-2,-2,2,2,0,0,0,0]],[[0,2,0,1,2],[0,0,0,0,-2,-2,2,-2,0,0,0,0,2,-2,2,2]],[[0,2,0,1,3],[0,0,0,0,2,-2,2,2,2,-2,2,2,0,0,0,0]],[[0,2,0,2,1],[0,0,0,0,0,0,0,0,2,-2,2,2,2,-2,2,2]],[[0,2,1,0,0],[0,0,-2,-2,0,0,2,-2,0,0,2,2,0,0,-2,2]],[[0,2,1,0,1],[0,0,-2,-2,0,0,2,-2,2,-2,0,0,2,2,0,0]],[[0,2,1,0,2],[0,0,2,-2,0,0,2,-2,0,0,2,2,0,0,2,2]],[[0,2,1,0,3],[0,0,-2,-2,0,0,2,-2,2,-2,0,0,2,2,0,0]],[[0,2,1,1,0],[0,0,-2,-2,2,2,0,0,0,0,-2,2,2,-2,0,0]],[[0,2,1,1,1],[0,0,-2,2,-2,-2,0,0,2,-2,0,0,0,0,-2,-2]],[[0,2,1,1,2],[0,0,-2,-2,2,2,0,0,0,0,-2,2,2,-2,0,0]],[[0,2,1,1,3],[0,0,-2,2,-2,-2,0,0,2,-2,0,0,0,0,-2,-2]],[[0,2,1,2,0],[0,0,-2,-2,0,0,2,-2,0,0,2,2,0,0,-2,2]],[[0,2,1,2,1],[0,0,-2,-2,0,0,2,-2,2,-2,0,0,2,2,0,0]],[[0,2,1,2,2],[0,0,2,-2,0,0,2,-2,0,0,2,2,0,0,2,2]],[[0,2,1,2,3],[0,0,-2,-2,0,0,2,-2,2,-2,0,0,2,2,0,0]],[[0,2,1,3,0],[0,0,-2,-2,-2,2,0,0,0,0,-2,-2,2,-2,0,0]],[[0,2,1,3,1],[0,0,-2,2,-2,-2,0,0,2,-2,0,0,0,0,-2,-2]],[[0,2,1,3,2],[0,0,-2,-2,-2,2,0,0,0,0,-2,-2,2,-2,0,0]],[[0,2,1,3,3],[0,0,2,-2,-2,2,0,0,-2,2,0,0,0,0,-2,2]],[[0,2,2,0,1],[0,0,0,0,0,0,0,0,-2,-2,2,-2,-2,-2,2,-2]],[[0,2,2,1,0],[0,0,0,0,-2,-2,2,-2,0,0,0,0,2,2,-2,2]],[[0,2,2,1,1],[0,0,0,0,-2,-2,2,2,2,-2,2,-2,0,0,0,0]],[[0,2,2,1,2],[0,0,0,0,-2,-2,2,-2,0,0,0,0,2,2,-2,2]],[[0,2,2,1,3],[0,0,0,0,-2,-2,2,-2,-2,-2,2,-2,0,0,0,0]],[[0,2,2,2,1],[0,0,0,0,0,0,0,0,-2,-2,2,-2,-2,-2,2,-2]],[[1,0,0,0,0],[1,1,1,-3,-3,1,-3,1,1,1,1,1,1,1,-3,-3]],[[1,0,0,0,1],[-3,1,1,1,-3,1,1,-3,-1,-1,-1,3,-1,-1,-1,3]],[[1,0,0,0,2],[1,1,-3,1,1,1,-3,1,1,1,-3,1,1,1,-3,-3]],[[1,0,0,0,3],[1,1,-3,1,1,1,1,-3,3,-1,-1,3,-1,-1,3,-1]],[[1,0,0,1,0],[-3,1,-3,1,-1,-1,-1,-1,1,1,1,-3,-1,-1,3,3]],[[1,0,0,1,1],[1,1,-3,1,3,-1,-1,3,-1,3,-1,-1,1,1,-3,1]],[[1,0,0,1,2],[-3,1,1,1,3,-1,-1,-1,-3,1,-3,1,-1,-1,3,-1]],[[1,0,0,1,3],[-3,1,1,1,-1,-1,-1,3,-1,-1,-1,-1,-3,-3,1,-3]],[[1,0,0,2,0],[1,1,1,-3,1,1,1,1,-3,1,-3,1,1,1,-3,-3]],[[1,0,0,2,1],[-3,1,1,1,-3,1,1,1,3,-1,-1,3,-1,-1,-1,3]],[[1,0,0,2,2],[1,1,-3,1,-3,-3,1,1,1,1,1,1,1,-3,-3,1]],[[1,0,0,2,3],[1,1,1,-3,1,1,-3,1,-1,-1,3,3,3,-1,-1,-1]],[[1,0,0,3,0],[-3,1,-3,1,-1,-1,-1,-1,-3,-3,1,-3,-1,-1,-1,-1]],[[1,0,0,3,1],[-3,1,1,1,-1,3,-1,3,3,-1,-1,-1,-3,1,1,1]],[[1,0,0,3,2],[1,-3,1,1,3,-1,3,-1,1,-3,1,1,-1,3,-1,-1]],[[1,0,0,3,3],[1,1,-3,1,-1,3,-1,-1,3,-1,-1,3,1,-3,1,1]],[[1,0,1,0,0],[-3,1,-1,-1,1,1,-1,-1,-3,1,-1,3,-3,-3,-1,-1]],[[1,0,1,0,1],[-3,-3,-1,-1,1,1,3,-1,-1,-1,-3,1,-1,-1,-3,1]],[[1,0,1,0,2],[1,1,3,-1,-3,1,3,-1,1,-3,-1,3,1,1,-1,-1]],[[1,0,1,0,3],[-3,1,-1,-1,-3,1,-1,-1,-1,3,-3,-3,-1,-1,1,1]],[[1,0,1,1,0],[1,1,3,3,3,-1,1,1,-3,1,-1,-1,-1,3,1,1]],[[1,0,1,1,1],[1,-3,-1,3,-1,-1,1,1,3,-1,1,-3,1,1,-1,3]],[[1,0,1,1,2],[1,1,3,-1,-1,-1,1,1,1,-3,-1,3,3,-1,1,-3]],[[1,0,1,1,3],[1,1,3,3,-1,3,1,1,-1,-1,-3,1,1,1,-1,3]],[[1,0,1,2,0],[-3,1,-1,-1,1,1,-1,-1,-3,1,-1,3,-3,-3,-1,-1]],[[1,0,1,2,1],[-3,-3,-1,-1,-3,1,-1,-1,3,-1,1,1,-1,-1,-3,1]],[[1,0,1,2,2],[1,-3,3,3,-3,1,-1,-1,1,-3,-1,-1,1,1,-1,-1]],[[1,0,1,2,3],[1,1,-1,3,1,-3,-1,-1,3,-1,1,1,-1,3,1,-3]],[[1,0,1,3,0],[1,-3,3,3,-1,-1,1,-3,-3,1,-1,-1,-1,-1,1,1]],[[1,0,1,3,1],[1,-3,3,-1,3,-1,1,1,3,-1,1,1,1,1,3,-1]],[[1,0,1,3,2],[1,1,3,3,-1,-1,1,1,1,-3,-1,3,3,-1,1,1]],[[1,0,1,3,3],[1,1,3,-1,-1,3,1,1,3,-1,1,1,1,1,3,3]],[[1,0,2,0,0],[1,1,1,1,-3,-3,1,1,1,1,1,1,1,1,-3,1]],[[1,0,2,0,1],[-3,-3,-3,-3,1,1,1,-3,-1,-1,-1,-1,-1,-1,-1,-1]],[[1,0,2,0,2],[1,1,1,1,-3,1,-3,1,1,1,1,1,-3,1,-3,-3]],[[1,0,2,0,3],[1,1,-3,1,1,1,1,1,3,-1,-1,-1,-1,3,-1,-1]],[[1,0,2,1,0],[-3,1,-3,1,-1,-1,-1,-1,1,1,-3,1,-1,-1,-1,-1]],[[1,0,2,1,1],[1,1,1,1,-1,-1,-1,3,-1,3,3,-1,-3,1,-3,1]],[[1,0,2,1,2],[-3,1,-3,1,-1,-1,-1,-1,1,1,1,-3,-1,3,-1,3]],[[1,0,2,1,3],[1,1,1,1,-1,3,3,-1,-1,-1,-1,3,-3,-3,1,1]],[[1,0,2,2,0],[1,1,1,1,1,1,-3,1,1,-3,1,1,1,1,1,-3]],[[1,0,2,2,1],[1,1,1,1,1,1,1,-3,3,-1,-1,3,-1,3,3,-1]],[[1,0,2,2,2],[1,1,1,1,1,1,1,1,-3,1,-3,1,-3,1,-3,-3]],[[1,0,2,2,3],[1,1,-3,1,1,1,1,-3,-1,-1,-1,-1,-1,3,-1,-1]],[[1,0,2,3,0],[-3,1,1,1,-1,-1,-1,-1,-3,-3,1,-3,-1,3,-1,-1]],[[1,0,2,3,1],[1,-3,1,1,-1,3,3,-1,3,-1,-1,-1,-3,1,1,1]],[[1,0,2,3,2],[1,1,1,1,-1,3,3,3,1,-3,-3,1,-1,-1,-1,-1]],[[1,0,2,3,3],[1,1,-3,1,-1,-1,3,-1,3,-1,-1,3,1,1,-3,1]],[[1,0,3,0,0],[-3,1,-1,3,1,1,-1,-1,-3,-3,-1,-1,1,1,-1,3]],[[1,0,3,0,1],[-3,1,-1,3,-3,-3,-1,-1,-1,-1,1,1,-1,-1,-3,1]],[[1,0,3,0,2],[-3,1,3,-1,1,1,-1,3,1,1,-1,3,-3,1,-1,-1]],[[1,0,3,0,3],[-3,1,-1,3,-3,-3,-1,-1,-1,-1,1,1,-1,-1,-3,1]],[[1,0,3,1,0],[1,1,3,3,-1,-1,-3,1,-3,1,-1,-1,-1,-1,1,-3]],[[1,0,3,1,1],[1,1,-1,3,-1,3,1,1,-1,-1,-3,1,1,-3,-1,3]],[[1,0,3,1,2],[1,-3,-1,-1,-1,-1,1,1,1,-3,3,-1,3,-1,-3,1]],[[1,0,3,1,3],[1,1,-1,3,3,-1,-3,1,-1,-1,1,1,1,1,-1,-1]],[[1,0,3,2,0],[-3,1,-1,3,-3,-3,-1,-1,1,1,-1,-1,1,1,-1,3]],[[1,0,3,2,1],[1,1,-1,3,-3,1,3,-1,3,-1,-3,1,-1,-1,1,1]],[[1,0,3,2,2],[1,1,-1,-1,1,-3,-1,3,-3,1,3,-1,1,-3,-1,-1]],[[1,0,3,2,3],[1,1,-1,3,-3,1,3,-1,3,-1,-3,1,-1,-1,1,1]],[[1,0,3,3,0],[1,1,-1,3,3,-1,-3,1,1,1,3,3,-1,-1,1,1]],[[1,0,3,3,1],[1,1,-1,3,-1,3,1,1,-1,-1,-3,1,1,-3,-1,3]],[[1,0,3,3,2],[1,1,-1,-1,3,3,1,1,1,-3,-1,3,3,-1,1,1]],[[1,0,3,3,3],[1,1,-1,-1,-1,3,1,1,3,3,-3,1,1,1,-1,3]],[[1,1,0,0,0],[1,-1,1,-1,1,-1,1,-1,-3,3,1,-1,1,-1,1,3]],[[1,1,0,0,1],[1,-1,1,3,-3,3,1,-1,-1,-3,-1,-3,-1,1,-1,1]],[[1,1,0,0,2],[1,3,-3,3,1,-1,1,-1,1,-1,1,-1,-3,3,1,-1]],[[1,1,0,0,3],[1,-1,1,3,-3,-1,1,-1,3,1,-1,1,-1,1,-1,1]],[[1,1,0,1,0],[1,3,1,3,-1,1,3,1,-3,-1,-3,-1,-1,1,-1,1]],[[1,1,0,1,1],[1,3,1,3,-1,1,-1,1,-1,-3,-1,1,1,3,-3,-1]],[[1,1,0,1,2],[1,3,1,3,-1,1,-1,1,-3,3,-3,-1,-1,1,-1,1]],[[1,1,0,1,3],[1,3,1,-1,-1,1,-1,1,3,-3,3,1,1,3,1,-1]],[[1,1,0,2,0],[-3,3,-3,-1,1,-1,1,-1,-3,-1,-3,-1,1,-1,1,-1]],[[1,1,0,2,1],[1,-1,1,-1,1,-1,1,3,-1,1,3,1,-1,-3,-1,1]],[[1,1,0,2,2],[1,-1,1,3,1,3,1,-1,1,-1,1,3,-3,-1,1,3]],[[1,1,0,2,3],[1,-1,1,3,1,3,1,-1,-1,-3,-1,1,-1,1,-1,1]],[[1,1,0,3,0],[1,-1,1,3,-1,-3,-1,-3,1,3,1,-1,-1,1,3,1]],[[1,1,0,3,1],[1,3,1,3,-1,1,-1,1,3,1,-1,1,1,3,1,3]],[[1,1,0,3,2],[1,3,-3,3,-1,-3,-1,1,1,-1,1,-1,3,1,-1,1]],[[1,1,0,3,3],[1,3,1,-1,3,1,3,1,-1,-3,-1,1,1,3,1,-1]],[[1,1,1,0,0],[1,-1,-1,1,-3,-1,3,-3,-3,-1,-1,-3,1,-1,-1,1]],[[1,1,1,0,1],[1,-1,3,1,1,-1,-1,1,3,1,-3,3,3,1,1,-1]],[[1,1,1,0,2],[1,-1,3,1,1,3,-1,1,1,-1,-1,1,1,-1,3,1]],[[1,1,1,0,3],[1,-1,3,1,-3,-1,-1,1,3,1,1,3,-1,-3,1,-1]],[[1,1,1,1,0],[1,3,-1,1,3,1,-3,-1,-3,3,-1,1,-1,1,1,-1]],[[1,1,1,1,1],[1,-1,3,1,-1,1,1,-1,-1,1,-3,-1,-3,-1,3,-3]],[[1,1,1,1,2],[1,3,-1,1,3,1,-3,3,1,3,-1,1,-1,1,1,-1]],[[1,1,1,1,3],[1,3,-1,1,3,1,-3,3,-1,1,1,-1,1,-1,3,1]],[[1,1,1,2,0],[1,3,-1,1,1,-1,-1,1,1,3,-1,1,-3,3,-1,-3]],[[1,1,1,2,1],[1,-1,-1,1,-3,3,-1,1,3,1,1,-1,-1,1,-3,3]],[[1,1,1,2,2],[1,-1,3,-3,1,-1,-1,1,1,3,-1,1,1,-1,3,-3]],[[1,1,1,2,3],[1,-1,3,1,-3,3,-1,1,-1,1,-3,-1,-1,1,-3,-1]],[[1,1,1,3,0],[1,3,-1,1,-1,1,1,-1,1,-1,-1,1,3,1,1,3]],[[1,1,1,3,1],[1,3,-1,1,-1,1,1,-1,3,1,-3,3,1,3,-1,1]],[[1,1,1,3,2],[1,-1,-1,1,-1,1,1,-1,-3,3,-1,1,-1,-3,-3,3]],[[1,1,1,3,3],[1,-1,-1,1,-1,1,1,-1,3,1,-3,3,-3,-1,-1,-3]],[[1,1,2,0,0],[1,-1,-3,3,1,3,1,-1,1,-1,-3,-1,1,-1,1,3]],[[1,1,2,0,1],[1,-1,-3,3,1,3,1,-1,-1,-3,-1,1,-1,-3,-1,1]],[[1,1,2,0,2],[-3,3,1,-1,1,-1,1,-1,-3,-1,1,3,-3,-1,1,-1]],[[1,1,2,0,3],[1,-1,-3,-1,1,3,1,-1,3,1,-1,1,-1,1,-1,1]],[[1,1,2,1,0],[1,-1,-3,-1,3,1,-1,-3,-3,-1,1,-1,-1,1,-1,-3]],[[1,1,2,1,1],[1,3,-3,3,-1,1,-1,1,3,1,-1,1,1,-1,1,3]],[[1,1,2,1,2],[1,3,1,3,-1,-3,3,1,-3,-1,1,-1,-1,1,-1,1]],[[1,1,2,1,3],[1,3,-3,3,-1,1,-1,-3,-1,1,-1,1,1,-1,1,3]],[[1,1,2,2,0],[-3,-1,1,-1,-3,-1,1,-1,1,-1,1,3,1,-1,-3,3]],[[1,1,2,2,1],[1,-1,-3,3,-3,-1,1,-1,3,1,-1,1,-1,-3,-1,1]],[[1,1,2,2,2],[1,3,1,-1,1,-1,-3,3,-3,3,1,-1,1,-1,1,-1]],[[1,1,2,2,3],[-3,3,1,-1,1,-1,1,-1,-1,1,-1,1,-1,1,3,1]],[[1,1,2,3,0],[1,3,-3,3,-1,1,-1,1,1,-1,1,3,-1,-3,-1,1]],[[1,1,2,3,1],[1,3,-3,-1,-1,1,-1,1,3,1,-1,1,1,3,-3,-1]],[[1,1,2,3,2],[1,3,-3,-1,-1,1,-1,1,1,3,1,-1,-1,-3,3,1]],[[1,1,2,3,3],[-3,-1,1,3,-1,-3,-1,1,-1,1,-1,1,1,-1,-3,3]],[[1,1,3,0,0],[1,-1,3,1,1,-1,-1,1,1,3,-1,1,1,3,-1,1]],[[1,1,3,0,1],[1,-1,3,1,-3,-1,3,-3,-1,1,1,-1,-1,1,1,3]],[[1,1,3,0,2],[1,-1,3,1,1,-1,3,1,1,-1,-1,1,1,3,-1,1]],[[1,1,3,0,3],[1,-1,-1,1,1,3,3,1,-1,1,-3,-1,-1,-3,1,3]],[[1,1,3,1,0],[1,3,-1,1,3,-3,1,3,1,-1,3,1,-1,1,1,-1]],[[1,1,3,1,1],[1,-1,3,1,-1,1,1,-1,-1,-3,1,-1,-3,3,-1,-3]],[[1,1,3,1,2],[1,3,-1,1,3,-3,1,3,1,-1,3,1,-1,1,1,-1]],[[1,1,3,1,3],[1,3,-1,1,3,-3,1,3,-1,1,1,-1,1,3,-1,1]],[[1,1,3,2,0],[1,-1,3,1,-3,-1,-1,1,1,3,3,1,-3,-1,-1,1]],[[1,1,3,2,1],[1,-1,3,1,-3,-1,3,-3,-1,1,1,-1,-1,1,1,3]],[[1,1,3,2,2],[1,-1,3,1,-3,-1,3,1,1,-1,3,1,-3,-1,-1,1]],[[1,1,3,2,3],[1,-1,3,1,1,3,3,1,-1,-3,1,-1,-1,1,1,3]],[[1,1,3,3,0],[1,3,-1,-3,-1,1,1,-1,1,-1,-1,1,3,1,1,-1]],[[1,1,3,3,1],[1,-1,3,1,-1,1,1,-1,3,1,1,-1,-3,3,3,1]],[[1,1,3,3,2],[1,3,-1,1,-1,-3,1,3,1,-1,3,-3,-1,1,1,-1]],[[1,1,3,3,3],[-3,3,-1,1,-1,1,-3,-1,-1,1,1,-1,-3,3,-1,1]],[[1,2,0,0,0],[1,1,1,1,-3,-3,-3,1,1,1,1,-3,1,1,1,-3]],[[1,2,0,0,1],[-3,1,-3,1,1,1,-3,1,-1,-1,-1,-1,-1,-1,-1,-1]],[[1,2,0,0,2],[1,-3,1,1,1,-3,1,1,1,-3,1,1,1,1,-3,-3]],[[1,2,0,0,3],[1,-3,1,1,1,1,1,-3,3,-1,-1,3,-1,-1,3,-1]],[[1,2,0,1,0],[1,1,1,1,3,3,-1,-1,1,-3,1,1,-1,3,3,-1]],[[1,2,0,1,1],[1,1,1,1,-1,3,-1,-1,3,-1,-1,3,-3,1,1,-3]],[[1,2,0,1,2],[1,1,1,1,-1,3,-1,-1,1,-3,1,-3,-1,3,3,-1]],[[1,2,0,1,3],[1,1,1,1,-1,-1,3,3,3,-1,-1,-1,-3,1,1,-3]],[[1,2,0,2,0],[1,1,1,1,1,1,-3,1,-3,1,1,1,-3,1,-3,-3]],[[1,2,0,2,1],[-3,1,-3,1,1,1,-3,1,-1,-1,-1,-1,-1,-1,-1,-1]],[[1,2,0,2,2],[1,1,1,1,1,-3,-3,1,1,1,1,1,1,1,1,-3]],[[1,2,0,2,3],[1,1,1,1,1,-3,-3,1,-1,3,3,3,-1,-1,-1,-1]],[[1,2,0,3,0],[1,1,1,1,-1,-1,3,-1,1,-3,1,-3,-1,3,3,-1]],[[1,2,0,3,1],[-3,-3,1,1,-1,-1,3,-1,-1,-1,-1,-1,-3,1,-3,1]],[[1,2,0,3,2],[1,1,1,1,-1,3,-1,-1,1,-3,1,-3,-1,3,3,-1]],[[1,2,0,3,3],[1,1,1,1,3,-1,3,-1,-1,-1,-1,3,-3,1,1,-3]],[[1,2,1,0,0],[1,1,-1,3,-3,1,-1,-1,1,-3,-1,-1,1,1,-1,-1]],[[1,2,1,0,1],[1,1,-1,3,1,1,3,3,3,-1,-3,1,-1,-1,1,1]],[[1,2,1,0,2],[1,1,-1,3,-3,1,-1,-1,1,-3,-1,-1,1,1,-1,-1]],[[1,2,1,0,3],[1,1,-1,-1,1,-3,-1,3,3,3,1,1,3,-1,1,1]],[[1,2,1,1,0],[1,1,3,3,-1,-1,-3,1,1,1,-1,3,-1,-1,1,-3]],[[1,2,1,1,1],[1,1,-1,3,3,-1,1,1,-1,-1,-3,1,1,1,-1,-1]],[[1,2,1,1,2],[1,1,3,-1,-1,-1,-3,1,1,1,-1,3,3,-1,1,-3]],[[1,2,1,1,3],[1,1,-1,-1,3,-1,1,1,3,-1,1,1,1,1,3,-1]],[[1,2,1,2,0],[-3,1,-1,3,-3,1,-1,-1,1,-3,-1,-1,1,1,-1,3]],[[1,2,1,2,1],[1,1,3,3,-3,1,-1,-1,-1,-1,-3,1,-1,-1,1,-3]],[[1,2,1,2,2],[-3,1,-1,3,-3,1,-1,-1,1,-3,-1,-1,1,1,-1,3]],[[1,2,1,2,3],[1,1,-1,-1,1,-3,-1,3,-1,-1,1,1,3,-1,-3,-3]],[[1,2,1,3,0],[1,1,-1,-1,3,-1,1,1,1,1,-1,3,3,-1,1,1]],[[1,2,1,3,1],[1,1,-1,3,-1,-1,-3,1,3,-1,1,1,1,1,-1,-1]],[[1,2,1,3,2],[1,1,-1,3,3,-1,1,1,1,1,-1,3,-1,-1,1,1]],[[1,2,1,3,3],[1,1,-1,3,-1,3,-3,1,-1,-1,1,1,1,-3,-1,3]],[[1,2,2,0,0],[1,1,-3,1,1,-3,-3,1,1,1,1,1,1,-3,1,-3]],[[1,2,2,0,1],[-3,1,-3,1,1,1,1,1,3,-1,-1,-1,-1,-1,3,3]],[[1,2,2,0,2],[1,1,1,-3,-3,1,1,1,1,1,-3,1,1,1,-3,-3]],[[1,2,2,0,3],[-3,1,1,1,-3,1,-3,1,3,-1,-1,-1,-1,-1,3,-1]],[[1,2,2,1,0],[-3,-3,1,1,-1,-1,-1,-1,1,1,1,-3,-1,-1,3,3]],[[1,2,2,1,1],[-3,-3,-3,1,-1,-1,-1,-1,3,-1,-1,-1,1,1,-3,1]],[[1,2,2,1,2],[1,1,1,-3,3,-1,-1,3,-3,1,1,1,3,-1,-1,-1]],[[1,2,2,1,3],[1,1,-3,1,3,-1,-1,-1,3,-1,-1,3,1,1,1,-3]],[[1,2,2,2,0],[1,1,1,1,-3,1,1,-3,-3,1,-3,1,1,-3,1,1]],[[1,2,2,2,1],[1,1,1,1,1,-3,-3,1,-1,3,-1,3,3,-1,-1,-1]],[[1,2,2,2,2],[1,1,1,1,-3,1,1,1,1,1,-3,1,1,-3,1,1]],[[1,2,2,2,3],[-3,1,1,1,1,1,-3,1,-1,-1,-1,-1,-1,3,-1,-1]],[[1,2,2,3,0],[-3,1,1,-3,-1,-1,3,-1,-3,-3,1,1,-1,-1,-1,-1]],[[1,2,2,3,1],[1,1,-3,1,-1,-1,-1,-1,3,-1,-1,-1,1,1,1,-3]],[[1,2,2,3,2],[1,1,1,-3,-1,-1,-1,3,-3,1,1,-3,3,-1,-1,-1]],[[1,2,2,3,3],[-3,-3,1,1,-1,-1,-1,-1,-1,3,-1,-1,-3,1,-3,1]],[[1,2,3,0,0],[1,1,3,-1,1,1,-1,3,1,1,3,-1,1,1,3,3]],[[1,2,3,0,1],[1,1,3,3,-3,1,-1,-1,3,-1,1,1,-1,3,1,1]],[[1,2,3,0,2],[1,1,3,-1,1,1,-1,3,1,1,3,-1,1,1,3,3]],[[1,2,3,0,3],[-3,-3,-1,-1,1,1,-1,-1,-1,-1,1,1,-1,-1,-3,1]],[[1,2,3,1,0],[1,1,3,3,3,-1,1,1,1,1,-1,3,-1,3,1,1]],[[1,2,3,1,1],[1,1,3,3,-1,3,-3,1,-1,-1,1,1,1,1,-1,3]],[[1,2,3,1,2],[1,1,3,-1,3,-1,1,1,1,1,-1,3,3,3,1,1]],[[1,2,3,1,3],[1,1,3,3,-1,3,-3,1,-1,-1,1,1,1,1,-1,3]],[[1,2,3,2,0],[1,1,3,-1,1,-3,-1,3,1,1,3,3,1,1,-1,-1]],[[1,2,3,2,1],[1,1,3,3,1,1,3,-1,-1,-1,-3,1,-1,3,1,1]],[[1,2,3,2,2],[1,1,3,-1,1,-3,-1,3,1,1,3,3,1,1,-1,-1]],[[1,2,3,2,3],[1,1,3,3,1,-3,-1,3,-1,-1,1,1,3,-1,1,1]],[[1,2,3,3,0],[1,1,-1,-1,-1,-1,1,1,1,1,-1,-1,-1,-1,1,-3]],[[1,2,3,3,1],[1,-3,-1,3,3,-1,1,1,-1,-1,1,-3,1,1,-1,3]],[[1,2,3,3,2],[1,1,3,3,-1,-1,1,1,1,1,-1,-1,-1,3,1,1]],[[1,2,3,3,3],[1,-3,-1,3,3,-1,1,1,-1,-1,1,-3,1,1,-1,3]],[[1,3,0,0,0],[1,3,1,-1,-3,-1,-3,3,1,3,1,-1,1,-1,1,-1]],[[1,3,0,0,1],[-3,3,1,-1,-3,-1,1,-1,3,1,-1,1,-1,1,3,1]],[[1,3,0,0,2],[-3,-1,1,-1,1,-1,1,-1,-3,-1,-3,-1,1,-1,1,-1]],[[1,3,0,0,3],[-3,-1,1,-1,1,3,-3,3,3,1,-1,1,-1,1,-1,1]],[[1,3,0,1,0],[1,-1,1,-1,3,1,-1,1,-3,-1,1,3,-1,-3,-1,-3]],[[1,3,0,1,1],[1,-1,1,-1,-1,1,-1,1,-1,1,-1,-3,1,-1,1,-1]],[[1,3,0,1,2],[1,-1,-3,3,-1,-3,-1,1,1,-1,1,-1,3,-3,-1,1]],[[1,3,0,1,3],[1,-1,-3,-1,-1,1,-1,1,3,1,3,-3,1,-1,1,3]],[[1,3,0,2,0],[1,3,1,-1,1,3,-3,3,-3,-1,1,-1,1,-1,1,-1]],[[1,3,0,2,1],[1,3,-3,-1,1,-1,1,3,-1,1,3,1,-1,-3,-1,1]],[[1,3,0,2,2],[1,3,1,-1,1,-1,-3,3,1,3,1,3,1,-1,1,-1]],[[1,3,0,2,3],[-3,-1,1,-1,1,-1,1,3,-1,-3,-1,1,-1,-3,-1,-3]],[[1,3,0,3,0],[1,3,1,-1,-1,1,-1,1,1,3,-3,3,3,1,-1,1]],[[1,3,0,3,1],[1,-1,-3,-1,3,1,-1,1,3,1,3,1,1,-1,1,3]],[[1,3,0,3,2],[1,-1,1,-1,-1,1,-1,1,1,3,-3,3,-1,-3,-1,-3]],[[1,3,0,3,3],[1,3,-3,-1,-1,1,3,1,-1,1,-1,1,1,-1,-3,3]],[[1,3,1,0,0],[1,3,-1,1,-3,-1,3,1,1,-1,3,1,-3,-1,-1,1]],[[1,3,1,0,1],[1,3,-1,1,-3,-1,3,-3,-1,1,1,-1,-1,1,1,3]],[[1,3,1,0,2],[-3,-1,-1,1,1,-1,-1,-3,1,-1,-1,1,-3,-1,3,-3]],[[1,3,1,0,3],[1,3,-1,1,1,-1,3,1,3,1,1,3,-1,1,1,3]],[[1,3,1,1,0],[1,3,-1,1,-1,1,1,-1,-3,3,-1,1,-1,-3,1,3]],[[1,3,1,1,1],[1,3,-1,-3,3,1,1,3,-1,1,1,3,1,-1,-1,1]],[[1,3,1,1,2],[1,3,3,1,-1,1,1,3,1,-1,3,1,-1,1,1,3]],[[1,3,1,1,3],[-3,-1,-1,1,-1,1,1,3,3,1,-3,-1,-3,-1,-1,1]],[[1,3,1,2,0],[1,3,-1,1,1,-1,3,-3,-3,-1,-1,1,1,3,-1,1]],[[1,3,1,2,1],[1,3,-1,1,1,-1,-1,1,-1,1,1,3,-1,-3,1,-1]],[[1,3,1,2,2],[-3,-1,-1,-3,1,-1,-1,1,1,3,-1,1,1,-1,-1,1]],[[1,3,1,2,3],[1,3,-1,1,1,3,3,1,-1,-3,1,-1,-1,1,1,3]],[[1,3,1,3,0],[1,-1,-1,1,-1,1,-3,-1,-3,3,-1,-3,-1,-3,1,-1]],[[1,3,1,3,1],[-3,3,-1,1,-1,1,-3,-1,-1,1,-3,3,1,-1,-1,1]],[[1,3,1,3,2],[1,3,-1,1,-1,-3,1,-1,1,-1,3,1,-1,1,1,-1]],[[1,3,1,3,3],[-3,3,-1,1,-1,1,1,-1,-1,-3,-3,3,1,-1,-1,1]],[[1,3,2,0,0],[1,3,1,-1,1,-1,1,3,1,3,1,-1,1,3,1,3]],[[1,3,2,0,1],[1,-1,1,3,-3,3,1,-1,3,-3,-1,1,-1,1,-1,1]],[[1,3,2,0,2],[1,3,1,-1,1,-1,1,3,1,3,1,-1,1,3,1,3]],[[1,3,2,0,3],[1,3,-3,3,-3,-1,1,-1,3,1,-1,1,-1,1,-1,1]],[[1,3,2,1,0],[1,-1,1,3,-1,1,3,1,-3,-1,-3,-1,-1,-3,-1,1]],[[1,3,2,1,1],[1,3,1,-1,-1,1,3,1,-1,1,-1,1,1,3,-3,3]],[[1,3,2,1,2],[1,-1,1,3,-1,1,-1,1,1,-1,1,3,-1,-3,-1,1]],[[1,3,2,1,3],[-3,-1,-3,-1,-1,1,-1,-3,3,-3,-1,1,1,-1,1,-1]],[[1,3,2,2,0],[-3,-1,1,-1,1,-1,1,-1,1,-1,1,-1,1,3,1,3]],[[1,3,2,2,1],[1,3,1,-1,-3,-1,1,3,-1,1,3,-3,-1,1,-1,1]],[[1,3,2,2,2],[-3,-1,1,-1,1,-1,1,-1,1,-1,1,-1,1,3,1,3]],[[1,3,2,2,3],[1,3,-3,3,1,3,1,-1,-1,-3,-1,1,-1,1,-1,1]],[[1,3,2,3,0],[1,-1,1,3,-1,1,3,1,-3,-1,-3,-1,-1,-3,-1,1]],[[1,3,2,3,1],[1,-1,1,3,-1,-3,-1,1,3,1,3,1,1,-1,1,3]],[[1,3,2,3,2],[1,3,1,-1,-1,1,3,1,1,-1,-3,3,3,1,-1,1]],[[1,3,2,3,3],[1,-1,1,3,-1,1,-1,1,-1,1,3,1,-3,-1,-3,3]],[[1,3,3,0,0],[1,3,-1,1,-3,3,-1,1,1,3,-1,1,-3,-1,-1,1]],[[1,3,3,0,1],[1,3,-1,1,1,-1,-1,1,3,1,-3,3,3,1,1,-1]],[[1,3,3,0,2],[1,3,-1,1,-3,-1,-1,1,1,3,3,1,-3,-1,-1,1]],[[1,3,3,0,3],[1,3,-1,1,1,3,-1,1,-1,1,1,-1,-1,1,1,3]],[[1,3,3,1,0],[1,-1,-1,1,-1,1,-3,-1,1,3,3,-3,-1,1,1,3]],[[1,3,3,1,1],[1,-1,-1,1,3,-3,1,3,-1,1,1,-1,1,-1,-1,1]],[[1,3,3,1,2],[1,3,-1,1,3,1,1,-1,-3,-1,-1,1,3,1,1,3]],[[1,3,3,1,3],[-3,-1,-1,1,-1,-3,1,-1,3,-3,1,-1,1,3,-1,1]],[[1,3,3,2,0],[1,3,-1,1,1,3,-1,-3,-3,-1,-1,1,1,-1,3,1]],[[1,3,3,2,1],[1,3,-1,1,1,-1,-1,1,3,1,-3,3,3,1,1,-1]],[[1,3,3,2,2],[1,3,-1,1,1,3,-1,1,-3,-1,3,1,-3,-1,-1,1]],[[1,3,3,2,3],[1,3,-1,1,1,-1,-1,1,-1,1,1,3,-1,1,-3,-1]],[[1,3,3,3,0],[1,3,-1,1,-1,1,1,-1,-3,3,-1,1,-1,1,-3,3]],[[1,3,3,3,1],[-3,3,-1,1,-1,-3,1,-1,-1,-3,1,3,1,-1,-1,1]],[[1,3,3,3,2],[1,3,-1,1,-1,1,1,3,1,3,-1,1,-1,1,-3,3]],[[1,3,3,3,3],[1,-1,-1,1,-1,1,1,-1,3,1,-3,3,1,-1,-1,1]],[[2,0,0,0,0],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,0,0,0,1],[-2,2,-2,-2,2,2,-2,2,0,0,0,0,0,0,0,0]],[[2,0,0,0,2],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,0,0,0,3],[-2,2,2,2,-2,-2,-2,2,0,0,0,0,0,0,0,0]],[[2,0,0,1,0],[2,-2,-2,2,0,0,0,0,2,2,-2,-2,0,0,0,0]],[[2,0,0,1,1],[2,2,-2,2,0,0,0,0,0,0,0,0,-2,-2,2,-2]],[[2,0,0,1,2],[2,-2,-2,2,0,0,0,0,2,2,-2,-2,0,0,0,0]],[[2,0,0,1,3],[-2,2,2,-2,0,0,0,0,0,0,0,0,2,2,2,2]],[[2,0,0,2,0],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,0,0,2,1],[-2,2,-2,-2,2,2,-2,2,0,0,0,0,0,0,0,0]],[[2,0,0,2,2],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,0,0,2,3],[-2,-2,2,2,2,-2,-2,2,0,0,0,0,0,0,0,0]],[[2,0,0,3,0],[-2,-2,-2,-2,0,0,0,0,2,2,-2,-2,0,0,0,0]],[[2,0,0,3,1],[2,2,-2,2,0,0,0,0,0,0,0,0,-2,-2,2,-2]],[[2,0,0,3,2],[-2,-2,-2,-2,0,0,0,0,2,2,-2,-2,0,0,0,0]],[[2,0,0,3,3],[-2,2,2,-2,0,0,0,0,0,0,0,0,2,2,2,2]],[[2,0,1,0,0],[-2,-2,0,0,2,2,0,0,-2,-2,0,0,-2,-2,0,0]],[[2,0,1,0,1],[-2,2,0,0,-2,-2,0,0,0,0,-2,-2,0,0,2,-2]],[[2,0,1,0,2],[-2,-2,0,0,2,2,0,0,-2,-2,0,0,-2,-2,0,0]],[[2,0,1,0,3],[2,-2,0,0,2,-2,0,0,0,0,2,2,0,0,-2,-2]],[[2,0,1,1,0],[-2,-2,0,0,0,0,-2,2,2,2,0,0,0,0,-2,2]],[[2,0,1,1,1],[2,-2,0,0,0,0,-2,-2,0,0,2,2,2,-2,0,0]],[[2,0,1,1,2],[2,2,0,0,0,0,2,2,-2,2,0,0,0,0,-2,2]],[[2,0,1,1,3],[-2,-2,0,0,0,0,-2,-2,0,0,2,-2,-2,2,0,0]],[[2,0,1,2,0],[-2,2,0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0]],[[2,0,1,2,1],[-2,-2,0,0,2,2,0,0,0,0,-2,2,0,0,-2,2]],[[2,0,1,2,2],[-2,2,0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0]],[[2,0,1,2,3],[-2,-2,0,0,-2,2,0,0,0,0,-2,-2,0,0,-2,2]],[[2,0,1,3,0],[2,2,0,0,0,0,2,-2,-2,-2,0,0,0,0,2,-2]],[[2,0,1,3,1],[2,-2,0,0,0,0,-2,-2,0,0,2,2,2,-2,0,0]],[[2,0,1,3,2],[-2,-2,0,0,0,0,-2,-2,-2,2,0,0,0,0,-2,2]],[[2,0,1,3,3],[2,-2,0,0,0,0,-2,-2,0,0,2,2,2,-2,0,0]],[[2,0,2,0,0],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,0,2,0,1],[-2,2,-2,-2,2,2,-2,2,0,0,0,0,0,0,0,0]],[[2,0,2,0,2],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,0,2,0,3],[-2,2,-2,-2,2,2,-2,2,0,0,0,0,0,0,0,0]],[[2,0,2,1,0],[-2,-2,-2,-2,0,0,0,0,2,-2,2,-2,0,0,0,0]],[[2,0,2,1,1],[-2,2,-2,-2,0,0,0,0,0,0,0,0,2,-2,2,2]],[[2,0,2,1,2],[-2,-2,-2,-2,0,0,0,0,2,-2,2,-2,0,0,0,0]],[[2,0,2,1,3],[2,-2,-2,2,0,0,0,0,0,0,0,0,-2,-2,-2,-2]],[[2,0,2,2,0],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,0,2,2,1],[-2,2,-2,-2,2,2,-2,2,0,0,0,0,0,0,0,0]],[[2,0,2,2,2],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,0,2,2,3],[-2,-2,2,2,2,-2,-2,2,0,0,0,0,0,0,0,0]],[[2,0,2,3,0],[-2,-2,-2,-2,0,0,0,0,2,-2,2,-2,0,0,0,0]],[[2,0,2,3,1],[-2,-2,2,-2,0,0,0,0,0,0,0,0,2,2,-2,2]],[[2,0,2,3,2],[-2,-2,-2,-2,0,0,0,0,2,-2,2,-2,0,0,0,0]],[[2,0,2,3,3],[2,2,2,2,0,0,0,0,0,0,0,0,-2,2,2,-2]],[[2,0,3,0,0],[-2,2,0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0]],[[2,0,3,0,1],[2,-2,0,0,-2,-2,0,0,0,0,2,-2,0,0,-2,-2]],[[2,0,3,0,2],[-2,2,0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0]],[[2,0,3,0,3],[2,-2,0,0,2,-2,0,0,0,0,2,2,0,0,-2,-2]],[[2,0,3,1,0],[2,2,0,0,0,0,2,2,2,-2,0,0,0,0,2,-2]],[[2,0,3,1,1],[2,-2,0,0,0,0,-2,2,0,0,2,-2,2,-2,0,0]],[[2,0,3,1,2],[-2,2,0,0,0,0,-2,2,-2,-2,0,0,0,0,-2,-2]],[[2,0,3,1,3],[-2,2,0,0,0,0,-2,2,0,0,-2,2,2,-2,0,0]],[[2,0,3,2,0],[-2,2,0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0]],[[2,0,3,2,1],[2,-2,0,0,2,-2,0,0,0,0,2,2,0,0,-2,-2]],[[2,0,3,2,2],[-2,2,0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0]],[[2,0,3,2,3],[2,-2,0,0,-2,-2,0,0,0,0,2,-2,0,0,-2,-2]],[[2,0,3,3,0],[2,2,0,0,0,0,2,-2,-2,-2,0,0,0,0,2,-2]],[[2,0,3,3,1],[2,-2,0,0,0,0,2,-2,0,0,-2,2,2,-2,0,0]],[[2,0,3,3,2],[-2,2,0,0,0,0,-2,-2,-2,2,0,0,0,0,2,2]],[[2,0,3,3,3],[2,-2,0,0,0,0,-2,2,0,0,2,-2,2,-2,0,0]],[[2,1,0,0,0],[-2,0,-2,0,2,0,-2,0,2,0,-2,0,2,0,2,0]],[[2,1,0,0,1],[-2,0,2,0,-2,0,2,0,0,-2,0,-2,0,2,0,2]],[[2,1,0,0,2],[-2,0,-2,0,2,0,-2,0,2,0,-2,0,2,0,2,0]],[[2,1,0,0,3],[-2,0,2,0,-2,0,2,0,0,-2,0,-2,0,2,0,2]],[[2,1,0,1,0],[-2,0,-2,0,0,-2,0,-2,2,0,-2,0,0,2,0,-2]],[[2,1,0,1,1],[2,0,2,0,0,2,0,2,0,2,0,-2,-2,0,2,0]],[[2,1,0,1,2],[-2,0,2,0,0,-2,0,-2,-2,0,2,0,0,2,0,2]],[[2,1,0,1,3],[2,0,2,0,0,2,0,2,0,2,0,-2,-2,0,2,0]],[[2,1,0,2,0],[-2,0,-2,0,2,0,2,0,-2,0,-2,0,-2,0,-2,0]],[[2,1,0,2,1],[-2,0,2,0,2,0,-2,0,0,2,0,2,0,2,0,2]],[[2,1,0,2,2],[-2,0,-2,0,2,0,2,0,-2,0,-2,0,-2,0,-2,0]],[[2,1,0,2,3],[-2,0,2,0,2,0,-2,0,0,2,0,2,0,2,0,2]],[[2,1,0,3,0],[2,0,-2,0,0,2,0,2,2,0,-2,0,0,-2,0,-2]],[[2,1,0,3,1],[2,0,2,0,0,2,0,2,0,2,0,-2,-2,0,2,0]],[[2,1,0,3,2],[2,0,-2,0,0,2,0,-2,-2,0,-2,0,0,-2,0,-2]],[[2,1,0,3,3],[2,0,2,0,0,2,0,2,0,2,0,-2,-2,0,2,0]],[[2,1,1,0,0],[-2,0,0,-2,-2,0,0,-2,2,0,0,2,-2,0,0,-2]],[[2,1,1,0,1],[2,0,0,2,2,0,0,-2,0,-2,2,0,0,2,2,0]],[[2,1,1,0,2],[-2,0,0,-2,-2,0,0,-2,2,0,0,2,-2,0,0,-2]],[[2,1,1,0,3],[-2,0,0,-2,-2,0,0,-2,0,2,-2,0,0,-2,2,0]],[[2,1,1,1,0],[-2,0,0,-2,0,2,-2,0,2,0,0,-2,0,2,2,0]],[[2,1,1,1,1],[-2,0,0,-2,0,2,2,0,0,-2,2,0,-2,0,0,2]],[[2,1,1,1,2],[2,0,0,-2,0,2,2,0,-2,0,0,2,0,-2,-2,0]],[[2,1,1,1,3],[-2,0,0,-2,0,2,2,0,0,2,-2,0,-2,0,0,2]],[[2,1,1,2,0],[-2,0,0,-2,-2,0,0,-2,2,0,0,2,-2,0,0,-2]],[[2,1,1,2,1],[-2,0,0,-2,-2,0,0,2,0,-2,2,0,0,-2,-2,0]],[[2,1,1,2,2],[-2,0,0,-2,-2,0,0,-2,2,0,0,2,-2,0,0,-2]],[[2,1,1,2,3],[-2,0,0,-2,-2,0,0,2,0,-2,2,0,0,-2,-2,0]],[[2,1,1,3,0],[-2,0,0,-2,0,-2,2,0,-2,0,0,-2,0,2,-2,0]],[[2,1,1,3,1],[-2,0,0,2,0,-2,2,0,0,-2,-2,0,-2,0,0,-2]],[[2,1,1,3,2],[2,0,0,2,0,-2,2,0,2,0,0,2,0,2,-2,0]],[[2,1,1,3,3],[-2,0,0,2,0,-2,-2,0,0,2,-2,0,-2,0,0,-2]],[[2,1,2,0,0],[-2,0,-2,0,2,0,2,0,-2,0,-2,0,-2,0,-2,0]],[[2,1,2,0,1],[2,0,2,0,-2,0,2,0,0,-2,0,2,0,-2,0,-2]],[[2,1,2,0,2],[-2,0,-2,0,2,0,2,0,-2,0,-2,0,-2,0,-2,0]],[[2,1,2,0,3],[2,0,2,0,-2,0,2,0,0,-2,0,2,0,-2,0,-2]],[[2,1,2,1,0],[-2,0,2,0,0,-2,0,-2,-2,0,2,0,0,2,0,2]],[[2,1,2,1,1],[2,0,2,0,0,2,0,2,0,2,0,-2,-2,0,2,0]],[[2,1,2,1,2],[-2,0,-2,0,0,-2,0,-2,2,0,-2,0,0,2,0,-2]],[[2,1,2,1,3],[2,0,2,0,0,2,0,2,0,2,0,-2,-2,0,2,0]],[[2,1,2,2,0],[-2,0,-2,0,2,0,-2,0,2,0,-2,0,2,0,2,0]],[[2,1,2,2,1],[-2,0,2,0,-2,0,-2,0,0,-2,0,2,0,-2,0,-2]],[[2,1,2,2,2],[-2,0,2,0,-2,0,-2,0,-2,0,-2,0,2,0,-2,0]],[[2,1,2,2,3],[-2,0,2,0,-2,0,-2,0,0,-2,0,2,0,-2,0,-2]],[[2,1,2,3,0],[2,0,2,0,0,2,0,-2,-2,0,-2,0,0,2,0,-2]],[[2,1,2,3,1],[-2,0,2,0,0,-2,0,-2,0,-2,0,2,2,0,2,0]],[[2,1,2,3,2],[2,0,-2,0,0,2,0,-2,2,0,2,0,0,2,0,2]],[[2,1,2,3,3],[-2,0,2,0,0,-2,0,-2,0,-2,0,2,2,0,2,0]],[[2,1,3,0,0],[-2,0,0,-2,-2,0,0,2,2,0,0,-2,-2,0,0,-2]],[[2,1,3,0,1],[-2,0,0,-2,-2,0,0,-2,0,-2,2,0,0,2,-2,0]],[[2,1,3,0,2],[-2,0,0,-2,2,0,0,-2,-2,0,0,2,-2,0,0,-2]],[[2,1,3,0,3],[-2,0,0,-2,-2,0,0,-2,0,-2,2,0,0,2,-2,0]],[[2,1,3,1,0],[-2,0,0,-2,0,-2,2,0,-2,0,0,-2,0,-2,2,0]],[[2,1,3,1,1],[-2,0,0,-2,0,2,2,0,0,2,-2,0,-2,0,0,2]],[[2,1,3,1,2],[-2,0,0,-2,0,-2,2,0,-2,0,0,-2,0,-2,2,0]],[[2,1,3,1,3],[-2,0,0,2,0,-2,-2,0,0,2,-2,0,-2,0,0,-2]],[[2,1,3,2,0],[-2,0,0,2,2,0,0,-2,-2,0,0,2,-2,0,0,2]],[[2,1,3,2,1],[-2,0,0,-2,-2,0,0,-2,0,2,-2,0,0,-2,2,0]],[[2,1,3,2,2],[-2,0,0,2,2,0,0,2,2,0,0,2,-2,0,0,2]],[[2,1,3,2,3],[-2,0,0,-2,2,0,0,2,0,-2,2,0,0,-2,2,0]],[[2,1,3,3,0],[-2,0,0,-2,0,-2,2,0,-2,0,0,-2,0,-2,2,0]],[[2,1,3,3,1],[-2,0,0,-2,0,-2,2,0,0,2,2,0,-2,0,0,2]],[[2,1,3,3,2],[2,0,0,2,0,2,-2,0,2,0,0,2,0,-2,2,0]],[[2,1,3,3,3],[-2,0,0,-2,0,-2,2,0,0,-2,-2,0,2,0,0,-2]],[[2,2,0,0,0],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,2,0,0,1],[-2,-2,2,2,-2,-2,-2,-2,0,0,0,0,0,0,0,0]],[[2,2,0,0,2],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,2,0,0,3],[-2,-2,2,2,-2,-2,-2,-2,0,0,0,0,0,0,0,0]],[[2,2,0,1,0],[-2,-2,2,-2,0,0,0,0,2,-2,2,2,0,0,0,0]],[[2,2,0,1,1],[-2,2,-2,-2,0,0,0,0,0,0,0,0,2,-2,2,2]],[[2,2,0,1,2],[-2,-2,2,-2,0,0,0,0,2,-2,2,2,0,0,0,0]],[[2,2,0,1,3],[-2,2,-2,-2,0,0,0,0,0,0,0,0,2,-2,2,2]],[[2,2,0,2,0],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,2,0,2,1],[-2,-2,2,-2,2,2,-2,2,0,0,0,0,0,0,0,0]],[[2,2,0,2,2],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,2,0,2,3],[-2,-2,2,-2,2,2,-2,2,0,0,0,0,0,0,0,0]],[[2,2,0,3,0],[-2,-2,2,-2,0,0,0,0,2,2,-2,2,0,0,0,0]],[[2,2,0,3,1],[2,2,2,2,0,0,0,0,0,0,0,0,-2,2,2,-2]],[[2,2,0,3,2],[-2,-2,2,-2,0,0,0,0,2,2,-2,2,0,0,0,0]],[[2,2,0,3,3],[2,2,2,2,0,0,0,0,0,0,0,0,-2,2,2,-2]],[[2,2,1,0,0],[-2,2,0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0]],[[2,2,1,0,1],[-2,-2,0,0,2,-2,0,0,0,0,-2,2,0,0,-2,-2]],[[2,2,1,0,2],[-2,2,0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0]],[[2,2,1,0,3],[2,-2,0,0,-2,-2,0,0,0,0,2,-2,0,0,-2,-2]],[[2,2,1,1,0],[-2,-2,0,0,0,0,-2,-2,-2,2,0,0,0,0,-2,2]],[[2,2,1,1,1],[2,2,0,0,0,0,-2,-2,0,0,2,2,2,2,0,0]],[[2,2,1,1,2],[2,2,0,0,0,0,2,2,-2,2,0,0,0,0,-2,2]],[[2,2,1,1,3],[2,2,0,0,0,0,-2,-2,0,0,2,2,2,2,0,0]],[[2,2,1,2,0],[-2,-2,0,0,2,-2,0,0,2,-2,0,0,2,2,0,0]],[[2,2,1,2,1],[-2,-2,0,0,2,2,0,0,0,0,-2,2,0,0,-2,2]],[[2,2,1,2,2],[-2,-2,0,0,2,-2,0,0,2,-2,0,0,2,2,0,0]],[[2,2,1,2,3],[-2,-2,0,0,2,2,0,0,0,0,-2,2,0,0,-2,2]],[[2,2,1,3,0],[-2,-2,0,0,0,0,-2,-2,2,-2,0,0,0,0,2,-2]],[[2,2,1,3,1],[-2,2,0,0,0,0,2,-2,0,0,-2,2,-2,2,0,0]],[[2,2,1,3,2],[2,2,0,0,0,0,2,-2,-2,-2,0,0,0,0,2,-2]],[[2,2,1,3,3],[2,-2,0,0,0,0,2,-2,0,0,2,-2,-2,2,0,0]],[[2,2,2,0,0],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,2,2,0,1],[-2,-2,2,2,2,-2,-2,2,0,0,0,0,0,0,0,0]],[[2,2,2,0,2],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,2,2,0,3],[-2,-2,2,2,2,-2,-2,2,0,0,0,0,0,0,0,0]],[[2,2,2,1,0],[-2,2,-2,-2,0,0,0,0,2,-2,2,2,0,0,0,0]],[[2,2,2,1,1],[-2,2,-2,-2,0,0,0,0,0,0,0,0,2,2,-2,2]],[[2,2,2,1,2],[-2,2,-2,-2,0,0,0,0,2,-2,2,2,0,0,0,0]],[[2,2,2,1,3],[-2,2,-2,-2,0,0,0,0,0,0,0,0,2,2,-2,2]],[[2,2,2,2,0],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,2,2,2,1],[-2,-2,2,2,2,-2,-2,2,0,0,0,0,0,0,0,0]],[[2,2,2,2,2],[-2,-2,-2,-2,-2,2,2,-2,2,-2,2,-2,-2,-2,2,2]],[[2,2,2,2,3],[-2,-2,2,2,2,-2,-2,2,0,0,0,0,0,0,0,0]],[[2,2,2,3,0],[-2,-2,2,2,0,0,0,0,-2,-2,-2,-2,0,0,0,0]],[[2,2,2,3,1],[-2,2,-2,-2,0,0,0,0,0,0,0,0,2,-2,2,2]],[[2,2,2,3,2],[-2,-2,2,2,0,0,0,0,-2,-2,-2,-2,0,0,0,0]],[[2,2,2,3,3],[-2,2,-2,-2,0,0,0,0,0,0,0,0,2,-2,2,2]],[[2,2,3,0,0],[-2,-2,0,0,2,-2,0,0,2,-2,0,0,2,2,0,0]],[[2,2,3,0,1],[2,2,0,0,-2,2,0,0,0,0,2,-2,0,0,2,2]],[[2,2,3,0,2],[-2,-2,0,0,2,-2,0,0,2,-2,0,0,2,2,0,0]],[[2,2,3,0,3],[2,-2,0,0,-2,-2,0,0,0,0,2,-2,0,0,-2,-2]],[[2,2,3,1,0],[2,2,0,0,0,0,2,-2,-2,-2,0,0,0,0,2,-2]],[[2,2,3,1,1],[2,2,0,0,0,0,-2,-2,0,0,2,2,2,2,0,0]],[[2,2,3,1,2],[2,2,0,0,0,0,2,-2,-2,-2,0,0,0,0,2,-2]],[[2,2,3,1,3],[2,2,0,0,0,0,-2,-2,0,0,2,2,2,2,0,0]],[[2,2,3,2,0],[2,-2,0,0,2,2,0,0,-2,2,0,0,-2,-2,0,0]],[[2,2,3,2,1],[2,-2,0,0,2,-2,0,0,0,0,2,2,0,0,-2,-2]],[[2,2,3,2,2],[2,2,0,0,-2,2,0,0,-2,2,0,0,-2,-2,0,0]],[[2,2,3,2,3],[2,2,0,0,-2,2,0,0,0,0,2,-2,0,0,2,2]],[[2,2,3,3,0],[2,2,0,0,0,0,2,-2,-2,-2,0,0,0,0,2,-2]],[[2,2,3,3,1],[2,2,0,0,0,0,-2,2,0,0,2,-2,2,2,0,0]],[[2,2,3,3,2],[2,2,0,0,0,0,2,-2,-2,-2,0,0,0,0,2,-2]],[[2,2,3,3,3],[2,2,0,0,0,0,-2,2,0,0,2,-2,2,2,0,0]],[[2,3,0,0,0],[2,0,2,0,-2,0,2,0,-2,0,2,0,-2,0,-2,0]],[[2,3,0,0,1],[-2,0,-2,0,2,0,-2,0,0,-2,0,2,0,-2,0,-2]],[[2,3,0,0,2],[2,0,2,0,-2,0,2,0,-2,0,2,0,-2,0,-2,0]],[[2,3,0,0,3],[-2,0,2,0,-2,0,-2,0,0,-2,0,-2,0,2,0,-2]],[[2,3,0,1,0],[2,0,2,0,0,2,0,-2,-2,0,-2,0,0,2,0,-2]],[[2,3,0,1,1],[2,0,-2,0,0,-2,0,-2,0,2,0,-2,2,0,2,0]],[[2,3,0,1,2],[2,0,-2,0,0,2,0,-2,2,0,2,0,0,2,0,2]],[[2,3,0,1,3],[2,0,-2,0,0,-2,0,-2,0,2,0,-2,2,0,2,0]],[[2,3,0,2,0],[-2,0,2,0,2,0,-2,0,-2,0,-2,0,2,0,2,0]],[[2,3,0,2,1],[-2,0,2,0,-2,0,-2,0,0,-2,0,-2,0,2,0,-2]],[[2,3,0,2,2],[2,0,2,0,-2,0,2,0,2,0,-2,0,2,0,2,0]],[[2,3,0,2,3],[-2,0,2,0,2,0,2,0,0,-2,0,2,0,2,0,2]],[[2,3,0,3,0],[2,0,-2,0,0,2,0,-2,-2,0,-2,0,0,-2,0,-2]],[[2,3,0,3,1],[2,0,-2,0,0,-2,0,-2,0,2,0,-2,2,0,2,0]],[[2,3,0,3,2],[2,0,-2,0,0,2,0,2,2,0,-2,0,0,-2,0,-2]],[[2,3,0,3,3],[2,0,-2,0,0,-2,0,-2,0,2,0,-2,2,0,2,0]],[[2,3,1,0,0],[-2,0,0,-2,2,0,0,-2,-2,0,0,2,2,0,0,2]],[[2,3,1,0,1],[-2,0,0,2,-2,0,0,-2,0,-2,-2,0,0,2,-2,0]],[[2,3,1,0,2],[-2,0,0,-2,2,0,0,-2,-2,0,0,2,2,0,0,2]],[[2,3,1,0,3],[2,0,0,2,-2,0,0,-2,0,-2,2,0,0,-2,2,0]],[[2,3,1,1,0],[2,0,0,2,0,2,-2,0,2,0,0,2,0,-2,2,0]],[[2,3,1,1,1],[-2,0,0,-2,0,2,-2,0,0,2,-2,0,-2,0,0,-2]],[[2,3,1,1,2],[2,0,0,-2,0,2,2,0,2,0,0,-2,0,2,2,0]],[[2,3,1,1,3],[-2,0,0,2,0,-2,-2,0,0,2,-2,0,-2,0,0,-2]],[[2,3,1,2,0],[-2,0,0,2,-2,0,0,-2,-2,0,0,-2,-2,0,0,2]],[[2,3,1,2,1],[2,0,0,-2,2,0,0,2,0,2,2,0,0,-2,2,0]],[[2,3,1,2,2],[-2,0,0,2,-2,0,0,2,2,0,0,-2,-2,0,0,2]],[[2,3,1,2,3],[2,0,0,-2,2,0,0,2,0,2,2,0,0,-2,2,0]],[[2,3,1,3,0],[2,0,0,2,0,-2,2,0,2,0,0,2,0,2,-2,0]],[[2,3,1,3,1],[-2,0,0,2,0,-2,2,0,0,2,-2,0,-2,0,0,2]],[[2,3,1,3,2],[2,0,0,2,0,2,-2,0,2,0,0,2,0,-2,2,0]],[[2,3,1,3,3],[-2,0,0,-2,0,-2,2,0,0,-2,-2,0,2,0,0,-2]],[[2,3,2,0,0],[2,0,-2,0,-2,0,2,0,2,0,-2,0,2,0,-2,0]],[[2,3,2,0,1],[-2,0,2,0,-2,0,-2,0,0,-2,0,2,0,-2,0,-2]],[[2,3,2,0,2],[2,0,2,0,2,0,-2,0,-2,0,2,0,2,0,2,0]],[[2,3,2,0,3],[-2,0,-2,0,2,0,2,0,0,-2,0,2,0,-2,0,2]],[[2,3,2,1,0],[2,0,-2,0,0,2,0,-2,2,0,2,0,0,2,0,2]],[[2,3,2,1,1],[2,0,2,0,0,2,0,2,0,-2,0,2,2,0,-2,0]],[[2,3,2,1,2],[2,0,2,0,0,2,0,-2,-2,0,-2,0,0,2,0,-2]],[[2,3,2,1,3],[2,0,2,0,0,2,0,2,0,-2,0,2,2,0,-2,0]],[[2,3,2,2,0],[2,0,-2,0,-2,0,2,0,2,0,2,0,-2,0,-2,0]],[[2,3,2,2,1],[-2,0,2,0,2,0,2,0,0,-2,0,2,0,2,0,2]],[[2,3,2,2,2],[2,0,-2,0,-2,0,2,0,2,0,2,0,-2,0,-2,0]],[[2,3,2,2,3],[-2,0,2,0,-2,0,2,0,0,-2,0,-2,0,2,0,2]],[[2,3,2,3,0],[-2,0,2,0,0,2,0,-2,-2,0,-2,0,0,2,0,2]],[[2,3,2,3,1],[-2,0,-2,0,0,-2,0,-2,0,2,0,-2,-2,0,2,0]],[[2,3,2,3,2],[-2,0,2,0,0,2,0,2,2,0,-2,0,0,2,0,2]],[[2,3,2,3,3],[-2,0,-2,0,0,-2,0,-2,0,2,0,-2,-2,0,2,0]],[[2,3,3,0,0],[-2,0,0,2,-2,0,0,2,2,0,0,-2,-2,0,0,2]],[[2,3,3,0,1],[2,0,0,-2,-2,0,0,2,0,2,2,0,0,-2,-2,0]],[[2,3,3,0,2],[-2,0,0,2,2,0,0,2,2,0,0,2,-2,0,0,2]],[[2,3,3,0,3],[2,0,0,-2,-2,0,0,2,0,2,2,0,0,-2,-2,0]],[[2,3,3,1,0],[2,0,0,-2,0,2,2,0,2,0,0,-2,0,2,2,0]],[[2,3,3,1,1],[-2,0,0,-2,0,2,2,0,0,2,-2,0,-2,0,0,2]],[[2,3,3,1,2],[2,0,0,-2,0,2,2,0,2,0,0,-2,0,2,2,0]],[[2,3,3,1,3],[-2,0,0,-2,0,2,2,0,0,2,-2,0,-2,0,0,2]],[[2,3,3,2,0],[-2,0,0,2,2,0,0,2,2,0,0,2,-2,0,0,2]],[[2,3,3,2,1],[2,0,0,-2,-2,0,0,2,0,2,2,0,0,-2,-2,0]],[[2,3,3,2,2],[-2,0,0,2,-2,0,0,2,2,0,0,-2,-2,0,0,2]],[[2,3,3,2,3],[2,0,0,-2,-2,0,0,2,0,2,2,0,0,-2,-2,0]],[[2,3,3,3,0],[2,0,0,-2,0,2,2,0,2,0,0,-2,0,2,2,0]],[[2,3,3,3,1],[-2,0,0,-2,0,-2,2,0,0,-2,-2,0,2,0,0,-2]],[[2,3,3,3,2],[2,0,0,2,0,-2,2,0,2,0,0,2,0,2,-2,0]],[[2,3,3,3,3],[-2,0,0,-2,0,-2,-2,0,0,-2,2,0,2,0,0,-2]],[[3,0,0,0,0],[-1,-1,-1,-1,3,-1,-1,-1,-1,3,-1,-1,3,-1,3,3]],[[3,0,0,0,1],[-1,-1,-1,-1,-1,-1,-1,-1,-3,-3,1,-3,1,-3,1,-3]],[[3,0,0,0,2],[-1,-1,3,-1,-1,-1,-1,3,-1,3,-1,-1,3,-1,-1,3]],[[3,0,0,0,3],[-1,-1,3,-1,-1,-1,-1,-1,1,1,-3,1,1,1,1,-3]],[[3,0,0,1,0],[-1,3,-1,-1,1,-3,1,1,3,-1,-1,3,1,1,1,-3]],[[3,0,0,1,1],[-1,3,-1,-1,1,1,-3,1,1,1,1,1,-1,-1,3,-1]],[[3,0,0,1,2],[-1,-1,-1,3,1,1,-3,-3,-1,3,-1,-1,-3,1,1,1]],[[3,0,0,1,3],[-1,3,-1,-1,1,1,-3,-3,-3,1,1,1,-1,-1,3,-1]],[[3,0,0,2,0],[-1,-1,-1,-1,3,-1,-1,3,-1,-1,-1,-1,3,-1,-1,-1]],[[3,0,0,2,1],[-1,-1,-1,-1,-1,-1,-1,-1,1,-3,1,1,1,1,-3,-3]],[[3,0,0,2,2],[-1,-1,-1,-1,-1,-1,3,-1,3,-1,-1,-1,-1,-1,3,-1]],[[3,0,0,2,3],[-1,-1,-1,-1,-1,3,-1,-1,-3,1,1,-3,-3,-3,1,1]],[[3,0,0,3,0],[-1,3,-1,-1,1,1,-3,1,-1,-1,-1,-1,1,1,1,-3]],[[3,0,0,3,1],[-1,-1,-1,-1,1,1,-3,-3,1,1,1,-3,-1,3,3,-1]],[[3,0,0,3,2],[-1,-1,-1,3,1,1,-3,1,3,3,-1,-1,-3,1,1,1]],[[3,0,0,3,3],[-1,-1,3,-1,-3,1,-3,1,1,1,-3,1,3,-1,-1,-1]],[[3,0,1,0,0],[-1,-1,-3,-3,3,-1,1,1,-1,-1,1,1,-1,-1,-3,-3]],[[3,0,1,0,1],[-1,-1,-3,-3,-1,3,1,-3,1,1,-1,-1,1,1,-1,3]],[[3,0,1,0,2],[-1,-1,1,-3,-1,3,1,-3,-1,3,-3,1,-1,-1,1,1]],[[3,0,1,0,3],[3,-1,1,1,3,3,1,1,1,-3,-1,3,1,1,-1,-1]],[[3,0,1,1,0],[3,-1,-3,1,1,1,3,-1,-1,-1,1,-3,1,1,-1,3]],[[3,0,1,1,1],[-1,3,1,-3,1,1,-1,3,-3,1,-1,-1,3,-1,1,1]],[[3,0,1,1,2],[3,-1,1,1,1,1,-1,3,3,-1,1,1,1,1,-1,-1]],[[3,0,1,1,3],[-1,3,-3,1,1,1,-1,-1,1,-3,-1,3,-1,-1,1,-3]],[[3,0,1,2,0],[-1,-1,-3,-3,-1,3,1,-3,-1,-1,1,1,-1,-1,-3,1]],[[3,0,1,2,1],[-1,-1,1,1,3,-1,1,1,-3,-3,3,-1,-3,1,-1,-1]],[[3,0,1,2,2],[-1,-1,-3,-3,-1,-1,1,-3,3,-1,1,1,3,-1,1,1]],[[3,0,1,2,3],[3,-1,1,1,-1,-1,1,-3,1,1,-1,3,1,1,-1,-1]],[[3,0,1,3,0],[-1,3,-3,1,1,1,-1,-1,3,-1,-3,1,1,1,3,-1]],[[3,0,1,3,1],[-1,3,-3,1,-3,1,-1,-1,1,-3,-1,-1,-1,-1,1,-3]],[[3,0,1,3,2],[3,-1,1,1,-3,-3,-1,-1,3,3,1,1,1,1,-1,-1]],[[3,0,1,3,3],[3,3,1,1,1,1,-1,-1,-3,1,3,-1,-1,3,1,1]],[[3,0,2,0,0],[3,-1,-1,-1,3,-1,-1,-1,-1,-1,3,-1,3,3,-1,-1]],[[3,0,2,0,1],[-1,-1,-1,-1,3,-1,3,-1,-3,-3,1,-3,1,1,1,1]],[[3,0,2,0,2],[-1,-1,-1,-1,3,-1,-1,-1,-1,-1,3,-1,3,3,-1,3]],[[3,0,2,0,3],[-1,-1,3,-1,3,-1,-1,3,1,-3,1,1,1,1,1,-3]],[[3,0,2,1,0],[3,-1,-1,-1,1,1,1,1,3,-1,-1,-1,1,1,1,-3]],[[3,0,2,1,1],[-1,3,-1,-1,1,-3,1,1,1,1,1,1,-1,3,-1,-1]],[[3,0,2,1,2],[-1,-1,-1,3,1,-3,1,-3,-1,-1,3,-1,-3,1,1,1]],[[3,0,2,1,3],[-1,3,-1,-1,1,-3,1,-3,-3,1,1,1,-1,3,-1,-1]],[[3,0,2,2,0],[-1,-1,3,-1,3,-1,-1,3,-1,-1,-1,-1,3,3,-1,-1]],[[3,0,2,2,1],[-1,-1,-1,-1,-1,-1,-1,-1,1,1,-3,1,1,-3,1,-3]],[[3,0,2,2,2],[-1,-1,-1,3,-1,-1,3,-1,3,-1,-1,-1,-1,3,-1,3]],[[3,0,2,2,3],[-1,-1,-1,-1,-1,-1,3,-1,-3,1,1,-3,-3,1,-3,1]],[[3,0,2,3,0],[3,-1,-1,-1,1,1,1,-3,-1,-1,-1,-1,1,1,1,-3]],[[3,0,2,3,1],[-1,-1,-1,3,1,-3,1,1,1,-3,1,-3,-1,3,-1,-1]],[[3,0,2,3,2],[-1,-1,-1,-1,-3,1,1,-3,-1,-1,-1,3,1,-3,-3,1]],[[3,0,2,3,3],[-1,-1,-1,3,1,-3,-3,1,1,1,1,-3,-1,3,-1,-1]],[[3,0,3,0,0],[-1,3,1,1,-1,-1,-3,1,3,-1,1,1,-1,3,1,-3]],[[3,0,3,0,1],[-1,3,1,1,3,-1,1,1,1,1,-1,3,-3,1,3,-1]],[[3,0,3,0,2],[-1,-1,1,-3,-1,3,1,-3,-1,-1,1,1,-1,3,-3,1]],[[3,0,3,0,3],[-1,3,1,-3,3,-1,1,1,1,1,-1,3,1,1,3,-1]],[[3,0,3,1,0],[-1,-1,1,-3,1,1,3,3,-1,-1,1,1,1,-3,-1,3]],[[3,0,3,1,1],[3,-1,1,-3,1,1,3,-1,-3,1,-1,-1,3,-1,1,1]],[[3,0,3,1,2],[-1,-1,1,1,1,-3,-1,3,-1,3,1,-3,1,1,-1,3]],[[3,0,3,1,3],[-1,3,1,1,-3,1,-1,-1,1,-3,-1,-1,-1,3,1,-3]],[[3,0,3,2,0],[-1,-1,1,1,3,-1,-3,1,-1,-1,1,1,-1,-1,1,-3]],[[3,0,3,2,1],[-1,-1,1,1,-1,3,1,-3,-3,-3,-1,-1,1,1,-1,3]],[[3,0,3,2,2],[-1,-1,-3,1,-1,-1,-3,1,3,3,1,-3,-1,-1,1,1]],[[3,0,3,2,3],[-1,-1,1,1,-1,-1,1,-3,1,1,-1,3,1,1,-1,3]],[[3,0,3,3,0],[-1,3,1,1,-3,1,-1,-1,3,-1,1,1,-3,1,3,-1]],[[3,0,3,3,1],[-1,3,-3,1,1,1,3,-1,1,-3,-1,-1,-1,3,1,1]],[[3,0,3,3,2],[3,-1,-3,-3,1,1,-1,-1,3,3,1,1,1,1,-1,-1]],[[3,0,3,3,3],[-1,3,1,-3,1,1,-1,3,-3,1,-1,-1,-1,-1,1,-3]],[[3,1,0,0,0],[-1,-3,-1,-3,3,1,-1,-3,-1,1,-1,1,3,1,-1,1]],[[3,1,0,0,1],[-1,1,3,1,-1,1,-1,-3,-3,-1,-3,3,1,-1,1,-1]],[[3,1,0,0,2],[3,1,3,1,-1,1,3,1,3,1,-1,1,-1,1,3,1]],[[3,1,0,0,3],[-1,1,-1,1,3,1,-1,1,-3,3,-3,-1,-3,-1,1,-1]],[[3,1,0,1,0],[-1,-3,-1,-3,1,-1,-3,-1,-1,1,3,-3,1,-1,1,-1]],[[3,1,0,1,1],[3,-3,3,1,1,-1,1,-1,1,-1,1,3,3,1,-1,1]],[[3,1,0,1,2],[-1,1,-1,-3,1,-1,1,3,-1,1,3,-3,1,-1,1,3]],[[3,1,0,1,3],[3,-3,3,1,1,-1,1,-1,1,-1,1,3,3,1,-1,1]],[[3,1,0,2,0],[-1,-3,-1,-3,-1,1,-1,1,3,1,-1,-3,3,1,-1,1]],[[3,1,0,2,1],[-1,-3,-1,-3,3,1,-1,-3,1,-1,1,-1,1,3,1,-1]],[[3,1,0,2,2],[-1,-3,-1,-3,-1,1,-1,-3,-1,1,-1,-3,3,1,-1,1]],[[3,1,0,2,3],[-1,-3,-1,-3,3,1,-1,1,1,-1,1,3,1,-1,-3,-1]],[[3,1,0,3,0],[-1,1,-1,-3,1,-1,1,3,-1,1,-1,1,1,-1,-3,-1]],[[3,1,0,3,1],[-1,1,-1,-3,1,-1,-3,-1,1,3,1,3,3,1,-1,1]],[[3,1,0,3,2],[-1,1,3,-3,1,3,-3,3,-1,1,-1,1,1,-1,1,-1]],[[3,1,0,3,3],[-1,1,-1,-3,1,-1,-3,-1,1,3,1,3,3,1,-1,1]],[[3,1,1,0,0],[3,1,-3,-1,-1,1,-3,-1,-1,1,1,-1,3,-3,1,-1]],[[3,1,1,0,1],[3,1,1,-1,-1,1,1,-1,-3,-1,3,-3,1,3,-1,1]],[[3,1,1,0,2],[-1,1,-3,-1,3,1,-3,3,-1,1,1,-1,-1,-3,1,-1]],[[3,1,1,0,3],[3,1,1,-1,-1,-3,1,-1,1,3,3,1,1,3,-1,1]],[[3,1,1,1,0],[3,1,-3,-1,1,-1,3,1,3,1,1,-1,1,3,-1,1]],[[3,1,1,1,1],[3,1,-3,-1,1,-1,3,-3,1,-1,3,1,-1,1,1,-1]],[[3,1,1,1,2],[3,1,-3,-1,1,-1,3,-3,-1,1,1,-1,1,3,-1,1]],[[3,1,1,1,3],[3,1,1,3,-3,-1,3,-3,1,-1,-1,1,-1,1,1,-1]],[[3,1,1,2,0],[-1,-3,-3,-1,3,1,1,-1,3,1,-3,-1,-1,1,1,-1]],[[3,1,1,2,1],[-1,-3,-3,-1,3,1,1,-1,1,-1,-1,1,-3,-1,-1,-3]],[[3,1,1,2,2],[-1,1,-3,-1,3,1,-3,3,-1,1,1,-1,-1,-3,1,-1]],[[3,1,1,2,3],[3,1,1,-1,3,1,1,-1,-3,-1,3,1,1,3,-1,1]],[[3,1,1,3,0],[3,-3,1,3,1,-1,-1,1,-1,1,1,-1,-3,-1,-1,-3]],[[3,1,1,3,1],[-1,-3,1,-1,1,3,-1,1,1,-1,-1,1,-1,-3,1,-1]],[[3,1,1,3,2],[3,1,1,-1,1,-1,-1,1,3,1,1,3,1,3,-1,-3]],[[3,1,1,3,3],[-1,-3,-3,-1,1,-1,-1,1,1,-1,-1,-3,3,-3,1,-1]],[[3,1,2,0,0],[-1,-3,3,-3,-1,1,-1,-3,-1,1,3,1,-1,1,-1,1]],[[3,1,2,0,1],[-1,1,-1,1,3,-3,-1,1,1,-1,1,-1,1,3,1,-1]],[[3,1,2,0,2],[3,-3,-1,1,3,1,-1,1,3,1,-1,1,-1,1,-1,-3]],[[3,1,2,0,3],[-1,1,-1,1,3,-3,-1,-3,-3,-1,1,-1,1,3,1,-1]],[[3,1,2,1,0],[3,-3,3,-3,1,-1,1,-1,-1,1,3,1,1,-1,1,-1]],[[3,1,2,1,1],[-1,1,3,-3,1,-1,1,3,1,-1,1,-1,3,1,3,1]],[[3,1,2,1,2],[-1,1,-1,1,1,3,1,-1,3,-3,-1,1,-3,3,1,-1]],[[3,1,2,1,3],[-1,1,3,-3,1,-1,1,-1,-3,-1,1,-1,3,1,3,1]],[[3,1,2,2,0],[-1,-3,3,-3,3,1,3,1,-1,1,-1,1,-1,1,-1,1]],[[3,1,2,2,1],[-1,-3,3,1,-1,-3,-1,-3,1,-1,1,-1,1,3,1,-1]],[[3,1,2,2,2],[-1,1,-1,1,3,-3,-1,1,3,1,3,1,-1,1,3,1]],[[3,1,2,2,3],[-1,-3,3,-3,-1,-3,3,1,1,-1,1,-1,1,-1,1,-1]],[[3,1,2,3,0],[-1,1,-1,1,1,-1,1,-1,3,-3,3,1,-3,3,1,-1]],[[3,1,2,3,1],[3,1,-1,1,1,-1,1,-1,-3,-1,1,-1,-1,-3,3,-3]],[[3,1,2,3,2],[-1,1,-1,1,1,3,1,-1,3,-3,-1,1,-3,3,1,-1]],[[3,1,2,3,3],[-1,-3,3,1,1,-1,-3,3,1,3,1,-1,-1,1,-1,1]],[[3,1,3,0,0],[-1,-3,1,3,3,1,1,-1,-1,-3,-3,-1,-1,1,1,-1]],[[3,1,3,0,1],[3,1,-3,-1,3,1,1,-1,-3,-1,3,1,1,-1,-1,1]],[[3,1,3,0,2],[3,1,1,-1,-1,1,-3,-1,-1,1,1,-1,3,1,1,-1]],[[3,1,3,0,3],[-1,-3,1,-1,3,1,1,-1,1,-1,-1,1,-3,3,-1,-3]],[[3,1,3,1,0],[3,1,-3,-1,1,-1,-1,1,3,1,1,3,1,-1,-1,-3]],[[3,1,3,1,1],[-1,-3,1,-1,1,-1,3,-3,-3,-1,-1,1,-1,1,-3,-1]],[[3,1,3,1,2],[3,1,-3,-1,-3,-1,-1,-3,-1,1,1,-1,1,-1,-1,-3]],[[3,1,3,1,3],[3,1,-3,-1,1,3,3,-3,1,-1,-1,1,-1,1,1,-1]],[[3,1,3,2,0],[-1,-3,1,3,-1,-3,1,-1,3,1,-3,-1,-1,1,1,-1]],[[3,1,3,2,1],[-1,-3,1,-1,-1,1,1,-1,1,-1,-1,-3,-3,3,-1,-3]],[[3,1,3,2,2],[3,1,1,-1,-1,1,-3,-1,-1,1,1,-1,3,1,1,-1]],[[3,1,3,2,3],[3,1,1,-1,-1,-3,1,-1,-3,3,-1,1,1,-1,-1,-3]],[[3,1,3,3,0],[3,1,-3,-1,1,-1,-1,-3,-1,1,1,3,1,-1,-1,-3]],[[3,1,3,3,1],[-1,-3,1,-1,1,-1,3,1,1,-1,-1,1,-1,1,-3,-1]],[[3,1,3,3,2],[3,1,1,3,-3,-1,-1,-3,-1,1,1,-1,1,3,-1,1]],[[3,1,3,3,3],[-1,-3,1,-1,1,-1,-1,1,1,-1,-1,-3,3,1,1,-1]],[[3,2,0,0,0],[3,-1,-1,3,-1,-1,3,-1,-1,3,-1,-1,-1,-1,-1,3]],[[3,2,0,0,1],[-1,-1,3,-1,-1,-1,3,-1,-3,-3,1,1,1,1,-3,1]],[[3,2,0,0,2],[3,-1,-1,-1,-1,-1,3,-1,-1,3,-1,-1,3,-1,-1,3]],[[3,2,0,0,3],[3,-1,-1,-1,3,-1,3,-1,1,-3,1,1,1,1,1,-3]],[[3,2,0,1,0],[-1,-1,-1,-1,1,-3,1,1,-1,-1,-1,-1,1,-3,1,-3]],[[3,2,0,1,1],[-1,-1,-1,-1,-3,1,1,-3,1,1,1,-3,-1,3,-1,3]],[[3,2,0,1,2],[-1,-1,-1,-1,1,1,-3,1,-1,-1,-1,-1,1,-3,1,-3]],[[3,2,0,1,3],[3,3,-1,-1,1,1,1,-3,1,1,1,1,-1,3,3,-1]],[[3,2,0,2,0],[-1,-1,-1,3,3,-1,-1,-1,3,-1,-1,-1,-1,3,3,-1]],[[3,2,0,2,1],[-1,-1,-1,-1,-1,3,-1,3,1,1,-3,1,1,-3,-3,1]],[[3,2,0,2,2],[3,-1,-1,-1,-1,-1,-1,-1,3,-1,3,-1,3,3,-1,-1]],[[3,2,0,2,3],[-1,-1,-1,-1,-1,3,-1,-1,-3,1,-3,1,1,-3,-3,1]],[[3,2,0,3,0],[-1,-1,-1,-1,-3,1,1,-3,-1,-1,3,-1,-3,1,-3,1]],[[3,2,0,3,1],[-1,-1,-1,3,1,1,1,-3,-3,-3,1,1,-1,-1,-1,3]],[[3,2,0,3,2],[-1,-1,-1,-1,-3,-3,1,-3,3,-1,3,-1,1,1,1,1]],[[3,2,0,3,3],[-1,-1,-1,-1,1,1,1,-3,1,1,1,1,-1,3,-1,3]],[[3,2,1,0,0],[-1,-1,-3,-3,-1,-1,1,-3,-1,-1,1,-3,-1,-1,1,-3]],[[3,2,1,0,1],[-1,-1,1,-3,-1,-1,1,-3,-3,-3,3,-1,1,1,-1,-1]],[[3,2,1,0,2],[-1,-1,1,1,-1,-1,-3,1,3,-1,1,1,-1,-1,1,-3]],[[3,2,1,0,3],[-1,-1,-3,1,3,-1,1,-3,-3,-3,-1,-1,1,1,-1,-1]],[[3,2,1,1,0],[-1,-1,1,1,1,-3,-1,-1,-1,3,1,1,1,1,-1,3]],[[3,2,1,1,1],[3,-1,1,1,1,-3,-1,-1,1,1,3,-1,3,3,1,1]],[[3,2,1,1,2],[3,3,-3,1,1,1,-1,3,3,-1,1,1,1,1,-1,-1]],[[3,2,1,1,3],[3,3,-3,1,1,1,3,-1,-3,1,-1,-1,-1,-1,1,1]],[[3,2,1,2,0],[-1,-1,-3,1,3,-1,1,1,3,-1,1,1,-1,-1,1,1]],[[3,2,1,2,1],[-1,-1,1,1,-1,-1,1,1,1,1,-1,-1,1,1,-1,3]],[[3,2,1,2,2],[-1,-1,1,1,3,-1,1,1,-1,-1,-3,1,-1,-1,1,-3]],[[3,2,1,2,3],[-1,-1,-3,-3,-1,-1,1,-3,1,1,3,-1,-3,1,-1,-1]],[[3,2,1,3,0],[-1,-1,1,-3,1,-3,3,3,-1,-1,1,-3,1,1,-1,-1]],[[3,2,1,3,1],[3,3,1,1,-3,1,-1,-1,-3,1,-1,-1,-1,-1,1,-3]],[[3,2,1,3,2],[-1,-1,1,1,1,1,3,-1,-1,-1,-3,1,-3,-3,3,-1]],[[3,2,1,3,3],[-1,-1,-3,1,1,1,3,-1,1,-3,-1,-1,-1,-1,1,1]],[[3,2,2,0,0],[-1,-1,3,-1,-1,-1,-1,-1,-1,3,-1,3,3,-1,-1,3]],[[3,2,2,0,1],[-1,-1,3,-1,-1,-1,3,-1,-3,1,-3,1,1,-3,1,1]],[[3,2,2,0,2],[-1,3,-1,-1,-1,-1,-1,3,-1,3,-1,-1,3,-1,-1,3]],[[3,2,2,0,3],[-1,3,-1,-1,-1,-1,-1,-1,1,1,-3,1,1,1,1,-3]],[[3,2,2,1,0],[3,-1,3,-1,1,-3,1,1,-1,3,3,-1,1,1,1,1]],[[3,2,2,1,1],[-1,-1,-1,-1,1,-3,1,-3,-3,1,1,1,-1,-1,-1,-1]],[[3,2,2,1,2],[-1,-1,-1,-1,-3,-3,1,1,3,-1,-1,-1,1,-3,1,-3]],[[3,2,2,1,3],[-1,-1,-1,-1,1,1,1,-3,-3,1,-3,1,-1,-1,-1,-1]],[[3,2,2,2,0],[-1,3,-1,-1,-1,-1,-1,3,-1,-1,3,-1,-1,-1,-1,-1]],[[3,2,2,2,1],[-1,-1,-1,-1,-1,-1,3,3,1,-3,1,1,1,-3,-3,1]],[[3,2,2,2,2],[3,-1,-1,-1,-1,-1,-1,-1,3,3,-1,-1,3,-1,3,-1]],[[3,2,2,2,3],[-1,-1,-1,-1,-1,-1,3,-1,-3,-3,1,1,1,-3,-3,1]],[[3,2,2,3,0],[-1,-1,-1,-1,-3,1,1,-3,-1,3,-1,-1,-3,-3,1,1]],[[3,2,2,3,1],[-1,-1,-1,-1,-3,-3,1,1,1,1,1,-3,-1,-1,-1,-1]],[[3,2,2,3,2],[-1,-1,-1,-1,-3,1,-3,-3,3,3,-1,-1,1,1,1,1]],[[3,2,2,3,3],[-1,-1,-1,-1,-3,-3,1,-3,-3,1,1,-3,-1,-1,-1,-1]],[[3,2,3,0,0],[-1,-1,-3,-3,3,-1,1,-3,-1,-1,1,1,3,-1,1,1]],[[3,2,3,0,1],[-1,-1,1,-3,-1,-1,1,-3,-3,1,-1,-1,1,-3,3,-1]],[[3,2,3,0,2],[-1,-1,1,1,3,-1,1,1,3,-1,1,1,-1,3,1,1]],[[3,2,3,0,3],[-1,-1,-3,1,-1,-1,1,1,1,1,-1,-1,1,-3,-1,3]],[[3,2,3,1,0],[3,-1,1,1,1,-3,-1,3,3,3,1,1,1,1,-1,-1]],[[3,2,3,1,1],[-1,-1,1,-3,1,-3,-1,3,1,1,-1,-1,3,-1,1,-3]],[[3,2,3,1,2],[3,-1,1,1,1,-3,-1,3,3,3,1,1,1,1,-1,-1]],[[3,2,3,1,3],[-1,-1,1,-3,1,-3,-1,-1,-3,1,-1,-1,3,-1,1,-3]],[[3,2,3,2,0],[-1,-1,-3,-3,-1,-1,1,1,3,-1,1,-3,3,-1,1,1]],[[3,2,3,2,1],[-1,-1,-3,-3,-1,-1,1,1,1,-3,3,-1,1,-3,-1,-1]],[[3,2,3,2,2],[-1,-1,-3,-3,-1,-1,1,-3,-1,-1,1,-3,3,-1,1,1]],[[3,2,3,2,3],[-1,-1,-3,1,-1,-1,-3,-3,1,1,-1,-1,1,-3,3,-1]],[[3,2,3,3,0],[-1,-1,-3,-3,1,1,-1,-1,-1,3,1,-3,1,1,-1,3]],[[3,2,3,3,1],[3,3,1,1,1,1,3,-1,-3,1,-1,-1,-1,3,1,1]],[[3,2,3,3,2],[-1,-1,-3,-3,1,1,-1,-1,-1,3,1,-3,1,1,-1,3]],[[3,2,3,3,3],[-1,3,1,-3,-3,1,-1,3,1,1,-1,-1,3,-1,1,1]],[[3,3,0,0,0],[-1,1,3,1,-1,-3,-1,1,3,1,-1,1,-1,1,3,-3]],[[3,3,0,0,1],[-1,-3,3,1,3,-3,-1,1,1,-1,1,-1,1,3,1,-1]],[[3,3,0,0,2],[-1,-3,3,-3,-1,1,3,-3,-1,1,-1,1,-1,1,-1,1]],[[3,3,0,0,3],[-1,1,-1,-3,3,1,3,1,1,-1,1,-1,-3,3,1,-1]],[[3,3,0,1,0],[-1,1,3,1,-3,3,1,-1,-1,-3,-1,1,-3,-1,1,-1]],[[3,3,0,1,1],[3,1,-1,-3,1,-1,1,3,1,-1,1,-1,3,1,-1,-3]],[[3,3,0,1,2],[3,-3,-1,1,1,-1,1,-1,-1,-3,3,-3,1,-1,1,-1]],[[3,3,0,1,3],[3,1,-1,1,-3,-1,1,-1,-3,3,1,-1,-1,-3,-1,1]],[[3,3,0,2,0],[-1,1,3,1,3,1,-1,1,-1,-3,-1,1,-1,1,3,-3]],[[3,3,0,2,1],[-1,1,-1,1,-1,-3,-1,-3,1,-1,1,-1,1,3,1,-1]],[[3,3,0,2,2],[-1,-3,3,-3,-1,1,3,1,3,1,-1,1,-1,1,-1,1]],[[3,3,0,2,3],[-1,1,-1,-3,-1,1,-1,1,1,3,-3,-1,1,-1,1,-1]],[[3,3,0,3,0],[-1,-3,-1,1,1,-1,1,-1,3,-3,-1,-3,1,3,1,-1]],[[3,3,0,3,1],[-1,-3,3,1,1,-1,1,-1,1,-1,-3,-1,-1,1,3,-3]],[[3,3,0,3,2],[3,1,-1,-3,1,-1,1,-1,-1,1,3,1,1,-1,1,-1]],[[3,3,0,3,3],[3,1,-1,-3,1,3,1,-1,-3,3,1,-1,-1,1,-1,1]],[[3,3,1,0,0],[-1,1,1,-1,-1,-3,1,-1,-1,1,1,-1,3,1,1,3]],[[3,3,1,0,1],[-1,1,1,-1,-1,-3,1,-1,-3,-1,3,1,1,-1,-1,1]],[[3,3,1,0,2],[3,1,-3,-1,3,1,1,3,3,1,1,-1,-1,1,1,-1]],[[3,3,1,0,3],[-1,1,-3,-1,3,1,1,-1,1,-1,-1,1,-3,3,-1,-3]],[[3,3,1,1,0],[3,-3,1,-1,1,-1,3,-3,-1,1,1,-1,1,-1,3,1]],[[3,3,1,1,1],[-1,1,1,-1,-3,-1,-1,-3,-3,-1,3,-3,-1,1,1,-1]],[[3,3,1,1,2],[3,-3,1,-1,1,-1,-1,-3,-1,1,1,3,1,-1,-1,-3]],[[3,3,1,1,3],[-1,1,-3,-1,1,-1,3,-3,-3,-1,-1,1,-1,1,-3,-1]],[[3,3,1,2,0],[-1,-3,1,-1,3,-3,1,3,-1,1,1,-1,-1,1,-3,-1]],[[3,3,1,2,1],[-1,1,-3,-1,-1,1,1,-1,1,-1,-1,-3,-3,3,-1,-3]],[[3,3,1,2,2],[-1,1,-3,3,3,1,1,-1,-1,-3,-3,-1,-1,1,1,-1]],[[3,3,1,2,3],[-1,1,-3,-1,3,1,1,-1,1,-1,-1,1,-3,3,-1,-3]],[[3,3,1,3,0],[-1,1,1,-1,1,-1,-1,1,-1,1,1,-1,1,3,-1,1]],[[3,3,1,3,1],[-1,-3,1,-1,1,-1,3,1,1,-1,-1,1,3,1,-3,3]],[[3,3,1,3,2],[3,-3,1,-1,-3,-1,-1,1,3,1,1,-1,1,-1,-1,-3]],[[3,3,1,3,3],[-1,-3,-3,-1,1,-1,-1,-3,1,-1,3,-3,-1,1,1,-1]],[[3,3,2,0,0],[-1,1,-1,-3,-1,1,-1,1,3,1,-1,-3,-1,1,3,-3]],[[3,3,2,0,1],[-1,1,-1,-3,3,-3,3,1,1,-1,1,3,1,-1,1,-1]],[[3,3,2,0,2],[-1,1,-1,-3,3,1,3,1,-1,1,-1,1,-1,1,-1,1]],[[3,3,2,0,3],[-1,1,-1,1,3,1,-1,1,1,3,-3,3,-3,-1,1,-1]],[[3,3,2,1,0],[3,1,-1,1,1,-1,1,-1,-1,1,3,1,1,3,-3,3]],[[3,3,2,1,1],[3,1,3,1,1,-1,1,3,1,-1,1,-1,3,1,3,1]],[[3,3,2,1,2],[-1,-3,3,-3,1,-1,1,3,-1,1,-1,1,1,-1,-3,-1]],[[3,3,2,1,3],[3,1,3,1,1,-1,1,3,1,-1,1,-1,3,1,3,1]],[[3,3,2,2,0],[-1,-3,-1,-3,-1,1,3,-3,-1,1,-1,1,-1,-3,-1,1]],[[3,3,2,2,1],[-1,1,-1,1,-1,1,-1,1,1,3,-3,-1,-3,-1,1,-1]],[[3,3,2,2,2],[-1,-3,-1,-3,-1,1,-1,-3,3,1,-1,1,3,1,-1,1]],[[3,3,2,2,3],[-1,-3,-1,1,3,-3,-1,1,1,-1,1,-1,1,-1,1,-1]],[[3,3,2,3,0],[-1,-3,-1,1,1,3,-3,-1,3,1,-1,1,-3,-1,1,-1]],[[3,3,2,3,1],[-1,1,-1,1,-3,3,1,-1,1,-1,-3,-1,-1,-3,3,1]],[[3,3,2,3,2],[-1,-3,-1,1,1,3,1,-1,3,-3,-1,1,-3,-1,1,-1]],[[3,3,2,3,3],[-1,1,-1,1,-3,3,1,-1,1,-1,-3,-1,-1,-3,3,1]],[[3,3,3,0,0],[3,1,1,3,-1,-3,1,-1,-1,1,1,-1,-1,1,1,-1]],[[3,3,3,0,1],[3,-3,1,-1,-1,1,1,-1,-3,-1,3,-3,1,-1,-1,1]],[[3,3,3,0,2],[3,1,1,3,-1,-3,1,-1,-1,1,1,-1,-1,1,1,-1]],[[3,3,3,0,3],[-1,1,1,-1,-1,1,-3,-1,-3,3,-1,1,1,-1,-1,1]],[[3,3,3,1,0],[-1,1,-3,-1,1,-1,-1,1,-1,1,1,-1,1,-1,-1,1]],[[3,3,3,1,1],[-1,1,-3,-1,1,-1,-1,-3,-3,-1,-1,-3,3,1,1,-1]],[[3,3,3,1,2],[-1,1,-3,-1,1,-1,-1,1,-1,1,1,-1,1,-1,-1,1]],[[3,3,3,1,3],[-1,1,-3,-1,1,3,-1,-3,-3,-1,-1,1,-1,-3,1,-1]],[[3,3,3,2,0],[-1,1,-3,-1,-1,-3,1,-1,-1,1,1,-1,3,-3,1,3]],[[3,3,3,2,1],[3,-3,1,-1,-1,1,1,-1,-3,-1,3,-3,1,-1,-1,1]],[[3,3,3,2,2],[-1,1,-3,-1,-1,-3,1,-1,-1,1,1,-1,3,-3,1,3]],[[3,3,3,2,3],[-1,1,1,3,-1,1,1,-1,1,-1,-1,-3,-3,3,3,1]],[[3,3,3,3,0],[3,1,1,3,1,-1,-1,1,-1,1,1,-1,-3,3,-1,-3]],[[3,3,3,3,1],[-1,-3,1,-1,-3,-1,-1,1,1,-1,-1,1,3,-3,-3,-1]],[[3,3,3,3,2],[3,1,1,3,1,-1,-1,1,-1,1,1,-1,-3,3,-1,-3]],[[3,3,3,3,3],[-1,1,-3,-1,-3,-1,-1,-3,1,3,-1,1,-1,-3,1,-1]],[[4,0,0,0,1],[0,0,0,0,0,0,0,0,-2,-2,2,-2,2,-2,2,2]],[[4,0,0,1,0],[0,0,0,0,-2,-2,2,-2,0,0,0,0,-2,-2,2,-2]],[[4,0,0,1,1],[0,0,0,0,-2,-2,-2,-2,-2,2,2,-2,0,0,0,0]],[[4,0,0,1,2],[0,0,0,0,-2,-2,2,-2,0,0,0,0,-2,-2,2,-2]],[[4,0,0,1,3],[0,0,0,0,-2,-2,-2,2,2,2,2,-2,0,0,0,0]],[[4,0,0,2,1],[0,0,0,0,0,0,0,0,-2,-2,2,-2,2,-2,2,2]],[[4,0,1,0,0],[0,0,-2,-2,0,0,2,2,0,0,2,-2,0,0,-2,2]],[[4,0,1,0,1],[0,0,2,-2,0,0,2,2,-2,-2,0,0,2,-2,0,0]],[[4,0,1,0,2],[0,0,-2,-2,0,0,2,2,0,0,2,-2,0,0,-2,2]],[[4,0,1,0,3],[0,0,2,-2,0,0,2,2,-2,-2,0,0,2,-2,0,0]],[[4,0,1,1,0],[0,0,-2,-2,-2,-2,0,0,0,0,2,-2,2,-2,0,0]],[[4,0,1,1,1],[0,0,-2,2,2,-2,0,0,2,-2,0,0,0,0,2,-2]],[[4,0,1,1,2],[0,0,-2,-2,2,2,0,0,0,0,-2,2,2,-2,0,0]],[[4,0,1,1,3],[0,0,2,-2,-2,2,0,0,-2,2,0,0,0,0,-2,2]],[[4,0,1,2,0],[0,0,-2,2,0,0,2,-2,0,0,-2,-2,0,0,2,2]],[[4,0,1,2,1],[0,0,-2,-2,0,0,-2,2,2,2,0,0,2,-2,0,0]],[[4,0,1,2,2],[0,0,2,-2,0,0,-2,2,0,0,2,2,0,0,-2,-2]],[[4,0,1,2,3],[0,0,-2,-2,0,0,-2,-2,-2,2,0,0,2,-2,0,0]],[[4,0,1,3,0],[0,0,-2,-2,2,2,0,0,0,0,-2,2,2,-2,0,0]],[[4,0,1,3,1],[0,0,-2,2,2,-2,0,0,2,-2,0,0,0,0,2,-2]],[[4,0,1,3,2],[0,0,-2,-2,2,2,0,0,0,0,-2,2,2,-2,0,0]],[[4,0,1,3,3],[0,0,-2,2,2,-2,0,0,2,-2,0,0,0,0,2,-2]],[[4,0,2,0,1],[0,0,0,0,0,0,0,0,-2,-2,2,-2,2,-2,2,2]],[[4,0,2,1,0],[0,0,0,0,-2,2,-2,-2,0,0,0,0,-2,-2,2,-2]],[[4,0,2,1,1],[0,0,0,0,-2,2,-2,-2,2,2,-2,2,0,0,0,0]],[[4,0,2,1,2],[0,0,0,0,-2,2,-2,-2,0,0,0,0,-2,-2,2,-2]],[[4,0,2,1,3],[0,0,0,0,-2,2,-2,-2,2,2,-2,2,0,0,0,0]],[[4,0,2,2,1],[0,0,0,0,0,0,0,0,-2,-2,2,-2,2,2,-2,2]],[[4,1,0,0,0],[0,-2,0,2,0,2,0,-2,0,-2,0,-2,0,2,0,2]],[[4,1,0,0,1],[0,-2,0,-2,0,2,0,-2,-2,0,2,0,-2,0,-2,0]],[[4,1,0,0,2],[0,-2,0,2,0,2,0,-2,0,-2,0,-2,0,2,0,2]],[[4,1,0,0,3],[0,2,0,2,0,-2,0,2,2,0,2,0,-2,0,2,0]],[[4,1,0,1,0],[0,-2,0,-2,-2,0,-2,0,0,2,0,-2,2,0,-2,0]],[[4,1,0,1,1],[0,-2,0,-2,2,0,2,0,2,0,-2,0,0,2,0,-2]],[[4,1,0,1,2],[0,-2,0,-2,-2,0,-2,0,0,2,0,-2,2,0,-2,0]],[[4,1,0,1,3],[0,-2,0,2,-2,0,-2,0,2,0,-2,0,0,-2,0,-2]],[[4,1,0,2,0],[0,-2,0,-2,0,2,0,-2,0,-2,0,-2,0,2,0,-2]],[[4,1,0,2,1],[0,-2,0,-2,0,-2,0,-2,-2,0,2,0,2,0,-2,0]],[[4,1,0,2,2],[0,-2,0,-2,0,2,0,-2,0,-2,0,-2,0,2,0,-2]],[[4,1,0,2,3],[0,-2,0,-2,0,-2,0,2,2,0,2,0,2,0,-2,0]],[[4,1,0,3,0],[0,-2,0,-2,2,0,-2,0,0,2,0,2,2,0,-2,0]],[[4,1,0,3,1],[0,-2,0,-2,2,0,2,0,2,0,-2,0,0,2,0,-2]],[[4,1,0,3,2],[0,-2,0,-2,2,0,-2,0,0,2,0,2,2,0,-2,0]],[[4,1,0,3,3],[0,-2,0,2,-2,0,-2,0,2,0,-2,0,0,-2,0,-2]],[[4,1,1,0,0],[0,-2,-2,0,0,2,2,0,0,-2,-2,0,0,-2,-2,0]],[[4,1,1,0,1],[0,-2,-2,0,0,2,-2,0,2,0,0,-2,2,0,0,2]],[[4,1,1,0,2],[0,-2,2,0,0,-2,-2,0,0,2,2,0,0,2,-2,0]],[[4,1,1,0,3],[0,-2,-2,0,0,2,-2,0,2,0,0,-2,2,0,0,2]],[[4,1,1,1,0],[0,2,-2,0,2,0,0,2,0,2,-2,0,-2,0,0,-2]],[[4,1,1,1,1],[0,-2,-2,0,2,0,0,-2,-2,0,0,-2,0,2,-2,0]],[[4,1,1,1,2],[0,2,-2,0,2,0,0,2,0,2,-2,0,-2,0,0,-2]],[[4,1,1,1,3],[0,-2,-2,0,2,0,0,-2,-2,0,0,-2,0,2,-2,0]],[[4,1,1,2,0],[0,-2,-2,0,0,-2,-2,0,0,2,2,0,0,-2,-2,0]],[[4,1,1,2,1],[0,-2,-2,0,0,-2,2,0,2,0,0,-2,2,0,0,2]],[[4,1,1,2,2],[0,-2,-2,0,0,-2,-2,0,0,2,2,0,0,-2,-2,0]],[[4,1,1,2,3],[0,-2,-2,0,0,-2,2,0,2,0,0,-2,2,0,0,2]],[[4,1,1,3,0],[0,2,-2,0,2,0,0,2,0,-2,2,0,-2,0,0,-2]],[[4,1,1,3,1],[0,2,-2,0,-2,0,0,2,2,0,0,-2,0,2,-2,0]],[[4,1,1,3,2],[0,2,-2,0,2,0,0,2,0,-2,2,0,-2,0,0,-2]],[[4,1,1,3,3],[0,2,-2,0,2,0,0,2,2,0,0,2,0,2,-2,0]],[[4,1,2,0,0],[0,-2,0,-2,0,2,0,-2,0,-2,0,-2,0,2,0,-2]],[[4,1,2,0,1],[0,-2,0,-2,0,-2,0,-2,-2,0,2,0,2,0,-2,0]],[[4,1,2,0,2],[0,-2,0,-2,0,2,0,-2,0,-2,0,-2,0,2,0,-2]],[[4,1,2,0,3],[0,-2,0,-2,0,-2,0,2,2,0,2,0,2,0,-2,0]],[[4,1,2,1,0],[0,-2,0,-2,-2,0,-2,0,0,2,0,-2,2,0,-2,0]],[[4,1,2,1,1],[0,-2,0,-2,2,0,2,0,-2,0,2,0,0,-2,0,2]],[[4,1,2,1,2],[0,-2,0,-2,-2,0,-2,0,0,2,0,-2,2,0,-2,0]],[[4,1,2,1,3],[0,-2,0,-2,2,0,2,0,-2,0,2,0,0,-2,0,2]],[[4,1,2,2,0],[0,-2,0,-2,0,2,0,-2,0,-2,0,-2,0,2,0,-2]],[[4,1,2,2,1],[0,-2,0,-2,0,-2,0,-2,-2,0,2,0,2,0,-2,0]],[[4,1,2,2,2],[0,-2,0,-2,0,2,0,-2,0,-2,0,-2,0,2,0,-2]],[[4,1,2,2,3],[0,-2,0,-2,0,-2,0,2,2,0,2,0,2,0,-2,0]],[[4,1,2,3,0],[0,-2,0,-2,2,0,-2,0,0,2,0,2,2,0,-2,0]],[[4,1,2,3,1],[0,-2,0,-2,2,0,2,0,2,0,-2,0,0,2,0,-2]],[[4,1,2,3,2],[0,-2,0,-2,2,0,-2,0,0,2,0,2,2,0,-2,0]],[[4,1,2,3,3],[0,-2,0,-2,-2,0,2,0,2,0,-2,0,0,-2,0,-2]],[[4,1,3,0,0],[0,-2,-2,0,0,-2,-2,0,0,2,2,0,0,-2,-2,0]],[[4,1,3,0,1],[0,-2,2,0,0,-2,-2,0,2,0,0,2,2,0,0,-2]],[[4,1,3,0,2],[0,-2,2,0,0,-2,-2,0,0,2,2,0,0,2,-2,0]],[[4,1,3,0,3],[0,-2,2,0,0,-2,-2,0,2,0,0,2,2,0,0,-2]],[[4,1,3,1,0],[0,-2,-2,0,2,0,0,-2,0,2,2,0,-2,0,0,2]],[[4,1,3,1,1],[0,2,-2,0,2,0,0,-2,-2,0,0,2,0,2,-2,0]],[[4,1,3,1,2],[0,-2,-2,0,2,0,0,-2,0,2,2,0,-2,0,0,2]],[[4,1,3,1,3],[0,2,-2,0,-2,0,0,-2,-2,0,0,-2,0,2,-2,0]],[[4,1,3,2,0],[0,-2,2,0,0,-2,-2,0,0,2,2,0,0,2,-2,0]],[[4,1,3,2,1],[0,-2,-2,0,0,2,-2,0,2,0,0,-2,2,0,0,2]],[[4,1,3,2,2],[0,-2,2,0,0,-2,-2,0,0,2,2,0,0,2,-2,0]],[[4,1,3,2,3],[0,-2,-2,0,0,2,-2,0,2,0,0,-2,2,0,0,2]],[[4,1,3,3,0],[0,2,-2,0,2,0,0,2,0,2,-2,0,-2,0,0,-2]],[[4,1,3,3,1],[0,2,-2,0,-2,0,0,2,2,0,0,-2,0,2,-2,0]],[[4,1,3,3,2],[0,2,-2,0,2,0,0,2,0,2,-2,0,-2,0,0,-2]],[[4,1,3,3,3],[0,2,-2,0,-2,0,0,-2,-2,0,0,-2,0,2,-2,0]],[[4,2,0,0,1],[0,0,0,0,0,0,0,0,-2,2,-2,2,2,-2,-2,2]],[[4,2,0,1,0],[0,0,0,0,-2,-2,2,2,0,0,0,0,2,-2,-2,2]],[[4,2,0,1,1],[0,0,0,0,-2,-2,-2,-2,-2,2,2,-2,0,0,0,0]],[[4,2,0,1,2],[0,0,0,0,-2,-2,2,2,0,0,0,0,2,-2,-2,2]],[[4,2,0,1,3],[0,0,0,0,-2,-2,-2,2,2,2,2,-2,0,0,0,0]],[[4,2,0,2,1],[0,0,0,0,0,0,0,0,2,-2,2,2,2,2,-2,2]],[[4,2,1,0,0],[0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0,2,-2]],[[4,2,1,0,1],[0,0,-2,-2,0,0,-2,-2,-2,2,0,0,2,-2,0,0]],[[4,2,1,0,2],[0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0,2,-2]],[[4,2,1,0,3],[0,0,-2,-2,0,0,-2,2,2,2,0,0,2,-2,0,0]],[[4,2,1,1,0],[0,0,-2,-2,-2,-2,0,0,0,0,2,-2,2,-2,0,0]],[[4,2,1,1,1],[0,0,2,2,2,-2,0,0,-2,2,0,0,0,0,2,2]],[[4,2,1,1,2],[0,0,-2,-2,-2,-2,0,0,0,0,2,-2,2,-2,0,0]],[[4,2,1,1,3],[0,0,2,2,2,-2,0,0,-2,2,0,0,0,0,2,2]],[[4,2,1,2,0],[0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0,2,-2]],[[4,2,1,2,1],[0,0,-2,-2,0,0,-2,-2,-2,2,0,0,2,-2,0,0]],[[4,2,1,2,2],[0,0,-2,2,0,0,-2,-2,0,0,-2,-2,0,0,2,-2]],[[4,2,1,2,3],[0,0,-2,-2,0,0,-2,2,2,2,0,0,2,-2,0,0]],[[4,2,1,3,0],[0,0,-2,-2,2,-2,0,0,0,0,2,2,2,-2,0,0]],[[4,2,1,3,1],[0,0,2,2,2,-2,0,0,-2,2,0,0,0,0,2,2]],[[4,2,1,3,2],[0,0,-2,-2,2,-2,0,0,0,0,2,2,2,-2,0,0]],[[4,2,1,3,3],[0,0,2,2,2,-2,0,0,-2,2,0,0,0,0,2,2]],[[4,2,2,0,1],[0,0,0,0,0,0,0,0,-2,2,-2,2,2,-2,-2,2]],[[4,2,2,1,0],[0,0,0,0,-2,-2,2,2,0,0,0,0,2,-2,-2,2]],[[4,2,2,1,1],[0,0,0,0,-2,2,-2,-2,2,2,-2,2,0,0,0,0]],[[4,2,2,1,2],[0,0,0,0,-2,-2,2,2,0,0,0,0,2,-2,-2,2]],[[4,2,2,1,3],[0,0,0,0,-2,2,-2,-2,2,2,-2,2,0,0,0,0]],[[4,2,2,2,1],[0,0,0,0,0,0,0,0,-2,-2,2,2,2,-2,-2,2]]]} diff --git a/research/four-axis-phase-covariant-grid/NOTICE.md b/research/four-axis-phase-covariant-grid/NOTICE.md new file mode 100644 index 0000000000..bd02d662d7 --- /dev/null +++ b/research/four-axis-phase-covariant-grid/NOTICE.md @@ -0,0 +1,44 @@ +# Attribution and source notices + +New work: @CubeJerry, with substantial OpenAI Codex assistance. The research +session used parallel AI work for the period-lattice and matching discovery, +compact quotient and independent proof/checker, and retained caller integration. +New files are released under the repository's Apache-2.0 license. + +Nick Petalas's #6574, `research/four-axis-reversible-grid`, head +`48e312ff18d5b66b0969148f615fdf5ce0f92edd`, supplies the sharp four-axis +Walsh reduction, native diagonal convention, error/correction predicates, +matching candidate family, literal inverse template and half-grid optimality +witness. The production block follows that endpoint convention and adapts its +reference structure to different input/output quotients. Its source notice is: +“This contribution was produced by Nick Petalas. Apache-2.0.” + +Ali Romman's #6509, `research/conservative-gaussian-rounding`, head +`a4173e810c4d34a1d13b9745af123ad0ec6cfed5`, supplies the actual retained +backend interface, conservative phase-covariant context, port proof and budget. +`inputs/retained_ports.py` and `inputs/retained_rounded.py` are unchanged copies +of its `ports.py` and `inputs/rounded.py`; their original file notices remain. +They are authenticated by `CALLER-SOURCES.json` before import. + +Brian / JoyboyBrian, with Codex assistance, supplies #5485's retained native +rounded-call implementation, exact monomial/mix program and port budget, head +`47c4e95f2aad7b33637aca3ac0dde0a0a2a9ebfe`. #4743, head +`158048812f4e0aeb132408f4d7cda57ba008b0d5`, is the underlying channel/port +lineage. These merged source heads are historical provenance; the imported +bytes are pinned at the #6509 snapshot actually consumed here. + +Ali Romman is also credited for #6536's three-axis construction and four-axis +question, #6534's two-axis construction, and #5821's Gaussian Smith execution. +David Ganz / Dugongue is credited for #5815's Gaussian Smith construction and +the retained Gaussian native conventions. Classical Walsh identities, lattice +quotients and bipartite matching are not claimed as new. + +ToikY's concurrent #6755 review, head +`4475dc90bbe6037981bfc8ce0dd55efb6bdbc6a0`, is credited for identifying the +remaining symmetry and caller/billing boundaries of #6574. It is not treated +as an execution certificate, source dependency or acceptance of this work. + +All predecessor mathematical claims retain their original authorship. This +package neither audits their full results nor transfers any admission from +them. Exact inspected-source and retained-file pins are in `SOURCES.json` and +`CALLER-SOURCES.json`. diff --git a/research/four-axis-phase-covariant-grid/PROOF.md b/research/four-axis-phase-covariant-grid/PROOF.md new file mode 100644 index 0000000000..bd5fb90ec3 --- /dev/null +++ b/research/four-axis-phase-covariant-grid/PROOF.md @@ -0,0 +1,404 @@ +# Sharp four-axis rounding with Gaussian phase covariance + +Prepared by @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +The native factorization, sharp half-grid witness and correction predicates +come from Nick Petalas's #6574. The new work is the minimal odd-compatible +period, its negation-equivariant matching, the compact quotient, and the +retained caller binding in [CALLER.md](CALLER.md). Exact sources and further +lineage credit are in [SOURCES.json](SOURCES.json) and [NOTICE.md](NOTICE.md). + +## 1. Statement and scope + +Index sixteen coordinates by four-bit integers, and put + +$$ + W_{rs}=(-1)^{\operatorname{popcount}(r\mathbin\&s)},\qquad + A=W/4,\qquad D_{jj}=(-i)^{\operatorname{popcount}(j)}. +$$ + +The native four-axis operator is + +$$ + U=(1+i)^{-4}\begin{pmatrix}i&1\\1&i\end{pmatrix}^{\otimes4} + =-DAD. +$$ + +Indeed, $(1+i)^4=-4$ and +$\operatorname{wt}(r\mathbin\oplus s)=\operatorname{wt}(r)+ +\operatorname{wt}(s)-2\operatorname{wt}(r\mathbin\&s)$, which gives +the displayed factorization entry by entry. + +**Theorem.** The finite certificate in this package defines a bijection +$F:\mathbb Z[i]^{16}\to\mathbb Z[i]^{16}$, with a literal inverse, +such that for all Gaussian integer vectors $x,y$: + +$$ +\begin{split} + F(0)&=0,\qquad F(ix)=iF(x),\qquad \sum_j F(x)_j=\sum_j x_j,\\ + \|F(x)-Ux\|_2&\le\sqrt8,\qquad + \|F^{-1}(y)-U^*y\|_2\le\sqrt8. +\end{split} +$$ + +Both error constants are sharp among all integer-output maps. For this +certificate, every complex coordinate error is at most $3\sqrt2/4$ +forward and $5\sqrt2/4$ inverse. The corresponding statements on a grid +$h\mathbb Z[i]$, for $h>0$, follow by scaling and multiply each +error by $h$. + +The real map used by $F$ has a full-rank affine period with exactly +2,048 classes. This is the smallest possible period index for any odd map +approximating $A$ in the affine-period sense defined below, irrespective +of its error bound or bijectivity. The resulting native period has index +$2^{22}=4,194,304$, also minimal among globally odd native maps with such +a period, including maps with coupled real/imaginary corrections. +These statements concern quotient indices, not minimum table bytes, lookup +costs, or arbitrary nonperiodic algorithms. + +The particular $F$ does **not** satisfy $F^4=I$. A checked exact +counterexample appears in Section 8. The proof is a scoped mathematical +argument with a finite certificate checked by exact Python arithmetic; it +is not a formal proof-kernel verification or a multiplication theorem. + +## 2. Why the predecessor quotient cannot be odd + +The Walsh identities give $A^2=I$, and $A$ is orthogonal. Define + +$$ + L=\{z\in\mathbb Z^{16}:Az\in\mathbb Z^{16}\}. +$$ + +For an integer vector $z$, let +$T=\sum_s z_s$ and $B_j=\sum_{s:\operatorname{bit}_j(s)=1}z_s$. +Expansion of the signs modulo four gives + +$$ + (Wz)_r\equiv T-2\sum_j\operatorname{bit}_j(r)B_j\pmod4. +$$ + +Consequently $z\in L$ exactly when $T=0\pmod4$ and all four +$B_j=0\pmod2$. The homomorphism +$z\mapsto(T\bmod4,B_0\bmod2,\ldots,B_3\bmod2)$ is onto: +$e_0$ supplies the first factor and $e_{2^j}-e_0$ supplies each +binary factor. Thus + +$$ + \mathbb Z^{16}/L\simeq\mathbb Z/4\oplus(\mathbb Z/2)^4, + \qquad [\mathbb Z^{16}:L]=64. +$$ + +#6574 uses a fixed correction on each of these 64 classes. Consider any +map $R(z)=(Wz+e(Wz\bmod4))/4$ of that form. The inputs $2e_0$ +and $-2e_0$ have the same residue $(2,\ldots,2)$. Oddness would +therefore force its correction to satisfy $e=-e$, hence $e=0$. +But zero cannot cancel that residue modulo four. This rules out oddness in +the fixed 64-class architecture. It does not rule out refinement, extra +state, or a different architecture. The construction below refines it. + +## 3. A compact quotient of index 2,048 + +Let $H=(7,11,13,14,15)$ and + +$$ + Q=\mathbb Z/8\oplus(\mathbb Z/4)^4. +$$ + +Define the source homomorphism $\alpha:\mathbb Z^{16}\to Q$ by + +$$ + \alpha_0(z)=4z_7-T\pmod8,\qquad + \alpha_{j+1}(z)=2z_{H_{j+1}}-B_j\pmod4\quad(0\le j<4). +$$ + +For $a=(a_0,\ldots,a_4)\in Q$, using canonical nonnegative residues, +the vector + +$$ + r(a)=\Bigl(\sum_{j=1}^4a_j-a_0\Bigr)e_0 + -\sum_{j=0}^3a_{j+1}e_{2^j} +$$ + +has $\alpha(r(a))=a$. Hence $\alpha$ is onto. Write +$\Lambda=\ker\alpha$. It has index 2,048, and $\Lambda\subset L$: +$\alpha_0(z)=0$ forces $T=0\pmod4$, while the other equations +force all $B_j$ even. + +The output quotient is different. For $v=Wy$, define + +$$ + \beta_0(y)=v_7-4y_0\pmod8,\qquad + \beta_{j+1}(y)=\frac{v_{H_{j+1}}-v_7}{2}+2y_{2^j}\pmod4. +$$ + +Each numerator in the half difference is even for every integer $y$, +so this is an integer homomorphism. It is onto. One explicit section is +as follows: if the final four coordinates of a key are $(a,b,c,d)$, put + +$$ + (t_0,t_1,t_2,t_3)= + (2a+c+3d,\ 3b+3d,\ a+2c+3d,\ d)\pmod4, +$$ + +set $y_{2^j}=t_j$, set +$y_0=5(a_0+t_0+t_1+t_2-t_3)\pmod8$, and set all other +coordinates to zero. Substitution gives $\beta(y)=a$. + +For $z\in L$ and $y=Az$, the unreduced expressions satisfy + +$$ + \beta_0(y)=4z_7-T,\qquad + \beta_{j+1}(y)=2z_{H_{j+1}}-B_j-(4z_7-T)/2 +$$ + +with the respective moduli understood. Thus $A\Lambda\subset\ker\beta$. +Since $|\det A|=1$, both lattices have index 2,048, giving + +$$ + A\Lambda=\ker\beta. +$$ + +It follows that $\alpha$ classifies the source cosets and $\beta$ +classifies the target cosets. The target table must use $\beta$; +substituting the source classifier is not a justified inverse. + +### Independent lattice normal forms + +The checker reconstructs lattice bases without using these quotient formulas. +Let $u_0=4e_0$, $u_{j+1}=2(e_{2^j}-e_0)$, and, for +$\operatorname{wt}(s)\ge2$, let + +$$ + k_s=e_s+(\operatorname{wt}(s)-1)e_0 + -\sum_{j:\operatorname{bit}_j(s)=1}e_{2^j}. +$$ + +The five $u$'s followed by the eleven $k$'s form an integral basis +of $L$. For each $s\in H$, put +$v_s=k_s-\sum_{t\subset s,\operatorname{wt}(t)=2}k_t$. +A basis matrix $M$ for $\Lambda$ has columns + +$$ + (u_i+v_{H_i})_{i=0}^4,\quad + (k_s)_{\operatorname{wt}(s)=2},\quad + (2v_s)_{s\in H}. +$$ + +Replacing the five high-weight $k_s$'s by $v_s$'s is an integral +unimodular column change. Relative to the resulting basis of $L$, the +five replacements $(u_i,v_{H_i})\mapsto(u_i+v_{H_i},2v_{H_i})$ +each have determinant two. Thus $|\det M|=64\cdot2^5=2048$. +Direct substitution gives $\alpha(M)=0$, so the index calculation +also proves that these columns span exactly $\Lambda$. + +The checker obtains $|\det M|=|\det(AM)|=2,048$, verifies +$\alpha(M)=0$, $\beta(AM)=0$, and computes the inverse matrices +over the rationals. Both inverses become integral after multiplication by +eight. The sixteen-coordinate residues $8M^{-1}z\bmod8$ and +$8(AM)^{-1}y\bmod8$ independently classify all 2,048 representatives +on each side. This is a separate normal-form check of the compact quotient. + +## 4. The finite negation-equivariant matching + +Negation on $Q$ is coordinatewise. It has 32 fixed keys, with +$a_0\in\{0,4\}$ and $a_j\in\{0,2\}$ for $j>0$, and +$(2048-32)/2=1008$ free pairs. The certificate contains one row for +each free pair, using the lexicographically smaller key. Each row supplies +an integer correction $e(a)$; define $e(-a)=-e(a)$. Set $e=0$ +at every fixed key. + +For a source key $a$, compute + +$$ + y(a)=\frac{Wr(a)+e(a)}4,\qquad p(a)=\beta(y(a)). +$$ + +The finite certificate checker verifies all of the following: + +1. Every key occurs exactly once; every correction has sixteen integer entries. +2. $Wr(a)+e(a)$ is divisible by four coordinatewise. +3. $\|e(a)\|_2^2\le64$ and $\sum_jD_{jj}e(a)_j=0$. +4. $e(-a)=-e(a)$, including zero at the 32 fixed keys. +5. The 2,048 target keys $p(a)$ are distinct and exhaust $Q$. +6. The inverse offsets $f(p(a))=-We(a)/4$ are integers, have squared + norm at most 64, and satisfy $\sum_jD_{jj}f(p(a))_j=0$. +7. All forward correction coordinates have magnitude at most 3; all inverse + correction coordinates have magnitude at most 5. Both maxima are attained. + +The fixed classes require no search: $Ar(a)$ is integral and their +target keys are +$(a_0,a_1-a_0/2,\ldots,a_4-a_0/2)$ with the displayed moduli. +This permutes the 32 fixed keys. The remaining rows were obtained by a +finite bipartite matching on free negation orbits using the predecessor's +admissible correction candidates. The witness is retained directly, so replay +needs no matching solver, search transcript or assertion of search completeness. +Its correctness depends only on the checked predicates. + +## 5. The all-integer real map and its inverse + +Define + +$$ + R(z)=\frac{Wz+e(\alpha(z))}{4}. +$$ + +If $z=r(a)+\lambda$ with $\lambda\in\Lambda$, then +$R(z)=y(a)+A\lambda$. This is an integer vector, and its target key +is $p(a)$. On each source coset the map is the affine lattice bijection +$\lambda\mapsto A\lambda$ from $\Lambda$ onto $A\Lambda$. +The finite permutation of cosets therefore proves that $R$ is bijective +on **all** integer vectors, not merely on the tested representatives. + +The literal inverse is + +$$ + R^{-1}(y)=\frac{Wy+f(\beta(y))}{4},\qquad f(p(a))=-We(a)/4. +$$ + +Indeed, if $y=Az+e(a)/4$, then +$Ay=z+Ae(a)/4$, and $f(p(a))=-Ae(a)$ cancels the latter term. +This also proves inverse integrality throughout each target coset. +Orthogonality gives $\|f\|_2=\|e\|_2$, so both real errors are at +most 2. Linearity of $\alpha$ and the opposite corrections imply +$R(-z)=-R(z)$. Its inverse is odd as well. At the zero class the +correction vanishes, so $R(0)=0$. + +## 6. Native phase, sum, inverse and sharp error + +Extend the real map componentwise: +$R_{\mathbb C}(a+ib)=R(a)+iR(b)$. Then define + +$$ + F(x)=-D R_{\mathbb C}(Dx),\qquad + F^{-1}(y)=D^{-1}R_{\mathbb C}^{-1}(-D^{-1}y). +$$ + +These are literal inverse bijections of the Gaussian lattice. Oddness of +$R$ is precisely what makes this componentwise extension commute with +global multiplication by $i$: +$R_{\mathbb C}(i(a+ib))=R(-b)+iR(a)=iR_{\mathbb C}(a+ib)$. +Diagonal quarter rotations commute with global $i$, so both $F$ +and its inverse have Gaussian phase covariance. Iterating this identity also +gives covariance under the other Gaussian units. + +The ideal $U$ is unitary and preserves the sum because each one-axis +matrix has those properties. The forward error is a diagonal rotation of +$(e_{\rm re}+ie_{\rm im})/4$. Its sum is zero by the two real +weighted-sum checks, and its squared norm is at most +$(64+64)/16=8$. For the inverse, use the offsets $f$ and +$D^{-1}$; the required weighted sum is the complex conjugate of the +checked weighted sum for each real offset. The same error bound follows. +The coordinate bounds follow from +$\sqrt{3^2+3^2}/4=3\sqrt2/4$ and +$\sqrt{5^2+5^2}/4=5\sqrt2/4$. + +For sharpness, take $x=(2+2i)e_0$. Every coordinate of $Ux$ has +both real and imaginary part equal to a signed half-integer. Every Gaussian +integer output therefore has squared distance at least $1/2$ in each +of sixteen coordinates, hence at least 8 in total. The same argument applies +to $U^*x$. Our upper bounds attain these unavoidable lower bounds. + +For independent sixteen-point fibers in an $N$-coordinate field, squared +errors add, giving the sharp uniform bound $h\sqrt{N/2}$. The retained +caller proof in [CALLER.md](CALLER.md) uses the stronger coordinate constants +to lower its grid request by two fractional bits at exactly $f=4$. + +## 7. Minimal affine-period indices + +An **affine period lattice** for an integer-output map $R$ relative to +$A$ is a full-rank sublattice $\Gamma\subset\mathbb Z^{16}$ +such that + +$$ + R(z+\lambda)=R(z)+A\lambda + \quad\text{for every }z\in\mathbb Z^{16},\ \lambda\in\Gamma. +$$ + +Necessarily $\Gamma\subset L$. Suppose $R$ is odd. If +$\lambda\in\Gamma\cap2\mathbb Z^{16}$, apply the period identity +at $-\lambda/2$ and use oddness: +$2R(\lambda/2)=A\lambda$. Thus $A\lambda$ is even and +$\lambda/2\in L$, so + +$$ + \Gamma\cap2\mathbb Z^{16}\subset2L. +$$ + +In $V=L/2L$, the subspace +$E=(L\cap2\mathbb Z^{16})/2L$ is isomorphic to +$(\mathbb Z^{16}/L)[2]$: send the class of $z$, with $2z\in L$, +to $2z+2L$. From the quotient in Section 2, $\dim E=5$, while +$\dim V=16$. The image +$J=(\Gamma+2L)/2L$ meets $E$ trivially, so $\dim J\le11$. +Consequently + +$$ + [L:\Gamma]\ge[L:\Gamma+2L]\ge2^5,\qquad + [\mathbb Z^{16}:\Gamma]\ge64\cdot32=2048. +$$ + +This argument does not assume $2L\subset\Gamma$, does not use a +radius bound, and does not require bijectivity. The period $\Lambda$ +of the constructed odd map attains the bound. For a bijective odd map, +applying the same reasoning to the inverse also forces +$\lambda$ even if and only if $A\lambda$ is even on its period. +The reconstructed bases independently check this two-sided condition. + +For the native extension, regard $Z=\mathbb Z[i]^{16}$ as a rank-32 +integer lattice. Its integrality lattice is + +$$ + L_U=\{x\in Z:Ux\in Z\}=D^{-1}(L+iL), + \qquad Z/L_U\simeq(\mathbb Z/4\oplus(\mathbb Z/2)^4)^2. +$$ + +It has index $2^{12}$, and its even-class subspace +$(L_U\cap2Z)/2L_U$ has dimension 10. Any globally odd native map +with full-rank affine period $\Gamma$ satisfies +$\Gamma\cap2Z\subset2L_U$, by the same half-period argument. +Its image in $L_U/2L_U$, a 32-dimensional vector space, has dimension +at most 22. Thus + +$$ + [Z:\Gamma]\ge2^{12}\,2^{10}=2^{22}=4,194,304. +$$ + +Gaussian phase covariance implies global oddness, so this includes coupled +real/imaginary correction tables. The constructed native map has period +$D^{-1}(\Lambda+i\Lambda)$, of index $2048^2=2^{22}$, and the +appropriate affine image under $U$. It attains this native bound while +sharing the same real correction table between both components. Nothing in +this proof gives a memory lower bound: separability, table compression, +algebraic evaluation and nonperiodic schemes are separate questions. + +## 8. Exact fourth-power failure and verification limits + +The ideal operator has $U^2=J$, where $J$ complements all four +coordinate bits, and $U^4=I$. The certified rounded map instead has + +$$ + F^4(e_0)=e_0-ie_1-ie_4-ie_7-e_{10}+e_{12}+2ie_{13}+ie_{14}\ne e_0. +$$ + +The checker computes and retains this exact vector. It proves failure for +this particular certificate, not impossibility for a different sharp +phase-covariant map. The retained two-/three-call ports require the literal +inverse, so their exact dirty-bank return does not require the failed identity. + +`verify.py` checks all real source and target classes, rational period normal +forms, the complete matching, literal real round trips and all finite error +and sum predicates. A separate native-coefficient oracle checks 4,096 paired +complex fixtures, both sharp witnesses, and signed large-word fixtures. It +does not enumerate all $2048^2$ complex class pairs; the componentwise +proof establishes their universal coverage. Failure controls preserve local +correction admissibility while breaking negation or creating a target collision, +and also reject a corrupted period, wrong native phase, a false smaller radius, +forward-as-inverse substitution, and malformed executable inputs. + +The mathematical formulas are defined on every integer vector. `kernel.py` +places a 4,096-bit-per-component guard on its public reference entry point; +4,090-bit fixtures leave room for intermediate round-trip growth. This guard +is not a mathematical restriction of the theorem. The retained caller has its +own explicitly checked signed-word interface. Neither replay establishes +norm-inward rounding, a nearest-output rule, graph flatness, a Boolean/tape +lowering, complete compiler costs, or any of the selected multiplier's five +inherited assumptions. diff --git a/research/four-axis-phase-covariant-grid/README.md b/research/four-axis-phase-covariant-grid/README.md new file mode 100644 index 0000000000..b2ec3b274a --- /dev/null +++ b/research/four-axis-phase-covariant-grid/README.md @@ -0,0 +1,201 @@ +# Sharp phase-covariant four-axis Gaussian rounding + +**A sharp reversible Gaussian lattice map can acquire global phase covariance +by refining its period quotient.** This package adds that symmetry to Nick +Petalas's four-axis construction in +[#6574](https://github.com/CrocSwap/integer-mult-bounds/pull/6574), retains +its optimal Euclidean error, exact complex sum and literal inverse, and binds +the new map to the actual two-/three-call dirty-bank ports retained in Ali +Romman's [#6509](https://github.com/CrocSwap/integer-mult-bounds/pull/6509). +At exactly four axes, the retained callers use two fewer fractional bits and +two fewer signed component bits for the same stated external accuracy. + +The phase-compatible period is provably minimal within the full-rank +affine-period model. The particular certified map fails exact fourth power; +that boundary is recorded explicitly. This is a scoped written proof with +exact finite certificates and caller replays. It supplies no new kappa and +discharges none of the selected multiplication result's five assumptions. + +## Results + +Write $W_{rs}=(-1)^{\operatorname{popcount}(r\mathbin\&s)}$, +$D_{jj}=(-i)^{\operatorname{popcount}(j)}$, and $U=-DWD/4$. +This is the retained native four-axis Gaussian operator on sixteen entries. +The package constructs a bijection $F:\mathbb Z[i]^{16}\to\mathbb Z[i]^{16}$ +with a literal inverse and the following guarantees. + +| Property | Result | +|---|---| +| Global Gaussian phase | $F(ix)=iF(x)$, and the inverse has the same covariance | +| Conserved quantity | The complex sum is preserved exactly; zero is fixed | +| Uniform Euclidean error | $\sqrt8\,h$ for both the forward and adjoint ideal operator, sharp among all grid-output rules | +| Coordinate error | At most $3\sqrt2\,h/4$ forward and $5\sqrt2\,h/4$ inverse | +| Real correction quotient | 2,048 classes, with 32 negation-fixed classes and 1,008 free pairs | +| Minimum real affine-period index | 2,048 for any odd map with ideal linear part $W/4$ | +| Minimum native affine-period index | 4,194,304, including coupled real/imaginary maps; attained by the componentwise construction | +| Exact fourth power | Fails for this certificate; an explicit $F^4(e_0)\ne e_0$ witness is retained | + +The period lower bounds count cosets, not unavoidable table bytes or physical +operations. The native map reuses the same real correction tables for both +components. No 4,194,304-row native table is stored. A nonperiodic architecture +is outside the lower-bound theorem. + +The predecessor uses 64 real quotient classes. The refined construction uses +32 times as many; the lower bound proves that this increase is necessary for +oddness within the affine-period model. Its benefit is a stronger symmetry +contract at the same sharp error. The larger classification and lookup remain +part of the implementation cost. + +The mechanism is an odd real map $R(z)=(Wz+e(\alpha(z)))/4$, where +$\alpha$ takes values in $\mathbb Z/8\oplus(\mathbb Z/4)^4$. +The output uses a different quotient $\beta$. A finite matching assigns +opposite offsets to opposite classes; a class bijection plus its exact period +map proves the all-integer bijection. Then $F=-D R_{\mathbb C}D$, with +the same $R$ on real and imaginary parts. The complete argument, compact +classifiers, minimal-period theorem and sharpness witness are in +[PROOF.md](PROOF.md). + +## Actual retained caller benefit + +[CALLER.md](CALLER.md) binds the map to the unchanged two-/three-call port +bodies from #6509, at $f=4$, $N=8^4=4096$, and native axes zero and +two. Each call partitions the field into 256 sixteen-point spectator fibers. +Literal reverse execution restores both stored dirty banks for arbitrary values +within the stated no-overflow domain, in either composition order. The proof uses +the true inverse of each rounded block; +it does not require the failed fourth-power identity. + +Because both coordinate constants are less than 2, a completed call requesting +tolerance $2^{-q}$ can use $g=q+1$, replacing the predecessor's +$g=q+3$ at four axes. The retained source-ordered external requests stay +unchanged: + +| Port direction | Call request $q$ | New grid exponent $g$ | Prior $g$ | +|---|---|---|---| +| Two calls forward | $P+7$ | $P+8$ | $P+10$ | +| Three calls forward | $P+9$ | $P+10$ | $P+12$ | +| Two calls reverse | $P+4$ | $P+5$ | $P+7$ | +| Three calls reverse | $P+6$ | $P+7$ | $P+9$ | + +For original coordinate magnitude at most $2^H$, the retained width formula +is $w=H+g+19$, so the width also falls by two. The new largest raw +numerator is bounded by $16M+5$ for input components of magnitude at most +$M$, within that width margin. Initial quantization remains separately +charged. The full field Euclidean error is $h\sqrt{N/2}$, compared with +the predecessor's four-layer triangle bound $4h\sqrt{N/2}$. + +The fast reference block uses 160 full-word additions/subtractions and 32 exact +quarter shifts. Classification, table access, signs, reads, writes, range checks, +and scratch/control cleanup are additional payable work; [CALLER.md](CALLER.md) +states the direct implementation bound and retained monomial/mix costs. No +accelerated recursive tariff, physical tape schedule, supplier admission or +complete multiplication improvement follows from saving two retained bits. + +## Evidence and reproduction + +The package uses CPython 3.12 and its standard library. From the repository root: + +```sh +python3.12 -W error -B research/four-axis-phase-covariant-grid/verify.py +python3.12 -O -W error -B research/four-axis-phase-covariant-grid/verify.py +python3.12 -W error -B research/four-axis-phase-covariant-grid/verify_caller.py +python3.12 -O -W error -B research/four-axis-phase-covariant-grid/verify_caller.py +python3.12 -B scripts/research_package.py --package research/four-axis-phase-covariant-grid --check-only +python3.12 -B scripts/research_package.py --package research/four-axis-phase-covariant-grid +python3.12 -B scripts/check_research_commit.py --package research/four-axis-phase-covariant-grid --check-modes +python3.12 -B scripts/check_research_commit.py --package research/four-axis-phase-covariant-grid --check-source-history +``` + +The package runner registers ordinary and optimization-mode checks for both +verifiers. Its fresh bytecode namespace binds imports to the current source +files. The final source-history command requires the package to be committed. +All verifiers write only stdout and do not regenerate shared files. + +Executed with CPython 3.12.14: both verifiers passed in normal and optimization +modes, the registered package replay and metadata/pin checks passed, and the +committed-byte/mode preflight passed. The source-history preflight was attempted +but refused to run because the supplied repository is shallow; it requires full +Git history. That unavailable gate is not reported as a pass. The source-pinned +retained port has an original trailing blank line; its exact bytes are preserved. + +`verify.py` reconstructs the period matrices with rational arithmetic and +classifies cosets using their inverse matrices, independently of the production +compact quotient formulas. It checks all 2,048 source classes and all 2,048 +target classes, all matching rows, the literal inverse, both coordinate maxima, +weighted sums and sharp energy. A direct native coefficient oracle checks +4,096 paired complex fixtures, sharp forward/inverse witnesses, and eight +signed/large-word fixtures, with components through 4,090 bits. Eleven failure +controls include a locally admissible but colliding matching, broken negation, +a corrupted period, wrong phase, wrong inverse and a false smaller radius. +The core replay emits a receipt with exact file hashes and the fourth-power +counterexample. The all-input theorem follows from the coset and componentwise +proof; no claim is made to enumerate all $2048^2$ complex class pairs. + +`verify_caller.py` checks fast/dense block equality on 4,096 quotient fixtures, +16 port-direction cases over four dirty-bank families, 40 actual paid input +cuts, both exact composition orders, phase covariance, every spectator-fiber +sum and the full transform/correction arithmetic counts. Four additional +boundary-grid cases exercise the reduced precision and word width. Five +failure controls cover aliasing, unsupported size, overflow, forward-as-inverse +substitution and a wrong native axis that fails the operator error bound. + +The mathematical formulas apply to all integers. The public dense reference +kernel rejects components above 4,096 bits; this executable guard is separate +from the proof. The finite-word caller checks its own stated signed width. +Neither checker uses floating point, a numerical tolerance or Python `assert` +for a proof-relevant predicate. + +## Sources, scope and attribution + +Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, +selected #6030. [TASK.json](TASK.json) preserves the full original +`uniform-transfer-audit` card and records the changed scope: one pending native +precision interface, not a discharge of an all-size inherited assumption. +The original metadata baseline was blocked by sparse omitted inputs; this +package does not claim that baseline or the selected multiplier replay passed. + +Nick Petalas's #6574 is pinned at +`48e312ff18d5b66b0969148f615fdf5ce0f92edd`. Its sharp four-axis error, +native factorization, correction predicates and half-grid lower bound are +predecessor results. The new contribution is the compatible period/matching, +phase covariance, minimal-period proof, compact quotient and retained caller +precision binding. Ali Romman's #6509 is pinned at +`a4173e810c4d34a1d13b9745af123ad0ec6cfed5`; the exact retained caller files +are vendored with SHA256 and Git-blob checks before import. Brian / JoyboyBrian's +#5485 and the #4743 channel lineage supply the retained rounded port context. +Further native lineage credit is retained in [NOTICE.md](NOTICE.md). + +[SOURCES.json](SOURCES.json) pins the historical task/selected provenance through +Git and separately records the external source heads and inspected file bytes. +[CALLER-SOURCES.json](CALLER-SOURCES.json) authenticates the two local retained +caller files. Pending predecessor commits need not be present in a clean +checkout: their external publication ancestry is recorded, not proved by the +repository's source-history checker. No live predecessor file or network service +is needed for replay. Package-local files trigger replay automatically, so +there are no undeclared external runtime inputs. + +The concurrent review in #6755 (ToikY, +`4475dc90bbe6037981bfc8ce0dd55efb6bdbc6a0`) identified phase covariance, +fourth power and actual caller/rounding costs as open scope. It is credited as +review context, not a mathematical dependency or endorsement of this package. +No norm-inward condition, pointwise nearest-output property, native graph +flatness, formal proof review or physical compiler lowering is claimed. + +## Open next questions + +1. **Can sharp phase covariance coexist with exact fourth power?** The displayed + certificate fails on $e_0$. A next experiment should impose the four-step + orbit relation on a precisely declared quotient or additional state, then + recheck the sharp error, sum and literal inverse together. Negation matching + alone supplies no such relation; no general obstruction has been proved. +2. **Does the two-bit precision gain survive a complete physical bill?** Lower + the fast transforms, residue classifiers and shared lookup into one declared + reversible Boolean/tape implementation, including routing, scratch return, + source traffic and compiler stock, before comparing its complete paid profile + with a current supplier. The local state count and arithmetic savings do not + price those operations or establish an all-size port implementation. + +The structured questions and blockers are in [TASK.json](TASK.json). New work +was prepared by @CubeJerry with substantial OpenAI Codex assistance, including +parallel period/matching, compact-quotient proof/checker and caller-integration +work. All new work is Apache-2.0; retained files preserve their original notices. diff --git a/research/four-axis-phase-covariant-grid/SOURCES.json b/research/four-axis-phase-covariant-grid/SOURCES.json new file mode 100644 index 0000000000..1f55abc56a --- /dev/null +++ b/research/four-axis-phase-covariant-grid/SOURCES.json @@ -0,0 +1,81 @@ +{ + "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" + } + ], + "external_provenance": [ + { + "repository": "petalas/integer-mult-bounds", + "pull_request": "CrocSwap/integer-mult-bounds#6574", + "commit": "48e312ff18d5b66b0969148f615fdf5ce0f92edd", + "author": "Nick Petalas", + "usage": "Inspected predecessor mathematics and candidate family; not a runtime input or an imported pending Git object.", + "files": [ + { + "path": "research/four-axis-reversible-grid/README.md", + "size": 5145, + "sha256": "3de89dd46929a80ed6b15138cf3702507b7888b1c6cf9a2437e6827f7f783bdb", + "git_blob": "93fad26d02f1a5c2691af1a3ad21639fcbe59b7a" + }, + { + "path": "research/four-axis-reversible-grid/PROOF.md", + "size": 7584, + "sha256": "ea1433e935d65d84bcefbe8d933122ca1a179ab710859e4ac87ba07c85ea7250", + "git_blob": "fc3baa1e271cd89acabcb40248fb5e17dfdfac59" + }, + { + "path": "research/four-axis-reversible-grid/construction.py", + "size": 4140, + "sha256": "e9d1ab29c12d1f55261231b1d4188600e0abc0f5c740083c8177ef99eeaff47f", + "git_blob": "c80d588ef9ca33494ca78b8abd737e6e8722b4c4" + }, + { + "path": "research/four-axis-reversible-grid/kernel.py", + "size": 1805, + "sha256": "96da171633fe15cb491c184af893304b752af9e1875360b5bc21f02a1c65a9fe", + "git_blob": "883c1c317d2d4394f534e785a5d46b443549db9a" + } + ] + }, + { + "repository": "aliromman/integer-mult-bounds", + "pull_request": "CrocSwap/integer-mult-bounds#6509", + "commit": "a4173e810c4d34a1d13b9745af123ad0ec6cfed5", + "author": "Ali Romman", + "usage": "Two unchanged package-local retained caller sources, authenticated before import.", + "manifest": "CALLER-SOURCES.json" + } + ], + "cited_lineage": [ + { + "pull_request": "CrocSwap/integer-mult-bounds#5485", + "commit": "47c4e95f2aad7b33637aca3ac0dde0a0a2a9ebfe", + "author": "Brian / JoyboyBrian", + "usage": "Retained rounded port and source-ordered budget lineage, consumed at the #6509 snapshot." + }, + { + "pull_request": "CrocSwap/integer-mult-bounds#4743", + "commit": "158048812f4e0aeb132408f4d7cda57ba008b0d5", + "usage": "Underlying retained channel and port lineage." + }, + { + "pull_request": "CrocSwap/integer-mult-bounds#6755", + "commit": "4475dc90bbe6037981bfc8ce0dd55efb6bdbc6a0", + "author": "ToikY", + "usage": "Concurrent review context only; not a proof dependency, execution certificate or endorsement." + } + ], + "external_pin_boundary": "External head/file pins document inspected provenance. Generic Git source-history validation covers the files inventory only; caller.py independently checks package-local retained bytes. No pending commit, scratch path or network request is required for replay." +} diff --git a/research/four-axis-phase-covariant-grid/TASK.json b/research/four-axis-phase-covariant-grid/TASK.json new file mode 100644 index 0000000000..bac9a8e28d --- /dev/null +++ b/research/four-axis-phase-covariant-grid/TASK.json @@ -0,0 +1,96 @@ +{ + "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 and certify a sharp phase-covariant four-axis Gaussian lattice bijection with literal inverse, determine its affine-period state requirement and fourth-power behavior, and bind it to the retained f=4 dirty ports and precision budget.", + "scope_change_reason": "The assigned uniform-transfer audit was narrowed to the open symmetry and actual-caller precision interface of pending #6574 and #6509. The old 64-class correction architecture cannot be odd; one evidence-driven refinement to a larger period quotient yields a constructive phase result. This is not closure of an inherited all-size assumption.", + "bottleneck_link": "The complex native service is the selected construction bottleneck. The new map strengthens one precision_tape/native_all_columns interface and saves two retained fractional bits at exactly f=4. Its lookup, physical routing and compiler stock remain payable and unadmitted; no complete signed paid profile or kappa changes.", + "budget_minutes": 90, + "stop_rule": "Stop after an independently checked sharp phase-compatible finite certificate, a scoped minimum affine-period theorem, an exact fourth-power witness and one source-bound retained caller. Preserve unknown physical tariffs and all five selected assumptions; do not extend local success into a full supplier claim.", + "outcome": "partial", + "evidence": "PROOF.md proves the all-integer map and minimal affine-period indices. verify.py checks all 2048 source and 2048 target classes, literal inverses, sharp error, 3/5 coordinate maxima and eleven failure controls. CALLER.md and verify_caller.py bind f=4 retained two-/three-call ports, 16 direction cases, 40 actual input cuts, four reduced-grid cases and five controls.", + "author": "@CubeJerry, with substantial AI assistance (lead period/matching; Worker B compact quotient/proof/checker)", + "ai_assistance": "Substantial OpenAI Codex assistance: lead period-lattice derivation and negation-orbit matching search; Worker B compact quotient, proof, exact certificate oracle and packaging; lead retained-caller integration and independent source review. Integer/rational Python experiments and independent cross-checks were used. No human proof-kernel audit is claimed.", + "open_questions": [ + { + "question": "Can a sharp phase-covariant four-axis Gaussian map also satisfy exact fourth power?", + "why_it_matters": "The present certificate fails F^4=I on e0; native algebraic graph identities require a separate contract beyond literal inverse and global phase.", + "first_step": "Declare one finite period or additional state and impose four-step orbit constraints together with sharp error, exact sum and literal inverse; keep the present counterexample as a control.", + "blocked_by": "Negation matching supplies no fourth-power relation, and no generic impossibility or alternative certificate is established." + }, + { + "question": "Does the two-bit retained precision gain survive a complete physical implementation bill?", + "why_it_matters": "Finite table size and full-word arithmetic counts do not price lookup, physical routing, scratch return or compiler stock, so the local gain cannot yet change the selected multiplier.", + "first_step": "Lower the f=4 fast transforms, residue classifiers and shared lookup into one declared reversible Boolean/tape implementation and compare the complete paid profile at an exact current caller.", + "blocked_by": "Physical lowering, source traffic, routing and compiler-stock costs remain unproved; the retained caller theorem is only for f=4." + } + ], + "verification_boundary": { + "selected_baseline": "Not passed: the initial baseline command was blocked by sparse omitted inputs. No selected supplier replay is claimed.", + "phase_result": "All-integer scoped proof with exact finite certificate.", + "fourth_power": "Explicit failure for this certificate; general feasibility remains open.", + "publication": "Local work only; scientific admission and selected-frontier changes unclaimed.", + "source_history": "Attempted but unavailable: check_research_commit.py --check-source-history requires full Git history and the supplied repository is shallow. Ordinary committed-byte and executable-mode preflight passed; no source-history PASS is claimed." + } +} diff --git a/research/four-axis-phase-covariant-grid/VERIFY.json b/research/four-axis-phase-covariant-grid/VERIFY.json new file mode 100644 index 0000000000..af85e742d2 --- /dev/null +++ b/research/four-axis-phase-covariant-grid/VERIFY.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact rational period normal forms, all source/target classes, negation matching, inverse, sharp error, 3/5 coordinate maxima, native symmetry and eleven meaningful failure controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact rational period normal forms, all source/target classes, negation matching, inverse, sharp error, 3/5 coordinate maxima, native symmetry and eleven meaningful failure controls. Optimization-mode control: proof predicates remain active." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify_caller.py" + ], + "timeout_seconds": 180, + "checks": "Exact retained f=4 ports, fast/dense agreement, both dirty-bank composition orders, actual paid cuts, full-word operation counts, reduced-grid/width boundaries and five failure controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify_caller.py" + ], + "timeout_seconds": 180, + "checks": "Exact retained f=4 ports, fast/dense agreement, both dirty-bank composition orders, actual paid cuts, full-word operation counts, reduced-grid/width boundaries and five failure controls. Optimization-mode control: proof predicates remain active." + } + ] +} diff --git a/research/four-axis-phase-covariant-grid/caller.py b/research/four-axis-phase-covariant-grid/caller.py new file mode 100644 index 0000000000..523888ec6c --- /dev/null +++ b/research/four-axis-phase-covariant-grid/caller.py @@ -0,0 +1,115 @@ +"""Checked four-axis backend for the retained dirty ports. + +@CubeJerry with substantial OpenAI Codex assistance; Apache-2.0. +Retained port schedules are by Ali Romman and JoyboyBrian. +""" +from hashlib import sha1, sha256 +import importlib.util +import json +from pathlib import Path + +from construction import build_tables, need, source_key, target_key +from kernel import rotate + +HERE = Path(__file__).resolve().parent + + +def load_ports(): + """Authenticate unchanged predecessor bytes before loading either module.""" + pins = json.loads((HERE / 'CALLER-SOURCES.json').read_text()) + modules = [] + for item in pins['files']: + raw = (HERE / item['local_path']).read_bytes() + need(len(raw) == item['size'] and sha256(raw).hexdigest() == item['sha256'] + and sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == item['git_blob'], + 'Exact retained caller source: '+item['local_path']) + spec = importlib.util.spec_from_file_location(item['module'], HERE / item['local_path']) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + modules.append(module) + return tuple(modules) + + +def checked_block(values, tables, width, inverse=False, trace=None): + """Same certified map, with fast butterflies and checked finite words.""" + need(type(width) is int and width >= 2 and type(inverse) is bool, 'Block word format') + need(type(values) in (tuple, list) and len(values) == 16 + and all(type(z) in (tuple, list) and len(z) == 2 for z in values), 'Block dimensions') + trace = trace if trace is not None else {} + def word(x): + need(type(x) is int and -(1 << (width-1)) <= x < (1 << (width-1)), 'Word overflow') + trace['checked_values'] = trace.get('checked_values', 0)+1 + trace['peak_integer'] = max(trace.get('peak_integer', 0), abs(x)) + return x + for z in values: + for x in z: + word(x) + z = [rotate(tuple(word(-a) for a in values[j]), j.bit_count()) if inverse + else rotate(values[j], -j.bit_count()) for j in range(16)] + for pair in z: + for x in pair: + word(x) + out = [] + for component in range(2): + a = [pair[component] for pair in z] + # Classification acts only on three-bit residues, but is payable work. + residues = [x % 8 for x in a] + key = target_key(residues) if inverse else source_key(residues) + correction = tables[1 if inverse else 0][key] + for bit in range(4): + step = 1 << bit + for base in range(0, 16, 2*step): + for low in range(step): + i, j = base+low, base+low+step + x, y = a[i], a[j] + a[i], a[j] = word(x+y), word(x-y) + for j in range(16): + a[j] = word(a[j]+correction[j]) + need(a[j] % 4 == 0, 'Exact quarter') + a[j] = word(a[j]//4) + out.append(a) + result = [rotate((out[0][j], out[1][j]), j.bit_count()) if inverse + else rotate((-out[0][j], -out[1][j]), -j.bit_count()) for j in range(16)] + for pair in result: + for x in pair: + word(x) + trace['blocks'] = trace.get('blocks', 0)+1 + trace['data_additions'] = trace.get('data_additions', 0)+160 + trace['quarter_shifts'] = trace.get('quarter_shifts', 0)+32 + return result + + +def fibers(axis): + bits = [3*j+axis for j in range(4)] + mask = sum(1 << bit for bit in bits) + offsets = [sum(((j >> k) & 1) << bits[k] for k in range(4)) for j in range(16)] + for base in range(4096): + if base & mask == 0: + yield [base | offset for offset in offsets] + + +def make_backend(tables): + """Bind the authenticated certificate once; return the retained call API.""" + def call(values, f, axis, width, adjoint=False, trace=None): + need(type(f) is int and f == 4 and type(axis) is int and axis in (0, 2) + and len(values) == 4096 and type(adjoint) is bool, 'Four-axis dimensions') + trace = trace if trace is not None else {} + for indices in fibers(axis): + result = checked_block([values[i] for i in indices], tables, width, adjoint, trace) + for i, z in zip(indices, result): + values[i] = z + return values + return call + + +def request_bits(P, kind, reverse): + """Retain source q while using the new g=q+1 at exactly four axes.""" + need(type(P) is int and P >= 0 and type(kind) is int and kind in (2, 3) + and type(reverse) is bool, 'Port precision format') + q = P + ((4 if kind == 2 else 6) if reverse else (7 if kind == 2 else 9)) + return q+1 + + +def signed_width(H, P, kind, reverse): + need(type(H) is int and H >= 0, 'Port magnitude format') + return H+request_bits(P, kind, reverse)+19 diff --git a/research/four-axis-phase-covariant-grid/construction.py b/research/four-axis-phase-covariant-grid/construction.py new file mode 100644 index 0000000000..c5a604d9c4 --- /dev/null +++ b/research/four-axis-phase-covariant-grid/construction.py @@ -0,0 +1,107 @@ +"""Exact finite certificate for a sharp phase-covariant Walsh-16 map. + +@CubeJerry with substantial AI assistance. Apache-2.0. +Candidate offsets and native conventions follow Nick Petalas, #6574; +this package changes the period quotient and enforces negation orbits. +""" +from itertools import product +import json +from pathlib import Path + +SIZE = 16 +MODULI = (8, 4, 4, 4, 4) +HIGH = (7, 11, 13, 14, 15) +KEYS = tuple(product(*(range(m) for m in MODULI))) +WALSH = tuple(tuple(1 if (r & s).bit_count() % 2 == 0 else -1 + for s in range(SIZE)) for r in range(SIZE)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def walsh(values): + return tuple(sum(a * b for a, b in zip(row, values)) for row in WALSH) + + +def negate_key(key): + return tuple(-a % m for a, m in zip(key, MODULI)) + + +def source_key(values): + return ((4 * values[7] - sum(values)) % 8,) + tuple( + (2 * values[HIGH[j + 1]] - sum(values[s] for s in range(SIZE) + if s >> j & 1)) % 4 for j in range(4)) + + +def target_key(values): + numerator = walsh(values) + return ((numerator[7] - 4 * values[0]) % 8,) + tuple( + ((numerator[HIGH[j + 1]] - numerator[7]) // 2 + + 2 * values[1 << j]) % 4 for j in range(4)) + + +def source_representative(key): + values = [0] * SIZE + values[0] = sum(key[1:]) - key[0] + for j in range(4): + values[1 << j] = -key[j + 1] + return tuple(values) + + +def target_representative(key): + a, b, c, d = key[1:] + low = ((2 * a + c + 3 * d) % 4, (3 * b + 3 * d) % 4, + (a + 2 * c + 3 * d) % 4, d) + values = [0] * SIZE + values[0] = (5 * (key[0] + sum(low[:3]) - low[3])) % 8 + for j in range(4): + values[1 << j] = low[j] + return tuple(values) + + +def build_tables(): + """Expand and validate 1008 signed-orbit witnesses plus 32 fixed classes.""" + certificate = json.loads(Path(__file__).with_name('CERTIFICATE.json').read_text()) + need(certificate.get('schema_version') == 1 and + tuple(certificate.get('moduli', ())) == MODULI, 'Certificate schema') + rows = certificate.get('rows', []) + need(type(rows) is list and len(rows) == 1008, '1008 free negation orbits') + forward, backward = {}, {} + for key, offset in rows: + key, offset = tuple(key), tuple(offset) + need(key in KEYS and key < negate_key(key), 'Canonical free orbit') + need(len(offset) == SIZE and all(type(x) is int for x in offset), + 'Sixteen integer correction coordinates') + numerator = tuple(a + b for a, b in zip(walsh(source_representative(key)), offset)) + need(all(x % 4 == 0 for x in numerator), 'Integral corrected output') + target = target_key(tuple(x // 4 for x in numerator)) + image = walsh(offset) + need(all(x % 4 == 0 for x in image), 'Integral inverse correction') + inverse = tuple(-x // 4 for x in image) + for source, destination, e, f in ( + (key, target, offset, inverse), + (negate_key(key), negate_key(target), + tuple(-x for x in offset), tuple(-x for x in inverse))): + need(source not in forward and destination not in backward, + 'Distinct source and target classes') + forward[source], backward[destination] = e, f + for key in KEYS: + if key == negate_key(key): + numerator = walsh(source_representative(key)) + need(all(x % 4 == 0 for x in numerator), 'Integral fixed class') + target = target_key(tuple(x // 4 for x in numerator)) + need(key not in forward and target not in backward, 'Distinct fixed class') + forward[key] = backward[target] = (0,) * SIZE + need(set(forward) == set(backward) == set(KEYS), 'Complete class bijection') + for table, coordinate_bound in ((forward, 3), (backward, 5)): + for e in table.values(): + need(sum(x * x for x in e) <= 64, 'Sharp real energy') + need(max(abs(x) for x in e) <= coordinate_bound, + 'Certified forward/inverse coordinate bound') + need(sum((1, 0, -1, 0)[j.bit_count() % 4] * e[j] + for j in range(SIZE)) == 0 and + sum((0, -1, 0, 1)[j.bit_count() % 4] * e[j] + for j in range(SIZE)) == 0, 'Exact weighted sum') + return forward, backward diff --git a/research/four-axis-phase-covariant-grid/inputs/retained_ports.py b/research/four-axis-phase-covariant-grid/inputs/retained_ports.py new file mode 100644 index 0000000000..a9d5d0268f --- /dev/null +++ b/research/four-axis-phase-covariant-grid/inputs/retained_ports.py @@ -0,0 +1,26 @@ +"""Use an explicit numerical backend in the retained complete port. + +Port source: JoyboyBrian / PR5485 and the credited PR4743 lineage. +Interface: Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from kernel import need + +def port(x,y,f,kind,reverse,width,backend,source,capture=False): + monomial,mix=source.monomial,source.mix + need(x is not y, 'Distinct dirty banks') + need(kind in (2,3),'two or three calls') + if capture:x=list(x);y=list(y) + trace={};cuts=[] + def paid(v,axis,adj=False): + before=list(v) if capture else None + backend(v,f,axis,width,adj,trace) + if capture:cuts.append((axis,adj,before,list(v))) + if reverse: + if kind==3: + monomial(y,'M',f,width,True);paid(y,2,True);monomial(y,'W',f,width,True) + paid(y,0,True);mix(x,y,f,width,-1);paid(x,0,True) + else: + paid(x,0);mix(x,y,f,width,1);paid(y,0) + if kind==3:monomial(y,'W',f,width);paid(y,2);monomial(y,'M',f,width) + return x,y,trace,cuts + diff --git a/research/four-axis-phase-covariant-grid/inputs/retained_rounded.py b/research/four-axis-phase-covariant-grid/inputs/retained_rounded.py new file mode 100644 index 0000000000..8ae18373f2 --- /dev/null +++ b/research/four-axis-phase-covariant-grid/inputs/retained_rounded.py @@ -0,0 +1,123 @@ +"""Fixed-grid Gaussian calls and literal ports; JoyboyBrian, Codex assistance.""" + + +def need(ok,why): + if not ok:raise ValueError(why) + + +def half_even(n): + q=n>>1 + return q+((n&1)&(q&1)) + + +def checkword(n,width): + need(type(n) is int and -(1<<(width-1))<=n<(1<<(width-1)),'signed word overflow') + return n + + +def call(v,f,axis,width,adjoint=False,trace=None): + need(type(f) is int and f>=1 and axis in (0,2) and len(v)==8**f,'literal Gaussian call dimensions') + need(type(width) is int and width>=2,'word width') + for z in v: + need(len(z)==2,'complex pair') + for value in z:checkword(value,width) + trace=trace if trace is not None else {} + for j in range(f): + bit=3*j+axis; step=1<>1) + if name=='P':y=x^(4 if x&1 else 0); q=x.bit_count()+y.bit_count() + elif name=='Q':y=swap;q=x.bit_count()+y.bit_count() + elif name=='W':y=x;q=2*((x&5).bit_count()%2) + else:y=swap;q=2*((y>>1)&1) + perm.append(y);phase.append(q%4) + return perm,phase + + +def rotate(z,q): + a,b=z + return ((a,b),(-b,a),(-a,-b),(b,-a))[q] + + +def route(name,f,inverse=False): + p,q=letters(name) + if inverse: + back=[0]*8;ph=[0]*8 + for x,y in enumerate(p):back[y]=x;ph[y]=-q[x]%4 + p,q=back,ph + out=[] + for x in range(8**f): + y=z=0 + for j in range(f): + a=(x>>(3*j))&7;y|=p[a]<<(3*j);z+=q[a] + out.append((y,z%4)) + return out + + +def monomial(v,name,f,width,inverse=False): + routing=route(name,f,inverse); seen=bytearray(len(v)) + for start in range(len(v)): + if seen[start]:continue + x=start;saved=v[x] + while True: + seen[x]=1;y,q=routing[x];following=v[y] + v[y]=tuple(checkword(z,width) for z in rotate(saved,q));x=y;saved=following + if x==start:break + # These are owned control fields, explicitly returned zero after use. + for i in range(len(seen)):seen[i]=0;routing[i]=(0,0) + + +def mix(t,y,f,width,sign): + for name,coefficient in [('P',1),('Q',2)]: + monomial(t,name,f,width) + for i,((a,b),(c,d)) in enumerate(zip(t,y)): + ca=checkword(a if coefficient==1 else a<<1,width);cb=checkword(b if coefficient==1 else b<<1,width) + y[i]=(checkword(c+sign*ca,width),checkword(d+sign*cb,width)) + monomial(t,name,f,width,True) + + +def port(x,y,f,kind,reverse,width,capture=False): + need(kind in (2,3),'two or three calls') + if capture:x=list(x);y=list(y) + trace={};cuts=[] + def paid(v,axis,adj=False): + before=list(v) if capture else None + call(v,f,axis,width,adj,trace) + if capture:cuts.append((axis,adj,before,list(v))) + if reverse: + if kind==3: + monomial(y,'M',f,width,True);paid(y,2,True);monomial(y,'W',f,width,True) + paid(y,0,True);mix(x,y,f,width,-1);paid(x,0,True) + else: + paid(x,0);mix(x,y,f,width,1);paid(y,0) + if kind==3:monomial(y,'W',f,width);paid(y,2);monomial(y,'M',f,width) + return x,y,trace,cuts + + +def request_bits(P,f,kind,reverse): + need(type(P) is int and P>=0 and type(f) is int and f>=1 and kind in (2,3),'accuracy domain') + if reverse:external=(f+1)//2+2 if kind==2 else f+2 + else:external=f+3 if kind==2 else (3*f+1)//2+3 + return P+external+(f+1)//2+1 + + +def signed_width(H,P,f,kind,reverse): + need(type(H) is int and H>=0,'magnitude domain') + return H+request_bits(P,f,kind,reverse)+2*f+(f+1)//2+9 diff --git a/research/four-axis-phase-covariant-grid/kernel.py b/research/four-axis-phase-covariant-grid/kernel.py new file mode 100644 index 0000000000..d7b329b539 --- /dev/null +++ b/research/four-axis-phase-covariant-grid/kernel.py @@ -0,0 +1,45 @@ +"""Literal forward/inverse Gaussian block; @CubeJerry/AI, Apache-2.0. + +Diagonal phases and the endpoint convention follow Nick Petalas #6574, +Ali Romman's Gaussian rounding lineage, and David Ganz / Dugongue. +""" +from construction import SIZE, need, source_key, target_key, walsh + +MAX_BITS = 4096 + + +def rotate(value, exponent): + a, b = value + return ((a, b), (-b, a), (-a, -b), (b, -a))[exponent % 4] + + +def real_map(values, table, inverse=False): + key = target_key(values) if inverse else source_key(values) + need(key in table, 'Known real quotient class') + numerator = tuple(a + b for a, b in zip(walsh(values), table[key])) + need(all(x % 4 == 0 for x in numerator), 'Exact quarter shift') + return tuple(x // 4 for x in numerator) + + +def block(values, tables, inverse=False): + """Return sixteen Gaussian pairs; never mutate inputs or correction tables.""" + need(type(values) in (tuple, list) and len(values) == SIZE, + 'Sixteen Gaussian integer inputs') + need(all(type(z) in (tuple, list) and len(z) == 2 for z in values), + 'Real/imaginary component pairs') + need(all(type(v) is int and v.bit_length() <= MAX_BITS + for z in values for v in z), 'At most 4096 bits per component') + need(type(inverse) is bool, 'Boolean inverse selector') + if inverse: + rotated = tuple(rotate((-a, -b), j.bit_count()) + for j, (a, b) in enumerate(values)) + else: + rotated = tuple(rotate(z, -j.bit_count()) for j, z in enumerate(values)) + table = tables[1 if inverse else 0] + real = real_map(tuple(z[0] for z in rotated), table, inverse) + imag = real_map(tuple(z[1] for z in rotated), table, inverse) + if inverse: + return tuple(rotate((a, b), j.bit_count()) + for j, (a, b) in enumerate(zip(real, imag))) + return tuple(rotate((-a, -b), -j.bit_count()) + for j, (a, b) in enumerate(zip(real, imag))) diff --git a/research/four-axis-phase-covariant-grid/verify.py b/research/four-axis-phase-covariant-grid/verify.py new file mode 100644 index 0000000000..d701187919 --- /dev/null +++ b/research/four-axis-phase-covariant-grid/verify.py @@ -0,0 +1,413 @@ +#!/usr/bin/env python3 +"""Independent exact lattice/certificate oracle; @CubeJerry/AI, Apache-2.0. + +The oracle reconstructs rational period bases, uses their inverse matrices to +classify cosets, and evaluates the native complex tensor directly. It does not +use the production quotient formulas to decide the certificate predicates. +""" +from fractions import Fraction +import hashlib +from itertools import product +import json +from pathlib import Path +import sys + +import construction as impl +from kernel import block, real_map + +HERE = Path(__file__).resolve().parent +N = 16 +MOD = (8, 4, 4, 4, 4) +KEYS = tuple(product(*(range(m) for m in MOD))) +ZERO = (0,) * N +W = tuple(tuple((-1) ** ((i & j).bit_count()) for j in range(N)) + for i in range(N)) +CHECKS = 0 +CONTROLS = [] + + +def require(condition, message): + global CHECKS + CHECKS += 1 + if not condition: + raise ValueError(message) + + +def reject(label, action, reason=None): + try: + action() + except (ValueError, TypeError, KeyError, IndexError) as error: + require(reason is None or reason in str(error), 'Intended failure control: ' + label) + CONTROLS.append(label) + else: + raise ValueError('Failure control was accepted: ' + label) + + +def mv(matrix, vector): + return tuple(sum(a * b for a, b in zip(row, vector)) for row in matrix) + + +def transform(vector): + """Independent butterfly, whereas construction.walsh uses dense rows.""" + out = list(vector) + width = 1 + while width < N: + for start in range(0, N, 2 * width): + for j in range(start, start + width): + a, b = out[j], out[j + width] + out[j], out[j + width] = a + b, a - b + width *= 2 + return tuple(out) + + +def inverse_and_determinant(matrix): + n = len(matrix) + rows = [[Fraction(x) for x in row] + [Fraction(i == j) for j in range(n)] + for i, row in enumerate(matrix)] + determinant = Fraction(1) + for j in range(n): + pivot = next((k for k in range(j, n) if rows[k][j]), None) + require(pivot is not None, 'Nonsingular period matrix') + if pivot != j: + rows[j], rows[pivot] = rows[pivot], rows[j] + determinant = -determinant + q = rows[j][j] + determinant *= q + rows[j] = [x / q for x in rows[j]] + for k in range(n): + if k != j and rows[k][j]: + q = rows[k][j] + rows[k] = [a - q * b for a, b in zip(rows[k], rows[j])] + return tuple(tuple(row[n:]) for row in rows), determinant + + +def rank_mod2(matrix): + pivots = {} + for row in matrix: + bits = sum((v % 2) << j for j, v in enumerate(row)) + while bits: + p = bits.bit_length() - 1 + if p in pivots: + bits ^= pivots[p] + else: + pivots[p] = bits + break + return len(pivots) + + +def unit(i): + return tuple(int(i == j) for j in range(N)) + + +def add(a, b, scale=1): + return tuple(x + scale * y for x, y in zip(a, b)) + + +def kernel_column(s): + out = list(unit(s)) + out[0] = s.bit_count() - 1 + for j in range(4): + if s >> j & 1: + out[1 << j] = -1 + return tuple(out) + + +def period_bases(): + pairs = tuple(s for s in range(N) if s.bit_count() == 2) + high = tuple(s for s in range(N) if s.bit_count() >= 3) + u = [(4,) + (0,) * 15] + u += [tuple(2 * x for x in add(unit(1 << j), unit(0), -1)) + for j in range(4)] + v = [] + for s in high: + out = kernel_column(s) + for t in pairs: + if t & s == t: + out = add(out, kernel_column(t), -1) + v.append(out) + lcols = u + [kernel_column(s) for s in pairs + high] + mcols = [add(a, b) for a, b in zip(u, v)] + mcols += [kernel_column(s) for s in pairs] + mcols += [tuple(2 * x for x in a) for a in v] + gcols = [] + for column in mcols: + numerator = transform(column) + require(all(x % 4 == 0 for x in numerator), 'Integral image periods') + gcols.append(tuple(x // 4 for x in numerator)) + return tuple(zip(*lcols)), tuple(zip(*mcols)), tuple(zip(*gcols)) + + +def period_checker(matrix, image, expected=2048): + inverse, determinant = inverse_and_determinant(matrix) + require(abs(determinant) == expected, 'Declared period index') + require(all((8 * x).denominator == 1 for row in inverse for x in row), + 'Eightfold inverse period matrix is integral') + scaled = tuple(tuple(int(8 * x) for x in row) for row in inverse) + for j, column in enumerate(zip(*matrix)): + require(mv(scaled, column) == tuple(8 * int(i == j) for i in range(N)), + 'Independent inverse period matrix') + if image is not None: + require(transform(column) == tuple(4 * row[j] for row in image), + 'Period carries exact ideal image') + return scaled + + +def normal_key(inverse8, vector): + return tuple(x % 8 for x in mv(inverse8, vector)) + + +def negate(key): + return tuple(-x % m for x, m in zip(key, MOD)) + + +def weighted_zero(offset): + real = imag = 0 + phase = ((1, 0), (0, -1), (-1, 0), (0, 1)) + for j, value in enumerate(offset): + a, b = phase[j.bit_count() % 4] + real += a * value + imag += b * value + return real == imag == 0 + + +def validate_forward(forward, reps, target_labels, inverse8): + require(set(forward) == set(KEYS), 'Complete source classes') + for key, offset in forward.items(): + require(len(offset) == N and all(type(x) is int for x in offset), + 'Integer correction dimensions') + require(sum(x * x for x in offset) <= 64, 'Real error radius') + require(weighted_zero(offset), 'Native weighted sum cancellation') + require(forward[negate(key)] == tuple(-x for x in offset), + 'Negation orbit consistency') + backward = {} + destinations = {} + for key in KEYS: + offset = forward[key] + numerator = add(transform(reps[key]), offset) + require(all(x % 4 == 0 for x in numerator), 'Source integrality') + output = tuple(x // 4 for x in numerator) + destination = target_labels[normal_key(inverse8, output)] + require(destination not in backward, 'Target class collision') + inverse_numerator = tuple(-x for x in transform(offset)) + require(all(x % 4 == 0 for x in inverse_numerator), 'Inverse integrality') + inverse = tuple(x // 4 for x in inverse_numerator) + require(sum(x * x for x in inverse) == sum(x * x for x in offset), + 'Orthogonal inverse error') + require(weighted_zero(inverse), 'Inverse weighted sum cancellation') + backward[destination] = inverse + destinations[key] = destination + require(set(backward) == set(KEYS), 'Complete target classes') + return backward, destinations + + +def phase(value, exponent): + a, b = value + c, d = ((1, 0), (0, 1), (-1, 0), (0, -1))[exponent % 4] + return a * c - b * d, a * d + b * c + + +def ideal_scaled4(values, inverse=False): + """4U from its native tensor entries, without Walsh or D factorization.""" + result = [] + for r in range(N): + total_re = total_im = 0 + for s, value in enumerate(values): + exponent = 4 - (r ^ s).bit_count() + a, b = phase(value, -exponent if inverse else exponent) + total_re -= a + total_im -= b + result.append((total_re, total_im)) + return tuple(result) + + +def scaled_error(values, output, inverse=False): + return sum((4 * a - c) ** 2 + (4 * b - d) ** 2 + for (a, b), (c, d) in zip(output, ideal_scaled4(values, inverse))) + + +def native_check(values, tables, inverse=False): + before = tuple(tuple(z) for z in values) + output = block(values, tables, inverse) + require(tuple(tuple(z) for z in values) == before, 'Input nonmutation') + require(scaled_error(values, output, inverse) <= 128, 'Sharp native error') + require(tuple(map(sum, zip(*values))) == tuple(map(sum, zip(*output))), + 'Exact native complex sum') + rotated = tuple(phase(z, 1) for z in values) + require(block(rotated, tables, inverse) == tuple(phase(z, 1) for z in output), + 'Global Gaussian phase covariance') + require(block(output, tables, not inverse) == before, 'Literal native inverse') + return scaled_error(values, output, inverse) + + +def main(): + lmat, mmat, gmat = period_bases() + _, determinant_l = inverse_and_determinant(lmat) + require(abs(determinant_l) == 64, 'Coarse integrality index64') + for column in zip(*lmat): + require(all(x % 4 == 0 for x in transform(column)), 'Coarse integrality periods') + imat = period_checker(mmat, gmat) + igmat = period_checker(gmat, mmat) + require([rank_mod2(x) for x in (mmat, gmat, mmat + gmat)] == [11, 11, 11], + 'Both parity kernels agree on the minimizing period') + image_l = tuple(zip(*(tuple(v // 4 for v in transform(c)) for c in zip(*lmat)))) + require([rank_mod2(x) for x in (lmat, image_l, lmat + image_l)] == [11, 11, 16], + 'Disjoint five-dimensional parity kernels in L') + for j in range(N): + require(transform(unit(j)) == tuple(row[j] for row in W), 'Walsh convention') + require(transform(transform(unit(j))) == tuple(16 * x for x in unit(j)), + 'Exact Walsh square') + source_reps = {key: impl.source_representative(key) for key in KEYS} + target_reps = {key: impl.target_representative(key) for key in KEYS} + source_labels = {normal_key(imat, z): key for key, z in source_reps.items()} + target_labels = {normal_key(igmat, z): key for key, z in target_reps.items()} + require(len(source_labels) == len(target_labels) == 2048, + 'Independent source and target normal forms') + for key in KEYS: + require(impl.source_key(source_reps[key]) == key, 'Source section') + require(impl.target_key(target_reps[key]) == key, 'Target section') + for column in zip(*mmat): + require(impl.source_key(column) == (0,) * 5, 'Source classifier periods') + for column in zip(*gmat): + require(impl.target_key(column) == (0,) * 5, 'Target classifier periods') + certificate = json.loads((HERE / 'CERTIFICATE.json').read_text()) + require(certificate['schema_version'] == 1 and certificate['moduli'] == list(MOD), + 'Certificate format') + require(len(certificate['rows']) == 1008, '1008 free sign orbits') + forward = {} + for key, offset in certificate['rows']: + require(type(key) is list and all(type(x) is int for x in key), 'Integer key') + key, offset = tuple(key), tuple(offset) + require(key in KEYS and key < negate(key), 'Canonical nonfixed source orbit') + require(key not in forward and negate(key) not in forward, 'Unique orbit witness') + forward[key] = offset + forward[negate(key)] = tuple(-x for x in offset) + fixed = [key for key in KEYS if key == negate(key)] + require(len(fixed) == 32, 'Exactly32 fixed classes') + for key in fixed: + require(key not in forward, 'Fixed/free disjointness') + forward[key] = ZERO + backward, destinations = validate_forward(forward, source_reps, target_labels, igmat) + tables = impl.build_tables() + require(tables == (forward, backward), 'Production tables match independent certificate') + max_forward = max(abs(x) for e in forward.values() for x in e) + max_inverse = max(abs(x) for e in backward.values() for x in e) + require((max_forward, max_inverse) == (3, 5), 'Coordinate correction maxima3/5') + require(max(sum(x * x for x in e) for e in forward.values()) == 64, + 'Attained real correction energy64') + for inverse, representatives, table in ((False, source_reps, forward), + (True, target_reps, backward)): + for key, vector in representatives.items(): + output = real_map(vector, table, inverse) + require(real_map(output, forward if inverse else backward, not inverse) == vector, + 'Both real composition orders on every class') + difference = add(tuple(4 * x for x in output), transform(vector), -1) + require(difference == table[key], 'Literal real correction') + max_native_energy = 0 + for inverse, representatives in ((False, source_reps), (True, target_reps)): + for index, key in enumerate(KEYS): + a, b = representatives[key], representatives[KEYS[(73 * index + 19) % 2048]] + if inverse: + values = tuple(phase((-x, -y), -j.bit_count()) + for j, (x, y) in enumerate(zip(a, b))) + else: + values = tuple(phase((x, y), j.bit_count()) + for j, (x, y) in enumerate(zip(a, b))) + max_native_energy = max(max_native_energy, native_check(values, tables, inverse)) + witness = ((2, 2),) + ((0, 0),) * 15 + for inverse in (False, True): + energy = native_check(witness, tables, inverse) + require(energy == 128, 'Sharp half-grid witness') + max_native_energy = max(max_native_energy, energy) + zero = ((0, 0),) * 16 + require(block(zero, tables) == block(zero, tables, True) == zero, 'Zero fixed') + large_cases = 0 + for bits in (1, 128, 1024, 4090): + size = (1 << bits) - 1 + values = tuple((((-1) ** j) * (size - j), ((-1) ** (j // 2)) * (size + 3 * j)) + for j in range(16)) + for inverse in (False, True): + native_check(values, tables, inverse) + large_cases += 1 + for index in (0, 1, 31, 511, 2047): + vector = source_reps[KEYS[index]] + shift = mv(mmat, tuple(((-1) ** j) * (j + 1) for j in range(N))) + image = mv(gmat, tuple(((-1) ** j) * (j + 1) for j in range(N))) + require(real_map(add(vector, shift), forward) == add(real_map(vector, forward), image), + 'Affine period translation') + first = ((1, 0),) + ((0, 0),) * 15 + fourth = first + for _ in range(4): + fourth = block(fourth, tables) + expected_fourth = ((1, 0), (0, -1), (0, 0), (0, 0), (0, -1), (0, 0), + (0, 0), (0, -1), (0, 0), (0, 0), (-1, 0), (0, 0), + (1, 0), (0, 2), (0, 1), (0, 0)) + require(fourth == expected_fourth and fourth != first, 'Retained fourth-power counterexample') + + # Preserve local edge predicates while deliberately breaking orbit matching. + alternatives = {} + for offset in forward.values(): + alternatives.setdefault(tuple(x % 4 for x in offset), set()).add(offset) + mutation = None + for key in KEYS: + if key == negate(key): + continue + old = forward[key] + for candidate in sorted(alternatives[tuple(x % 4 for x in old)]): + numerator = add(transform(source_reps[key]), candidate) + target = target_labels[normal_key(igmat, tuple(x // 4 for x in numerator))] + if target not in (destinations[key], destinations[negate(key)]): + mutation = key, candidate + break + if mutation is not None: + break + require(mutation is not None, 'Nontrivial locally admissible mutation exists') + key, alternative = mutation + bad = dict(forward) + bad[key] = alternative + reject('locally admissible broken negation', + lambda: validate_forward(bad, source_reps, target_labels, igmat), + 'Negation orbit consistency') + bad[negate(key)] = tuple(-x for x in alternative) + reject('locally admissible sign-paired target collision', + lambda: validate_forward(bad, source_reps, target_labels, igmat), + 'Target class collision') + corrupted = [list(row) for row in mmat] + corrupted[0][0] += 1 + reject('corrupted affine period', lambda: period_checker(tuple(map(tuple, corrupted)), gmat)) + reject('false 127/16 native squared-radius claim', + lambda: require(scaled_error(witness, block(witness, tables)) <= 127, 'Too-small radius')) + clean = ((4, 0),) + ((0, 0),) * 15 + wrong_phase = tuple((-a, -b) for a, b in block(clean, tables)) + reject('wrong native phase with reversible endpoint', + lambda: require(scaled_error(clean, wrong_phase) <= 128, 'Wrong native operator')) + reject('forward substituted for literal inverse', + lambda: require(block(block(first, tables), tables) == first, 'Wrong inverse')) + for label, value, inverse in ( + ('fifteen coordinates', zero[:-1], False), + ('noninteger component', ((0.5, 0),) + zero[1:], False), + ('boolean component', ((True, 0),) + zero[1:], False), + ('4097-bit component', ((1 << 4096, 0),) + zero[1:], False), + ('nonboolean inverse selector', zero, 1)): + reject(label, lambda value=value, inverse=inverse: block(value, tables, inverse)) + hashes = {path.relative_to(HERE).as_posix(): hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted(HERE.rglob('*')) + if path.is_file() and '__pycache__' not in path.parts} + print(json.dumps({ + 'status': 'PASS_PHASE_COVARIANT_GRID', 'python': sys.version.split()[0], + 'assertions_enabled': __debug__, 'predicate_checks': CHECKS, + 'real_source_classes': 2048, 'real_target_classes': 2048, + 'fixed_classes': 32, 'free_negation_orbits': 1008, + 'native_fixture_pairs': 4096, 'large_integer_fixtures': large_cases, + 'all_native_class_pairs_enumerated': False, + 'coordinate_correction_maxima': [max_forward, max_inverse], + 'max_native_squared_error_times16': max_native_energy, + 'minimal_real_affine_period_index': 2048, + 'minimal_native_affine_period_index': 4194304, + 'fourth_power_counterexample': {'input': first, 'fourth_iterate': fourth}, + 'failure_controls': CONTROLS, 'sha256': hashes, + 'scope': 'Finite certificate plus scoped all-integer proof; no multiplication theorem or tariff admission' + }, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/four-axis-phase-covariant-grid/verify_caller.py b/research/four-axis-phase-covariant-grid/verify_caller.py new file mode 100644 index 0000000000..205cafa427 --- /dev/null +++ b/research/four-axis-phase-covariant-grid/verify_caller.py @@ -0,0 +1,140 @@ +"""Exact native-coefficient caller oracle; @CubeJerry/AI, Apache-2.0.""" +import json +import random + +from construction import build_tables, need, KEYS, source_representative, target_representative +from kernel import block, rotate +from caller import load_ports, checked_block, fibers, make_backend, request_bits, signed_width + +tables = build_tables() +ports, retained = load_ports() +candidate = make_backend(tables) + + +def ideal(v, f, axis, width, adjoint=False, trace=None): + # Independent coefficient formula for C_axis tensor 4; no Walsh factorization. + for indices in fibers(axis): + old = [v[i] for i in indices] + for r, index in enumerate(indices): + terms = [rotate(old[s], (-1 if adjoint else 1)*(4-(r ^ s).bit_count())) + for s in range(16)] + numerator = [-sum(z[k] for z in terms) for k in range(2)] + need(all(a % 4 == 0 for a in numerator), 'Oracle scale exhausted') + v[index] = tuple(a//4 for a in numerator) + return v + + +def run(): + # Independently bind the fast checked arithmetic to the certified dense map. + for inverse, section in ((False, source_representative), (True, target_representative)): + for key in KEYS: + v = section(key) + z = tuple((a, v[(5*j+3) % 16]) for j, a in enumerate(v)) + need(tuple(checked_block(z, tables, 64, inverse)) == block(z, tables, inverse), + 'Fast/dense block equality') + rng = random.Random(2026110627) + fixtures = [([(0, 0)]*4096, [(0, 0)]*4096), + ([(rng.randrange(-8, 9), rng.randrange(-8, 9)) for _ in range(4096)], + [(rng.randrange(-8, 9), rng.randrange(-8, 9)) for _ in range(4096)]), + ([((j % 7)-3, ((j*5) % 11)-5) for j in range(4096)], + [((j % 13)-6, ((j*3) % 17)-8) for j in range(4096)]), + ([((1 << 30)+(j % 7), -(1 << 29)-(j % 5)) for j in range(4096)], + [(-(1 << 31)+(j % 11), (1 << 28)+(j % 3)) for j in range(4096)])] + cases = cuts_checked = 0 + maxima = {} + for number, (x, y) in enumerate(fixtures): + for kind in (2, 3): + for reverse in (False, True): + gotx, goty, trace, cuts = ports.port(x, y, 4, kind, reverse, 64, + candidate, retained, True) + backx, backy, _, _ = ports.port(gotx, goty, 4, kind, not reverse, 64, + candidate, retained, True) + need((backx, backy) == (x, y), 'Exact two-bank return') + phasex, phasey, _, _ = ports.port([rotate(z, 1) for z in x], + [rotate(z, 1) for z in y], 4, kind, reverse, 64, candidate, retained, True) + need(phasex == [rotate(z, 1) for z in gotx] + and phasey == [rotate(z, 1) for z in goty], 'Port phase covariance') + exactx, exacty, _, _ = ports.port([tuple(64*a for a in z) for z in x], + [tuple(64*a for a in z) for z in y], 4, kind, reverse, 80, ideal, retained, True) + error = max(sum((64*a-b)**2 for a, b in zip(v, w)) + for v, w in zip(gotx+goty, exactx+exacty)) + multiplier = (1 if kind == 2 else 5) if reverse else (13 if kind == 2 else 53) + radius = 50 if reverse else 18 + need(error <= 256*multiplier**2*radius, 'Complete port error') + maxima[f'{kind}-{reverse}'] = max(maxima.get(f'{kind}-{reverse}', 0), error) + need(trace['blocks'] == kind*256 and trace['data_additions'] == kind*40960 + and trace['quarter_shifts'] == kind*8192, 'Complete block arithmetic count') + for axis, adjoint, before, after in cuts: + exact = [tuple(4*a for a in z) for z in before] + ideal(exact, 4, axis, 80, adjoint) + need(max(sum((4*a-b)**2 for a, b in zip(v, w)) + for v, w in zip(after, exact)) <= (50 if adjoint else 18), + 'Actual-input call coordinate error') + for ids in fibers(axis): + need(tuple(sum(before[i][k] for i in ids) for k in (0, 1)) == + tuple(sum(after[i][k] for i in ids) for k in (0, 1)), 'Fiber sum') + cuts_checked += 1 + cases += 1 + rejected = [] + bad_cases = [('alias', lambda: ports.port(fixtures[1][0], fixtures[1][0], 4, 2, False, + 64, candidate, retained)), + ('wrong-size', lambda: candidate([(0, 0)]*4096, 3, 0, 64)), + ('word-overflow', lambda: candidate([(127, 127)]*4096, 4, 0, 8))] + for name, action in bad_cases: + try: + action() + except ValueError: + rejected.append(name) + else: + raise ValueError('Negative control survived: '+name) + def wrong_inverse(v, f, axis, width, adjoint=False, trace=None): + return candidate(v, f, axis, width, False, trace) + x, y = fixtures[1] + fx, fy, _, _ = ports.port(x, y, 4, 3, False, 64, candidate, retained, True) + bx, by, _, _ = ports.port(fx, fy, 4, 3, True, 64, wrong_inverse, retained, True) + need((bx, by) != (x, y), 'Wrong inverse must fail return') + rejected.append('forward-as-inverse') + def wrong_axis(v, f, axis, width, adjoint=False, trace=None): + return candidate(v, f, 0, width, adjoint, trace) + x = [tuple(1024*a for a in z) for z in x] + y = [tuple(1024*a for a in z) for z in y] + fx, fy, _, _ = ports.port(x, y, 4, 3, False, 64, wrong_axis, retained, True) + ex, ey, _, _ = ports.port([tuple(64*a for a in z) for z in x], + [tuple(64*a for a in z) for z in y], 4, 3, False, 80, ideal, retained, True) + wrong_error = max(sum((64*a-b)**2 for a, b in zip(v, w)) + for v, w in zip(fx+fy, ex+ey)) + need(wrong_error > 256*53**2*18, 'Wrong axis must fail native accuracy') + rejected.append('wrong-native-axis') + grid_cases = [] + for kind in (2, 3): + for reverse in (False, True): + P, H = 4, 3 + old_g = retained.request_bits(P, 4, kind, reverse) + g = request_bits(P, kind, reverse) + width = signed_width(H, P, kind, reverse) + need(g == old_g-2 and width == retained.signed_width(H, P, 4, kind, reverse)-2, 'Two-bit retained reduction') + magnitude = 1 << (H+g) + x = [(magnitude if j % 3 else -magnitude, 0) for j in range(4096)] + y = [(0, magnitude if j % 5 else -magnitude) for j in range(4096)] + # Break alignment without violating the initial magnitude bound. + x[7] = (magnitude-1, 0) + y[11] = (0, -magnitude+3) + fx, fy, _, _ = ports.port(x, y, 4, kind, reverse, width, candidate, retained, True) + ex, ey, _, _ = ports.port([tuple(64*a for a in z) for z in x], + [tuple(64*a for a in z) for z in y], 4, kind, reverse, width+8, ideal, retained, True) + error = max(sum((64*a-b)**2 for a, b in zip(v, w)) + for v, w in zip(fx+fy, ex+ey)) + need(error <= (64 << (g-P))**2, 'Retained complete physical accuracy') + bx, by, _, _ = ports.port(fx, fy, 4, kind, not reverse, width, candidate, retained, True) + need((bx, by) == (x, y), 'Finite-word exact return') + grid_cases.append({'kind': kind, 'reverse': reverse, 'P': P, 'H': H, + 'g': g, 'width': width, 'old_g': old_g}) + print(json.dumps({'status': 'PASS_FOUR_AXIS_RETAINED_PORTS', 'fixtures': len(fixtures), + 'port_directions': cases, 'actual_input_cuts': cuts_checked, + 'max_squared_errors_scaled_by_4096': maxima, 'negative_controls': rejected, + 'native_grid': 'g=q+1', 'retained_grid': 'g=q+3', 'fractional_bits_saved': 2, + 'grid_cases': grid_cases}, sort_keys=True)) + + +if __name__ == '__main__': + run()