diff --git a/research/p112-householder-gauge-seed06ace/README.md b/research/p112-householder-gauge-seed06ace/README.md new file mode 100644 index 0000000000..5360fcc1e7 --- /dev/null +++ b/research/p112-householder-gauge-seed06ace/README.md @@ -0,0 +1,51 @@ +# P112 ten-term Householder gauge cost screen + +**Scoped negative result for one exact witness orbit. No new `κ` or supplier admission.** + +## Result + +The P112 symmetric ten-term decoder witness from open PR1633 has exact per-term binary support ranks `(8,8,8,8,8,8,8,8,9,9)`, total 82. This package exhausts every rational Householder term gauge + +```text +O_s = I - 2 s s^T / (s^T s), +s ∈ {-1,0,1}^10 \ {0}, modulo s ~ -s. +``` + +The domain has 29,524 reflections. All preserve the ordinary-transpose P112 identity, all ten terms remain active, and the support invoices form only nine histograms. Every histogram uses ranks 8 and 9; the minimum total stays 82. The best candidate is just a signed-column reflection and retains the predecessor's `(8^8,9^2)` profile. + +To screen the result, the candidate decoder replaces the selected profile's eight rank-8 centre children by its ten priced terms. Even waiving every coefficient, frame, precision, hosting, storage, and restoration expense, its best exact ceiling is + +```text +0.000834274164361244 ≤ a_cap ≤ 0.000834274164361245 +``` + +The selected fixed-word ceiling is `0.001690054109089`; its 5% acceptance target is `0.00177455681454345`. The entire searched family misses the target before any extra charge, so this route stops here. This does not rule out a different P112 witness, an asymmetric two-sided decoder, other coefficient choices, or another support family. + +`RESULT.json` records all nine histograms, their exact ceiling intervals, candidate counts, and the best normal. `verify.py` regenerates and compares that receipt. It rebuilds the 112 roots, checks the base witness on all 12,544 ordered root pairs, proves each Householder numerator orthogonal by exact integer arithmetic, directly checks the best transformed identity, computes support ranks over F2, and runs five positive/failure controls. The ceiling calculation uses the pinned exact-rational interval implementation. + +## Provenance and overlap + +- Cycle seed `06ace58bfc2b63b47b02129f729e35d4`, track `complex-mechanisms`, task `complex-rank-shape-decoder`, priority revision 3. The card is marked **changed** in [TASK.json](TASK.json): the diagonal rank-16 batching route overlaps open PRs #1779/#1817 and their child-contract follow-up; this package tests the separate open overcomplete-decoder question. +- Exact base `0b1cccf86e2f5132ed286a26ef0a681a495740ea`; selected-record SHA-256 `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. The actual selected review, source manifest and assembly certificate are pinned in [SOURCES.json](SOURCES.json); the selected reproduction command is `make frontier1094-verify`. The selected frontier remains untouched. +- The witness is extracted from Hanson Sun's open PR1633, head `652264fa1f70820139b2730363a0056b7fadc689`, `research/decoder-excess-rank/RESULT.json`, pinned by both Git blob and SHA-256 in `WITNESS.json` and [SOURCES.json](SOURCES.json). PR1633 proves the rank-one residual normal form and explicitly leaves support-aware ten-term copy optimization open. Its witness invoice 82 and dense-gauge control 90 are reproduced here. PR1224 supplies the earlier projection equations; PR1077 and PR968 supply the E8/Gaussian decoder conventions. +- The full overlap refresh at 2026-10-14 13:27 UTC covered 543 open PRs and 529 Discussion records with complete pagination and no warnings. The bounded scope claim is [Discussion #1622 comment 18925227](https://github.com/CrocSwap/integer-mult-bounds/discussions/1622#discussioncomment-18925227). The result is limited to this witness and this finite gauge family. + +## Reproduce + +From the repository root: + +```sh +python3 -B research/p112-householder-gauge-seed06ace/verify.py +python3 scripts/research_package.py --package research/p112-householder-gauge-seed06ace --check-only +python3.12 scripts/research_package.py --package research/p112-householder-gauge-seed06ace +``` + +The direct verifier and metadata/source-pin check pass under the local Python 3.14.7. Python 3.12 is unavailable locally, so the registered Python 3.12 replay remains for CI/reviewer confirmation. A metadata pass checks package structure and pins; it is not a mathematical acceptance check. + +## Open next questions + +Can an asymmetric two-sided ten-term P112 decoder outside this symmetric witness orbit reduce the 64-rank copy bill? This remains relevant because a lower exact support profile could change the selected centre children. A feasible first step is to search the original term coordinates under the rank-one residual equations in [TASK.json](TASK.json), charging every term support before applying the selected ceiling. The unrestricted coefficient/support space and the absence of a native frame and precision invoice are the blockers. + +## Credit + +The exact witness and rank-normal-form predecessor are Hanson Sun / PR1633; earlier decoder equations are joaqcoo / PR1224, with E8 and Gaussian arithmetic from woklerx / PR1077 and themilkman216 / PR968. Prepared by Cinna Davis with substantial OpenAI Codex assistance in scoping, exact finite search, support-rank computation, ceiling screening, verifier implementation, and writing. No subagents or independent human review are claimed. New material is Apache-2.0. diff --git a/research/p112-householder-gauge-seed06ace/RESULT.json b/research/p112-householder-gauge-seed06ace/RESULT.json new file mode 100644 index 0000000000..1af9b63e62 --- /dev/null +++ b/research/p112-householder-gauge-seed06ace/RESULT.json @@ -0,0 +1,516 @@ +{ + "status": "PASS_P112_HOUSEHOLDER_GAUGE_SEARCH", + "seed": "06ace58bfc2b63b47b02129f729e35d4", + "track": "complex-mechanisms", + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "predecessor": { + "pr": 1633, + "head": "652264fa1f70820139b2730363a0056b7fadc689", + "result_git_blob": "0c1a85768b3e3dbb727149b3a8dbb345ff029f88", + "result_sha256": "f62fbac3f31d088c9b81a7a01b2012145589b1bb5687f6c5e70be786b17745c2" + }, + "domain": { + "support": "P112", + "terms": 10, + "householder_normals": "{-1,0,1}^10 minus zero, modulo s~-s", + "candidate_count": 29524, + "all_terms_active_candidates": 29524, + "inactive_candidates": 0, + "distinct_rank_histograms": 9 + }, + "base": { + "costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 9 + ], + "centre_rank_mass": 64, + "a_cap_interval": [ + "338010821817739/200000000000000000", + "211256763636087/125000000000000000" + ] + }, + "gate": { + "target_a": "35491136290869/20000000000000000", + "best_zero_extra_charge_a_cap_interval": [ + "208568541090311/250000000000000000", + "166854832872249/200000000000000000" + ], + "best_candidate_passes": false, + "best_rank_histogram": { + "8": 8, + "9": 2 + }, + "best_ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 9 + ], + "best_normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "best_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8, + "9": 2 + }, + "best_centre_rank_mass": 82 + }, + "profiles": [ + { + "rank_histogram": { + "8": 8, + "9": 2 + }, + "candidate_count": 100, + "centre_rank_mass": 82, + "profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8, + "9": 2 + }, + "a_cap_interval": [ + "208568541090311/250000000000000000", + "166854832872249/200000000000000000" + ], + "passes_five_percent_gate": false, + "example_normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 9 + ] + }, + { + "rank_histogram": { + "8": 7, + "9": 3 + }, + "candidate_count": 32, + "centre_rank_mass": 83, + "profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 7, + "9": 3 + }, + "a_cap_interval": [ + "78677748145519/100000000000000000", + "786777481455191/1000000000000000000" + ], + "passes_five_percent_gate": false, + "example_normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + -1 + ], + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 9, + 9 + ] + }, + { + "rank_histogram": { + "8": 6, + "9": 4 + }, + "candidate_count": 448, + "centre_rank_mass": 84, + "profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 6, + "9": 4 + }, + "a_cap_interval": [ + "46204859063753/62500000000000000", + "739277745020049/1000000000000000000" + ], + "passes_five_percent_gate": false, + "example_normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + -1 + ], + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9 + ] + }, + { + "rank_histogram": { + "8": 5, + "9": 5 + }, + "candidate_count": 2016, + "centre_rank_mass": 85, + "profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 5, + "9": 5 + }, + "a_cap_interval": [ + "5534199642913/8000000000000000", + "345887477682063/500000000000000000" + ], + "passes_five_percent_gate": false, + "example_normal": [ + 0, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + -1, + -1 + ], + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 9 + ] + }, + { + "rank_histogram": { + "8": 4, + "9": 6 + }, + "candidate_count": 5040, + "centre_rank_mass": 86, + "profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 4, + "9": 6 + }, + "a_cap_interval": [ + "644269112795963/1000000000000000000", + "161067278198991/250000000000000000" + ], + "passes_five_percent_gate": false, + "example_normal": [ + 0, + 0, + 0, + 0, + 1, + -1, + -1, + -1, + -1, + -1 + ], + "ordered_costs": [ + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9 + ] + }, + { + "rank_histogram": { + "8": 3, + "9": 7 + }, + "candidate_count": 8064, + "centre_rank_mass": 87, + "profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 3, + "9": 7 + }, + "a_cap_interval": [ + "74595027203043/125000000000000000", + "119352043524869/200000000000000000" + ], + "passes_five_percent_gate": false, + "example_normal": [ + 0, + 0, + 0, + 1, + -1, + -1, + -1, + -1, + -1, + -1 + ], + "ordered_costs": [ + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ] + }, + { + "rank_histogram": { + "8": 2, + "9": 8 + }, + "candidate_count": 8064, + "centre_rank_mass": 88, + "profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 2, + "9": 8 + }, + "a_cap_interval": [ + "137312067539571/250000000000000000", + "109849654031657/200000000000000000" + ], + "passes_five_percent_gate": false, + "example_normal": [ + 0, + 0, + 1, + -1, + -1, + -1, + -1, + -1, + -1, + -1 + ], + "ordered_costs": [ + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ] + }, + { + "rank_histogram": { + "8": 1, + "9": 9 + }, + "candidate_count": 4608, + "centre_rank_mass": 89, + "profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 1, + "9": 9 + }, + "a_cap_interval": [ + "501733270707037/1000000000000000000", + "250866635353519/500000000000000000" + ], + "passes_five_percent_gate": false, + "example_normal": [ + 0, + 1, + -1, + -1, + -1, + -1, + -1, + -1, + -1, + -1 + ], + "ordered_costs": [ + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ] + }, + { + "rank_histogram": { + "9": 10 + }, + "candidate_count": 1152, + "centre_rank_mass": 90, + "profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "9": 10 + }, + "a_cap_interval": [ + "227107609790047/500000000000000000", + "90843043916019/200000000000000000" + ], + "passes_five_percent_gate": false, + "example_normal": [ + 1, + -1, + -1, + -1, + -1, + -1, + -1, + -1, + -1, + -1 + ], + "ordered_costs": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ] + } + ], + "controls": [ + "signed-column reflection preserves the base invoice", + "all-ones Householder reproduces the 90-copy gauge", + "nonorthogonal coefficient fails the exact identity", + "omitted residual term fails the exact identity", + "mutated witness entry fails the exact identity" + ], + "limitations": [ + "Only one symmetric ten-term witness orbit is searched.", + "Rational Householder coefficients have not been priced in a native supplier.", + "No physical frame, hosting, precision/tape, restoration or controller invoice is established.", + "No selected supplier adoption or new kappa is claimed." + ] +} diff --git a/research/p112-householder-gauge-seed06ace/SOURCES.json b/research/p112-householder-gauge-seed06ace/SOURCES.json new file mode 100644 index 0000000000..b6a14995ce --- /dev/null +++ b/research/p112-householder-gauge-seed06ace/SOURCES.json @@ -0,0 +1,51 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "provenance", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + } + ], + "external_predecessor": { + "pr": 1633, + "head": "652264fa1f70820139b2730363a0056b7fadc689", + "path": "research/decoder-excess-rank/RESULT.json", + "git_blob": "0c1a85768b3e3dbb727149b3a8dbb345ff029f88", + "sha256": "f62fbac3f31d088c9b81a7a01b2012145589b1bb5687f6c5e70be786b17745c2", + "copied_subset": "WITNESS.json", + "copied_subset_sha256": "eb2d042139f4cc369389311b7ed0cea7bb523a112114fb5f767024aff34473b3" + } +} diff --git a/research/p112-householder-gauge-seed06ace/TASK.json b/research/p112-householder-gauge-seed06ace/TASK.json new file mode 100644 index 0000000000..96b3fc2fda --- /dev/null +++ b/research/p112-householder-gauge-seed06ace/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "For the exact symmetric ten-term P112 decoder witness pinned in PR1633, exhaust every rational Householder term-coordinate gauge with normal in {-1,0,1}^10 modulo sign, and price the exact per-term binary support ranks in the selected centre profile.", + "scope_change_reason": "The direct rank-16 diagonal-batch route was already covered by open PR1779/1817 and a later exact child-contract obstruction. PR1633 leaves the support-aware ten-term P112 copy-cost question open. This bounded construction test changes the exact eight-term decoder premise to one specified ten-term symmetric witness and searches a finite identity-preserving gauge family, rather than repeating the all-pairs eight-term theorem or block-batch route.", + "bottleneck_link": "If an exact ten-term P112 decoder reduced the selected 64-rank centre path while preserving all-pairs exactness, its support ranks could replace the eight rank-8 centre children in the per-call profile. The computed profile is charged through the pinned fixed-word ceiling; this screen is not supplier admission.", + "budget_minutes": 60, + "stop_rule": "Enumerate all (3^10-1)/2 = 29,524 nonzero ternary normals modulo sign. Verify every Householder numerator exactly, compute every active term's binary P112 support rank, and apply the resulting child ranks with zero extra coefficient/frame/hosting/restoration charges. Stop if no exact ceiling clears the selected word's 5% threshold. Do not search other witness or coefficient families in this cycle.", + "outcome": "negative-result", + "evidence": "All 29,524 reflections preserve the exact P112 decoder identity and all ten terms remain active. The family yields only nine support-rank histograms, all with per-term ranks 8 or 9; the minimum is (8,8,8,8,8,8,8,8,9,9), total 82. Replacing the eight rank-8 centre children by this best zero-extra-charge profile gives the exact ceiling interval recorded in RESULT.json, strictly below both the selected ceiling and its 5% acceptance target. Five controls pass. This is only a negative result for one witness orbit, not for all ten-term or two-sided decoders.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in scoping, exact search, support-rank computation, moment screening, verifier and writing; no subagents.", + "open_questions": [ + { + "question": "Can any two-sided ten-term P112 decoder outside this symmetric Householder orbit reduce the 64-rank copy bill below the eight-term frame?", + "why_it_matters": "That is the remaining support-aware overcomplete route that could lower the selected complex centre profile under the same all-pairs contract.", + "first_step": "Search the original term coordinates in D=RA+uz^T, T=RB+vw^T under AB^T=2I, Bz=0, Aw=0 and z^Tw=0, and price every term support before applying the selected ceiling.", + "blocked_by": "The coefficient and support search is unrestricted, and no native frame, coefficient precision, hosting or restoration realization is supplied. The current cycle only exhausts one exact symmetric witness's finite rational gauge family." + } + ] +} diff --git a/research/p112-householder-gauge-seed06ace/VERIFY.json b/research/p112-householder-gauge-seed06ace/VERIFY.json new file mode 100644 index 0000000000..4e8a7b4201 --- /dev/null +++ b/research/p112-householder-gauge-seed06ace/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/complex-local-word-ceiling/ceiling.py", + "research/p112-householder-gauge-seed06ace/WITNESS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Rebuild the exact P112 support matrix, verify the pinned witness, exhaust all 29,524 rational ternary Householder gauges, calculate all distinct support-rank profiles and exact ceiling intervals, and exercise five positive and negative controls." + } + ] +} diff --git a/research/p112-householder-gauge-seed06ace/WITNESS.json b/research/p112-householder-gauge-seed06ace/WITNESS.json new file mode 100644 index 0000000000..6271795767 --- /dev/null +++ b/research/p112-householder-gauge-seed06ace/WITNESS.json @@ -0,0 +1,5235 @@ +{ + "schema_version": 1, + "origin": { + "pr": 1633, + "head": "652264fa1f70820139b2730363a0056b7fadc689", + "path": "research/decoder-excess-rank/RESULT.json", + "git_blob": "0c1a85768b3e3dbb727149b3a8dbb345ff029f88", + "sha256": "f62fbac3f31d088c9b81a7a01b2012145589b1bb5687f6c5e70be786b17745c2" + }, + "representative": { + "D": [ + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "13/14", + "0" + ], + [ + "0", + "13/14" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "-1/28" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "-1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ] + ], + "costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 9 + ], + "domain": "P112", + "mixed_costs": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "residual_channel": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "1" + ] + ], + "residual_vector": [ + [ + "13/14", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1/28", + "0" + ], + [ + "-1/28", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ] + } +} diff --git a/research/p112-householder-gauge-seed06ace/verify.py b/research/p112-householder-gauge-seed06ace/verify.py new file mode 100644 index 0000000000..270213a629 --- /dev/null +++ b/research/p112-householder-gauge-seed06ace/verify.py @@ -0,0 +1,346 @@ +#!/usr/bin/env python3 +"""Exact bounded P112 term-gauge search and selected-profile screen. + +Searches every rational Householder reflection with ternary normal in ten +term coordinates. Ordinary-transpose exactness follows from O O^T = I; the +base witness and the winning transformed identity are also checked directly. +""" +from __future__ import annotations + +import hashlib +import importlib.util +import itertools +import json +import math +import sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WITNESS_PATH = HERE / "WITNESS.json" +RESULT_PATH = HERE / "RESULT.json" +SELECTED_SHA256 = "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" +CATALOG_SHA256 = "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" +CEILING_SHA256 = "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" +PRED_RESULT_SHA256 = "f62fbac3f31d088c9b81a7a01b2012145589b1bb5687f6c5e70be786b17745c2" +PRED_RESULT_BLOB = "0c1a85768b3e3dbb727149b3a8dbb345ff029f88" +PRED_HEAD = "652264fa1f70820139b2730363a0056b7fadc689" +WITNESS_SHA256 = "eb2d042139f4cc369389311b7ed0cea7bb523a112114fb5f767024aff34473b3" +BASE_PROFILE = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} +BASE_CENTRE = 64 +BASE_A_HI = Q(1690054109089, 10**15) +TARGET_A = BASE_A_HI * Q(21, 20) +HOUSEHOLDERS = (3**10 - 1) // 2 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def sha256(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def load_ceiling(): + path = ROOT / "research/complex-local-word-ceiling/ceiling.py" + spec = importlib.util.spec_from_file_location("p112_gauge_ceiling", path) + module = importlib.util.module_from_spec(spec) + assert spec.loader is not None + spec.loader.exec_module(module) + return module + + +def roots_p112(): + lines = [] + for a, b in itertools.combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[a], row[b] = 2, sign * 2 + lines.append(tuple(row)) + for signs in itertools.product((-1, 1), repeat=7): + if signs.count(-1) % 2 == 0: + lines.append((1, *signs)) + removed = set() + for a in range(0, 8, 2): + for sign in (-1, 1): + row = [0] * 8 + row[a], row[a + 1] = 2, sign * 2 + removed.add(tuple(row)) + roots = sorted(set(lines) - removed) + require(len(roots) == 112 and len(set(roots)) == 112, "P112 root construction") + require(all(sum(r[a] * r[b] for r in roots) == 112 * (a == b) + for a in range(8) for b in range(8)), "P112 Gram identity") + return roots + + +def parse_witness(): + raw = WITNESS_PATH.read_bytes() + record = json.loads(raw) + origin = record["origin"] + require(origin["pr"] == 1633 and origin["head"] == PRED_HEAD, "predecessor head pin") + require(origin["path"] == "research/decoder-excess-rank/RESULT.json", "predecessor path pin") + require(origin["git_blob"] == PRED_RESULT_BLOB and origin["sha256"] == PRED_RESULT_SHA256, + "predecessor result pin") + witness = record["representative"] + require(witness["domain"] == "P112", "witness domain") + require(witness["costs"] == [8] * 8 + [9, 9], "predecessor cost receipt") + require(witness["mixed_costs"] == [9] * 10, "predecessor gauge control receipt") + encoded = witness["D"] + require(len(encoded) == 112 and all(len(row) == 10 for row in encoded), "witness shape") + parsed = [[(Q(cell[0]), Q(cell[1])) for cell in row] for row in encoded] + den = math.lcm(*(part.denominator for row in parsed for cell in row for part in cell)) + matrix = [[(int(cell[0] * den), int(cell[1] * den)) for cell in row] for row in parsed] + return record, matrix, den + + +def pairing_rows(roots): + return [sum(((((sum(x * y for x, y in zip(ra, rb)) // 4) + 1) % 2) << j) + for j, rb in enumerate(roots)) for ra in roots] + + +def gf2_rank(mask_rows): + pivots = {} + rank = 0 + for value in mask_rows: + while value: + pivot = value.bit_length() - 1 + old = pivots.get(pivot) + if old is None: + pivots[pivot] = value + rank += 1 + break + value ^= old + return rank + + +def support_bill(matrix, pair_rows, rank_cache): + costs = [] + masks = [] + for k in range(10): + support = 0 + for i, row in enumerate(matrix): + if row[k] != (0, 0): + support |= 1 << i + masks.append(support) + if support not in rank_cache: + selected = [] + todo = support + while todo: + bit = todo & -todo + i = bit.bit_length() - 1 + selected.append(pair_rows[i] & support) + todo ^= bit + rank_cache[support] = gf2_rank(selected) + costs.append(rank_cache[support]) + return costs, masks + + +def identity(matrix, den, roots): + for i, ri in enumerate(roots): + for j, rj in enumerate(roots): + re = im = 0 + for ar, ai in zip(matrix[i], matrix[j]): + re += ar[0] * ai[0] - ar[1] * ai[1] + im += ar[0] * ai[1] + ar[1] * ai[0] + if im or 2 * re != den * den * sum(x * y for x, y in zip(ri, rj)): + return False + return True + + +def householder_numerator(matrix, s, scale=2): + norm = sum(x * x for x in s) + require(norm > 0, "zero Householder normal") + total = [] + for row in matrix: + total.append((sum(s[k] * row[k][0] for k in range(10)), + sum(s[k] * row[k][1] for k in range(10)))) + out = [] + for i, row in enumerate(matrix): + outrow = [] + for j in range(10): + c = scale * s[j] + outrow.append((norm * row[j][0] - c * total[i][0], + norm * row[j][1] - c * total[i][1])) + out.append(outrow) + return out, norm + + +def is_canonical(s): + first = next((x for x in s if x), 0) + return first == 1 + + +def orthogonal_numerator(s): + norm = sum(x * x for x in s) + mat = [[norm * (i == j) - 2 * s[i] * s[j] for j in range(10)] for i in range(10)] + return norm, mat + + +def profile_for(costs): + profile = dict(BASE_PROFILE) + profile[8] -= 8 + for r, n in Counter(costs).items(): + profile[r] = profile.get(r, 0) + n + return {r: n for r, n in profile.items() if n} + + +def screen_profile(profile, centre, model): + return model.ceiling(profile, 73, 896, 9, centre, grid=Q(1, 10**18)) + + +def run(): + require(sha256(ROOT / "certificates/selected-result.json") == SELECTED_SHA256, + "selected record SHA-256") + require(sha256(ROOT / "docs/research/agent-task-catalog.json") == CATALOG_SHA256, + "priority catalogue SHA-256") + require(sha256(ROOT / "research/complex-local-word-ceiling/ceiling.py") == CEILING_SHA256, + "ceiling source SHA-256") + require(sha256(WITNESS_PATH) == WITNESS_SHA256, "derived witness input SHA-256") + + record, base, den = parse_witness() + roots = roots_p112() + pairs = pairing_rows(roots) + require(gf2_rank(pairs) == 9, "P112 label rank") + require(identity(base, den, roots), "predecessor P112 identity") + cache = {} + base_costs, base_masks = support_bill(base, pairs, cache) + require(base_costs == [8] * 8 + [9, 9], "exact predecessor support invoice") + + # Positive and negative controls. + axis = (1,) + (0,) * 9 + axis_num, axis_norm = householder_numerator(base, axis) + axis_costs, _ = support_bill(axis_num, pairs, cache) + require(axis_norm == 1 and axis_costs == base_costs, "signed-column reflection control") + ones = (1,) * 10 + ones_num, ones_norm = householder_numerator(base, ones) + ones_costs, _ = support_bill(ones_num, pairs, cache) + require(ones_norm == 10 and ones_costs == [9] * 10, "known dense-gauge control") + bad_num, bad_norm = householder_numerator(base, axis, scale=3) + require(not identity(bad_num, den * bad_norm, roots), "nonorthogonal coefficient control") + omitted = [row[:9] for row in base] + require(not identity(omitted, den, roots), "omitted isotropic-pair member control") + mutated = [list(row) for row in base] + mutated[0][0] = (mutated[0][0][0] + 1, mutated[0][0][1]) + require(not identity(mutated, den, roots), "mutated witness control") + + profiles = {} + best_candidates = {} + rank_cache = cache + total = active = inactive = 0 + for s in itertools.product((-1, 0, 1), repeat=10): + if not any(s) or not is_canonical(s): + continue + total += 1 + norm, m = orthogonal_numerator(s) + require(all(sum(m[i][k] * m[j][k] for k in range(10)) == + norm * norm * (i == j) for i in range(10) for j in range(10)), + "Householder exact orthogonality") + changed, scale = householder_numerator(base, s) + require(scale == norm, "Householder common denominator") + costs, masks = support_bill(changed, pairs, rank_cache) + if not all(masks): + inactive += 1 + continue + active += 1 + hist = tuple(sorted(costs)) + profiles[hist] = profiles.get(hist, 0) + 1 + prior = best_candidates.get(hist) + if prior is None or tuple(costs) < prior["ordered_costs"]: + best_candidates[hist] = {"s": list(s), "ordered_costs": tuple(costs)} + require(total == HOUSEHOLDERS, "Householder search coverage") + require(active == total and inactive == 0, "all searched decoder terms stay active") + require(sum(profiles.values()) == active, "rank-profile count coverage") + require(all(set(hist) <= {8, 9} for hist in profiles), "unexpected support-rank class") + require(min(map(sum, profiles)) == 82, "minimum support invoice in searched family") + + model = load_ceiling() + screened = [] + for hist, count in sorted(profiles.items()): + local = profile_for(hist) + centre = sum(hist) + lo, hi = screen_profile(local, centre, model) + screened.append({ + "rank_histogram": dict(sorted(Counter(hist).items())), + "candidate_count": count, + "centre_rank_mass": centre, + "profile": {str(r): n for r, n in sorted(local.items())}, + "a_cap_interval": [str(lo), str(hi)], + "passes_five_percent_gate": lo >= TARGET_A, + "example_normal": best_candidates[hist]["s"], + "ordered_costs": list(best_candidates[hist]["ordered_costs"]), + }) + screened.sort(key=lambda x: Q(x["a_cap_interval"][1]), reverse=True) + require(all(Q(row["a_cap_interval"][1]) < TARGET_A for row in screened), + "a Householder profile unexpectedly meets the 5% gate") + best = screened[0] + best_s = tuple(best["example_normal"]) + best_matrix, best_norm = householder_numerator(base, best_s) + require(identity(best_matrix, den * best_norm, roots), "best candidate direct P112 identity") + + baseline = screen_profile(BASE_PROFILE, BASE_CENTRE, model) + result = { + "status": "PASS_P112_HOUSEHOLDER_GAUGE_SEARCH", + "seed": "06ace58bfc2b63b47b02129f729e35d4", + "track": "complex-mechanisms", + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "selected_record_sha256": SELECTED_SHA256, + "predecessor": {"pr": 1633, "head": PRED_HEAD, + "result_git_blob": PRED_RESULT_BLOB, + "result_sha256": PRED_RESULT_SHA256}, + "domain": {"support": "P112", "terms": 10, + "householder_normals": "{-1,0,1}^10 minus zero, modulo s~-s", + "candidate_count": total, + "all_terms_active_candidates": active, + "inactive_candidates": inactive, + "distinct_rank_histograms": len(profiles)}, + "base": {"costs": base_costs, "centre_rank_mass": BASE_CENTRE, + "a_cap_interval": [str(x) for x in baseline]}, + "gate": {"target_a": str(TARGET_A), + "best_zero_extra_charge_a_cap_interval": best["a_cap_interval"], + "best_candidate_passes": best["passes_five_percent_gate"], + "best_rank_histogram": best["rank_histogram"], + "best_ordered_costs": best["ordered_costs"], + "best_normal": best["example_normal"], + "best_profile": best["profile"], + "best_centre_rank_mass": best["centre_rank_mass"]}, + "profiles": screened, + "controls": ["signed-column reflection preserves the base invoice", + "all-ones Householder reproduces the 90-copy gauge", + "nonorthogonal coefficient fails the exact identity", + "omitted residual term fails the exact identity", + "mutated witness entry fails the exact identity"], + "limitations": ["Only one symmetric ten-term witness orbit is searched.", + "Rational Householder coefficients have not been priced in a native supplier.", + "No physical frame, hosting, precision/tape, restoration or controller invoice is established.", + "No selected supplier adoption or new kappa is claimed."], + } + return result, roots, best_matrix, den * best_norm + + +def main(): + write = "--write" in sys.argv[1:] + result, roots, matrix, den = run() + if write: + RESULT_PATH.write_text(json.dumps(result, indent=2) + "\n") + else: + expected = json.loads(RESULT_PATH.read_text()) + canonical = json.loads(json.dumps(result)) + require(canonical == expected, "stored bounded-search receipt mismatch") + gate = result["gate"] + print("PASS_P112_HOUSEHOLDER_GAUGE_SEARCH " + f"candidates={result['domain']['candidate_count']} " + f"active={result['domain']['all_terms_active_candidates']} " + f"profiles={result['domain']['distinct_rank_histograms']} " + f"best_costs={gate['best_ordered_costs']} " + f"best_a_hi={gate['best_zero_extra_charge_a_cap_interval'][1]} " + f"gate={gate['best_candidate_passes']} controls={len(result['controls'])}") + + +if __name__ == "__main__": + main()