diff --git a/research/complex-prefix-bounded-dyadic/CLAIM.json b/research/complex-prefix-bounded-dyadic/CLAIM.json new file mode 100644 index 0000000000..9830537c05 --- /dev/null +++ b/research/complex-prefix-bounded-dyadic/CLAIM.json @@ -0,0 +1,95 @@ +{ + "status": "completed; research PR submitted for review", + "assignment_seed": 23, + "randomness": "Python secrets.randbelow(100), OS entropy; drawn once at session start", + "track": "complex supplier", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "started_utc": "2026-10-13T04:37:48Z", + "expected_finish_utc": "2026-10-13T05:18:00Z", + "verification_reserved_from_utc": "2026-10-13T05:08:00Z", + "selected_kappa": "51110230636731/31250000000000000", + "candidates": [ + { + "task": "Reorder one raw K-triangle read window with exact minimal frames", + "decision": "defer: PR687 already closes the closest narrow relocation class; seed change alone adds little" + }, + { + "task": "Resynthesize one fixed coordinate-total factory map with restoration", + "decision": "defer: PR681 already supplies exact fixed-map elimination; another block alone adds little" + }, + { + "task": "Prefix-bounded signed-digit Horner for selected complex dyadic additions", + "decision": "chosen: changes coefficient synthesis; PR696 only replaces leading clear/add and unit macros" + } + ], + "seed_use": "23 mod 3 = 2 selects third candidate; 23 mod 2 = 1 prioritizes JP8 backward for screening; final coverage includes both providers and orientations", + "object": "Dyadic addition coefficients in the pinned PR626 CK and JP8 LOCAL-PROGRAMS; unchanged scalar boundaries, frames and paid recursive profile", + "method": "Finite signed-binary Horner recurrence with every intermediate integer coefficient in [1, abs(numerator)]; compare explicit cost and exact prefix envelope against binary Horner and PR696 copy/unit lowering", + "expected_deliverable": "Standalone circuit, exact rational verifier, finite deterministic certificate, adverse controls and scoped proof; no new kappa claim", + "stopping_rule": "Complete all distinct selected coefficients and four selected scalar event streams; stop if no further fully charged primitive saving or if the inherited prefix envelope cannot be retained", + "coordination": { + "pinned_issue": null, + "viewer_permission": "READ", + "checked_utc": "2026-10-13T04:41:00Z", + "local_claim_reason": "No pinned coordination issue exists; no reservation issue opened", + "open_pr_count": 533, + "latest_pr": 714 + }, + "predecessor_prs": [ + 411, + 622, + 626, + 696 + ], + "initial_screen": { + "additional_real_primitives_saved_vs_pr696": { + "ck/forward": 122, + "ck/backward": 122, + "jp8/forward": 3090, + "jp8/backward": 3090 + }, + "status": "exploratory counts only; verification pending" + }, + "attribution": "Chris Pagolu (@AllStars101-sudo), with substantial OpenAI Codex assistance; Apache-2.0", + "prior_negative_result": { + "path": "research/experiment-log/campaign-100/algebraic-word-construction.md#38-signed-digit-coefficients", + "contributor": "Rohan Arun", + "source_head": "fa8ab946df57ebadae1a470b637c2a590a0a5317", + "finding": "Coefficient-3 rewrites at rank zero do not improve paid climbs", + "distinction": "This contribution changes primitive synthesis for the later selected large numerators, retains the exact intermediate coefficient envelope, and claims only scalar cost savings; it agrees that the paid profile and kappa do not improve." + }, + "completed_utc": "2026-10-13T05:00:13Z", + "implementation_commit": "21606831df4b08f79d87fd420c558a520dca571e", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/734", + "result": { + "classification": "finite complex-supplier circuit improvement / research note; no new kappa", + "saved_real_primitives_beyond_pr696": { + "ck/forward": 122, + "ck/backward": 122, + "jp8/forward": 3090, + "jp8/backward": 3090 + }, + "coverage": "All 686 selected dyadic coefficient types and four complete scalar programs; 716 native + 9 private formal columns each; 8256 independent digit-graph comparisons; 12 mathematical controls and four package/algorithm corruption controls. No search timeout or unfinished case.", + "prefix_bound": "Original per-macro numerator cap and inherited exact global scalar envelope retained", + "verification_started_utc": "2026-10-13T04:52:04Z", + "reproduce": "python3 -B research/complex-prefix-bounded-dyadic/verify.py", + "expected": "PASS_PREFIX_BOUNDED_DYADIC programs=4 columns=716+9 coefficients=686 extra_savings=122,122,3090,3090 controls=12", + "limitations": "No production emitter integration, new global invoice/admission, full theorem proof, new kappa or practical runtime claim." + }, + "concurrent_result": { + "pr": 723, + "head": "d3bc41b87fc7d23f50d064a0f06f1a89e3ab02a7", + "credit": "Sagar Thakrar independently developed JP8 signed-digit lowering during this session", + "distinct_evidence": "Hard per-macro numerator cap with unchanged exact prefix envelope; optimal recurrence for this restricted class; separate forward graph check; CK coverage and explicit composition with pinned PR696. PR723 permits numerator+1 and saves 186 more recoding primitives per JP8 orientation. Its implementation is not independently verified here." + }, + "final_overlap_refresh": { + "utc": "2026-10-13T04:59:42Z", + "latest_other_pr": 732, + "related_heads_unchanged": [ + 696, + 722, + 723 + ], + "coordination_issue": null + } +} diff --git a/research/complex-prefix-bounded-dyadic/EXPECTED.json b/research/complex-prefix-bounded-dyadic/EXPECTED.json new file mode 100644 index 0000000000..e12142d29a --- /dev/null +++ b/research/complex-prefix-bounded-dyadic/EXPECTED.json @@ -0,0 +1,851 @@ +{ + "additional_private_registers": 0, + "coefficient_census": [ + {"coefficient":"-67108862","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0],"occurrences":1,"pr696_real_cost":52,"signed_real_cost":30,"work_peak_multiple":"67108862"}, + {"coefficient":"-33525759","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,-1,0,0,1,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":48,"signed_real_cost":32,"work_peak_multiple":"33525759"}, + {"coefficient":"-33497087","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,1,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":48,"signed_real_cost":32,"work_peak_multiple":"33497087"}, + {"coefficient":"-20971400","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,1,0,0,0],"occurrences":1,"pr696_real_cost":43,"signed_real_cost":30,"work_peak_multiple":"20971400"}, + {"coefficient":"-41902077/2","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":49,"signed_real_cost":34,"work_peak_multiple":"41902077"}, + {"coefficient":"-17039357","digits_after_leading_one":[0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":44,"signed_real_cost":30,"work_peak_multiple":"17039357"}, + {"coefficient":"-33685503/2","digits_after_leading_one":[0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":46,"signed_real_cost":32,"work_peak_multiple":"33685503"}, + {"coefficient":"-33612031/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,-1,0,0,0,0,1,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":40,"signed_real_cost":34,"work_peak_multiple":"33612031"}, + {"coefficient":"-33570817/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":31,"signed_real_cost":31,"work_peak_multiple":"33570817"}, + {"coefficient":"-16777216","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":5,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"16777216"}, + {"coefficient":"-33554431/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":3,"pr696_real_cost":52,"signed_real_cost":31,"work_peak_multiple":"33554431"}, + {"coefficient":"-16777215","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":49,"signed_real_cost":29,"work_peak_multiple":"16777215"}, + {"coefficient":"-16777088","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":42,"signed_real_cost":28,"work_peak_multiple":"16777088"}, + {"coefficient":"-33538055/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,1,1,1],"occurrences":2,"pr696_real_cost":41,"signed_real_cost":33,"work_peak_multiple":"33538055"}, + {"coefficient":"-16762880","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,-1,0,0,1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":36,"signed_real_cost":29,"work_peak_multiple":"16762880"}, + {"coefficient":"-16748544","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":35,"signed_real_cost":29,"work_peak_multiple":"16748544"}, + {"coefficient":"-12582776","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,-1,0,0,0],"occurrences":1,"pr696_real_cost":44,"signed_real_cost":29,"work_peak_multiple":"12582776"}, + {"coefficient":"-10485700","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,1,0,0],"occurrences":1,"pr696_real_cost":42,"signed_real_cost":29,"work_peak_multiple":"10485700"}, + {"coefficient":"-20951039/2","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":48,"signed_real_cost":33,"work_peak_multiple":"20951039"}, + {"coefficient":"-17301503/2","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":47,"signed_real_cost":31,"work_peak_multiple":"17301503"}, + {"coefficient":"-34078711/4","digits_after_leading_one":[0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,-1,1],"occurrences":1,"pr696_real_cost":48,"signed_real_cost":34,"work_peak_multiple":"34078711"}, + {"coefficient":"-33685499/4","digits_after_leading_one":[0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,1,1],"occurrences":1,"pr696_real_cost":46,"signed_real_cost":34,"work_peak_multiple":"33685499"}, + {"coefficient":"-8403008","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,-1,0,0,0,0,1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":29,"work_peak_multiple":"8403008"}, + {"coefficient":"-16785409/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":30,"work_peak_multiple":"16785409"}, + {"coefficient":"-8388608","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":9,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"8388608"}, + {"coefficient":"-16777215/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":3,"pr696_real_cost":50,"signed_real_cost":30,"work_peak_multiple":"16777215"}, + {"coefficient":"-33554177/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":46,"signed_real_cost":32,"work_peak_multiple":"33554177"}, + {"coefficient":"-8384514","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,1,0],"occurrences":2,"pr696_real_cost":36,"signed_real_cost":28,"work_peak_multiple":"8384514"}, + {"coefficient":"-8384384","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,-1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":39,"signed_real_cost":28,"work_peak_multiple":"8384384"}, + {"coefficient":"-8378366","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,-1,0],"occurrences":1,"pr696_real_cost":44,"signed_real_cost":29,"work_peak_multiple":"8378366"}, + {"coefficient":"-8372224","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":33,"signed_real_cost":27,"work_peak_multiple":"8372224"}, + {"coefficient":"-7340032","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"7340032"}, + {"coefficient":"-6291388","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,-1,0,0],"occurrences":1,"pr696_real_cost":43,"signed_real_cost":28,"work_peak_multiple":"6291388"}, + {"coefficient":"-17301503/4","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":48,"signed_real_cost":32,"work_peak_multiple":"17301503"}, + {"coefficient":"-4204480","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,1,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":31,"signed_real_cost":28,"work_peak_multiple":"4204480"}, + {"coefficient":"-4202496","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"4202496"}, + {"coefficient":"-4198401","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"4198401"}, + {"coefficient":"-4194305","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"4194305"}, + {"coefficient":"-8388609/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":28,"work_peak_multiple":"8388609"}, + {"coefficient":"-4194304","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"4194304"}, + {"coefficient":"-16777215/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":51,"signed_real_cost":31,"work_peak_multiple":"16777215"}, + {"coefficient":"-16777213/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":50,"signed_real_cost":31,"work_peak_multiple":"16777213"}, + {"coefficient":"-4194303","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":45,"signed_real_cost":27,"work_peak_multiple":"4194303"}, + {"coefficient":"-4192192","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":38,"signed_real_cost":27,"work_peak_multiple":"4192192"}, + {"coefficient":"-4189183","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":43,"signed_real_cost":29,"work_peak_multiple":"4189183"}, + {"coefficient":"-4186112","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":32,"signed_real_cost":26,"work_peak_multiple":"4186112"}, + {"coefficient":"-4184064","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":33,"signed_real_cost":27,"work_peak_multiple":"4184064"}, + {"coefficient":"-4167616","digits_after_leading_one":[0,0,0,0,0,0,-1,0,0,1,1,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":36,"signed_real_cost":29,"work_peak_multiple":"4167616"}, + {"coefficient":"-3670016","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"3670016"}, + {"coefficient":"-3132416","digits_after_leading_one":[1,0,0,0,0,0,-1,0,0,1,1,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":32,"signed_real_cost":28,"work_peak_multiple":"3132416"}, + {"coefficient":"-2637808","digits_after_leading_one":[0,1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,-1,0,0,0,0],"occurrences":2,"pr696_real_cost":35,"signed_real_cost":27,"work_peak_multiple":"2637808"}, + {"coefficient":"-2102240","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,1,0,0,0,0,-1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":30,"signed_real_cost":27,"work_peak_multiple":"2102240"}, + {"coefficient":"-2101248","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"2101248"}, + {"coefficient":"-8396807/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1,1],"occurrences":1,"pr696_real_cost":32,"signed_real_cost":32,"work_peak_multiple":"8396807"}, + {"coefficient":"-4198401/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":28,"work_peak_multiple":"4198401"}, + {"coefficient":"-2098336","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"2098336"}, + {"coefficient":"-2097220","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,1,0,0],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"2097220"}, + {"coefficient":"-4194307/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":28,"work_peak_multiple":"4194307"}, + {"coefficient":"-8388613/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,1],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":30,"work_peak_multiple":"8388613"}, + {"coefficient":"-2097153","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":3,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"2097153"}, + {"coefficient":"-4194305/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"4194305"}, + {"coefficient":"-2097152","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":24,"signed_real_cost":24,"work_peak_multiple":"2097152"}, + {"coefficient":"-8388607/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":49,"signed_real_cost":30,"work_peak_multiple":"8388607"}, + {"coefficient":"-4194303/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":46,"signed_real_cost":28,"work_peak_multiple":"4194303"}, + {"coefficient":"-2097092","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,1,0,0],"occurrences":1,"pr696_real_cost":38,"signed_real_cost":26,"work_peak_multiple":"2097092"}, + {"coefficient":"-2092032","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":32,"signed_real_cost":26,"work_peak_multiple":"2092032"}, + {"coefficient":"-2088960","digits_after_leading_one":[0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":30,"signed_real_cost":25,"work_peak_multiple":"2088960"}, + {"coefficient":"-8347645/4","digits_after_leading_one":[0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":46,"signed_real_cost":32,"work_peak_multiple":"8347645"}, + {"coefficient":"-2083808","digits_after_leading_one":[0,0,0,0,0,0,-1,0,0,1,1,0,0,0,0,-1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":35,"signed_real_cost":28,"work_peak_multiple":"2083808"}, + {"coefficient":"-2033040","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,1,0,1,1,0,0,1,0,0,0,0],"occurrences":2,"pr696_real_cost":31,"signed_real_cost":29,"work_peak_multiple":"2033040"}, + {"coefficient":"-1967520","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,1,0,1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":30,"signed_real_cost":29,"work_peak_multiple":"1967520"}, + {"coefficient":"-1566208","digits_after_leading_one":[1,0,0,0,0,0,-1,0,0,1,1,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":31,"signed_real_cost":27,"work_peak_multiple":"1566208"}, + {"coefficient":"-1318904","digits_after_leading_one":[0,1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,-1,0,0,0],"occurrences":4,"pr696_real_cost":34,"signed_real_cost":26,"work_peak_multiple":"1318904"}, + {"coefficient":"-1081312","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,0],"occurrences":1,"pr696_real_cost":33,"signed_real_cost":25,"work_peak_multiple":"1081312"}, + {"coefficient":"-1051648","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"1051648"}, + {"coefficient":"-1049280","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,1,1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"1049280"}, + {"coefficient":"-1049168","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0,0,0,0],"occurrences":5,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"1049168"}, + {"coefficient":"-2098335/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":32,"signed_real_cost":30,"work_peak_multiple":"2098335"}, + {"coefficient":"-1049024","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,-1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":25,"work_peak_multiple":"1049024"}, + {"coefficient":"-4194307/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":29,"work_peak_multiple":"4194307"}, + {"coefficient":"-2097153/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":5,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"2097153"}, + {"coefficient":"-1048576","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":11,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"1048576"}, + {"coefficient":"-1048440","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,-1,0,0,0],"occurrences":1,"pr696_real_cost":37,"signed_real_cost":25,"work_peak_multiple":"1048440"}, + {"coefficient":"-1044480","digits_after_leading_one":[0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":6,"pr696_real_cost":29,"signed_real_cost":24,"work_peak_multiple":"1044480"}, + {"coefficient":"-1032192","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":24,"work_peak_multiple":"1032192"}, + {"coefficient":"-1020032","digits_after_leading_one":[0,0,0,0,-1,0,0,1,0,0,0,0,1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":26,"work_peak_multiple":"1020032"}, + {"coefficient":"-1016520","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,1,0,1,1,0,0,1,0,0,0],"occurrences":4,"pr696_real_cost":30,"signed_real_cost":28,"work_peak_multiple":"1016520"}, + {"coefficient":"-1015808","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":26,"signed_real_cost":24,"work_peak_multiple":"1015808"}, + {"coefficient":"-1011840","digits_after_leading_one":[0,0,0,0,-1,0,0,-1,0,0,0,0,1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":26,"work_peak_multiple":"1011840"}, + {"coefficient":"-983760","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,1,0,1,0,0,0,0],"occurrences":5,"pr696_real_cost":29,"signed_real_cost":28,"work_peak_multiple":"983760"}, + {"coefficient":"-983728","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,0,1,1,0,0,0,0],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":28,"work_peak_multiple":"983728"}, + {"coefficient":"-918208","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,1,0,1,1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"918208"}, + {"coefficient":"-540656","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,-1,0,0,0,0],"occurrences":2,"pr696_real_cost":32,"signed_real_cost":24,"work_peak_multiple":"540656"}, + {"coefficient":"-540608","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":24,"work_peak_multiple":"540608"}, + {"coefficient":"-525824","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":24,"signed_real_cost":24,"work_peak_multiple":"525824"}, + {"coefficient":"-524640","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,1,1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"524640"}, + {"coefficient":"-524584","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0,0,0],"occurrences":3,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"524584"}, + {"coefficient":"-2098335/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0,0,0,-1,1],"occurrences":3,"pr696_real_cost":33,"signed_real_cost":31,"work_peak_multiple":"2098335"}, + {"coefficient":"-524512","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,-1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":25,"signed_real_cost":24,"work_peak_multiple":"524512"}, + {"coefficient":"-524288","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":10,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"524288"}, + {"coefficient":"-524286","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0],"occurrences":1,"pr696_real_cost":38,"signed_real_cost":23,"work_peak_multiple":"524286"}, + {"coefficient":"-524220","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,-1,0,0],"occurrences":2,"pr696_real_cost":36,"signed_real_cost":24,"work_peak_multiple":"524220"}, + {"coefficient":"-524092","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,1,0,0,0,-1,0,0],"occurrences":1,"pr696_real_cost":35,"signed_real_cost":25,"work_peak_multiple":"524092"}, + {"coefficient":"-516096","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":26,"signed_real_cost":23,"work_peak_multiple":"516096"}, + {"coefficient":"-510016","digits_after_leading_one":[0,0,0,0,-1,0,0,1,0,0,0,0,1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":27,"signed_real_cost":25,"work_peak_multiple":"510016"}, + {"coefficient":"-507904","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":5,"pr696_real_cost":25,"signed_real_cost":23,"work_peak_multiple":"507904"}, + {"coefficient":"-505920","digits_after_leading_one":[0,0,0,0,-1,0,0,-1,0,0,0,0,1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":28,"signed_real_cost":25,"work_peak_multiple":"505920"}, + {"coefficient":"-495544","digits_after_leading_one":[0,0,0,-1,0,0,1,0,0,0,0,0,-1,0,0,-1,0,0,0],"occurrences":1,"pr696_real_cost":32,"signed_real_cost":26,"work_peak_multiple":"495544"}, + {"coefficient":"-491880","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,1,0,1,0,0,0],"occurrences":2,"pr696_real_cost":28,"signed_real_cost":27,"work_peak_multiple":"491880"}, + {"coefficient":"-983729/2","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,0,1,1,0,0,0,1],"occurrences":1,"pr696_real_cost":31,"signed_real_cost":30,"work_peak_multiple":"983729"}, + {"coefficient":"-491864","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,0,1,1,0,0,0],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":27,"work_peak_multiple":"491864"}, + {"coefficient":"-918209/2","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,1,0,1,1,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":29,"work_peak_multiple":"918209"}, + {"coefficient":"-459104","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,1,0,1,1,0,0,0,0,0],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"459104"}, + {"coefficient":"-458752","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"458752"}, + {"coefficient":"-393216","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"393216"}, + {"coefficient":"-360448","digits_after_leading_one":[0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"360448"}, + {"coefficient":"-294912","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"294912"}, + {"coefficient":"-278529","digits_after_leading_one":[0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"278529"}, + {"coefficient":"-270336","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"270336"}, + {"coefficient":"-270304","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,-1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":29,"signed_real_cost":23,"work_peak_multiple":"270304"}, + {"coefficient":"-262145","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"262145"}, + {"coefficient":"-262144","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":5,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"262144"}, + {"coefficient":"-262143","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":3,"pr696_real_cost":37,"signed_real_cost":23,"work_peak_multiple":"262143"}, + {"coefficient":"-262046","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,1,0,0,0,-1,0],"occurrences":2,"pr696_real_cost":34,"signed_real_cost":24,"work_peak_multiple":"262046"}, + {"coefficient":"-253952","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":24,"signed_real_cost":22,"work_peak_multiple":"253952"}, + {"coefficient":"-247772","digits_after_leading_one":[0,0,0,-1,0,0,1,0,0,0,0,0,-1,0,0,-1,0,0],"occurrences":2,"pr696_real_cost":31,"signed_real_cost":25,"work_peak_multiple":"247772"}, + {"coefficient":"-229376","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":5,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"229376"}, + {"coefficient":"-196608","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"196608"}, + {"coefficient":"-180224","digits_after_leading_one":[0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"180224"}, + {"coefficient":"-294913/2","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":24,"signed_real_cost":24,"work_peak_multiple":"294913"}, + {"coefficient":"-147456","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"147456"}, + {"coefficient":"-278529/2","digits_after_leading_one":[0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":5,"pr696_real_cost":24,"signed_real_cost":24,"work_peak_multiple":"278529"}, + {"coefficient":"-135168","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"135168"}, + {"coefficient":"-262145/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":9,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"262145"}, + {"coefficient":"-131072","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":17,"pr696_real_cost":20,"signed_real_cost":20,"work_peak_multiple":"131072"}, + {"coefficient":"-262143/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":3,"pr696_real_cost":38,"signed_real_cost":24,"work_peak_multiple":"262143"}, + {"coefficient":"-262141/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":37,"signed_real_cost":24,"work_peak_multiple":"262141"}, + {"coefficient":"-245761/2","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":25,"signed_real_cost":24,"work_peak_multiple":"245761"}, + {"coefficient":"-114688","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":6,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"114688"}, + {"coefficient":"-294913/4","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":4,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"294913"}, + {"coefficient":"-278529/4","digits_after_leading_one":[0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"278529"}, + {"coefficient":"-65664","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":20,"signed_real_cost":20,"work_peak_multiple":"65664"}, + {"coefficient":"-262145/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":10,"pr696_real_cost":24,"signed_real_cost":24,"work_peak_multiple":"262145"}, + {"coefficient":"-65536","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":26,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"65536"}, + {"coefficient":"-131071/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":36,"signed_real_cost":23,"work_peak_multiple":"131071"}, + {"coefficient":"-65535","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":33,"signed_real_cost":21,"work_peak_multiple":"65535"}, + {"coefficient":"-65520","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":20,"work_peak_multiple":"65520"}, + {"coefficient":"-65408","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":26,"signed_real_cost":20,"work_peak_multiple":"65408"}, + {"coefficient":"-245763/4","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":26,"work_peak_multiple":"245763"}, + {"coefficient":"-245761/4","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":25,"work_peak_multiple":"245761"}, + {"coefficient":"-57344","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":20,"signed_real_cost":20,"work_peak_multiple":"57344"}, + {"coefficient":"-49153","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":20,"signed_real_cost":20,"work_peak_multiple":"49153"}, + {"coefficient":"-49152","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"49152"}, + {"coefficient":"-49151","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":32,"signed_real_cost":21,"work_peak_multiple":"49151"}, + {"coefficient":"-36864","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"36864"}, + {"coefficient":"-32832","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"32832"}, + {"coefficient":"-131327/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":25,"work_peak_multiple":"131327"}, + {"coefficient":"-32800","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,1,0,0,0,0,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"32800"}, + {"coefficient":"-32770","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,1,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"32770"}, + {"coefficient":"-32768","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":11,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"32768"}, + {"coefficient":"-131071/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":37,"signed_real_cost":24,"work_peak_multiple":"131071"}, + {"coefficient":"-32766","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":19,"work_peak_multiple":"32766"}, + {"coefficient":"-32760","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0],"occurrences":2,"pr696_real_cost":28,"signed_real_cost":19,"work_peak_multiple":"32760"}, + {"coefficient":"-32720","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,1,0,0,0,0],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":20,"work_peak_multiple":"32720"}, + {"coefficient":"-32704","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":25,"signed_real_cost":19,"work_peak_multiple":"32704"}, + {"coefficient":"-130815/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":36,"signed_real_cost":25,"work_peak_multiple":"130815"}, + {"coefficient":"-57345/2","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":6,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"57345"}, + {"coefficient":"-28672","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":5,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"28672"}, + {"coefficient":"-24576","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"24576"}, + {"coefficient":"-20480","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"20480"}, + {"coefficient":"-18432","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"18432"}, + {"coefficient":"-16394","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,1,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"16394"}, + {"coefficient":"-16385","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"16385"}, + {"coefficient":"-16384","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":16,"pr696_real_cost":17,"signed_real_cost":17,"work_peak_multiple":"16384"}, + {"coefficient":"-16383","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":19,"work_peak_multiple":"16383"}, + {"coefficient":"-16256","digits_after_leading_one":[0,0,0,0,0,0,-1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":22,"signed_real_cost":18,"work_peak_multiple":"16256"}, + {"coefficient":"-57599/4","digits_after_leading_one":[1,1,0,0,0,0,1,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":25,"work_peak_multiple":"57599"}, + {"coefficient":"-28673/2","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"28673"}, + {"coefficient":"-57345/4","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":4,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"57345"}, + {"coefficient":"-14336","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":6,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"14336"}, + {"coefficient":"-12288","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":17,"signed_real_cost":17,"work_peak_multiple":"12288"}, + {"coefficient":"-10240","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":6,"pr696_real_cost":17,"signed_real_cost":17,"work_peak_multiple":"10240"}, + {"coefficient":"-8198","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,1,0],"occurrences":1,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"8198"}, + {"coefficient":"-8197","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,1],"occurrences":1,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"8197"}, + {"coefficient":"-8196","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0],"occurrences":2,"pr696_real_cost":17,"signed_real_cost":17,"work_peak_multiple":"8196"}, + {"coefficient":"-8195","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"8195"}, + {"coefficient":"-8193","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":17,"signed_real_cost":17,"work_peak_multiple":"8193"}, + {"coefficient":"-8192","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":20,"pr696_real_cost":16,"signed_real_cost":16,"work_peak_multiple":"8192"}, + {"coefficient":"-8191","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":27,"signed_real_cost":18,"work_peak_multiple":"8191"}, + {"coefficient":"-8128","digits_after_leading_one":[0,0,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":21,"signed_real_cost":17,"work_peak_multiple":"8128"}, + {"coefficient":"-8068","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,1,0,0],"occurrences":1,"pr696_real_cost":21,"signed_real_cost":18,"work_peak_multiple":"8068"}, + {"coefficient":"-6144","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":16,"signed_real_cost":16,"work_peak_multiple":"6144"}, + {"coefficient":"-5120","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":16,"signed_real_cost":16,"work_peak_multiple":"5120"}, + {"coefficient":"-4098","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0],"occurrences":5,"pr696_real_cost":16,"signed_real_cost":16,"work_peak_multiple":"4098"}, + {"coefficient":"-8195/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"8195"}, + {"coefficient":"-8193/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"8193"}, + {"coefficient":"-16385/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":20,"signed_real_cost":20,"work_peak_multiple":"16385"}, + {"coefficient":"-4096","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":24,"pr696_real_cost":15,"signed_real_cost":15,"work_peak_multiple":"4096"}, + {"coefficient":"-8191/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":5,"pr696_real_cost":28,"signed_real_cost":19,"work_peak_multiple":"8191"}, + {"coefficient":"-8189/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":19,"work_peak_multiple":"8189"}, + {"coefficient":"-16377/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,0,1],"occurrences":2,"pr696_real_cost":29,"signed_real_cost":21,"work_peak_multiple":"16377"}, + {"coefficient":"-4079","digits_after_leading_one":[0,0,0,0,0,0,0,-1,0,0,-1,1],"occurrences":1,"pr696_real_cost":24,"signed_real_cost":18,"work_peak_multiple":"4079"}, + {"coefficient":"-4034","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,1,0],"occurrences":2,"pr696_real_cost":20,"signed_real_cost":17,"work_peak_multiple":"4034"}, + {"coefficient":"-4032","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":19,"signed_real_cost":16,"work_peak_multiple":"4032"}, + {"coefficient":"-4000","digits_after_leading_one":[0,0,0,0,-1,0,1,0,0,0,0,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":17,"work_peak_multiple":"4000"}, + {"coefficient":"-3968","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":18,"signed_real_cost":16,"work_peak_multiple":"3968"}, + {"coefficient":"-2560","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":15,"signed_real_cost":15,"work_peak_multiple":"2560"}, + {"coefficient":"-2048","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0],"occurrences":8,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"2048"}, + {"coefficient":"-4095/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":18,"work_peak_multiple":"4095"}, + {"coefficient":"-8189/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":20,"work_peak_multiple":"8189"}, + {"coefficient":"-4079/2","digits_after_leading_one":[0,0,0,0,0,0,0,-1,0,0,-1,1],"occurrences":2,"pr696_real_cost":25,"signed_real_cost":19,"work_peak_multiple":"4079"}, + {"coefficient":"-2016","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,0],"occurrences":4,"pr696_real_cost":18,"signed_real_cost":15,"work_peak_multiple":"2016"}, + {"coefficient":"-2000","digits_after_leading_one":[0,0,0,0,-1,0,1,0,0,0,0],"occurrences":2,"pr696_real_cost":18,"signed_real_cost":16,"work_peak_multiple":"2000"}, + {"coefficient":"-1984","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":17,"signed_real_cost":15,"work_peak_multiple":"1984"}, + {"coefficient":"-1408","digits_after_leading_one":[0,1,1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":15,"signed_real_cost":15,"work_peak_multiple":"1408"}, + {"coefficient":"-1280","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"1280"}, + {"coefficient":"-1152","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"1152"}, + {"coefficient":"-1024","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0],"occurrences":10,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"1024"}, + {"coefficient":"-960","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":15,"signed_real_cost":14,"work_peak_multiple":"960"}, + {"coefficient":"-832","digits_after_leading_one":[1,0,1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"832"}, + {"coefficient":"-768","digits_after_leading_one":[1,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"768"}, + {"coefficient":"-704","digits_after_leading_one":[0,1,1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"704"}, + {"coefficient":"-640","digits_after_leading_one":[0,1,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"640"}, + {"coefficient":"-576","digits_after_leading_one":[0,0,1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"576"}, + {"coefficient":"-512","digits_after_leading_one":[0,0,0,0,0,0,0,0,0],"occurrences":17,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"512"}, + {"coefficient":"-480","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":14,"signed_real_cost":13,"work_peak_multiple":"480"}, + {"coefficient":"-416","digits_after_leading_one":[1,0,1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"416"}, + {"coefficient":"-384","digits_after_leading_one":[1,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"384"}, + {"coefficient":"-320","digits_after_leading_one":[0,1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"320"}, + {"coefficient":"-260","digits_after_leading_one":[0,0,0,0,0,1,0,0],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"260"}, + {"coefficient":"-256","digits_after_leading_one":[0,0,0,0,0,0,0,0],"occurrences":13,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"256"}, + {"coefficient":"-255","digits_after_leading_one":[0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":17,"signed_real_cost":13,"work_peak_multiple":"255"}, + {"coefficient":"-252","digits_after_leading_one":[0,0,0,0,0,-1,0,0],"occurrences":2,"pr696_real_cost":15,"signed_real_cost":12,"work_peak_multiple":"252"}, + {"coefficient":"-249","digits_after_leading_one":[0,0,0,0,-1,0,0,1],"occurrences":1,"pr696_real_cost":15,"signed_real_cost":13,"work_peak_multiple":"249"}, + {"coefficient":"-160","digits_after_leading_one":[0,1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"160"}, + {"coefficient":"-144","digits_after_leading_one":[0,0,1,0,0,0,0],"occurrences":2,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"144"}, + {"coefficient":"-134","digits_after_leading_one":[0,0,0,0,1,1,0],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"134"}, + {"coefficient":"-130","digits_after_leading_one":[0,0,0,0,0,1,0],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"130"}, + {"coefficient":"-257/2","digits_after_leading_one":[0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"257"}, + {"coefficient":"-128","digits_after_leading_one":[0,0,0,0,0,0,0],"occurrences":20,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"128"}, + {"coefficient":"-126","digits_after_leading_one":[0,0,0,0,0,-1,0],"occurrences":4,"pr696_real_cost":14,"signed_real_cost":11,"work_peak_multiple":"126"}, + {"coefficient":"-125","digits_after_leading_one":[0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":12,"work_peak_multiple":"125"}, + {"coefficient":"-247/2","digits_after_leading_one":[0,0,0,0,-1,0,-1,1],"occurrences":1,"pr696_real_cost":17,"signed_real_cost":15,"work_peak_multiple":"247"}, + {"coefficient":"-120","digits_after_leading_one":[0,0,0,-1,0,0,0],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":11,"work_peak_multiple":"120"}, + {"coefficient":"-108","digits_after_leading_one":[1,0,1,1,0,0],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"108"}, + {"coefficient":"-96","digits_after_leading_one":[1,0,0,0,0,0],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"96"}, + {"coefficient":"-80","digits_after_leading_one":[0,1,0,0,0,0],"occurrences":4,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"80"}, + {"coefficient":"-79","digits_after_leading_one":[0,1,0,0,-1,1],"occurrences":1,"pr696_real_cost":13,"signed_real_cost":12,"work_peak_multiple":"79"}, + {"coefficient":"-76","digits_after_leading_one":[0,0,1,1,0,0],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"76"}, + {"coefficient":"-72","digits_after_leading_one":[0,0,1,0,0,0],"occurrences":5,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"72"}, + {"coefficient":"-68","digits_after_leading_one":[0,0,0,1,0,0],"occurrences":4,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"68"}, + {"coefficient":"-67","digits_after_leading_one":[0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"67"}, + {"coefficient":"-65","digits_after_leading_one":[0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"65"}, + {"coefficient":"-257/4","digits_after_leading_one":[0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"257"}, + {"coefficient":"-64","digits_after_leading_one":[0,0,0,0,0,0],"occurrences":68,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"64"}, + {"coefficient":"-63","digits_after_leading_one":[0,0,0,0,-1,1],"occurrences":5,"pr696_real_cost":13,"signed_real_cost":11,"work_peak_multiple":"63"}, + {"coefficient":"-62","digits_after_leading_one":[0,0,0,0,-1,0],"occurrences":2,"pr696_real_cost":12,"signed_real_cost":10,"work_peak_multiple":"62"}, + {"coefficient":"-60","digits_after_leading_one":[0,0,0,-1,0,0],"occurrences":6,"pr696_real_cost":11,"signed_real_cost":10,"work_peak_multiple":"60"}, + {"coefficient":"-58","digits_after_leading_one":[1,1,0,1,0],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"58"}, + {"coefficient":"-54","digits_after_leading_one":[1,0,1,1,0],"occurrences":3,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"54"}, + {"coefficient":"-52","digits_after_leading_one":[1,0,1,0,0],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"52"}, + {"coefficient":"-48","digits_after_leading_one":[1,0,0,0,0],"occurrences":2,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"48"}, + {"coefficient":"-40","digits_after_leading_one":[0,1,0,0,0],"occurrences":2,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"40"}, + {"coefficient":"-79/2","digits_after_leading_one":[0,1,0,0,-1,1],"occurrences":2,"pr696_real_cost":14,"signed_real_cost":13,"work_peak_multiple":"79"}, + {"coefficient":"-38","digits_after_leading_one":[0,0,1,1,0],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"38"}, + {"coefficient":"-36","digits_after_leading_one":[0,0,1,0,0],"occurrences":4,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"36"}, + {"coefficient":"-34","digits_after_leading_one":[0,0,0,1,0],"occurrences":6,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"34"}, + {"coefficient":"-67/2","digits_after_leading_one":[0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"67"}, + {"coefficient":"-32","digits_after_leading_one":[0,0,0,0,0],"occurrences":148,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"32"}, + {"coefficient":"-63/2","digits_after_leading_one":[0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":12,"work_peak_multiple":"63"}, + {"coefficient":"-31","digits_after_leading_one":[0,0,0,-1,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":10,"work_peak_multiple":"31"}, + {"coefficient":"-30","digits_after_leading_one":[0,0,0,-1,0],"occurrences":5,"pr696_real_cost":10,"signed_real_cost":9,"work_peak_multiple":"30"}, + {"coefficient":"-29","digits_after_leading_one":[1,1,0,1],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"29"}, + {"coefficient":"-28","digits_after_leading_one":[1,1,0,0],"occurrences":2,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"28"}, + {"coefficient":"-27","digits_after_leading_one":[1,0,1,1],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"27"}, + {"coefficient":"-26","digits_after_leading_one":[1,0,1,0],"occurrences":3,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"26"}, + {"coefficient":"-24","digits_after_leading_one":[1,0,0,0],"occurrences":9,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"24"}, + {"coefficient":"-22","digits_after_leading_one":[0,1,1,0],"occurrences":1,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"22"}, + {"coefficient":"-21","digits_after_leading_one":[0,1,0,1],"occurrences":2,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"21"}, + {"coefficient":"-20","digits_after_leading_one":[0,1,0,0],"occurrences":16,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"20"}, + {"coefficient":"-39/2","digits_after_leading_one":[0,0,1,1,1],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"39"}, + {"coefficient":"-19","digits_after_leading_one":[0,0,1,1],"occurrences":1,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"19"}, + {"coefficient":"-18","digits_after_leading_one":[0,0,1,0],"occurrences":16,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"18"}, + {"coefficient":"-17","digits_after_leading_one":[0,0,0,1],"occurrences":11,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"17"}, + {"coefficient":"-33/2","digits_after_leading_one":[0,0,0,0,1],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"33"}, + {"coefficient":"-16","digits_after_leading_one":[0,0,0,0],"occurrences":253,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"16"}, + {"coefficient":"-31/2","digits_after_leading_one":[0,0,0,-1,1],"occurrences":11,"pr696_real_cost":12,"signed_real_cost":11,"work_peak_multiple":"31"}, + {"coefficient":"-15","digits_after_leading_one":[1,1,1],"occurrences":19,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"15"}, + {"coefficient":"-29/2","digits_after_leading_one":[1,1,0,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"29"}, + {"coefficient":"-14","digits_after_leading_one":[1,1,0],"occurrences":10,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"14"}, + {"coefficient":"-27/2","digits_after_leading_one":[1,0,1,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"27"}, + {"coefficient":"-13","digits_after_leading_one":[1,0,1],"occurrences":3,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"13"}, + {"coefficient":"-12","digits_after_leading_one":[1,0,0],"occurrences":21,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"12"}, + {"coefficient":"-23/2","digits_after_leading_one":[0,1,1,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"23"}, + {"coefficient":"-11","digits_after_leading_one":[0,1,1],"occurrences":7,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"11"}, + {"coefficient":"-10","digits_after_leading_one":[0,1,0],"occurrences":26,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"10"}, + {"coefficient":"-19/2","digits_after_leading_one":[0,0,1,1],"occurrences":3,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"19"}, + {"coefficient":"-9","digits_after_leading_one":[0,0,1],"occurrences":25,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"9"}, + {"coefficient":"-17/2","digits_after_leading_one":[0,0,0,1],"occurrences":12,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"17"}, + {"coefficient":"-8","digits_after_leading_one":[0,0,0],"occurrences":502,"pr696_real_cost":6,"signed_real_cost":6,"work_peak_multiple":"8"}, + {"coefficient":"-31/4","digits_after_leading_one":[0,0,0,-1,1],"occurrences":4,"pr696_real_cost":13,"signed_real_cost":12,"work_peak_multiple":"31"}, + {"coefficient":"-15/2","digits_after_leading_one":[1,1,1],"occurrences":17,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"15"}, + {"coefficient":"-7","digits_after_leading_one":[1,1],"occurrences":32,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"7"}, + {"coefficient":"-13/2","digits_after_leading_one":[1,0,1],"occurrences":15,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"13"}, + {"coefficient":"-6","digits_after_leading_one":[1,0],"occurrences":55,"pr696_real_cost":6,"signed_real_cost":6,"work_peak_multiple":"6"}, + {"coefficient":"-11/2","digits_after_leading_one":[0,1,1],"occurrences":7,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"11"}, + {"coefficient":"-21/4","digits_after_leading_one":[0,1,0,1],"occurrences":2,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"21"}, + {"coefficient":"-5","digits_after_leading_one":[0,1],"occurrences":59,"pr696_real_cost":6,"signed_real_cost":6,"work_peak_multiple":"5"}, + {"coefficient":"-39/8","digits_after_leading_one":[0,0,1,1,1],"occurrences":2,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"39"}, + {"coefficient":"-19/4","digits_after_leading_one":[0,0,1,1],"occurrences":4,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"19"}, + {"coefficient":"-9/2","digits_after_leading_one":[0,0,1],"occurrences":31,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"9"}, + {"coefficient":"-35/8","digits_after_leading_one":[0,0,0,1,1],"occurrences":1,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"35"}, + {"coefficient":"-17/4","digits_after_leading_one":[0,0,0,1],"occurrences":4,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"17"}, + {"coefficient":"-4","digits_after_leading_one":[0,0],"occurrences":833,"pr696_real_cost":5,"signed_real_cost":5,"work_peak_multiple":"4"}, + {"coefficient":"-31/8","digits_after_leading_one":[0,0,0,-1,1],"occurrences":4,"pr696_real_cost":14,"signed_real_cost":13,"work_peak_multiple":"31"}, + {"coefficient":"-15/4","digits_after_leading_one":[1,1,1],"occurrences":8,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"15"}, + {"coefficient":"-29/8","digits_after_leading_one":[1,1,0,1],"occurrences":1,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"29"}, + {"coefficient":"-7/2","digits_after_leading_one":[1,1],"occurrences":36,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"7"}, + {"coefficient":"-13/4","digits_after_leading_one":[1,0,1],"occurrences":2,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"13"}, + {"coefficient":"-3","digits_after_leading_one":[1],"occurrences":196,"pr696_real_cost":5,"signed_real_cost":5,"work_peak_multiple":"3"}, + {"coefficient":"-23/8","digits_after_leading_one":[0,1,1,1],"occurrences":5,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"23"}, + {"coefficient":"-11/4","digits_after_leading_one":[0,1,1],"occurrences":2,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"11"}, + {"coefficient":"-5/2","digits_after_leading_one":[0,1],"occurrences":74,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"5"}, + {"coefficient":"-9/4","digits_after_leading_one":[0,0,1],"occurrences":7,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"9"}, + {"coefficient":"-17/8","digits_after_leading_one":[0,0,0,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"17"}, + {"coefficient":"-2","digits_after_leading_one":[0],"occurrences":2790,"pr696_real_cost":4,"signed_real_cost":4,"work_peak_multiple":"2"}, + {"coefficient":"-15/8","digits_after_leading_one":[1,1,1],"occurrences":3,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"15"}, + {"coefficient":"-7/4","digits_after_leading_one":[1,1],"occurrences":8,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"7"}, + {"coefficient":"-3/2","digits_after_leading_one":[1],"occurrences":213,"pr696_real_cost":6,"signed_real_cost":6,"work_peak_multiple":"3"}, + {"coefficient":"-5/4","digits_after_leading_one":[0,1],"occurrences":28,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"5"}, + {"coefficient":"-9/8","digits_after_leading_one":[0,0,1],"occurrences":3,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"9"}, + {"coefficient":"-1","digits_after_leading_one":[],"occurrences":12448,"pr696_real_cost":2,"signed_real_cost":2,"work_peak_multiple":"0"}, + {"coefficient":"-7/8","digits_after_leading_one":[1,1],"occurrences":2,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"7"}, + {"coefficient":"-3/4","digits_after_leading_one":[1],"occurrences":510,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"3"}, + {"coefficient":"-5/8","digits_after_leading_one":[0,1],"occurrences":5,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"5"}, + {"coefficient":"-1/2","digits_after_leading_one":[],"occurrences":11766,"pr696_real_cost":4,"signed_real_cost":4,"work_peak_multiple":"1"}, + {"coefficient":"-3/8","digits_after_leading_one":[1],"occurrences":11,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"3"}, + {"coefficient":"-1/4","digits_after_leading_one":[],"occurrences":12319,"pr696_real_cost":5,"signed_real_cost":5,"work_peak_multiple":"1"}, + {"coefficient":"-1/8","digits_after_leading_one":[],"occurrences":30,"pr696_real_cost":6,"signed_real_cost":6,"work_peak_multiple":"1"}, + {"coefficient":"-1/16","digits_after_leading_one":[],"occurrences":1,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"1"}, + {"coefficient":"-1/32","digits_after_leading_one":[],"occurrences":3,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"1"}, + {"coefficient":"-1/64","digits_after_leading_one":[],"occurrences":3,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"1"}, + {"coefficient":"-1/16777216","digits_after_leading_one":[],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"1"}, + {"coefficient":"1/16777216","digits_after_leading_one":[],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"1"}, + {"coefficient":"1/64","digits_after_leading_one":[],"occurrences":3,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"1"}, + {"coefficient":"1/32","digits_after_leading_one":[],"occurrences":3,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"1"}, + {"coefficient":"1/16","digits_after_leading_one":[],"occurrences":1,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"1"}, + {"coefficient":"1/8","digits_after_leading_one":[],"occurrences":30,"pr696_real_cost":6,"signed_real_cost":6,"work_peak_multiple":"1"}, + {"coefficient":"1/4","digits_after_leading_one":[],"occurrences":12767,"pr696_real_cost":5,"signed_real_cost":5,"work_peak_multiple":"1"}, + {"coefficient":"3/8","digits_after_leading_one":[1],"occurrences":11,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"3"}, + {"coefficient":"1/2","digits_after_leading_one":[],"occurrences":11766,"pr696_real_cost":4,"signed_real_cost":4,"work_peak_multiple":"1"}, + {"coefficient":"5/8","digits_after_leading_one":[0,1],"occurrences":5,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"5"}, + {"coefficient":"3/4","digits_after_leading_one":[1],"occurrences":510,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"3"}, + {"coefficient":"7/8","digits_after_leading_one":[1,1],"occurrences":2,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"7"}, + {"coefficient":"1","digits_after_leading_one":[],"occurrences":12432,"pr696_real_cost":2,"signed_real_cost":2,"work_peak_multiple":"0"}, + {"coefficient":"9/8","digits_after_leading_one":[0,0,1],"occurrences":3,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"9"}, + {"coefficient":"5/4","digits_after_leading_one":[0,1],"occurrences":28,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"5"}, + {"coefficient":"3/2","digits_after_leading_one":[1],"occurrences":213,"pr696_real_cost":6,"signed_real_cost":6,"work_peak_multiple":"3"}, + {"coefficient":"7/4","digits_after_leading_one":[1,1],"occurrences":8,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"7"}, + {"coefficient":"15/8","digits_after_leading_one":[1,1,1],"occurrences":3,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"15"}, + {"coefficient":"2","digits_after_leading_one":[0],"occurrences":2790,"pr696_real_cost":4,"signed_real_cost":4,"work_peak_multiple":"2"}, + {"coefficient":"17/8","digits_after_leading_one":[0,0,0,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"17"}, + {"coefficient":"9/4","digits_after_leading_one":[0,0,1],"occurrences":7,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"9"}, + {"coefficient":"5/2","digits_after_leading_one":[0,1],"occurrences":74,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"5"}, + {"coefficient":"11/4","digits_after_leading_one":[0,1,1],"occurrences":2,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"11"}, + {"coefficient":"23/8","digits_after_leading_one":[0,1,1,1],"occurrences":5,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"23"}, + {"coefficient":"3","digits_after_leading_one":[1],"occurrences":196,"pr696_real_cost":5,"signed_real_cost":5,"work_peak_multiple":"3"}, + {"coefficient":"13/4","digits_after_leading_one":[1,0,1],"occurrences":2,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"13"}, + {"coefficient":"7/2","digits_after_leading_one":[1,1],"occurrences":36,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"7"}, + {"coefficient":"29/8","digits_after_leading_one":[1,1,0,1],"occurrences":1,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"29"}, + {"coefficient":"15/4","digits_after_leading_one":[1,1,1],"occurrences":8,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"15"}, + {"coefficient":"31/8","digits_after_leading_one":[0,0,0,-1,1],"occurrences":4,"pr696_real_cost":14,"signed_real_cost":13,"work_peak_multiple":"31"}, + {"coefficient":"4","digits_after_leading_one":[0,0],"occurrences":833,"pr696_real_cost":5,"signed_real_cost":5,"work_peak_multiple":"4"}, + {"coefficient":"17/4","digits_after_leading_one":[0,0,0,1],"occurrences":4,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"17"}, + {"coefficient":"35/8","digits_after_leading_one":[0,0,0,1,1],"occurrences":1,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"35"}, + {"coefficient":"9/2","digits_after_leading_one":[0,0,1],"occurrences":31,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"9"}, + {"coefficient":"19/4","digits_after_leading_one":[0,0,1,1],"occurrences":4,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"19"}, + {"coefficient":"39/8","digits_after_leading_one":[0,0,1,1,1],"occurrences":2,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"39"}, + {"coefficient":"5","digits_after_leading_one":[0,1],"occurrences":59,"pr696_real_cost":6,"signed_real_cost":6,"work_peak_multiple":"5"}, + {"coefficient":"21/4","digits_after_leading_one":[0,1,0,1],"occurrences":2,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"21"}, + {"coefficient":"11/2","digits_after_leading_one":[0,1,1],"occurrences":7,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"11"}, + {"coefficient":"6","digits_after_leading_one":[1,0],"occurrences":55,"pr696_real_cost":6,"signed_real_cost":6,"work_peak_multiple":"6"}, + {"coefficient":"13/2","digits_after_leading_one":[1,0,1],"occurrences":15,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"13"}, + {"coefficient":"7","digits_after_leading_one":[1,1],"occurrences":32,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"7"}, + {"coefficient":"15/2","digits_after_leading_one":[1,1,1],"occurrences":17,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"15"}, + {"coefficient":"31/4","digits_after_leading_one":[0,0,0,-1,1],"occurrences":4,"pr696_real_cost":13,"signed_real_cost":12,"work_peak_multiple":"31"}, + {"coefficient":"8","digits_after_leading_one":[0,0,0],"occurrences":502,"pr696_real_cost":6,"signed_real_cost":6,"work_peak_multiple":"8"}, + {"coefficient":"17/2","digits_after_leading_one":[0,0,0,1],"occurrences":12,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"17"}, + {"coefficient":"9","digits_after_leading_one":[0,0,1],"occurrences":25,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"9"}, + {"coefficient":"19/2","digits_after_leading_one":[0,0,1,1],"occurrences":3,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"19"}, + {"coefficient":"10","digits_after_leading_one":[0,1,0],"occurrences":26,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"10"}, + {"coefficient":"11","digits_after_leading_one":[0,1,1],"occurrences":7,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"11"}, + {"coefficient":"23/2","digits_after_leading_one":[0,1,1,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"23"}, + {"coefficient":"12","digits_after_leading_one":[1,0,0],"occurrences":21,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"12"}, + {"coefficient":"13","digits_after_leading_one":[1,0,1],"occurrences":3,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"13"}, + {"coefficient":"27/2","digits_after_leading_one":[1,0,1,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"27"}, + {"coefficient":"14","digits_after_leading_one":[1,1,0],"occurrences":10,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"14"}, + {"coefficient":"29/2","digits_after_leading_one":[1,1,0,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"29"}, + {"coefficient":"15","digits_after_leading_one":[1,1,1],"occurrences":19,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"15"}, + {"coefficient":"31/2","digits_after_leading_one":[0,0,0,-1,1],"occurrences":11,"pr696_real_cost":12,"signed_real_cost":11,"work_peak_multiple":"31"}, + {"coefficient":"16","digits_after_leading_one":[0,0,0,0],"occurrences":253,"pr696_real_cost":7,"signed_real_cost":7,"work_peak_multiple":"16"}, + {"coefficient":"33/2","digits_after_leading_one":[0,0,0,0,1],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"33"}, + {"coefficient":"17","digits_after_leading_one":[0,0,0,1],"occurrences":11,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"17"}, + {"coefficient":"18","digits_after_leading_one":[0,0,1,0],"occurrences":16,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"18"}, + {"coefficient":"19","digits_after_leading_one":[0,0,1,1],"occurrences":1,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"19"}, + {"coefficient":"39/2","digits_after_leading_one":[0,0,1,1,1],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"39"}, + {"coefficient":"20","digits_after_leading_one":[0,1,0,0],"occurrences":16,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"20"}, + {"coefficient":"21","digits_after_leading_one":[0,1,0,1],"occurrences":2,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"21"}, + {"coefficient":"22","digits_after_leading_one":[0,1,1,0],"occurrences":1,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"22"}, + {"coefficient":"24","digits_after_leading_one":[1,0,0,0],"occurrences":9,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"24"}, + {"coefficient":"26","digits_after_leading_one":[1,0,1,0],"occurrences":3,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"26"}, + {"coefficient":"27","digits_after_leading_one":[1,0,1,1],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"27"}, + {"coefficient":"28","digits_after_leading_one":[1,1,0,0],"occurrences":2,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"28"}, + {"coefficient":"29","digits_after_leading_one":[1,1,0,1],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"29"}, + {"coefficient":"30","digits_after_leading_one":[0,0,0,-1,0],"occurrences":5,"pr696_real_cost":10,"signed_real_cost":9,"work_peak_multiple":"30"}, + {"coefficient":"31","digits_after_leading_one":[0,0,0,-1,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":10,"work_peak_multiple":"31"}, + {"coefficient":"63/2","digits_after_leading_one":[0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":12,"work_peak_multiple":"63"}, + {"coefficient":"32","digits_after_leading_one":[0,0,0,0,0],"occurrences":148,"pr696_real_cost":8,"signed_real_cost":8,"work_peak_multiple":"32"}, + {"coefficient":"67/2","digits_after_leading_one":[0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"67"}, + {"coefficient":"34","digits_after_leading_one":[0,0,0,1,0],"occurrences":6,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"34"}, + {"coefficient":"36","digits_after_leading_one":[0,0,1,0,0],"occurrences":4,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"36"}, + {"coefficient":"38","digits_after_leading_one":[0,0,1,1,0],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"38"}, + {"coefficient":"79/2","digits_after_leading_one":[0,1,0,0,-1,1],"occurrences":2,"pr696_real_cost":14,"signed_real_cost":13,"work_peak_multiple":"79"}, + {"coefficient":"40","digits_after_leading_one":[0,1,0,0,0],"occurrences":2,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"40"}, + {"coefficient":"48","digits_after_leading_one":[1,0,0,0,0],"occurrences":2,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"48"}, + {"coefficient":"52","digits_after_leading_one":[1,0,1,0,0],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"52"}, + {"coefficient":"54","digits_after_leading_one":[1,0,1,1,0],"occurrences":3,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"54"}, + {"coefficient":"58","digits_after_leading_one":[1,1,0,1,0],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"58"}, + {"coefficient":"60","digits_after_leading_one":[0,0,0,-1,0,0],"occurrences":6,"pr696_real_cost":11,"signed_real_cost":10,"work_peak_multiple":"60"}, + {"coefficient":"62","digits_after_leading_one":[0,0,0,0,-1,0],"occurrences":2,"pr696_real_cost":12,"signed_real_cost":10,"work_peak_multiple":"62"}, + {"coefficient":"63","digits_after_leading_one":[0,0,0,0,-1,1],"occurrences":5,"pr696_real_cost":13,"signed_real_cost":11,"work_peak_multiple":"63"}, + {"coefficient":"64","digits_after_leading_one":[0,0,0,0,0,0],"occurrences":68,"pr696_real_cost":9,"signed_real_cost":9,"work_peak_multiple":"64"}, + {"coefficient":"257/4","digits_after_leading_one":[0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"257"}, + {"coefficient":"65","digits_after_leading_one":[0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"65"}, + {"coefficient":"67","digits_after_leading_one":[0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"67"}, + {"coefficient":"68","digits_after_leading_one":[0,0,0,1,0,0],"occurrences":4,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"68"}, + {"coefficient":"72","digits_after_leading_one":[0,0,1,0,0,0],"occurrences":5,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"72"}, + {"coefficient":"76","digits_after_leading_one":[0,0,1,1,0,0],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"76"}, + {"coefficient":"79","digits_after_leading_one":[0,1,0,0,-1,1],"occurrences":1,"pr696_real_cost":13,"signed_real_cost":12,"work_peak_multiple":"79"}, + {"coefficient":"80","digits_after_leading_one":[0,1,0,0,0,0],"occurrences":4,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"80"}, + {"coefficient":"96","digits_after_leading_one":[1,0,0,0,0,0],"occurrences":1,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"96"}, + {"coefficient":"108","digits_after_leading_one":[1,0,1,1,0,0],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"108"}, + {"coefficient":"120","digits_after_leading_one":[0,0,0,-1,0,0,0],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":11,"work_peak_multiple":"120"}, + {"coefficient":"247/2","digits_after_leading_one":[0,0,0,0,-1,0,-1,1],"occurrences":1,"pr696_real_cost":17,"signed_real_cost":15,"work_peak_multiple":"247"}, + {"coefficient":"125","digits_after_leading_one":[0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":12,"work_peak_multiple":"125"}, + {"coefficient":"126","digits_after_leading_one":[0,0,0,0,0,-1,0],"occurrences":4,"pr696_real_cost":14,"signed_real_cost":11,"work_peak_multiple":"126"}, + {"coefficient":"128","digits_after_leading_one":[0,0,0,0,0,0,0],"occurrences":20,"pr696_real_cost":10,"signed_real_cost":10,"work_peak_multiple":"128"}, + {"coefficient":"257/2","digits_after_leading_one":[0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"257"}, + {"coefficient":"130","digits_after_leading_one":[0,0,0,0,0,1,0],"occurrences":1,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"130"}, + {"coefficient":"134","digits_after_leading_one":[0,0,0,0,1,1,0],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"134"}, + {"coefficient":"144","digits_after_leading_one":[0,0,1,0,0,0,0],"occurrences":2,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"144"}, + {"coefficient":"160","digits_after_leading_one":[0,1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"160"}, + {"coefficient":"249","digits_after_leading_one":[0,0,0,0,-1,0,0,1],"occurrences":1,"pr696_real_cost":15,"signed_real_cost":13,"work_peak_multiple":"249"}, + {"coefficient":"252","digits_after_leading_one":[0,0,0,0,0,-1,0,0],"occurrences":2,"pr696_real_cost":15,"signed_real_cost":12,"work_peak_multiple":"252"}, + {"coefficient":"255","digits_after_leading_one":[0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":17,"signed_real_cost":13,"work_peak_multiple":"255"}, + {"coefficient":"256","digits_after_leading_one":[0,0,0,0,0,0,0,0],"occurrences":13,"pr696_real_cost":11,"signed_real_cost":11,"work_peak_multiple":"256"}, + {"coefficient":"260","digits_after_leading_one":[0,0,0,0,0,1,0,0],"occurrences":1,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"260"}, + {"coefficient":"320","digits_after_leading_one":[0,1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"320"}, + {"coefficient":"384","digits_after_leading_one":[1,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"384"}, + {"coefficient":"416","digits_after_leading_one":[1,0,1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"416"}, + {"coefficient":"480","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":14,"signed_real_cost":13,"work_peak_multiple":"480"}, + {"coefficient":"512","digits_after_leading_one":[0,0,0,0,0,0,0,0,0],"occurrences":17,"pr696_real_cost":12,"signed_real_cost":12,"work_peak_multiple":"512"}, + {"coefficient":"576","digits_after_leading_one":[0,0,1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"576"}, + {"coefficient":"640","digits_after_leading_one":[0,1,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"640"}, + {"coefficient":"704","digits_after_leading_one":[0,1,1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"704"}, + {"coefficient":"768","digits_after_leading_one":[1,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"768"}, + {"coefficient":"832","digits_after_leading_one":[1,0,1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"832"}, + {"coefficient":"960","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":15,"signed_real_cost":14,"work_peak_multiple":"960"}, + {"coefficient":"1024","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0],"occurrences":10,"pr696_real_cost":13,"signed_real_cost":13,"work_peak_multiple":"1024"}, + {"coefficient":"1152","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"1152"}, + {"coefficient":"1280","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"1280"}, + {"coefficient":"1408","digits_after_leading_one":[0,1,1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":15,"signed_real_cost":15,"work_peak_multiple":"1408"}, + {"coefficient":"1984","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":17,"signed_real_cost":15,"work_peak_multiple":"1984"}, + {"coefficient":"2000","digits_after_leading_one":[0,0,0,0,-1,0,1,0,0,0,0],"occurrences":2,"pr696_real_cost":18,"signed_real_cost":16,"work_peak_multiple":"2000"}, + {"coefficient":"2016","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,0],"occurrences":4,"pr696_real_cost":18,"signed_real_cost":15,"work_peak_multiple":"2016"}, + {"coefficient":"4079/2","digits_after_leading_one":[0,0,0,0,0,0,0,-1,0,0,-1,1],"occurrences":2,"pr696_real_cost":25,"signed_real_cost":19,"work_peak_multiple":"4079"}, + {"coefficient":"8189/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":20,"work_peak_multiple":"8189"}, + {"coefficient":"4095/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":18,"work_peak_multiple":"4095"}, + {"coefficient":"2048","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0],"occurrences":8,"pr696_real_cost":14,"signed_real_cost":14,"work_peak_multiple":"2048"}, + {"coefficient":"2560","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":15,"signed_real_cost":15,"work_peak_multiple":"2560"}, + {"coefficient":"3968","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":18,"signed_real_cost":16,"work_peak_multiple":"3968"}, + {"coefficient":"4000","digits_after_leading_one":[0,0,0,0,-1,0,1,0,0,0,0,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":17,"work_peak_multiple":"4000"}, + {"coefficient":"4032","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":19,"signed_real_cost":16,"work_peak_multiple":"4032"}, + {"coefficient":"4034","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,1,0],"occurrences":2,"pr696_real_cost":20,"signed_real_cost":17,"work_peak_multiple":"4034"}, + {"coefficient":"4079","digits_after_leading_one":[0,0,0,0,0,0,0,-1,0,0,-1,1],"occurrences":1,"pr696_real_cost":24,"signed_real_cost":18,"work_peak_multiple":"4079"}, + {"coefficient":"16377/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,0,1],"occurrences":2,"pr696_real_cost":29,"signed_real_cost":21,"work_peak_multiple":"16377"}, + {"coefficient":"8189/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":19,"work_peak_multiple":"8189"}, + {"coefficient":"8191/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":5,"pr696_real_cost":28,"signed_real_cost":19,"work_peak_multiple":"8191"}, + {"coefficient":"4096","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":24,"pr696_real_cost":15,"signed_real_cost":15,"work_peak_multiple":"4096"}, + {"coefficient":"16385/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":20,"signed_real_cost":20,"work_peak_multiple":"16385"}, + {"coefficient":"8193/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"8193"}, + {"coefficient":"8195/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"8195"}, + {"coefficient":"4098","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0],"occurrences":5,"pr696_real_cost":16,"signed_real_cost":16,"work_peak_multiple":"4098"}, + {"coefficient":"5120","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":16,"signed_real_cost":16,"work_peak_multiple":"5120"}, + {"coefficient":"6144","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":16,"signed_real_cost":16,"work_peak_multiple":"6144"}, + {"coefficient":"8068","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,1,0,0],"occurrences":1,"pr696_real_cost":21,"signed_real_cost":18,"work_peak_multiple":"8068"}, + {"coefficient":"8128","digits_after_leading_one":[0,0,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":21,"signed_real_cost":17,"work_peak_multiple":"8128"}, + {"coefficient":"8191","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":27,"signed_real_cost":18,"work_peak_multiple":"8191"}, + {"coefficient":"8192","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":20,"pr696_real_cost":16,"signed_real_cost":16,"work_peak_multiple":"8192"}, + {"coefficient":"8193","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":17,"signed_real_cost":17,"work_peak_multiple":"8193"}, + {"coefficient":"8195","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"8195"}, + {"coefficient":"8196","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0],"occurrences":2,"pr696_real_cost":17,"signed_real_cost":17,"work_peak_multiple":"8196"}, + {"coefficient":"8197","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,1],"occurrences":1,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"8197"}, + {"coefficient":"8198","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,1,0],"occurrences":1,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"8198"}, + {"coefficient":"10240","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":6,"pr696_real_cost":17,"signed_real_cost":17,"work_peak_multiple":"10240"}, + {"coefficient":"12288","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":17,"signed_real_cost":17,"work_peak_multiple":"12288"}, + {"coefficient":"14336","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":6,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"14336"}, + {"coefficient":"57345/4","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":4,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"57345"}, + {"coefficient":"28673/2","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"28673"}, + {"coefficient":"57599/4","digits_after_leading_one":[1,1,0,0,0,0,1,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":25,"work_peak_multiple":"57599"}, + {"coefficient":"16256","digits_after_leading_one":[0,0,0,0,0,0,-1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":22,"signed_real_cost":18,"work_peak_multiple":"16256"}, + {"coefficient":"16383","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":19,"work_peak_multiple":"16383"}, + {"coefficient":"16384","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":16,"pr696_real_cost":17,"signed_real_cost":17,"work_peak_multiple":"16384"}, + {"coefficient":"16385","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"16385"}, + {"coefficient":"16394","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,1,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"16394"}, + {"coefficient":"18432","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"18432"}, + {"coefficient":"20480","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"20480"}, + {"coefficient":"24576","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"24576"}, + {"coefficient":"28672","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":5,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"28672"}, + {"coefficient":"57345/2","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":6,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"57345"}, + {"coefficient":"130815/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":36,"signed_real_cost":25,"work_peak_multiple":"130815"}, + {"coefficient":"32704","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":25,"signed_real_cost":19,"work_peak_multiple":"32704"}, + {"coefficient":"32720","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,1,0,0,0,0],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":20,"work_peak_multiple":"32720"}, + {"coefficient":"32760","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0],"occurrences":2,"pr696_real_cost":28,"signed_real_cost":19,"work_peak_multiple":"32760"}, + {"coefficient":"32766","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":19,"work_peak_multiple":"32766"}, + {"coefficient":"131071/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":37,"signed_real_cost":24,"work_peak_multiple":"131071"}, + {"coefficient":"32768","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":11,"pr696_real_cost":18,"signed_real_cost":18,"work_peak_multiple":"32768"}, + {"coefficient":"32770","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,1,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"32770"}, + {"coefficient":"32800","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,1,0,0,0,0,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"32800"}, + {"coefficient":"131327/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":25,"work_peak_multiple":"131327"}, + {"coefficient":"32832","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"32832"}, + {"coefficient":"36864","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"36864"}, + {"coefficient":"49151","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":32,"signed_real_cost":21,"work_peak_multiple":"49151"}, + {"coefficient":"49152","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"49152"}, + {"coefficient":"49153","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":20,"signed_real_cost":20,"work_peak_multiple":"49153"}, + {"coefficient":"57344","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":20,"signed_real_cost":20,"work_peak_multiple":"57344"}, + {"coefficient":"245761/4","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":25,"work_peak_multiple":"245761"}, + {"coefficient":"245763/4","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":26,"work_peak_multiple":"245763"}, + {"coefficient":"65408","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":26,"signed_real_cost":20,"work_peak_multiple":"65408"}, + {"coefficient":"65520","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":20,"work_peak_multiple":"65520"}, + {"coefficient":"65535","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":33,"signed_real_cost":21,"work_peak_multiple":"65535"}, + {"coefficient":"131071/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":36,"signed_real_cost":23,"work_peak_multiple":"131071"}, + {"coefficient":"65536","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":26,"pr696_real_cost":19,"signed_real_cost":19,"work_peak_multiple":"65536"}, + {"coefficient":"262145/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":10,"pr696_real_cost":24,"signed_real_cost":24,"work_peak_multiple":"262145"}, + {"coefficient":"65664","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":20,"signed_real_cost":20,"work_peak_multiple":"65664"}, + {"coefficient":"278529/4","digits_after_leading_one":[0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"278529"}, + {"coefficient":"294913/4","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":4,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"294913"}, + {"coefficient":"114688","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":6,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"114688"}, + {"coefficient":"245761/2","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":25,"signed_real_cost":24,"work_peak_multiple":"245761"}, + {"coefficient":"262141/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":37,"signed_real_cost":24,"work_peak_multiple":"262141"}, + {"coefficient":"262143/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":3,"pr696_real_cost":38,"signed_real_cost":24,"work_peak_multiple":"262143"}, + {"coefficient":"131072","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":17,"pr696_real_cost":20,"signed_real_cost":20,"work_peak_multiple":"131072"}, + {"coefficient":"262145/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":9,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"262145"}, + {"coefficient":"135168","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"135168"}, + {"coefficient":"278529/2","digits_after_leading_one":[0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":5,"pr696_real_cost":24,"signed_real_cost":24,"work_peak_multiple":"278529"}, + {"coefficient":"147456","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"147456"}, + {"coefficient":"294913/2","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":24,"signed_real_cost":24,"work_peak_multiple":"294913"}, + {"coefficient":"180224","digits_after_leading_one":[0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"180224"}, + {"coefficient":"196608","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"196608"}, + {"coefficient":"229376","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":5,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"229376"}, + {"coefficient":"247772","digits_after_leading_one":[0,0,0,-1,0,0,1,0,0,0,0,0,-1,0,0,-1,0,0],"occurrences":2,"pr696_real_cost":31,"signed_real_cost":25,"work_peak_multiple":"247772"}, + {"coefficient":"253952","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":24,"signed_real_cost":22,"work_peak_multiple":"253952"}, + {"coefficient":"262046","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,1,0,0,0,-1,0],"occurrences":2,"pr696_real_cost":34,"signed_real_cost":24,"work_peak_multiple":"262046"}, + {"coefficient":"262143","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":3,"pr696_real_cost":37,"signed_real_cost":23,"work_peak_multiple":"262143"}, + {"coefficient":"262144","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":5,"pr696_real_cost":21,"signed_real_cost":21,"work_peak_multiple":"262144"}, + {"coefficient":"262145","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"262145"}, + {"coefficient":"270304","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,-1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":29,"signed_real_cost":23,"work_peak_multiple":"270304"}, + {"coefficient":"270336","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"270336"}, + {"coefficient":"278529","digits_after_leading_one":[0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"278529"}, + {"coefficient":"294912","digits_after_leading_one":[0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"294912"}, + {"coefficient":"360448","digits_after_leading_one":[0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"360448"}, + {"coefficient":"393216","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"393216"}, + {"coefficient":"458752","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"458752"}, + {"coefficient":"459104","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,1,0,1,1,0,0,0,0,0],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"459104"}, + {"coefficient":"918209/2","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,1,0,1,1,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":29,"work_peak_multiple":"918209"}, + {"coefficient":"491864","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,0,1,1,0,0,0],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":27,"work_peak_multiple":"491864"}, + {"coefficient":"983729/2","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,0,1,1,0,0,0,1],"occurrences":1,"pr696_real_cost":31,"signed_real_cost":30,"work_peak_multiple":"983729"}, + {"coefficient":"491880","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,1,0,1,0,0,0],"occurrences":2,"pr696_real_cost":28,"signed_real_cost":27,"work_peak_multiple":"491880"}, + {"coefficient":"495544","digits_after_leading_one":[0,0,0,-1,0,0,1,0,0,0,0,0,-1,0,0,-1,0,0,0],"occurrences":1,"pr696_real_cost":32,"signed_real_cost":26,"work_peak_multiple":"495544"}, + {"coefficient":"505920","digits_after_leading_one":[0,0,0,0,-1,0,0,-1,0,0,0,0,1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":28,"signed_real_cost":25,"work_peak_multiple":"505920"}, + {"coefficient":"507904","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":5,"pr696_real_cost":25,"signed_real_cost":23,"work_peak_multiple":"507904"}, + {"coefficient":"510016","digits_after_leading_one":[0,0,0,0,-1,0,0,1,0,0,0,0,1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":27,"signed_real_cost":25,"work_peak_multiple":"510016"}, + {"coefficient":"516096","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":26,"signed_real_cost":23,"work_peak_multiple":"516096"}, + {"coefficient":"524092","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,1,0,0,0,-1,0,0],"occurrences":1,"pr696_real_cost":35,"signed_real_cost":25,"work_peak_multiple":"524092"}, + {"coefficient":"524220","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,-1,0,0],"occurrences":2,"pr696_real_cost":36,"signed_real_cost":24,"work_peak_multiple":"524220"}, + {"coefficient":"524286","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0],"occurrences":1,"pr696_real_cost":38,"signed_real_cost":23,"work_peak_multiple":"524286"}, + {"coefficient":"524288","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":10,"pr696_real_cost":22,"signed_real_cost":22,"work_peak_multiple":"524288"}, + {"coefficient":"524512","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,-1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":25,"signed_real_cost":24,"work_peak_multiple":"524512"}, + {"coefficient":"2098335/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0,0,0,-1,1],"occurrences":3,"pr696_real_cost":33,"signed_real_cost":31,"work_peak_multiple":"2098335"}, + {"coefficient":"524584","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0,0,0],"occurrences":3,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"524584"}, + {"coefficient":"524640","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,1,1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"524640"}, + {"coefficient":"525824","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":24,"signed_real_cost":24,"work_peak_multiple":"525824"}, + {"coefficient":"540608","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":24,"work_peak_multiple":"540608"}, + {"coefficient":"540656","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,-1,0,0,0,0],"occurrences":2,"pr696_real_cost":32,"signed_real_cost":24,"work_peak_multiple":"540656"}, + {"coefficient":"918208","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,1,0,1,1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"918208"}, + {"coefficient":"983728","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,0,1,1,0,0,0,0],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":28,"work_peak_multiple":"983728"}, + {"coefficient":"983760","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,1,0,1,0,0,0,0],"occurrences":5,"pr696_real_cost":29,"signed_real_cost":28,"work_peak_multiple":"983760"}, + {"coefficient":"1011840","digits_after_leading_one":[0,0,0,0,-1,0,0,-1,0,0,0,0,1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":26,"work_peak_multiple":"1011840"}, + {"coefficient":"1015808","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":26,"signed_real_cost":24,"work_peak_multiple":"1015808"}, + {"coefficient":"1016520","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,1,0,1,1,0,0,1,0,0,0],"occurrences":4,"pr696_real_cost":30,"signed_real_cost":28,"work_peak_multiple":"1016520"}, + {"coefficient":"1020032","digits_after_leading_one":[0,0,0,0,-1,0,0,1,0,0,0,0,1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":26,"work_peak_multiple":"1020032"}, + {"coefficient":"1032192","digits_after_leading_one":[0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":24,"work_peak_multiple":"1032192"}, + {"coefficient":"1044480","digits_after_leading_one":[0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":6,"pr696_real_cost":29,"signed_real_cost":24,"work_peak_multiple":"1044480"}, + {"coefficient":"1048440","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,-1,0,0,0],"occurrences":1,"pr696_real_cost":37,"signed_real_cost":25,"work_peak_multiple":"1048440"}, + {"coefficient":"1048576","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":11,"pr696_real_cost":23,"signed_real_cost":23,"work_peak_multiple":"1048576"}, + {"coefficient":"2097153/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":5,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"2097153"}, + {"coefficient":"4194307/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":29,"signed_real_cost":29,"work_peak_multiple":"4194307"}, + {"coefficient":"1049024","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,-1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":25,"work_peak_multiple":"1049024"}, + {"coefficient":"2098335/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":32,"signed_real_cost":30,"work_peak_multiple":"2098335"}, + {"coefficient":"1049168","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0,0,0,0],"occurrences":5,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"1049168"}, + {"coefficient":"1049280","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,1,1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"1049280"}, + {"coefficient":"1051648","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"1051648"}, + {"coefficient":"1081312","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,0],"occurrences":1,"pr696_real_cost":33,"signed_real_cost":25,"work_peak_multiple":"1081312"}, + {"coefficient":"1318904","digits_after_leading_one":[0,1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,-1,0,0,0],"occurrences":4,"pr696_real_cost":34,"signed_real_cost":26,"work_peak_multiple":"1318904"}, + {"coefficient":"1566208","digits_after_leading_one":[1,0,0,0,0,0,-1,0,0,1,1,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":31,"signed_real_cost":27,"work_peak_multiple":"1566208"}, + {"coefficient":"1967520","digits_after_leading_one":[0,0,0,-1,0,0,0,0,0,0,1,0,1,1,0,1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":30,"signed_real_cost":29,"work_peak_multiple":"1967520"}, + {"coefficient":"2033040","digits_after_leading_one":[0,0,0,0,-1,0,0,0,0,0,1,0,1,1,0,0,1,0,0,0,0],"occurrences":2,"pr696_real_cost":31,"signed_real_cost":29,"work_peak_multiple":"2033040"}, + {"coefficient":"2083808","digits_after_leading_one":[0,0,0,0,0,0,-1,0,0,1,1,0,0,0,0,-1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":35,"signed_real_cost":28,"work_peak_multiple":"2083808"}, + {"coefficient":"8347645/4","digits_after_leading_one":[0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":46,"signed_real_cost":32,"work_peak_multiple":"8347645"}, + {"coefficient":"2088960","digits_after_leading_one":[0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":30,"signed_real_cost":25,"work_peak_multiple":"2088960"}, + {"coefficient":"2092032","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":32,"signed_real_cost":26,"work_peak_multiple":"2092032"}, + {"coefficient":"2097092","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,1,0,0],"occurrences":1,"pr696_real_cost":38,"signed_real_cost":26,"work_peak_multiple":"2097092"}, + {"coefficient":"4194303/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":46,"signed_real_cost":28,"work_peak_multiple":"4194303"}, + {"coefficient":"8388607/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":49,"signed_real_cost":30,"work_peak_multiple":"8388607"}, + {"coefficient":"2097152","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":24,"signed_real_cost":24,"work_peak_multiple":"2097152"}, + {"coefficient":"4194305/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":2,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"4194305"}, + {"coefficient":"2097153","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":3,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"2097153"}, + {"coefficient":"8388613/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,1],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":30,"work_peak_multiple":"8388613"}, + {"coefficient":"4194307/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":28,"work_peak_multiple":"4194307"}, + {"coefficient":"2097220","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,1,0,0],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"2097220"}, + {"coefficient":"2098336","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"2098336"}, + {"coefficient":"4198401/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":28,"work_peak_multiple":"4198401"}, + {"coefficient":"8396807/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1,1],"occurrences":1,"pr696_real_cost":32,"signed_real_cost":32,"work_peak_multiple":"8396807"}, + {"coefficient":"2101248","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"2101248"}, + {"coefficient":"2102240","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,1,0,0,0,0,-1,0,0,0,0,0],"occurrences":2,"pr696_real_cost":30,"signed_real_cost":27,"work_peak_multiple":"2102240"}, + {"coefficient":"2637808","digits_after_leading_one":[0,1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,-1,0,0,0,0],"occurrences":2,"pr696_real_cost":35,"signed_real_cost":27,"work_peak_multiple":"2637808"}, + {"coefficient":"3132416","digits_after_leading_one":[1,0,0,0,0,0,-1,0,0,1,1,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":32,"signed_real_cost":28,"work_peak_multiple":"3132416"}, + {"coefficient":"3670016","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"3670016"}, + {"coefficient":"4167616","digits_after_leading_one":[0,0,0,0,0,0,-1,0,0,1,1,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":36,"signed_real_cost":29,"work_peak_multiple":"4167616"}, + {"coefficient":"4184064","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":33,"signed_real_cost":27,"work_peak_multiple":"4184064"}, + {"coefficient":"4186112","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":32,"signed_real_cost":26,"work_peak_multiple":"4186112"}, + {"coefficient":"4189183","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":43,"signed_real_cost":29,"work_peak_multiple":"4189183"}, + {"coefficient":"4192192","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":38,"signed_real_cost":27,"work_peak_multiple":"4192192"}, + {"coefficient":"4194303","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":45,"signed_real_cost":27,"work_peak_multiple":"4194303"}, + {"coefficient":"16777213/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":50,"signed_real_cost":31,"work_peak_multiple":"16777213"}, + {"coefficient":"16777215/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":51,"signed_real_cost":31,"work_peak_multiple":"16777215"}, + {"coefficient":"4194304","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":4,"pr696_real_cost":25,"signed_real_cost":25,"work_peak_multiple":"4194304"}, + {"coefficient":"8388609/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":28,"signed_real_cost":28,"work_peak_multiple":"8388609"}, + {"coefficient":"4194305","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"4194305"}, + {"coefficient":"4198401","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"4198401"}, + {"coefficient":"4202496","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"4202496"}, + {"coefficient":"4204480","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,1,0,0,0,0,-1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":31,"signed_real_cost":28,"work_peak_multiple":"4204480"}, + {"coefficient":"17301503/4","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":48,"signed_real_cost":32,"work_peak_multiple":"17301503"}, + {"coefficient":"6291388","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,-1,0,0],"occurrences":1,"pr696_real_cost":43,"signed_real_cost":28,"work_peak_multiple":"6291388"}, + {"coefficient":"7340032","digits_after_leading_one":[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":3,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"7340032"}, + {"coefficient":"8372224","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":33,"signed_real_cost":27,"work_peak_multiple":"8372224"}, + {"coefficient":"8378366","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,-1,0],"occurrences":1,"pr696_real_cost":44,"signed_real_cost":29,"work_peak_multiple":"8378366"}, + {"coefficient":"8384384","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,-1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":39,"signed_real_cost":28,"work_peak_multiple":"8384384"}, + {"coefficient":"8384514","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,1,0],"occurrences":2,"pr696_real_cost":36,"signed_real_cost":28,"work_peak_multiple":"8384514"}, + {"coefficient":"33554177/4","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":46,"signed_real_cost":32,"work_peak_multiple":"33554177"}, + {"coefficient":"16777215/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":3,"pr696_real_cost":50,"signed_real_cost":30,"work_peak_multiple":"16777215"}, + {"coefficient":"8388608","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":9,"pr696_real_cost":26,"signed_real_cost":26,"work_peak_multiple":"8388608"}, + {"coefficient":"16785409/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":30,"work_peak_multiple":"16785409"}, + {"coefficient":"8403008","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,-1,0,0,0,0,1,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":30,"signed_real_cost":29,"work_peak_multiple":"8403008"}, + {"coefficient":"33685499/4","digits_after_leading_one":[0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,1,1],"occurrences":1,"pr696_real_cost":46,"signed_real_cost":34,"work_peak_multiple":"33685499"}, + {"coefficient":"34078711/4","digits_after_leading_one":[0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,-1,1],"occurrences":1,"pr696_real_cost":48,"signed_real_cost":34,"work_peak_multiple":"34078711"}, + {"coefficient":"17301503/2","digits_after_leading_one":[0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":47,"signed_real_cost":31,"work_peak_multiple":"17301503"}, + {"coefficient":"20951039/2","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":48,"signed_real_cost":33,"work_peak_multiple":"20951039"}, + {"coefficient":"10485700","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,1,0,0],"occurrences":1,"pr696_real_cost":42,"signed_real_cost":29,"work_peak_multiple":"10485700"}, + {"coefficient":"12582776","digits_after_leading_one":[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,-1,0,0,0],"occurrences":1,"pr696_real_cost":44,"signed_real_cost":29,"work_peak_multiple":"12582776"}, + {"coefficient":"16748544","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":35,"signed_real_cost":29,"work_peak_multiple":"16748544"}, + {"coefficient":"16762880","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,-1,0,0,1,0,0,0,0,0,0,0,0,0,0,0],"occurrences":2,"pr696_real_cost":36,"signed_real_cost":29,"work_peak_multiple":"16762880"}, + {"coefficient":"33538055/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,1,1,1],"occurrences":2,"pr696_real_cost":41,"signed_real_cost":33,"work_peak_multiple":"33538055"}, + {"coefficient":"16777088","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,0,0,0,0],"occurrences":1,"pr696_real_cost":42,"signed_real_cost":28,"work_peak_multiple":"16777088"}, + {"coefficient":"16777215","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":49,"signed_real_cost":29,"work_peak_multiple":"16777215"}, + {"coefficient":"33554431/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":3,"pr696_real_cost":52,"signed_real_cost":31,"work_peak_multiple":"33554431"}, + {"coefficient":"16777216","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"occurrences":5,"pr696_real_cost":27,"signed_real_cost":27,"work_peak_multiple":"16777216"}, + {"coefficient":"33570817/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1],"occurrences":1,"pr696_real_cost":31,"signed_real_cost":31,"work_peak_multiple":"33570817"}, + {"coefficient":"33612031/2","digits_after_leading_one":[0,0,0,0,0,0,0,0,1,0,0,-1,0,0,0,0,1,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":40,"signed_real_cost":34,"work_peak_multiple":"33612031"}, + {"coefficient":"33685503/2","digits_after_leading_one":[0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":1,"pr696_real_cost":46,"signed_real_cost":32,"work_peak_multiple":"33685503"}, + {"coefficient":"17039357","digits_after_leading_one":[0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":44,"signed_real_cost":30,"work_peak_multiple":"17039357"}, + {"coefficient":"41902077/2","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,-1,0,-1,0,0,0,0,0,0,0,0,0,0,-1,0,1],"occurrences":1,"pr696_real_cost":49,"signed_real_cost":34,"work_peak_multiple":"41902077"}, + {"coefficient":"20971400","digits_after_leading_one":[0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0,0,0,1,0,0,0],"occurrences":1,"pr696_real_cost":43,"signed_real_cost":30,"work_peak_multiple":"20971400"}, + {"coefficient":"33497087","digits_after_leading_one":[0,0,0,0,0,0,0,0,-1,0,0,1,0,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":48,"signed_real_cost":32,"work_peak_multiple":"33497087"}, + {"coefficient":"33525759","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,-1,0,0,1,0,0,0,0,0,0,0,0,0,0,-1,1],"occurrences":2,"pr696_real_cost":48,"signed_real_cost":32,"work_peak_multiple":"33525759"}, + {"coefficient":"67108862","digits_after_leading_one":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,0],"occurrences":1,"pr696_real_cost":52,"signed_real_cost":30,"work_peak_multiple":"67108862"} + ], + "distinct_coefficients": 686, + "independent_digit_graph": { + "bounds": [ + 1, + 128 + ], + "status": "PASS", + "target_bound_pairs": 8256 + }, + "kappa_claim": null, + "negative_controls": { + "cost_inflation": "primitive budget exceeded", + "missing_clear": "macro endpoint / work clearing", + "missing_halving": "target prefix envelope", + "missing_source_copy": "work prefix envelope", + "non_dyadic": "addition requires distinct registers and a nonzero dyadic", + "source_growth_then_restore": "source was changed", + "source_target_alias": "addition requires distinct registers and a nonzero dyadic", + "unbounded_naf_overshoot": "work prefix envelope", + "unit_dirty_work": "macro endpoint / work clearing", + "work_alias": "addition requires distinct registers and a nonzero dyadic", + "wrong_signed_digit": "work prefix envelope", + "zero_addition": "addition requires distinct registers and a nonzero dyadic" + }, + "new_recursive_children": 0, + "programs": { + "ck/backward": { + "arbitrary_private_input_columns": 9, + "expanded_stream_sha256": "1c755cf410103d55fda5388fc8f99a1d99fd60b51fb1764f561977fa4103d84e", + "improved_macros_vs_pr696": 35, + "native_input_columns": 716, + "new_real_primitives": 169512, + "original_real_primitives": 224986, + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "pr696_real_primitives": 169634, + "real_primitive_counts": { + "add": 23972, + "clear": 42934, + "copy": 30452, + "double": 11240, + "halve": 38998, + "negate": 696, + "subtract": 21220 + }, + "retained_payload_bits": 192, + "retained_prefix_l1_bound": "146068000389976309073/32", + "saved_vs_original": 55474, + "saved_vs_pr696": 122, + "scalar_macros": 21936, + "source_reads_delta_vs_pr696_per_real_component": -96 + }, + "ck/forward": { + "arbitrary_private_input_columns": 9, + "expanded_stream_sha256": "1dcb9201612f1f6bed3139c2d6f5fab596f9f0b14fe262040f87a42efde3c0dc", + "improved_macros_vs_pr696": 35, + "native_input_columns": 716, + "new_real_primitives": 169496, + "original_real_primitives": 224938, + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "pr696_real_primitives": 169618, + "real_primitive_counts": { + "add": 23574, + "clear": 42918, + "copy": 30468, + "double": 11240, + "halve": 38998, + "negate": 696, + "subtract": 21602 + }, + "retained_payload_bits": 192, + "retained_prefix_l1_bound": "920709848294", + "saved_vs_original": 55442, + "saved_vs_pr696": 122, + "scalar_macros": 21936, + "source_reads_delta_vs_pr696_per_real_component": -96 + }, + "jp8/backward": { + "arbitrary_private_input_columns": 9, + "expanded_stream_sha256": "8f59ab6569ffd1af447befd7778575e6e2adb171070243284a68c92488434491", + "improved_macros_vs_pr696": 223, + "native_input_columns": 716, + "new_real_primitives": 197306, + "original_real_primitives": 257280, + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "pr696_real_primitives": 200396, + "real_primitive_counts": { + "add": 25188, + "clear": 44470, + "copy": 31992, + "double": 32930, + "halve": 39438, + "negate": 692, + "subtract": 22596 + }, + "retained_payload_bits": 192, + "retained_prefix_l1_bound": "16753412757380464429924108070201913461/8388608", + "saved_vs_original": 59974, + "saved_vs_pr696": 3090, + "scalar_macros": 22693, + "source_reads_delta_vs_pr696_per_real_component": -1722 + }, + "jp8/forward": { + "arbitrary_private_input_columns": 9, + "expanded_stream_sha256": "9ef431280382c6cdd428dc61b7448663ad1db430ddaad7d4574e895a0cde56af", + "improved_macros_vs_pr696": 223, + "native_input_columns": 716, + "new_real_primitives": 197290, + "original_real_primitives": 257232, + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "pr696_real_primitives": 200380, + "real_primitive_counts": { + "add": 25062, + "clear": 44454, + "copy": 32008, + "double": 32930, + "halve": 39438, + "negate": 692, + "subtract": 22706 + }, + "retained_payload_bits": 192, + "retained_prefix_l1_bound": "4536094588619580433782972610869617/281474976710656", + "saved_vs_original": 59942, + "saved_vs_pr696": 3090, + "scalar_macros": 22693, + "source_reads_delta_vs_pr696_per_real_component": -1722 + } + }, + "status": "PASS_PREFIX_BOUNDED_DYADIC" +} diff --git a/research/complex-prefix-bounded-dyadic/NOTICE.md b/research/complex-prefix-bounded-dyadic/NOTICE.md new file mode 100644 index 0000000000..465ff70d6d --- /dev/null +++ b/research/complex-prefix-bounded-dyadic/NOTICE.md @@ -0,0 +1,41 @@ +# Attribution and license + +New work: Chris Pagolu (@AllStars101-sudo), with substantial OpenAI Codex +assistance in mathematical analysis, code, verification and writing. +Apache-2.0, under the repository's [LICENSE](../../LICENSE). + +`vendor/pr696_lower.py` is retained **verbatim** from Sagar Thakrar's +[PR696](https://github.com/CrocSwap/integer-mult-bounds/pull/696), commit +`5a3f983715027c4fd83f50bc9001d4b18463bed1`, path +`research/complex-dyadic-lowering/lower.py`. Its original Apache-2.0 and +substantial OpenAI Codex assistance notice is retained. That work supplies the +copy/unit optimization; this package claims only the additional bounded +signed-digit saving. The comparison is with that exact pending implementation, +not a maintainer acceptance of PR696. + +The unchanged selected finite sources retain these predecessors' credit: + +- Jeremy Kothe / AtomScout's #622 K-triangle construction and #623 dispatch, + including the disclosed Claude Code construction work. +- Chafik Boukhalfa's #626 owner repair, source package and independent checks. +- icekylinx's #425/#433/#531 scalar primitive, common-frame and direct-delivery + lineage, including disclosed Codex assistance; the dyadic microcircuits in + eumemic's #411 are earlier related work. +- DreamingOfClouds' native/emitted audits and cold-helper construction, Dominik + Scholz's prefix work, Rohan Arun's #559 recurrence correction, and the other + contributors retained in the [selected review](../../docs/research/community-k492-review.md). +- eumemic's unchanged #543 bit supplier and its predecessors. +- Rohan Arun's campaign-100 signed-digit negative result, which remains valid + for its paid-climb scope. + +Concurrent #681 (Alluri), #687 (Charles Bethin) and #698 (Sagar Thakrar) helped +identify overlap boundaries. Their code and pending mathematical results are +not dependencies. Sagar Thakrar's concurrent #723 independently applies signed +digits to JP8 with a slightly larger prefix envelope; that discovery retains +credit. This package adds the strict prefix-bounded recurrence, unchanged exact +envelopes, CK coverage and an independent graph check. @ellipsi2's #722 instead +shares preparation across macro boundaries. Neither pending implementation is +imported or verified here, and no combined saving is claimed. + +This contribution has no delegated-agent or independent human review claim. +Existing source-specific notices and licenses are retained. diff --git a/research/complex-prefix-bounded-dyadic/OVERLAP.json b/research/complex-prefix-bounded-dyadic/OVERLAP.json new file mode 100644 index 0000000000..29d80309f9 --- /dev/null +++ b/research/complex-prefix-bounded-dyadic/OVERLAP.json @@ -0,0 +1,142 @@ +{ + "checked_utc": "2026-10-13T04:54:03Z", + "open_pr_count": 544, + "latest_pr": 725, + "pinned_coordination_issues": [], + "reviewed_related_metadata": [ + { + "headRefOid": "d3bc41b87fc7d23f50d064a0f06f1a89e3ab02a7", + "number": 723, + "title": "Research: save 3,276 JP8 scalar primitives per orientation with signed digits", + "updatedAt": "2026-10-13T04:52:24Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/723" + }, + { + "headRefOid": "a0766ab0fab379e1997fadc3ca157578d57986c1", + "number": 722, + "title": "Research: share JP8 cleanup coefficient work, saving 19,688 primitives (no new kappa)", + "updatedAt": "2026-10-13T04:50:10Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/722" + }, + { + "headRefOid": "ab78f797cffcbeddbb17a7eb069741085ffe3351", + "number": 698, + "title": "Scoped negative result: selected CK B frames are optimal at fixed boundaries", + "updatedAt": "2026-10-13T04:23:37Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/698" + }, + { + "headRefOid": "5a3f983715027c4fd83f50bc9001d4b18463bed1", + "number": 696, + "title": "Research: lower selected complex scalar primitives by 22\u201325% (no new kappa)", + "updatedAt": "2026-10-13T04:21:56Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/696" + }, + { + "headRefOid": "82bbb9c3ac34540f196410d137ebc59d9c2c43a9", + "number": 687, + "title": "Scoped negative result: certify one K-triangle relocation neighborhood", + "updatedAt": "2026-10-13T04:07:09Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/687" + }, + { + "headRefOid": "cbf30fdb56126d8cb7594f32e4d9a74ea7cd80a7", + "number": 683, + "title": "Scoped negative result: partial K/M face bypass requires four carriers", + "updatedAt": "2026-10-13T04:00:46Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/683" + }, + { + "headRefOid": "fdc2e4f3c6825530b02143b30deab5de10209479", + "number": 681, + "title": "Research: save 1,484 complex factory operations (no new kappa)", + "updatedAt": "2026-10-13T04:41:03Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/681" + }, + { + "headRefOid": "df5b9c41fcea749242af886646dfebb9d86319a7", + "number": 651, + "title": "Research: the complex delivery layer is rigid \u2014 target hosting and raw-face sharing closed exactly", + "updatedAt": "2026-10-13T01:41:20Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/651" + }, + { + "headRefOid": "e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87", + "number": 620, + "title": "Research notes (no \u03ba claim): E8 decoder floors are tight; #615 levers exhausted; +1.1e-7 \u03ba owner-map headroom on #617", + "updatedAt": "2026-10-13T02:36:29Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/620" + }, + { + "headRefOid": "f58d95f2c5da03445e704ea9c72cc55df9e68190", + "number": 411, + "title": "\u03ba = 1.017629458064773e-3: exact target-prefix resynthesis on sequential206", + "updatedAt": "2026-10-11T10:02:50Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/411" + } + ], + "distinction_from_concurrent_723": "Restricted signed-Horner optimum with a hard per-macro numerator bound; old exact prefix envelopes retained; CK as well as JP8; independent 8256-case forward digit graph. PR723 permits numerator+1 and its recoding saves 186 more JP8 primitives per orientation, excluding the separately credited PR696 copy/unit saving. Its implementation is not imported or independently verified.", + "distinction_from_concurrent_722": "Per-macro clearing retained, no cross-macro work sharing; no composed count claimed.", + "immediate_pre_submission_refresh": { + "checked_utc": "2026-10-13T04:57:56Z", + "open_pr_count": 551, + "latest_pr": 732, + "new_prs": [ + { + "headRefOid": "80431a74c31e807581f5c2258c87abe2084caacd", + "number": 732, + "title": "Research note: sharp off-target proper-star puncture threshold", + "updatedAt": "2026-10-13T04:57:07Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/732" + }, + { + "headRefOid": "0e10ed667c0cc435eb0f69c71a1d542599cad170", + "number": 731, + "title": "Independent verification: R420 compensation rank and minimum-weight kernel", + "updatedAt": "2026-10-13T04:57:06Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/731" + }, + { + "headRefOid": "d222e348179cc02a54d6d26dbd2838944f62c6e5", + "number": 730, + "title": "Research: optimize ordered dirty echoes at fixed scratch (no new kappa)", + "updatedAt": "2026-10-13T04:57:06Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/730" + }, + { + "headRefOid": "deaed262cebc50bdb0c27c6ba132b8f8289b3eef", + "number": 729, + "title": "Independent verification: audit helper-frame lifetimes with a scalar-preserving regression", + "updatedAt": "2026-10-13T04:56:24Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/729" + }, + { + "headRefOid": "d454ae19fdd474b4dfa7bd2c28bbe5b0996365fb", + "number": 728, + "title": "Research construction: save 20 R439 mini-node XORs (no new kappa)", + "updatedAt": "2026-10-13T04:55:42Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/728" + }, + { + "headRefOid": "71ba94c981477b3527ef21dd0f8140e795a7664d", + "number": 727, + "title": "Tooling: exact owner footprint masks reduce checker wall time by 13\u201319%", + "updatedAt": "2026-10-13T04:55:01Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/727" + }, + { + "headRefOid": "a3041f751114df12453afcb7ac7d0066973797fa", + "number": 726, + "title": "Exact E8 A2 Triple-Gather Census and Verification", + "updatedAt": "2026-10-13T04:54:30Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/726" + } + ], + "related_heads_unchanged": { + "723": "d3bc41b87fc7d23f50d064a0f06f1a89e3ab02a7", + "722": "a0766ab0fab379e1997fadc3ca157578d57986c1", + "696": "5a3f983715027c4fd83f50bc9001d4b18463bed1" + }, + "main_head": "66849e1475c930fd7732b1a0067ffee7e1e95f60" + } +} diff --git a/research/complex-prefix-bounded-dyadic/README.md b/research/complex-prefix-bounded-dyadic/README.md new file mode 100644 index 0000000000..a660c36093 --- /dev/null +++ b/research/complex-prefix-bounded-dyadic/README.md @@ -0,0 +1,185 @@ +# Prefix-bounded signed Horner circuits for the selected complex suppliers + +**Finite circuit improvement / research note; no new κ.** Signed binary +coefficient synthesis saves another **3,090 real primitives in each JP8 +orientation and 122 in each CK orientation**, beyond Sagar Thakrar's PR696 +copy/unit lowering. All coefficient-work intermediate multiples stay between +zero and the original numerator, so the inherited scalar prefix bound suffices. +The extra saving is the contribution of this package; the larger saving over +the selected emitter includes PR696's credited work. + +| Program | Selected emitter | Pinned PR696 | This circuit | Extra saving | +| --- | ---: | ---: | ---: | ---: | +| CK forward | 224,938 | 169,618 | 169,496 | 122 | +| CK backward | 224,986 | 169,634 | 169,512 | 122 | +| JP8 forward | 257,232 | 200,380 | 197,290 | 3,090 | +| JP8 backward | 257,280 | 200,396 | 197,306 | 3,090 | + +Counts cover both real components: source copies/reads, doubling, signed +addition, halving, accumulation, clearing, and unchanged scale/center macros. +There are **no added registers, recursive children, frame changes, wrappers, +copies outside the listed circuit, or restoration operations**. The private +coefficient register is erased after each addition. Source accesses decrease +by 96 per CK real component and 1,722 per JP8 real component. The helper count, +scalar macro boundaries, native frame paths and paid child histograms stay +fixed. The selected assembly remains complex-bound at the same conditional +κ = `51110230636731/31250000000000000`; neither supplier moment changes. + +## Reproduce + +From the repository, using Python 3.11+ and only the standard library: + +```sh +python3 -B research/complex-prefix-bounded-dyadic/verify.py +``` + +Expected: + +```text +PASS_PREFIX_BOUNDED_DYADIC programs=4 columns=716+9 coefficients=686 extra_savings=122,122,3090,3090 controls=12 +``` + +This is offline and makes no writes. `--json` prints the checked deterministic +certificate. The verifier binds the retained programs to the selected #626 +SPEC, freshly executes all their scalar primitives on **716 native formal +input columns plus nine arbitrary private columns**, and checks the intended +forward/inverse-transpose shear with every dirty helper restored and private +column erased. Non-scalar events are retained and counted; their geometry, +phases, wrappers and analytic meaning are inherited, not independently replayed +by this command. Source pins are checked before any replay. + +The [certificate](EXPECTED.json) contains every one of the **686** distinct +signed dyadic coefficients, its complete signed-digit word, multiplicity, cost +and work maximum. **282** coefficient types, occurring in **516** macros across +the four programs, improve over PR696. Exact three-input matrix checks cover +every coefficient with both lowerings. A separate forward Dijkstra search +agrees with the backward recurrence on all **8,256** `(target, bound)` pairs +with `1 <= target <= bound <= 128`. + +## Circuit and bounded search class + +Write a nonzero dyadic coefficient as `q = ±n / 2^d`, with `n > 0`. A signed +Horner word begins at integer 1, then appends digits in `{-1,0,+1}`. Each digit +first doubles the work register, then optionally adds or subtracts the unchanged +source. **Both** the doubled intermediate and the digit endpoint must lie in +`[1,B]`. The production circuit uses `B=n`. + +Let `C_B(n)` be the minimum number of doubling/addition/subtraction primitives +in this class, excluding the initial source copy. The recurrence is: + +```text +C_B(1) = 0 +C_B(2a) = C_B(a) + 1 +C_B(2a+1) = min(C_B(a) + 2, + C_B(a+1) + 2 if 2a+2 <= B), a >= 1. +``` + +Parity forces the last digit. Removing that digit produces exactly the displayed +predecessors; both are smaller than the target. Conversely, appending any +admitted last digit preserves the bound. Induction therefore proves the +recurrence optimal **within this signed-Horner class**. A nonempty cycle ending +at 1 has positive cost and cannot improve the base case. Binary Horner is an +admissible candidate, so this recurrence cannot cost more. Ties prefer fewer +subtractions and then lexicographic digit order; there is no random search. + +For nonunit `q`, the complete per-real-component cost is +`3 + C_n(n) + d`: one copy, the digit word, `d` halvings, one signed accumulation +and one clear. Unit coefficients retain PR696's two-primitive circuit. +The selected original add costs `3 + floor(log2 n) + popcount(n) + d`; +PR696 saves the leading clear/add replacement (and a further unit operation). +The present additional saving is exactly the decrease in digit-word length. +No accounting relies on dropping the initial copy or final clear. + +For example, numerator 31 has the seven-operation coefficient path +`1 → 2 → 4 → 8 → 16 → 15 → 30 → 31`, compared with eight binary operations. +The shorter unconstrained path through `32 → 31` is inadmissible. A negative +control has precisely this correct-endpoint overshoot and is rejected by the +prefix check, independently of its favorable cost. + +This exhausts the recurrence for all selected coefficients, whose absolute +numerators are at most **67,108,862**. It does not assert shortest unrestricted +addition chains, multi-register circuits, target borrowing, interleaved halving +or globally optimal suppliers. The finite graph comparison is a check of the +implementation, not a formal proof of the full multiplication theorem. + +## Prefix and substitution argument + +At a macro entrance let the target and source rows be `T` and `S`. After the +initial copy every work row is exactly `c S`, with `0 <= c <= n`, including +halvings. The source remains `S`; the target stays `T` until its single signed +accumulation, then becomes `T + q S`. Hence an existing bound `N_T, N_S` still +gives work bound `n N_S` and target bound `N_T + |q| N_S`. These are exactly +the quantities charged by the retained local auditor and finite invoice. +Arbitrary initial private values are independent formal columns and are erased; +their entry states were already present in the reference program. + +The proof uses coefficient bounds; the new intermediate rows need not literally +occur in the binary trace. The verifier checks the weighted row coefficients, +not just a clean-input evaluation or the endpoint. All primitives stay within +the macro's existing common frame. Each addition has the same three-register +boundary map `(T,S,W) -> (T+qS,S,0)`, so substitution preserves arbitrary +correlated inputs and composes across the fixed program. Both orientations +are nevertheless executed separately by an exact sparse rational interpreter. + +Twelve adverse controls cover missing copy/halving/clearing, wrong signed digits, +cost inflation, a correct-endpoint prefix overshoot, source growth followed by +restoration, uncleared unit work, nondyadic and zero coefficients, and aliasing. +See [validation](VALIDATION.md) for the checks actually run. + +## Provenance, overlap and limits + +Exact base: **`66849e1475c930fd7732b1a0067ffee7e1e95f60`**. The selected source +is #626 at `660de893d27bb7abd1d5b01b1640207528a5c851`, on #622 at +`f69477f4f6d3c7eb1f740b166881bffed4ffa9f6`, with the unchanged #543 bit source. +[SOURCES.json](SOURCES.json) pins all consumed repository artifacts and the +verbatim PR696 lowering at `5a3f983715027c4fd83f50bc9001d4b18463bed1`. +Compressed inputs are bound by their decompressed bytes, and program semantic +hashes are also checked against the selected SPEC. [NOTICE.md](NOTICE.md) +credits the construction and verification lineage. + +OS assignment seed **23** selected the complex-supplier track and the third +of three recorded candidate tasks. It prioritized JP8 backward for the initial +screen; final coverage includes both providers and both orientations. There +was no pinned coordination issue, so [CLAIM.json](CLAIM.json) records the scope, +overlap checks, stopping rule and handoff. The time budget was 40 minutes, +with at least the final quarter reserved for verification and handoff. + +Rohan Arun's archived [signed-digit negative result](../experiment-log/campaign-100/algebraic-word-construction.md#38-signed-digit-coefficients) +concerns rank-zero coefficient-3 rewrites and no paid-climb gain. This work +agrees with that conclusion and studies scalar primitive cost for the later +selected coefficients. PR696 is an explicit predecessor and comparison; +PR681 changes a factory map's implementation, PR687 changes read order, and +PR698 studies fixed-boundary frame assignments. None supplies this bounded +signed-Horner construction. Their open PR titles are not accepted-frontier +claims. + +**Concurrent overlap discovered during final verification:** Sagar Thakrar's +[PR723](https://github.com/CrocSwap/integer-mult-bounds/pull/723), at +`d3bc41b87fc7d23f50d064a0f06f1a89e3ab02a7`, independently uses signed digits for +JP8 and reports 3,276 saved primitives per orientation. It permits numerator +overshoot by one and increases the exact forward prefix envelope by +`34078712/34078711`. This contribution retains the old envelope **at every +macro**. Its recoding component saves 186 fewer primitives per JP8 orientation +(the PR696 copy/unit saving is accounted separately), also covers CK, +and gives a proved recurrence with an independent finite graph comparison for +the restricted class. Signed recoding itself is therefore concurrent work, +not an exclusive discovery here. Its PR description and file inventory were +inspected; its implementation and receipts are not independently verified by +this package. + +[PR722](https://github.com/CrocSwap/integer-mult-bounds/pull/722), by @ellipsi2 at +`a0766ab0fab379e1997fadc3ca157578d57986c1`, instead shares preparation across JP8 +cleanup macros and changes the private-clear boundary. This package retains +per-macro clearing. No composition with #722 or #723 is claimed. The final +overlap snapshot is recorded in [OVERLAP.json](OVERLAP.json). + +This package does **not** replace the selected emitter or issue a new global +invoice/admission certificate. The uniform compiler, common-label/mutable-basis +realization, hosting, precision/tape/recovery, analytic transfer and bit-supplier +assumptions remain inherited. No practical runtime speedup, unconditional +multiplication result, Lean proof or remote CI result is claimed. All existing +repository files, `upstream/`, and the selected frontier remain unchanged. + +Prepared by **Chris Pagolu (@AllStars101-sudo)** with substantial **OpenAI Codex +assistance** in research, implementation, verification and writing, under the +repository's Apache-2.0 license. diff --git a/research/complex-prefix-bounded-dyadic/SOURCES.json b/research/complex-prefix-bounded-dyadic/SOURCES.json new file mode 100644 index 0000000000..33dd4b449d --- /dev/null +++ b/research/complex-prefix-bounded-dyadic/SOURCES.json @@ -0,0 +1,67 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "reviewed_source_heads": { + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "543": "2065fe4f72a914d907f1046603f5a36f17018535" + }, + "files": { + "certificates/selected-result.json": { + "representation": "bytes", + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + }, + "research/complex-k492-owner-repair/data/SPEC.json": { + "representation": "bytes", + "sha256": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323" + }, + "research/complex-k492-owner-repair/code/hpe_emit_local.py": { + "representation": "bytes", + "sha256": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805" + }, + "research/complex-k492-owner-repair/code/hpe_audit_local.py": { + "representation": "bytes", + "sha256": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810" + }, + "research/complex-k492-owner-repair/code/invoice_allcold.py": { + "representation": "bytes", + "sha256": "141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec" + }, + "research/community-k492-audit/pr626/replay/ASSEMBLY.json": { + "representation": "bytes", + "sha256": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz": { + "representation": "decompressed", + "sha256": "854f17274092263dc25e60367f4cd0d29f60a8446becd17cc1883ebed7a97900" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-CHECKS.json": { + "representation": "bytes", + "sha256": "059c4e59142bdf5c19dc7c0afebcddfec28e6e60cbc7299b8bdcc624afbc0cbe" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/INDEPENDENT-LOCAL-REPLAY.json": { + "representation": "bytes", + "sha256": "ecefb9e661301d8081522be68bbe6640e175c011eb1177f643383d193c6fb2f0" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-PROGRAMS.json.gz": { + "representation": "decompressed", + "sha256": "efe45ce7fb025a6f53cc9eb54e951ac2211a5ed927e689a049e4f68ca680654b" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-CHECKS.json": { + "representation": "bytes", + "sha256": "0fad744aa863eedb288a9f87b1c23225a36b316b6275cc3b1bcedd42afe28a67" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/INDEPENDENT-LOCAL-REPLAY.json": { + "representation": "bytes", + "sha256": "cb2f99ed351925dd35434b73de16f4085884fe81a35a69e1c7ce2d5e96cb975b" + } + }, + "vendored_reference": { + "path": "vendor/pr696_lower.py", + "sha256": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753", + "source_pr": 696, + "source_head": "5a3f983715027c4fd83f50bc9001d4b18463bed1", + "source_path": "research/complex-dyadic-lowering/lower.py", + "author": "Sagar Thakrar, with substantial OpenAI Codex assistance", + "license": "Apache-2.0" + } +} diff --git a/research/complex-prefix-bounded-dyadic/VALIDATION.md b/research/complex-prefix-bounded-dyadic/VALIDATION.md new file mode 100644 index 0000000000..9a25ad2c0d --- /dev/null +++ b/research/complex-prefix-bounded-dyadic/VALIDATION.md @@ -0,0 +1,56 @@ +# Validation receipt + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Local Linux x86_64, 2026-10-13 UTC. No remote CI or human review is claimed. +New code, deterministic evidence, pins, proof and controls are confined to this +package; no existing generator, supplier, certificate or `upstream/` file changes. + +The bounded experiment completed at 04:48 UTC. Dedicated verification and +handoff began at 04:52 UTC, ahead of the originally reserved 05:08 start within +the 40-minute session budget. The claim records assignment seed 23, the initial +screen and the complete stopping rule. Final concurrency review found #722 and +#723; their distinct scopes and #723's concurrent signed-digit result are +explicitly credited. This was an overlap clarification, not an additional +uncompleted investigation. + +## Executed checks + +| Check | Result | +| --- | --- | +| `python3 -B research/complex-prefix-bounded-dyadic/verify.py`, CPython 3.15.0 | PASS; 4 full primitive replays, 716 native + 9 private formal columns each | +| `/usr/bin/python3.14 -I -O -B research/complex-prefix-bounded-dyadic/verify.py`, CPython 3.14.7 | Same deterministic certificate; PASS | +| CPython 3.12.14, `-I -O -B` with the same verifier | Same deterministic certificate; PASS | +| `ast.parse(..., feature_version=(3,11))` for every package Python file | PASS syntax; Python 3.11 runtime was not run | +| Exact dense three-input replay of all 686 coefficient types | Both pinned PR696 and replacement endpoints/prefix bounds pass | +| Separate forward digit-graph Dijkstra | All 8,256 target/bound pairs for bounds 1 through 128 agree with the backward recurrence | +| Twelve mathematical/alias controls | Every control rejected; overshoot and cost controls check their precise rejection reasons | +| `python3 -B research/complex-prefix-bounded-dyadic/test_package.py` | PASS relocation, gzip-container variation, read-only behavior and four corruption/algorithm controls | +| `make selected-record-check` | PASS selected record, exact κ, original source inventory and proof supplement | +| Package JSON parsing and staged whitespace check | PASS | + +The relocated check copies only this package and its 12 pinned repository +inputs, into a temporary path containing spaces. It changes gzip compression +and header time without changing the decompressed payload; reproduction still +passes. Mutations to a pinned source, the vendored PR696 file, the savings +receipt and the doubled-intermediate guard all fail. File snapshots before +and after each verifier invocation agree. No mutation touches the real checkout. + +The complete coefficient census records all 686 types and multiplicities; no +sample or timeout is represented as complete coverage. The independent graph +check covers small finite bounds; the written recurrence proof supplies the +restricted-class argument for the larger selected numerators. Full scalar +replay is finite exact rational evidence, not a formal proof of an asymptotic +integer-multiplication theorem. + +## Checks intentionally outside this unchanged-supplier scope + +No full `make verify`, selected cold rebuild, global invoice/admission replay, +phase/Clifford regeneration, Linux remote CI or Lean build was run. The selected +word, geometry, interfaces and artifacts were not edited. This package checks +an explicit scalar substitution against retained selected outputs, binding +them to the selected SPEC; it does not regenerate their construction. Production +integration of a changed emitter would require the appropriate cold and global +replays and refreshed literal primitive receipts. + +All uniform compiler, common-label/mutable-basis, hosting, precision/tape, +recovery, analytic-transfer and bit-supplier obligations remain inherited. diff --git a/research/complex-prefix-bounded-dyadic/lower.py b/research/complex-prefix-bounded-dyadic/lower.py new file mode 100644 index 0000000000..9acf5916ba --- /dev/null +++ b/research/complex-prefix-bounded-dyadic/lower.py @@ -0,0 +1,58 @@ +"""Prefix-bounded signed Horner circuits. Apache-2.0. + +Chris Pagolu, with substantial OpenAI Codex assistance. +The copied/unit baseline is Sagar Thakrar's pinned PR696 implementation. +The primitive interface follows icekylinx's PR425/433/531 lineage. +""" +from fractions import Fraction +from functools import lru_cache + +from vendor.pr696_lower import lower as binary_lower + + +@lru_cache(maxsize=None) +def bounded_digits(n, bound): + """Shortest signed-binary Horner word for n, with coefficient <= bound. + + A word begins at 1; each digit doubles then optionally adds/subtracts 1. + The doubled intermediate, not just the completed digit, must fit bound. + This is a restricted word class, not general addition-chain optimality. + Returns the digits after the leading 1. Digit costs are 1 + abs(digit). + """ + if not isinstance(n, int) or not isinstance(bound, int) or not 1 <= n <= bound: + raise ValueError("expected integers 1 <= n <= bound") + if n == 1: + return () + if n % 2 == 0: + return bounded_digits(n // 2, bound) + (0,) + choices = [bounded_digits((n - 1) // 2, bound) + (1,)] + if n + 1 <= bound: + choices.append(bounded_digits((n + 1) // 2, bound) + (-1,)) + # Prefer fewer subtractions on equal cost, then deterministic lexicography. + return min(choices, key=lambda ds: (sum(1 + abs(d) for d in ds), ds.count(-1), ds)) + + +def lower(op, work=("W", 0)): + """Lower one macro; additions accept dirty work and leave it zero. + + Source access, coefficient synthesis, halving, accumulation and clearing + are all explicit. Every primitive runs at the input macro's own frame. + """ + reference = binary_lower(op, work) # Also validates the inherited domain. + if op[0] != "add": + return reference + q = Fraction(op[3], op[4]) + if abs(q) == 1: + return reference + target, source = tuple(op[1]), tuple(op[2]) + n = abs(q.numerator) + result = [("copy", work, source)] + for digit in bounded_digits(n, n): + result.append(("double", work)) + if digit: + result.append(("add" if digit > 0 else "subtract", work, source)) + result += [("halve", work)] * (q.denominator.bit_length() - 1) + result += [("add" if q > 0 else "subtract", target, work), ("clear", work)] + if len(result) > len(reference): + raise ValueError("bounded word is worse than its binary candidate") + return result diff --git a/research/complex-prefix-bounded-dyadic/test_package.py b/research/complex-prefix-bounded-dyadic/test_package.py new file mode 100644 index 0000000000..fe645689b3 --- /dev/null +++ b/research/complex-prefix-bounded-dyadic/test_package.py @@ -0,0 +1,95 @@ +"""Relocated replay and failure controls for this standalone research package. + +Chris Pagolu, with substantial OpenAI Codex assistance. Apache-2.0. +Only a temporary minimal checkout is changed. Run with Python 3.11+. +""" +import gzip +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +RELATIVE = HERE.relative_to(ROOT) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def main(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + with tempfile.TemporaryDirectory(prefix="bounded dyadic relocation ") as tmp: + root = Path(tmp) + package = root / RELATIVE + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + for filename in pins["files"]: + target = root / filename + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / filename, target) + + def run(expected=None): + def snapshot(): + return {p.relative_to(root): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob("*") if p.is_file()} + + before = snapshot() + result = subprocess.run( + [sys.executable, "-I", "-O", "-B", str(package / "verify.py")], + cwd=root, capture_output=True, text=True, timeout=120, + ) + need(snapshot() == before, "verification changed the minimal checkout") + if expected is None: + need(result.returncode == 0 and "PASS_PREFIX_BOUNDED_DYADIC" in result.stdout, + "minimal replay failed: " + result.stderr) + else: + need(result.returncode != 0 and expected in result.stderr, + "mutation not rejected as expected: " + str(result)) + + # A gzip wrapper rewrite must not invalidate the mathematical input. + zipped = next(root / f for f in pins["files"] if f.endswith(".gz")) + data = gzip.decompress(zipped.read_bytes()) + zipped.write_bytes(gzip.compress(data, compresslevel=1, mtime=23)) + run() + rejected = [] + + def mutate(path, replacement, reason, name): + original = path.read_bytes() + try: + path.write_bytes(replacement) + run(reason) + rejected.append(name) + finally: + path.write_bytes(original) + + source = root / "research/complex-k492-owner-repair/data/SPEC.json" + mutate(source, source.read_bytes() + b"\n", "source pin mismatch", "altered_pinned_source") + + reference = package / "vendor/pr696_lower.py" + mutate(reference, reference.read_bytes() + b"\n# changed\n", + "vendored PR696 source mismatch", "altered_reference_source") + + certificate = package / "EXPECTED.json" + report = json.loads(certificate.read_text()) + report["programs"]["jp8/backward"]["saved_vs_pr696"] += 2 + mutate(certificate, json.dumps(report).encode(), "expected certificate mismatch", "inflated_savings") + + compiler = package / "lower.py" + text = compiler.read_text() + old = "if n + 1 <= bound:" + need(text.count(old) == 1, "guard mutation site") + mutate(compiler, text.replace(old, "if True:").encode(), + "DP / graph cost disagreement", "removed_intermediate_bound_guard") + + # Default verification is read-only, even with -I -O and a spaced path. + need(not list(root.rglob("__pycache__")), "unexpected bytecode output") + print("PASS_PACKAGE_RELOCATION_AND_CONTROLS " + ",".join(rejected)) + + +if __name__ == "__main__": + main() diff --git a/research/complex-prefix-bounded-dyadic/vendor/pr696_lower.py b/research/complex-prefix-bounded-dyadic/vendor/pr696_lower.py new file mode 100644 index 0000000000..a2c2889e5b --- /dev/null +++ b/research/complex-prefix-bounded-dyadic/vendor/pr696_lower.py @@ -0,0 +1,56 @@ +"""Smaller exact dyadic circuits for the fixed PR626 complex scalar words. + +Sagar Thakrar, with substantial OpenAI Codex assistance. Apache-2.0. +Primitive vocabulary and the original Horner circuit follow icekylinx's +PR425/433/531 lineage, retained by Jeremy Kothe's PR622 supplier. +""" +from fractions import Fraction + + +def power_of_two(n): + return n > 0 and n & (n - 1) == 0 + + +def lower(op, work=("W", 0)): + """Return real-component primitives; work may be dirty on entry. + + Every addition leaves work zero. All operations use the macro's frame. + The complex circuit applies this word separately to real and imaginary parts. + """ + tag, target = op[0], tuple(op[1]) + if target == work: + raise ValueError("coefficient work aliases a scalar register") + if tag == "clear": + return [("clear", target)] + if tag == "copy": + source = tuple(op[2]) + if source == work: + raise ValueError("coefficient work used as a scalar source") + return [("copy", target, source)] + if tag == "scale": + q = Fraction(op[2], op[3]) + if not power_of_two(abs(q.numerator)) or not power_of_two(q.denominator): + raise ValueError("scale is not a signed power of two") + shift = abs(q.numerator).bit_length() - q.denominator.bit_length() + result = [("double" if shift > 0 else "halve", target)] * abs(shift) + if q < 0: + result.append(("negate", target)) + return result + if tag != "add": + raise ValueError("unknown scalar macro") + source = tuple(op[2]) + q = Fraction(op[3], op[4]) + if source in (target, work) or not q or not power_of_two(q.denominator): + raise ValueError("addition requires distinct registers and a nonzero dyadic") + accumulate = "add" if q > 0 else "subtract" + if abs(q) == 1: + return [(accumulate, target, source), ("clear", work)] + # Copy replaces clear + addition of the leading binary digit. + result = [("copy", work, source)] + for bit in bin(abs(q.numerator))[3:]: + result.append(("double", work)) + if bit == "1": + result.append(("add", work, source)) + result.extend([("halve", work)] * (q.denominator.bit_length() - 1)) + result.extend([(accumulate, target, work), ("clear", work)]) + return result diff --git a/research/complex-prefix-bounded-dyadic/verify.py b/research/complex-prefix-bounded-dyadic/verify.py new file mode 100644 index 0000000000..47177b1b8f --- /dev/null +++ b/research/complex-prefix-bounded-dyadic/verify.py @@ -0,0 +1,354 @@ +"""Exact finite replay of prefix-bounded dyadic circuits; Python 3.11+. + +Chris Pagolu, with substantial OpenAI Codex assistance. Apache-2.0. +This checks scalar substitution, not the full multiplication theorem. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import heapq +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from lower import binary_lower, bounded_digits, lower + +WORK = ("W", 0) +T, S = ("T", 0), ("S", 0) +PROVIDERS = "research/community-k492-audit/pr626/replay/mixed-global/base/providers" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def read(path): + data = path.read_bytes() + return json.loads(gzip.decompress(data) if path.suffix == ".gz" else data) + + +def check_pins(): + pins = read(HERE / "SOURCES.json") + for name, pin in pins["files"].items(): + data = (ROOT / name).read_bytes() + if pin["representation"] == "decompressed": + data = gzip.decompress(data) + else: + need(pin["representation"] == "bytes", "unknown pin representation") + need(sha(data) == pin["sha256"], "source pin mismatch: " + name) + reference = pins["vendored_reference"] + need(sha((HERE / reference["path"]).read_bytes()) == reference["sha256"], + "vendored PR696 source mismatch") + selected = read(ROOT / "certificates/selected-result.json") + assembly = read(ROOT / selected["certificate"]) + need(sha((ROOT / selected["certificate"]).read_bytes()) == selected["certificate_sha256"], + "selected certificate hash") + spec = read(ROOT / "research/complex-k492-owner-repair/data/SPEC.json") + need(selected["kappa"] == assembly["kappa"] == spec["expected"]["kappa"], + "selected kappa binding") + return spec + + +def baseline_cost(op): + """Literal original emitter formula, counted per real component.""" + if op[0] in ("clear", "copy"): + return 1 + q = Q(*op[3:5]) if op[0] == "add" else Q(*op[2:4]) + n, d = abs(q.numerator), q.denominator + if op[0] == "scale": + return abs(n.bit_length() - d.bit_length()) + int(q < 0) + return 3 + (n.bit_length() - 1) + n.bit_count() + (d.bit_length() - 1) + + +def dense_step(matrix, primitive): + """Three formal inputs; deliberately separate from the sparse full replay.""" + tag, target = primitive[:2] + i = {T: 0, S: 1, WORK: 2}[target] + if tag == "clear": + matrix[i] = [Q(0)] * 3 + elif tag == "copy": + matrix[i] = matrix[{T: 0, S: 1, WORK: 2}[primitive[2]]].copy() + elif tag in ("double", "halve", "negate"): + factor = {"double": Q(2), "halve": Q(1, 2), "negate": Q(-1)}[tag] + matrix[i] = [factor * x for x in matrix[i]] + elif tag in ("add", "subtract"): + j = {T: 0, S: 1, WORK: 2}[primitive[2]] + factor = 1 if tag == "add" else -1 + matrix[i] = [a + factor * b for a, b in zip(matrix[i], matrix[j])] + else: + raise ValueError("unknown primitive") + + +def check_add(q, word, budget): + """Weighted prefix domination for arbitrary target, source and dirty work.""" + matrix = [[Q(i == j) for j in range(3)] for i in range(3)] + n = abs(q.numerator) + peak = Q(0) + overwritten = False + for primitive in word: + dense_step(matrix, primitive) + target, source, work = matrix + need(source == [0, 1, 0], "source was changed") + need(target[0] == 1 and abs(target[1]) <= abs(q) and target[2] == 0, + "target prefix envelope") + if work == [0, 0, 1] and not overwritten: + # The reference also has this arbitrary entry state. Unit circuits + # erase it after accumulating; it never enters a public register. + continue + overwritten = True + need(work[0] == work[2] == 0 and 0 <= work[1] <= n, + "work prefix envelope") + peak = max(peak, work[1]) + need(matrix == [[1, q, 0], [0, 1, 0], [0, 0, 0]], "macro endpoint / work clearing") + need(len(word) <= budget, "primitive budget exceeded") + return peak + + +def graph_crosscheck(limit=128): + """Dijkstra over forward digit transitions, independent of backward DP. + + Each edge c -> 2c+d costs 1+|d|, with the intermediate 2c <= B. + For every bound 1..limit, compare every reachable positive target <= B. + """ + checked = 0 + for bound in range(1, limit + 1): + distance = {1: 0} + queue = [(0, 1)] + while queue: + cost, c = heapq.heappop(queue) + if cost != distance[c] or 2 * c > bound: + continue + for digit in (-1, 0, 1): + target = 2 * c + digit + if not 1 <= target <= bound: + continue + value = cost + 1 + abs(digit) + if value < distance.get(target, value + 1): + distance[target] = value + heapq.heappush(queue, (value, target)) + need(len(distance) == bound, "digit graph coverage") + for n, cost in distance.items(): + digits = bounded_digits(n, bound) + need(sum(1 + abs(d) for d in digits) == cost, "DP / graph cost disagreement") + c = 1 + for d in digits: + need(1 <= 2 * c <= bound, "digit intermediate exceeds bound") + c = 2 * c + d + need(1 <= c <= bound, "digit endpoint exceeds bound") + need(c == n, "digit value disagreement") + checked += 1 + return {"bounds": [1, limit], "target_bound_pairs": checked, "status": "PASS"} + + +def sparse_step(rows, primitive): + tag, target = primitive[:2] + if tag == "clear": + rows[target] = {} + elif tag == "copy": + rows[target] = rows[primitive[2]].copy() + elif tag in ("double", "halve", "negate"): + factor = {"double": Q(2), "halve": Q(1, 2), "negate": Q(-1)}[tag] + rows[target] = {j: x * factor for j, x in rows[target].items()} + elif tag in ("add", "subtract"): + factor = 1 if tag == "add" else -1 + dest = rows[target] + for j, x in list(rows[primitive[2]].items()): + value = dest.get(j, Q(0)) + factor * x + if value: + dest[j] = value + else: + dest.pop(j, None) + else: + raise ValueError("unknown primitive") + + +def replay(events, checks, receipt, orientation, coefficients): + n, v = 716, 112 + rows = {("L", r): {r: Q(1)} for r in range(n)} + # Private columns are arbitrary on entry, then explicitly erased. + rows[WORK] = {n: Q(1)} + rows.update({("C", k): {n + 1 + k: Q(1)} for k in range(8)}) + envelope = {("L", r): Q(1) for r in range(n)} + peak = Q(1) + paid, tags, used = Counter(), Counter(), Counter() + before = reference = macros = changed = 0 + stream_hash = hashlib.sha256() + extra_source_reads = 0 + for event in events: + if event[0] != "scalar": + need(event[0] in ("climb", "center", "phase", "adapter", "residual_adapter"), + "unknown non-scalar event") + if event[0] == "climb": + paid[event[5]] += 1 + if event[0] == "center": + paid[event[4]] += 1 + # Preserve each recursive call, frame transition and adapter. + stream_hash.update(canonical(event) + b"\n") + continue + op, frame = event[1:] + target, tag = tuple(op[1]), op[0] + word = lower(op) + comparison = binary_lower(op) + need(len(word) <= len(comparison), "local cost regression") + before += 2 * baseline_cost(op) + reference += 2 * len(comparison) + macros += 1 + changed += len(word) < len(comparison) + if tag == "add": + q, source = Q(*op[3:5]), tuple(op[2]) + used[q] += 1 + peak = max(peak, abs(q.numerator) * envelope[source]) + envelope[target] = envelope.get(target, Q(0)) + abs(q) * envelope[source] + # Count ALL source accesses, including coefficient synthesis. + new_reads = sum(len(p) == 3 and p[2] == source for p in word) + old_reads = sum(len(p) == 3 and p[2] == source for p in comparison) + extra_source_reads += new_reads - old_reads + elif tag == "clear": + envelope[target] = Q(0) + elif tag == "copy": + envelope[target] = envelope[tuple(op[2])] + elif tag == "scale": + envelope[target] *= abs(Q(*op[2:4])) + peak = max(peak, envelope[target]) + for primitive in word: + sparse_step(rows, primitive) + tags[primitive[0]] += 2 + stream_hash.update(canonical(["primitive", primitive, frame]) + b"\n") + if tag == "add": + need(not rows[WORK], "work survives macro") + for r in range(n): + want = {r: Q(1)} + if orientation == "forward" and v <= r < 2 * v: + want[r - v] = Q(1) + if orientation == "backward" and r < v: + want[r + v] = Q(-1) + need(rows[("L", r)] == want, "complete scalar endpoint at register " + str(r)) + need(all(not row for reg, row in rows.items() if reg[0] != "L"), "private columns survive") + need(before == checks["real_component_primitive_bound"], "original primitive receipt") + need(macros == checks["scalar_macros"], "scalar count receipt") + need(dict(paid) == {int(k): v for k, v in checks["paid_profile"].items()}, "paid profile receipt") + need(peak == Q(receipt["prefix_l1_upper"]), "retained prefix bound") + need(peak < 2 ** receipt["charged_payload_bits"], "payload bound") + need(extra_source_reads <= 0, "additional source accesses") + coefficients.update(used) + after = sum(tags.values()) + return { + "native_input_columns": n, "arbitrary_private_input_columns": 9, + "scalar_macros": macros, "improved_macros_vs_pr696": changed, + "original_real_primitives": before, "pr696_real_primitives": reference, + "new_real_primitives": after, "saved_vs_original": before - after, + "saved_vs_pr696": reference - after, + "source_reads_delta_vs_pr696_per_real_component": extra_source_reads, + "real_primitive_counts": dict(sorted(tags.items())), + "expanded_stream_sha256": stream_hash.hexdigest(), + "paid_profile": {str(k): v for k, v in sorted(paid.items())}, + "retained_prefix_l1_bound": str(peak), + "retained_payload_bits": receipt["charged_payload_bits"], + } + + +def negative_controls(): + op = ["add", list(T), list(S), 31, 2] + good = lower(op) + tests = { + "missing_clear": (Q(31, 2), good[:-1], len(good)), + "missing_source_copy": (Q(31, 2), good[1:], len(good)), + "wrong_signed_digit": (Q(31, 2), [("add", *p[1:]) if p[0] == "subtract" else p for p in good], len(good)), + "missing_halving": (Q(31, 2), [p for p in good if p[0] != "halve"], len(good)), + "cost_inflation": (Q(31, 2), good + [("clear", WORK)], len(good)), + # Endpoint-correct and cheaper: 32-1 violates the required bound 31. + "unbounded_naf_overshoot": (Q(31, 2), [("copy", WORK, S)] + [("double", WORK)] * 5 + + [("subtract", WORK, S), ("halve", WORK), ("add", T, WORK), ("clear", WORK)], 100), + "source_growth_then_restore": (Q(31, 2), [("double", S), ("halve", S)] + good, 100), + "unit_dirty_work": (Q(1), [("add", T, S)], 2), + } + rejected = {} + for name, (q, word, budget) in tests.items(): + try: + check_add(q, word, budget) + except ValueError as error: + rejected[name] = str(error) + else: + raise ValueError("accepted negative control: " + name) + need(rejected["unbounded_naf_overshoot"] == "work prefix envelope", "overshoot control reason") + need(rejected["cost_inflation"] == "primitive budget exceeded", "cost control reason") + for name, invalid in { + "non_dyadic": ["add", list(T), list(S), 1, 3], + "source_target_alias": ["add", list(T), list(T), 1, 1], + "work_alias": ["add", list(T), list(WORK), 1, 1], + "zero_addition": ["add", list(T), list(S), 0, 1], + }.items(): + try: + lower(invalid) + except ValueError as error: + rejected[name] = str(error) + else: + raise ValueError("accepted invalid macro: " + name) + return rejected + + +def collect(): + spec = check_pins() + coefficients = Counter() + programs = {} + graph = graph_crosscheck() + controls = negative_controls() + # The seed-selected JP8 backward screen was followed by complete coverage. + for provider in ("ck", "jp8"): + folder = ROOT / PROVIDERS / provider + events, checks, inherited = [read(folder / name) for name in + ("LOCAL-PROGRAMS.json.gz", "LOCAL-CHECKS.json", "INDEPENDENT-LOCAL-REPLAY.json")] + need(set(events) == {"forward", "backward"}, "program orientation coverage") + need(sha(canonical(events)) == spec["providers"][provider]["artifact_semantic_sha256"]["LOCAL-PROGRAMS.json.gz"], + "selected SPEC program binding") + for orientation in ("forward", "backward"): + need(sha(canonical(events[orientation])) == checks[orientation]["sha256"] == + spec["providers"][provider]["program_hashes"][orientation], "orientation binding") + programs[provider + "/" + orientation] = replay(events[orientation], checks[orientation], + inherited["local"][orientation], orientation, coefficients) + census = [] + for q, occurrences in sorted(coefficients.items()): + op = ["add", list(T), list(S), q.numerator, q.denominator] + candidate, comparison = lower(op), binary_lower(op) + peak = check_add(q, candidate, len(candidate)) + check_add(q, comparison, len(comparison)) + n = abs(q.numerator) + digits = bounded_digits(n, n) + need(len(candidate) <= len(comparison) <= baseline_cost(op), "coefficient cost ordering") + census.append({"coefficient": str(q), "occurrences": occurrences, + "digits_after_leading_one": list(digits), + "signed_real_cost": len(candidate), "pr696_real_cost": len(comparison), + "work_peak_multiple": str(peak)}) + return {"status": "PASS_PREFIX_BOUNDED_DYADIC", "programs": programs, + "distinct_coefficients": len(census), "coefficient_census": census, + "independent_digit_graph": graph, "negative_controls": controls, + "new_recursive_children": 0, "additional_private_registers": 0, + "kappa_claim": None} + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--json", action="store_true", help="print the checked deterministic certificate") + args = parser.parse_args() + result = collect() + need(result == read(HERE / "EXPECTED.json"), "expected certificate mismatch") + if args.json: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + savings = ",".join(str(p["saved_vs_pr696"]) for p in result["programs"].values()) + print(f"PASS_PREFIX_BOUNDED_DYADIC programs=4 columns=716+9 coefficients={result['distinct_coefficients']} " + f"extra_savings={savings} controls={len(result['negative_controls'])}")