diff --git a/research/qq16-f17-demand-projection/PREDECESSORS.json b/research/qq16-f17-demand-projection/PREDECESSORS.json new file mode 100644 index 0000000000..0262824736 --- /dev/null +++ b/research/qq16-f17-demand-projection/PREDECESSORS.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "canonical_source_base": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "predecessors": [ + { + "pr": 2512, + "author": "ywz65", + "head": "851dd3486a2d0549b51e85978a65ccb4eec619c0", + "role": "Actual96-output F17 demand and native-current-frame lineage. Original requires eight earlier T records." + }, + { + "pr": 2707, + "author": "ywz65", + "head": "efa51a6c7ffec6edd556a98deedfe9deeba65809", + "role": "Source physical word and loader. replay.py explicitly adapts its replay: W-only ownership, Y-only borrowed inputs, ordinary output demand, selected temporary zeroing, only current B1 maps; removed unused future/F0/checkpoint branches." + }, + { + "pr": 2681, + "author": "Arham-Tahir64 / Arham Tahir", + "head": "ea96706295631be10d92ae149b63c3e24acaeabc", + "role": "Retained routed algebra, phase functions, packet/archive source reconstruction and complete logical inverse, authenticated through PR2707. These are reused, not independently rederived here." + }, + { + "pr": 3908, + "author": "1337isnot1337", + "head": "0d8880e38ed7c88d70eec6a48e5aa829d0fb22f3", + "role": "Fixed-profile obstruction and favorable rank8 waiver; new endpoint escapes that waiver but not the retained-eight model." + }, + { + "pr": 3946, + "author": "Clear1nsight / Chris R", + "head": "8dec5c663ace6285aeee49ec3f8eeae9a8bc9a58", + "source_sha256": "e12f3d810a6f659e4b2453d251e323aa5e2c4693c4b28a9cec611796cc2dd94a", + "role": "budget.py explicitly extracts/adapts exact rational quadrature, price, profile expansion and moment functions; no unmerged source executable is needed at replay." + }, + { + "pr": 3181, + "author": "dcharb78", + "head": "80fc72d14546088e9fce3c06dc12bc67270da0af", + "role": "Reported eight-rank8 profile premise; no universal claim that those copies survive the changed outer demand." + } + ], + "additional_credit": [ + "ywz65 PR2492/2468 native read machinery", + "thakrarsagar PR2470 L2 identity", + "Ali Romman PR1969 and conserved QQ16/native lineage", + "starship-s original decoder", + "Ross Richardson retained-record lineage", + "Douglas Colkitt and Sagar Thakrar coverage/ceiling lineage", + "Nick Petalas numerical/consumer boundary guidance" + ], + "license": "New work Apache-2.0. Retained source notices remain in unchanged dependency files.", + "new_contribution": "Actual published demand binding, semantic projection with complete cleanup invoice, and changed budget exclusion/thresholds." +} diff --git a/research/qq16-f17-demand-projection/PROOF.md b/research/qq16-f17-demand-projection/PROOF.md new file mode 100644 index 0000000000..97c66df9a9 --- /dev/null +++ b/research/qq16-f17-demand-projection/PROOF.md @@ -0,0 +1,216 @@ +# A projected F17 demand and its fixed-profile obstruction + +This is an exact local interface result under the retained QQ16 common-label +cover contract. It is not a global controller, physical supplier, optimal +consumer, or new multiplication bound. + +## 1. An actual demand, and the change of inputs + +PR2512 (`851dd3486a2d0549b51e85978a65ccb4eec619c0`, ywz65) explicitly +ends with 96 consumer subtractions `Z_p -= X2_p`, ordinary ports p in U_ports, +returning logical `y1_U` in `F_U1`. Its proof defines this frame as the product +of C lines on coordinate axes 0 through 16, exactly PR2707's **F17**. The port +set U_ports and the 17-dimensional coordinate subspace are distinct objects. +The verifier authenticates the actual proof, full word and receipt, and checks +the literal 96-event consumer epilogue and its named output contract. + +PR2512 reads 96 current X, 96 current Y and eight retained earlier T arrays. +Here the demand is supplied instead from **all 112 current Y arrays**, with no +X read or early T record. The extra sixteen selected current Y reads are +available under PR2707's 224-current-field contract; they are not available +merely by assuming PR2512's narrower interface. Every Y is borrowed, physically +in `F17 C_qp^-1`. The result needs 96 exclusively owned output arrays and sixteen +owned full-cover temporaries. Arbitrary owned dirt is erased by paid CLEARs. +No borrowed source is written. All sixteen temporaries and eight private scratch +arrays finish at zero in identity frame. There is no storage/hosting admission. + +This pins a real published *local endpoint*, rather than inventing an ordinary +frame tariff. It does not establish that a complete selected outer controller +needs only these 96 values; other outputs may still be required there. + +## 2. The projected logical operator + +Use the actual ordered owner actions D_p in B1 and the pinned eight raw R rows. +Define the query and ordinary injection in the normalization used by PR2681: + + Q(Y)_k = sum_(p=0..111) R[k,p] D_p Y_p, + (K_U q)_p = (1/4) sum_k R[k,p] D_p^-1 q_k, p in U_ports. + +The retained complete B1 inverse first computes + + u_U = Y2_U - K_U Q(Y2). + +Its future-logger reversal writes only selected A ports. Therefore it leaves +u_U unchanged, and + + y1_U = Y2_U - K_U Q(Y2). (1) + +This also follows from the conserved B1 equations: `Q(Y2)` is the old selected +T query and `Y2_U = y1_U + K_U Q(Y2)`. The three conserved queries must not be +interchanged. The source proof gives the identity over the ordered cover +coefficient ring, so no owner matrices are silently commuted. + +The checker compares every demanded routed row of the new word with (1) on +112 independent current Y symbols: 4,992 nonzero owner-labelled terms. It also +forms B1 from 224 *independent x1/y1 symbols*, without imposing an F0 relation, +and verifies that (1) recovers exactly those y1_U symbols. The latter replay +checks the actual selected-row coefficients and future logger, rather than +assuming a payload-constant or identity-owner special case. + +## 3. A legal native word + +`WORD.json` is regenerated deterministically from the complete authenticated +3,823-event PR2707 word. It has 1,410 events: + +1. For every port, clear owned W_p in the Y hole frame, copy borrowed Y_p, and + apply the positive rank-one line C_qp. W now has F17 and logical Y2. +2. Finish the source B1 alignment map on every W. With the actual source-derived + affine translation, `M_p F17 = F17 D_p`. All query operands have common F17. +3. At each owner execute the entire private body: clear eight F_k, form all + eight Q rows from the complete 112-port W bank, subtract `R[k,p] F_k/4` from + ordinary W_p only, then clear all F_k in identity frame. Every query is + formed before any W output is overwritten. Finish the owner body before + visiting the next owner. +4. Undo the alignment map on the 96 ordinary W outputs. Clear the sixteen + selected W temporaries directly in their existing frame, returning them + to zero in identity frame. Clearing owned dirt is a paid primitive; no + inverse map or native child is required to dispose of those owned values. + +The temporary disposal is an explicit addition to the projected prefix. It +prevents an unreported dirty full-cover workspace liability. Every borrowed +Y retains its exact initial content and frame, and every X is untouched. + +This projection is semantic: stage-2 map/line conjugations cancel on U because +that logger writes only A. A naive instruction-liveness pass would retain +conjugations on the demanded W fields. There is no reordering of native reads +or private bodies, and no claim of shortest code or a universal 112-child floor. + +The phase checker uses complete modulo-four quadratic coefficients on all 73 +coordinates at every ADD and output. A line contributes parity, and parity has +no terms above degree two modulo four. Thus these are full phase identities. +By Fourier spanning they hold on arbitrary payload arrays; owner pullback and +per-layer multiplication extend them to all owners and tensor layers under +the inherited cover contract. The source kernels are lowered using a basis +whose first column is q: one positive H1 child plus two inverse monomial +wrappers realizes C_q. All 112 bases and 57,344 basis columns are checked; +the other coordinates are spectators. This is not an execution on a huge +physical tape, or a proof of child precision/placement. + +## 4. Complete local invoice and real removed work + +| Charge | New demand word | Complete PR2707 decoder | Difference removed | +|---|---:|---:|---:| +| Positive rank-one children | 112 | 336 | 224 | +| Rank-eight children | 0 | 0 | 0 | +| Native monomial wrappers | 224 | 672 | 448 | +| Full-cover maps | 208 | 464 | 256 | +| Unit ADD macros | 560 | 1,808 | 1,248 | +| Quarter ADD macros | 384 | 896 | 512 | +| CLEAR macros | 144 | 312 | 168 | +| Real scalar primitive allowance | 9,376 | 25,840 | 16,464 | + +The scalar allowance is `8*560 + 12*384 + 2*144`. Its 144 clears include 112 +initial owned clears, sixteen private entry/exit clears and sixteen final +full-cover temporary clears. There are 96 owned outputs, sixteen full-cover +temporaries, eight owner-private scratch arrays, no early records and no X +reads. All 112 borrowed Y fields are restored by remaining read-only. + +What disappears is the future logger reversal, the F0 inverse and unrelated +X1/selected-output recovery, including the two complete future-frame line +sweeps. The final output contract changes from all 224 original arrays to the +96 published y1_U demand. These are actual deleted operations; no unchanged +recursive child is assigned a lower tariff merely because its bit axis became +cheaper. The comparison is not a same-output full-decoder improvement. + +Against PR2512's same logical *output* with different input/lifetime premises, +this replaces `192 H1 + 16 H8` with `112 H1`, keeps 208 cover maps, and raises +scalar allowance from 7,392 to 9,376. It removes early retention but needs the +sixteen additional current Y fields, sixteen owned temporaries and eight +private scratch arrays rather than one. No dominance or global memory saving +follows from comparing child rank mass alone. + +## 5. What the changed budget proves, and what it does not + +Recounting the literal source F0/B1 words gives per-call average + + n = {1:2428, 2:418, 3:432, 4:142, 5:82}. + +For the **same conditional pair-rate budget used by PR3908/PR3946**, allocate +one demand word per two calls: add 56 H1 per call. Retaining the reported +selected-profile eight H8 charges gives + + n_full = {1:2484, 2:418, 3:432, 4:142, 5:82, 8:8}. + +The eight H8 charges are the retained profile premise, not new children in +this demand word. This package does not prove that all eight remain needed +by an outer controller with a changed demand. That is an explicit next audit. +Likewise, this local pair amortization does not prove a full nine-call schedule +or the number of decoder invocations required globally. + +Keep m=73, W=896/9, centre=64, and total mass T=72W+64=7232. The largest idle +rank allowed by the outer halving guard is R=51 (`2*51^2 < 73^2 < 2*52^2`). +For a>=0, price per rank-mass unit is `73^(a-1) r^(-a)`, nonincreasing in r. +Every legal idle placement is therefore at least as expensive as fractional +rank-51 idle work. If L=sum r*n_r and I=T-L, the favorable necessary screen is + + G(a) = [sum_r n_r (r/73)^(1-a) + + (I/51) (51/73)^(1-a)] / W. + +For n_full, L=5658 and I=1574. For the rank-eight-waived variant, L=5594 and +I=1638. All maps, wrappers, scalar operations, storage, movement, placement, +precision and numerical-error costs are set favorably to zero in this screen. +Thus failure already excludes the fixed profile; passing supplies no physical +construction. The actual complete local invoice above remains a liability. + +At the selected `a=836330098538459/499163669901461541`, exact rational bounds are: + +| Hypothesis | Enclosure for G | +|---|---| +| Eight reported H8 charges retained | [1.000023149708, 1.000023150305] | +| All eight H8 charges waived into rank-51 idle mass | [0.999995759681, 0.999995760274] | + +The previous *rank-eight-waived* obstruction no longer applies to this changed +endpoint. Carrying it over would be wrong. The retained-eight profile still +fails even before physical overhead. With those eight charges fixed, at most +61 integer decoder H1 calls per pair pass this relaxation; 62 fail. Our word +has 112, so it needs at least 51 fewer pair calls, with no compensating charges, +merely to pass the optimistic integer screen. There is no theorem that 61 is +achievable, or that no different operator implementation can do better. + +Waiving all eight charges permits at most 121 integer pair calls; our 112 leaves +only [0.000004239726, 0.000004240319] normalized allowance. Neither removing those +children nor paying the remaining physical liabilities is constructed here. +With 112 H1 fixed, retaining two H8 across the pair gives +[0.999999183434, 0.999999184028], while three gives +[1.000000895311, 1.000000895905]. Thus at least fourteen of the reported sixteen +H8 charges across two calls must disappear, with no other new costs, to pass +this integer relaxation. This is a repayment target, not a claim that a copy +can be removed or that fractional per-call assignment is physically legal. +The exact fixed-profile exclusion is the stopping result; it is not a global +QQ16 obstruction and does not authorize construction expansion. + +The rational arithmetic is explicitly adapted from PR3946's independently +checked midpoint/trapezoid logarithm and exponential remainder implementation. +For convex 1/t on [1,y], midpoint sums are lower and trapezoid sums upper +bounds on log(y). Scale arguments into [1,2], round outwards to 2^-80, and use +the degree-six positive exponential sum with first omitted term divided by +`1-hi/(degree+2)` as geometric tail. Every final decision compares Fractions; +decimal formatting also rounds outward. Both sides of the 61/62 and 121/122 +thresholds are verified, rather than deriving a decision from rounded output. + +## 6. Bounded next question + +Audit the *actual eight H8 centre-copy outputs* in the retained supplier and +whether their downstream uses survive this 96-output demand. First bind each +copy's source, destination, frame and last use in the selected archive and a +single real continuation. Either identify legal retirement and recompute the +coverage mass (centre 64 cannot simply be kept or deleted by assertion), or +prove all eight copies are still required under that continuation. This decides +whether the relaxed opening has a valid premise before optimizing physical +kernels. If retained, stop this recipe unless producer/consumer fusion deletes +at least 51 genuine H1 pair charges or another priced premise changes. + +No new retained-query construction, further precision optimization or centre +change is implemented. Full controller demand, copy lifetimes, both supplier +caps, physical map/wrapper costs, numerical grids/dirty ranges, child placement +and all-depth cleanup remain open. diff --git a/research/qq16-f17-demand-projection/README.md b/research/qq16-f17-demand-projection/README.md new file mode 100644 index 0000000000..75097e5b75 --- /dev/null +++ b/research/qq16-f17-demand-projection/README.md @@ -0,0 +1,84 @@ +# A real F17 demand: 112-child projection and a conditional budget obstruction + +PR2512's published consumer demands 96 ordinary `y1_U` arrays in `F_U1=F17`. +Projecting PR2707's zero-retention inverse onto this demand removes real work: +**336 -> 112 rank-one children**, **464 -> 208 cover maps**, **672 -> 224 native +wrappers**, and **25,840 -> 9,376 scalar primitive allowance**. The complete +1,410-event word reads all 112 current Y fields, no X fields or early records; +it returns 96 owned outputs, clears sixteen full-cover temporaries and eight +owner-private scratch fields, and leaves all borrowed fields untouched. + +This changed demand **escapes PR3908's rank-eight-waived obstruction**. It does +not yield an admitted supplier. Retaining the reported eight H8 profile charges +still gives a favorable moment in **[1.000023149708, 1.000023150305]**, above one +at the selected saving even with physical overhead free. The waived profile +instead lies in **[0.999995759681, 0.999995760274]**, leaving only about +0.00000424 normalized allowance. The fixed-eight profile requires at least +51 fewer decoder H1 calls per pair just to pass the optimistic integer screen. + +[PROOF.md](PROOF.md) gives the operator identity, exact input/frame/ownership +contract, complete counts, rational bounds and limits. This is one source-bound +local endpoint and a conditional fixed-profile exclusion, not a shortest word, +whole-controller result, physical six-tape admission, net storage saving or new +kappa. The full 224-output decoder and its obstruction remain valid for their +original contract. PR2512's input contract differs: its eight retained T arrays +are replaced by sixteen additional selected current Y reads here. + +## Reproduce + +Standard library, CPython 3.12; from repository root: + +```sh +python3 -I -Werror -B research/qq16-f17-demand-projection/verify.py +python3 -I -O -Werror -B research/qq16-f17-demand-projection/test_verify.py +python3 -B scripts/research_package.py --package research/qq16-f17-demand-projection +``` + +`verify.py` checks the complete committed word and receipt without writing. +Expected marker: `PASS_QQ16_F17_DEMAND_PROJECTION no_new_kappa`. Its replay uses +explicitly adapted, source-authenticated predecessor operator primitives; +it is not a code-disjoint reimplementation of all inherited algebra. +Evidence includes independent x1/y1 B1 symbols, 4,992 demanded routed terms, +full 73-coordinate phases, 57,344 native basis columns, nine semantic mutants, +the complete local invoice and both sides of the budget thresholds. Seven +boundary test groups include a read-only Git-free export, pre-execution source +failure and complete word/typed receipt rejection. See VERIFICATION.json for +actual commands and publication checks. No huge payload, selected cold replay, +Lean/formal-kernel check or independent human review is claimed. + +## Scope and workflow + +Explicit assigned continuation of #3946/#3908; no task reroll. Canonical main +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6; exact inputs and +original task card in SOURCES.json/TASK.json. Only this scoped package is added. +Frozen sources and selected frontier are unchanged. The [advance claim and +canonical update](https://github.com/CrocSwap/integer-mult-bounds/pull/3946#issuecomment-6260950964) +records the stop rule. Live targeted PR searches and the overlap helper found +the named adjacent packages; the helper lacks gh, so remote coverage is partial, +not a novelty guarantee. PREDECESSORS.json retains exact heads and code reuse. + +## Open next questions + +The next useful audit is **the eight reported rank-eight centre copies under +this actual reduced demand**. Bind their literal source/destination/frame and +last uses to one real continuation; decide whether they can legally retire (at least fourteen of sixteen pair H8 charges must disappear with this 112-H1 word under unchanged centre 64), +and recompute coverage and physical costs. If they remain, this word is +excluded in the fixed model and needs at least 51 genuinely removed H1 pair +charges before further implementation is warranted. A hypothetical free centre +or arbitrary waiver is not that audit. Structured questions, first steps and +blockers are in TASK.json; the full stopping rule is in PROOF.md section 6. + +## Credit + +Chris R / Clear1nsight, with substantial OpenAI assistance in source inspection, +derivation, implementation, verification and writing. Apache-2.0. + +Credit ywz65's #2512/#2492/#2468 for the actual demand, L2 native maps and read +machinery; thakrarsagar/#2470 for L2; Arham Tahir/#2681 for the complete logical +inverse and routed/phase primitives; ywz65/#2707 for the line-normalized physical +word; 1337isnot1337/#3908 for the budget obstruction; dcharb78/#3181 for its +profile premise; Clear1nsight/#3946 for the independent budget arithmetic; +Ali Romman/#1969, starship-s, Ross Richardson and retained QQ16/native lineage; +Douglas Colkitt, Sagar Thakrar and coverage-ceiling contributors. Source notices +remain intact. The new result is the demanded projection, its complete local +invoice and the changed budget conclusion, not those predecessor identities. diff --git a/research/qq16-f17-demand-projection/RESULT.json b/research/qq16-f17-demand-projection/RESULT.json new file mode 100644 index 0000000000..8bace48d2d --- /dev/null +++ b/research/qq16-f17-demand-projection/RESULT.json @@ -0,0 +1,216 @@ +{ + "budget": { + "centre64_retaining_eight_rank8": { + "decimal_lower": "1.000023149708", + "decimal_upper": "1.000023150305", + "lower": "250005787427/250000000000", + "upper": "200004630061/200000000000" + }, + "centre64_waiving_eight_rank8": { + "decimal_lower": "0.999995759681", + "decimal_upper": "0.999995760274", + "lower": "999995759681/1000000000000", + "upper": "499997880137/500000000000" + }, + "pair_call_reduction_still_required_with_rank8_retained": 51, + "retained_profile_max_pair_calls": 61, + "three_H8_per_pair": { + "decimal_lower": "1.000000895311", + "decimal_upper": "1.000000895905", + "lower": "1000000895311/1000000000000", + "upper": "200000179181/200000000000" + }, + "two_H8_per_pair": { + "decimal_lower": "0.999999183434", + "decimal_upper": "0.999999184028", + "lower": "499999591717/500000000000", + "upper": "249999796007/250000000000" + }, + "waived_profile_max_pair_calls": 121, + "waived_profile_normalized_allowance": { + "decimal_lower": "0.000004239726", + "decimal_upper": "0.000004240319", + "lower": "2119863/500000000000", + "upper": "4240319/1000000000000" + }, + "with_112_H1_first_excluded_integer_H8_per_pair": 3, + "with_112_H1_max_integer_retained_H8_per_pair": 2 + }, + "controls": { + "borrowed clear": "clear borrowed input", + "injection sign": "wrong demanded output W1", + "map translation": "ADD frame mismatch 450", + "normalization": "ADD frame mismatch 449", + "output inverse map": "wrong demanded output W1", + "owned dirt": "ADD frame mismatch 0", + "private cleanup": "scratch leak", + "query sign": "wrong demanded output W2", + "temporary cleanup": "temporary leak" + }, + "counts": { + "add": 944, + "begin": 1, + "clear": 144, + "end": 1, + "line": 112, + "map": 208, + "quarter_ADD": 384, + "unit_ADD": 560 + }, + "demand": { + "cut": "immediate post-B1", + "frame": "F17", + "logical_output": "y1_U", + "new_retained_T": 0, + "ports": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 22, + 23, + 24, + 25, + 26, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 77, + 78, + 79, + 80, + 82, + 83, + 84, + 85, + 86, + 88, + 89, + 90, + 91, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109 + ], + "source_pr": 2512, + "source_retained_T": 8 + }, + "demanded_formal_terms": 4992, + "events": 1410, + "invoice": { + "CLEARs": 144, + "current_X_reads": 0, + "early_record_banks": 0, + "full_cover_maps": 208, + "native_monomial_wrappers": 224, + "native_rank_mass": 112, + "owned_full_cover_outputs": 96, + "owned_full_cover_temporaries": 16, + "peak_local_owned_scratch": 8, + "quarter_ADDs": 384, + "rank_eight_children": 0, + "rank_one_children": 112, + "real_scalar_primitive_allowance": 9376, + "unit_ADDs": 560, + "untouched_borrowed_current_Y": 112 + }, + "positive_native_kernel_columns": 57344, + "producer_profiles": { + "B_1_2": { + "1": 2436, + "2": 418, + "3": 432, + "4": 142, + "5": 82 + }, + "F_0": { + "1": 2420, + "2": 418, + "3": 432, + "4": 142, + "5": 82 + } + }, + "removed_from_full_decoder": { + "CLEARs": 168, + "full_cover_maps": 256, + "native_monomial_wrappers": 448, + "native_rank_mass": 224, + "quarter_ADDs": 512, + "rank_one_children": 224, + "real_scalar_primitive_allowance": 16464, + "unit_ADDs": 1248 + }, + "scope": "One demand; complete local primitive counts; fixed-profile optimistic screen only. No physical/global admission.", + "selected_a": "836330098538459/499163669901461541", + "status": "PASS_QQ16_F17_DEMAND_PROJECTION no_new_kappa", + "word_sha256": "ab81289ccf14365c681ded9c479d082d923b5510c839395045bf115e05f4e661" +} diff --git a/research/qq16-f17-demand-projection/SOURCES.json b/research/qq16-f17-demand-projection/SOURCES.json new file mode 100644 index 0000000000..65d3e66048 --- /dev/null +++ b/research/qq16-f17-demand-projection/SOURCES.json @@ -0,0 +1,150 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/complex-local-word-ceiling/RESULT.json", + "usage": "input", + "git_blob": "77f55043a679dd722330f1e2499863e36376d9f9", + "sha256": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + { + "path": "research/joint-query/verify_native.py", + "usage": "input", + "git_blob": "ede9e7e42744dd0c96790516a9acdfe07d180018", + "sha256": "1c58e7b6e8e1cde4df455c2129601c145ed763fc63a3ab427eb1058d1fc08bd2" + }, + { + "path": "research/joint-query/verify_scalar.py", + "usage": "input", + "git_blob": "7a7051fa8a70f48589fa1fccd5c38fccb5eacbf7", + "sha256": "33bdbad17a0531fe527aff306eb235d9c38c1629db4fd167b989725930b0327a" + }, + { + "path": "research/qq16-current-frame-consumer/PROOF.md", + "usage": "input", + "git_blob": "37bce9925fc21e970af3d39b36cc899b4ceebfb5", + "sha256": "a485fdf7fd44abe1b9004a8502871ef24d7617809879d1a6550ffa425e1a79f7" + }, + { + "path": "research/qq16-current-frame-consumer/RESULT.json", + "usage": "input", + "git_blob": "a62abbb72e4eaa4a35ade12ed97e75e99a300036", + "sha256": "1d0ba2a2d54a69a692a296e8f96838e36fc508df85b01b4260d2a5e5afced8a5" + }, + { + "path": "research/qq16-current-frame-consumer/WORD.json", + "usage": "input", + "git_blob": "86eb32f0b123b3e6c352e12aba65cde050e7c9c3", + "sha256": "d292a910884a75b4d486724092b7ab009c13a3f54c4feecf88a17cc712b6e92e" + }, + { + "path": "research/qq16-line-normalized-decoder/PREDECESSORS.json", + "usage": "input", + "git_blob": "db77dbf21b0f89b1f5bdbd308ab20d0045f61561", + "sha256": "a8be0439e350d7a634a188176894ec51180efc0d236a56b293d39dc96383a87d" + }, + { + "path": "research/qq16-line-normalized-decoder/RESULT.json", + "usage": "input", + "git_blob": "ba4167dbf133cff51513bb832802c290edcdffea", + "sha256": "58df4ad68e2ff335ee58fa4336a449d0f73f3366d840574e5e30b50f507c358d" + }, + { + "path": "research/qq16-line-normalized-decoder/SOURCES.json", + "usage": "input", + "git_blob": "300c183db8d263899ee1795033af215ba6522b9f", + "sha256": "66bf8f57019632ef45780769c6f112d287e145e23ff03336998589b474165fbe" + }, + { + "path": "research/qq16-line-normalized-decoder/WORD.json", + "usage": "input", + "git_blob": "e45320dcb07ef2dc89622e9ca68adfe826a6e9dd", + "sha256": "5623b9cd62635d47f84e78135d817cfddec7ae31c154c565bf6e16cf5ed75475" + }, + { + "path": "research/qq16-line-normalized-decoder/vendor/pr2681/PROOF.md", + "usage": "input", + "git_blob": "38cd38aa1d342f3bfe0d6d7f3c388aff0352f370", + "sha256": "471f6360cdac94d9e1054c6c9530ace1822b11942f7e141dfd344864d2357862" + }, + { + "path": "research/qq16-line-normalized-decoder/vendor/pr2681/README.md", + "usage": "input", + "git_blob": "c3d4d76b28fa47b86da37cc7428d5da362c7bf9a", + "sha256": "b658e00db095f1097b9ae7ec49d8dd465c1a317cdc84da4251cbdd3e0af597d3" + }, + { + "path": "research/qq16-line-normalized-decoder/vendor/pr2681/RESULT.json", + "usage": "input", + "git_blob": "a16a8f9a23cd00c9030f9b03cf0ae52c0ff4b526", + "sha256": "e4f3ff28be27f96c341b225a62a2ba84d3907ed3466122d18bcaaf5a60da740e" + }, + { + "path": "research/qq16-line-normalized-decoder/vendor/pr2681/SOURCES.json", + "usage": "input", + "git_blob": "1db7201ed145d1ef3707ab24bb599d341439050d", + "sha256": "30a88d8bf33c603836fffdcab3c3dabf663b98f2deda95893685e394c60ea95c" + }, + { + "path": "research/qq16-line-normalized-decoder/vendor/pr2681/WORD.json", + "usage": "input", + "git_blob": "80de97cf168441a888e7d05fc2c3cace919f31ec", + "sha256": "f02e57d238f127c8fd195dc6a4a9dce6db6bee9f6050bd9d5b9c14cf6e1946d0" + }, + { + "path": "research/qq16-line-normalized-decoder/vendor/pr2681/references/PR2540-PROOF.md", + "usage": "input", + "git_blob": "6ae136c8baef4793f4f7ae630720afff6c23a953", + "sha256": "09d587f1d6bc250e90e29fa8751a40f45be79f1a8a56af0b645c144cefaefa46" + }, + { + "path": "research/qq16-line-normalized-decoder/vendor/pr2681/references/PR2540-README.md", + "usage": "input", + "git_blob": "e91138fb0fabbc0fe0e9fd80ee189ed4366a0f61", + "sha256": "07588c3863b8d686497d9c0b263c35c47424fa3b63d43b7c2e5f788bd31a8d3f" + }, + { + "path": "research/qq16-line-normalized-decoder/vendor/pr2681/verify.py", + "usage": "input", + "git_blob": "99bd60a9139b4d7ef070b69f38a954e64e0f8aa1", + "sha256": "71f9a010553691e892703e3ec8d5eedf3e48d72b7f6af24b954a5442f4a52ccf" + }, + { + "path": "research/qq16-line-normalized-decoder/verify.py", + "usage": "input", + "git_blob": "a8f3c811108414eda0b507d295cfc9301c04d585", + "sha256": "0f6fb86aafb74b9722f20cc97af70a3a3c78bd012c142b2eaa19cb00e02d1fe9" + } + ] +} diff --git a/research/qq16-f17-demand-projection/TASK.json b/research/qq16-f17-demand-projection/TASK.json new file mode 100644 index 0000000000..5266219c8d --- /dev/null +++ b/research/qq16-f17-demand-projection/TASK.json @@ -0,0 +1,152 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "joint-query-controller", + "question": "Can a literal QQ16 producer meet the proposed completed-output error budgets with dirty helpers and an affordable physical consumer?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md", + "research/qq16-producer-defect-transfer/README.md" + ], + "methods": [ + "Derive one literal producer's completed-output defects and intermediate dirty-helper bounds, with its physical bill.", + "Design or audit one consumer, retention or hosting boundary and its complete cost for the pinned producer/decoder." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2965 producer-defect transfer after the local QQ16 decoder contract. Its author-checked output-error estimate does not implement producer interiors, bound dirty helpers, or pay for the consumer; independently check the implication used.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Pin one literal F0/B1 producer and its native-child contracts; derive the actual intermediate magnitude ledger and completed-output defects, including dirty helpers and correlations. Compare with #2965 budgets and price storage, movement, cleanup and F17 consumption. Stop with a precise missing bound if no producer contract supplies it; do not optimize another decoder precision constant in isolation.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer" + ] + }, + "scope_status": "refined", + "actual_scope": "Pin PR2512 ordinary y1_U in F17; project PR2707 without early retention; verify actual eliminated work, complete local invoice and fixed-centre pair-budget obstruction.", + "scope_change_reason": "Explicit assigned continuation of PR3946/PR3908. A concrete published local endpoint replaces the full224-output demand; no new producer or precision construction is authorized by this local result.", + "bottleneck_link": "The unchanged full decoder exceeded the favorable budget. An actual reduced F17 endpoint changes which operations are needed and exposes exactly which cost premise still blocks admission.", + "budget_minutes": 60, + "stop_rule": "Stop after exact routed/frame/ownership verification and a complete local primitive invoice. If the fully favorable retained profile exceeds one, retain a scoped obstruction and source-impact handoff; do not expand implementation on a passing waiver alone.", + "outcome": "completed", + "evidence": "PROOF.md gives the local theorem and scoped obstruction; WORD.json and RESULT.json are complete checked artifacts; verify.py/test_verify.py replay exact rows, frames, native kernels, invoices and failure controls; VERIFICATION.json records runs.", + "author": "Chris R / Clear1nsight with OpenAI assistance", + "ai_assistance": "Substantial OpenAI assistance in source audit, derivation, implementation, testing and writing. No subagent or independent human review.", + "open_questions": [ + { + "question": "Which of the eight reported H8 centre copies per call remain required by a real continuation of the 96-output demand?", + "why_it_matters": "At 112 H1 per pair, three retained H8 across the pair already fail the fixed-centre relaxation; at most two pass. Merely waiving all eight per call is not a construction.", + "first_step": "Bind each literal centre-copy source/destination/frame and last use in the selected archive, beginning with slots/local/CANONICAL-WORD.json.gz and its centre/frame metadata, then one actual continuation. Recompute coverage when a copy is retired.", + "blocked_by": "No copy-lifetime or changed-coverage construction is supplied; global demand may still require additional outputs." + }, + { + "question": "If all eight H8 per call remain, can producer-consumer fusion remove at least 51 of the 112 real H1 pair charges?", + "why_it_matters": "The fixed-profile integer relaxation permits only 61 decoder H1 per pair even before physical overhead.", + "first_step": "Trace the current Y hole encodings through the actual producer; accept a fused read only if an existing normalization or other native operation is deleted, with borrowed restoration and output lifetimes preserved.", + "blocked_by": "No such legal fusion, lower-cost operator word, physical allowance or all-depth admission is currently proved." + } + ], + "assignment": "Direct user assignment; no task picker draw or reroll.", + "scope_key": "QQ16/post-B1/PR2512-y1_U-F17/PR2707-zero-retention-demand-projection", + "canonical_investigation": "https://github.com/CrocSwap/integer-mult-bounds/pull/3946#issuecomment-6260950964", + "started_at_utc": "2026-10-19T06:08:46Z", + "checkpoints": [ + { + "at_utc": "2026-10-19T06:08:46Z", + "main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "decision": "Read canonical main entry guidance, preserve predecessor branch, start isolated assigned-task branch." + }, + { + "at_utc": "2026-10-19T06:22:56Z", + "main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "decision": "Main unchanged; stop construction after retained-profile failure and verify bounded demand artifact." + }, + { + "at_utc": "2026-10-19T06:30:19Z", + "main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "decision": "Prepublication refresh unchanged, guidance/selected inputs compatible. Exact demand search returns only predecessor3946; 3946 head unchanged. Preserve frozen scientific base." + } + ], + "overlap": { + "helper_at_utc": "2026-10-19T06:22:56Z", + "local_records": 37, + "remote_open_prs": null, + "remote_discussions": null, + "warnings": [ + "gh absent; no usable complete remote snapshots. Bounded coverage, not a novelty guarantee." + ], + "live_queries": [ + "QQ16 F17 consumer", + "QQ16 y1_U", + "QQ16 current-frame", + "QQ16 112 consumer" + ], + "nearest_prs": [ + 2512, + 2492, + 2707, + 2681, + 2651, + 2678, + 3181, + 3908, + 3946 + ], + "distinction": "New demand projection and precise changed budget; not a repeated complete decoder or old-frame tariff.", + "browser_check": { + "at_utc": "2026-10-19T06:27:00Z", + "pages": [ + "Discussion1163 claim conventions", + "Visible newest handoffs and rendered QQ16 mentions in Discussion1166" + ], + "coverage": "Visible loaded comments only; no complete pagination claimed." + }, + "additional_local_scope_check": { + "packages": [ + "qq16-output-slice-scratch", + "qq16-whole-source", + "qq16-readset-matroid-independent" + ], + "result": "Different scratch-allocation, scalar-source-value and readset-classification scopes." + } + } +} diff --git a/research/qq16-f17-demand-projection/VERIFICATION.json b/research/qq16-f17-demand-projection/VERIFICATION.json new file mode 100644 index 0000000000..f42953e022 --- /dev/null +++ b/research/qq16-f17-demand-projection/VERIFICATION.json @@ -0,0 +1,49 @@ +{ + "environment": "Linux x86_64, CPython 3.12.3, standard library", + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "completed_local": [ + { + "command": "python3 scripts/research_baseline.py", + "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; initial sparse-checkout missing-file attempts were resolved by restoring canonical reference paths; no source was edited." + }, + { + "command": "python3 -I -Werror -B research/qq16-f17-demand-projection/verify.py", + "result": "PASS_QQ16_F17_DEMAND_PROJECTION no_new_kappa; complete word/receipt, exact routed demand, arbitrary dirt, full phases, 57344 positive kernel columns, nine semantic controls and rational budget thresholds." + }, + { + "command": "python3 -I -O -Werror -B research/qq16-f17-demand-projection/test_verify.py", + "result": "Seven behavioral/boundary groups pass, including read-only Git-free export, authentication before execution, typed receipt and missing-cleanup word rejection; observed standalone times 29.4 to 30.0 seconds." + }, + { + "command": "python3 -B scripts/research_package.py --package research/qq16-f17-demand-projection --check-only", + "result": "PASS_PACKAGE_METADATA_AND_PINS. Draft metadata field-type/outcome errors were corrected before the successful registered replay." + }, + { + "command": "python3 -B scripts/research_package.py --package research/qq16-f17-demand-projection", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE research/qq16-f17-demand-projection outcome=completed; seven test groups pass in 31.167 seconds under the registered optimized warning-strict command." + }, + { + "command": "Independent Decimal calculation at precision80 using explicit retained profile and idle1574", + "result": "G=1.0000231499072846357374358890539252091932368344950370469424927566285279251247703, inside the proved rational enclosure. Numerical corroboration only; the rational proof determines the conclusion." + }, + { + "command": "git diff --check", + "result": "Pass for tracked diff; added files checked again against the published commit before submission." + } + ], + "publication_validation": { + "initial_head": "9a3b8ca06a86a8d09f9115c7b6bbe9933f6e4dd7", + "preflight": "PASS_RESEARCH_COMMIT_BYTES with source-history check for 36 package/input files; same scientific payload. Final whitespace-only budget.py EOF cleanup and this publication record follow as a GitHub-created commit; final-head preflight and hosted checks are recorded in the PR.", + "source_history_commits": [ + "20ecf2891d80b5acf18d980b2164fb44ea7faa90" + ] + }, + "unrun_or_open": [ + "Independent reimplementation of all inherited operator/phase primitives; replay.py explicitly adapts PR2707 and uses authenticated PR2681 primitives.", + "Independent human or proof-assistant review, huge physical payload execution, complete native F0/B1 core replay and selected frontier cold replay.", + "Physical six-tape caller admission, map/wrapper movement and placement, precision/dirty-range ledger and all-depth supplier caps.", + "A full outer continuation proving that only the 96 local outputs are needed and determining whether the reported eight rank8 charges per call remain required.", + "A complete physical tariff for the new word or a legal changed-coverage construction. Counts are complete local primitive counts; unknown physical costs are not zero." + ] +} diff --git a/research/qq16-f17-demand-projection/VERIFY.json b/research/qq16-f17-demand-projection/VERIFY.json new file mode 100644 index 0000000000..a1c75bbccd --- /dev/null +++ b/research/qq16-f17-demand-projection/VERIFY.json @@ -0,0 +1,57 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/complex-local-word-ceiling/RESULT.json", + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/verify_native.py", + "research/joint-query/verify_scalar.py", + "research/qq16-current-frame-consumer/PROOF.md", + "research/qq16-current-frame-consumer/RESULT.json", + "research/qq16-current-frame-consumer/WORD.json", + "research/qq16-line-normalized-decoder/PREDECESSORS.json", + "research/qq16-line-normalized-decoder/RESULT.json", + "research/qq16-line-normalized-decoder/SOURCES.json", + "research/qq16-line-normalized-decoder/WORD.json", + "research/qq16-line-normalized-decoder/vendor/pr2681/PROOF.md", + "research/qq16-line-normalized-decoder/vendor/pr2681/README.md", + "research/qq16-line-normalized-decoder/vendor/pr2681/RESULT.json", + "research/qq16-line-normalized-decoder/vendor/pr2681/SOURCES.json", + "research/qq16-line-normalized-decoder/vendor/pr2681/WORD.json", + "research/qq16-line-normalized-decoder/vendor/pr2681/references/PR2540-PROOF.md", + "research/qq16-line-normalized-decoder/vendor/pr2681/references/PR2540-README.md", + "research/qq16-line-normalized-decoder/vendor/pr2681/verify.py", + "research/qq16-line-normalized-decoder/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact demanded outputs, full frame phases, source pins, all private/full-cover cleanup, positive children, literal costs and rational budget rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Read-only Git-free replay, source authentication and complete receipt/word rejection." + } + ] +} diff --git a/research/qq16-f17-demand-projection/WORD.json b/research/qq16-f17-demand-projection/WORD.json new file mode 100644 index 0000000000..c23da2f205 --- /dev/null +++ b/research/qq16-f17-demand-projection/WORD.json @@ -0,0 +1,1412 @@ +[ + ["clear","W0","hole0"], + ["add","W0","Y0","1"], + ["line","W0",0,1], + ["clear","W1","hole1"], + ["add","W1","Y1","1"], + ["line","W1",1,1], + ["clear","W2","hole2"], + ["add","W2","Y2","1"], + ["line","W2",2,1], + ["clear","W3","hole3"], + ["add","W3","Y3","1"], + ["line","W3",3,1], + ["clear","W4","hole4"], + ["add","W4","Y4","1"], + ["line","W4",4,1], + ["clear","W5","hole5"], + ["add","W5","Y5","1"], + ["line","W5",5,1], + ["clear","W6","hole6"], + ["add","W6","Y6","1"], + ["line","W6",6,1], + ["clear","W7","hole7"], + ["add","W7","Y7","1"], + ["line","W7",7,1], + ["clear","W8","hole8"], + ["add","W8","Y8","1"], + ["line","W8",8,1], + ["clear","W9","hole9"], + ["add","W9","Y9","1"], + ["line","W9",9,1], + ["clear","W10","hole10"], + ["add","W10","Y10","1"], + ["line","W10",10,1], + ["clear","W11","hole11"], + ["add","W11","Y11","1"], + ["line","W11",11,1], + ["clear","W12","hole12"], + ["add","W12","Y12","1"], + ["line","W12",12,1], + ["clear","W13","hole13"], + ["add","W13","Y13","1"], + ["line","W13",13,1], + ["clear","W14","hole14"], + ["add","W14","Y14","1"], + ["line","W14",14,1], + ["clear","W15","hole15"], + ["add","W15","Y15","1"], + ["line","W15",15,1], + ["clear","W16","hole16"], + ["add","W16","Y16","1"], + ["line","W16",16,1], + ["clear","W17","hole17"], + ["add","W17","Y17","1"], + ["line","W17",17,1], + ["clear","W18","hole18"], + ["add","W18","Y18","1"], + ["line","W18",18,1], + ["clear","W19","hole19"], + ["add","W19","Y19","1"], + ["line","W19",19,1], + ["clear","W20","hole20"], + ["add","W20","Y20","1"], + ["line","W20",20,1], + ["clear","W21","hole21"], + ["add","W21","Y21","1"], + ["line","W21",21,1], + ["clear","W22","hole22"], + ["add","W22","Y22","1"], + ["line","W22",22,1], + ["clear","W23","hole23"], + ["add","W23","Y23","1"], + ["line","W23",23,1], + ["clear","W24","hole24"], + ["add","W24","Y24","1"], + ["line","W24",24,1], + ["clear","W25","hole25"], + ["add","W25","Y25","1"], + ["line","W25",25,1], + ["clear","W26","hole26"], + ["add","W26","Y26","1"], + ["line","W26",26,1], + ["clear","W27","hole27"], + ["add","W27","Y27","1"], + ["line","W27",27,1], + ["clear","W28","hole28"], + ["add","W28","Y28","1"], + ["line","W28",28,1], + ["clear","W29","hole29"], + ["add","W29","Y29","1"], + ["line","W29",29,1], + ["clear","W30","hole30"], + ["add","W30","Y30","1"], + ["line","W30",30,1], + ["clear","W31","hole31"], + ["add","W31","Y31","1"], + ["line","W31",31,1], + ["clear","W32","hole32"], + ["add","W32","Y32","1"], + ["line","W32",32,1], + ["clear","W33","hole33"], + ["add","W33","Y33","1"], + ["line","W33",33,1], + ["clear","W34","hole34"], + ["add","W34","Y34","1"], + ["line","W34",34,1], + ["clear","W35","hole35"], + ["add","W35","Y35","1"], + ["line","W35",35,1], + ["clear","W36","hole36"], + ["add","W36","Y36","1"], + ["line","W36",36,1], + ["clear","W37","hole37"], + ["add","W37","Y37","1"], + ["line","W37",37,1], + ["clear","W38","hole38"], + ["add","W38","Y38","1"], + ["line","W38",38,1], + ["clear","W39","hole39"], + ["add","W39","Y39","1"], + ["line","W39",39,1], + ["clear","W40","hole40"], + ["add","W40","Y40","1"], + ["line","W40",40,1], + ["clear","W41","hole41"], + ["add","W41","Y41","1"], + ["line","W41",41,1], + ["clear","W42","hole42"], + ["add","W42","Y42","1"], + ["line","W42",42,1], + ["clear","W43","hole43"], + ["add","W43","Y43","1"], + ["line","W43",43,1], + ["clear","W44","hole44"], + ["add","W44","Y44","1"], + ["line","W44",44,1], + ["clear","W45","hole45"], + ["add","W45","Y45","1"], + ["line","W45",45,1], + ["clear","W46","hole46"], + ["add","W46","Y46","1"], + ["line","W46",46,1], + ["clear","W47","hole47"], + ["add","W47","Y47","1"], + ["line","W47",47,1], + ["clear","W48","hole48"], + ["add","W48","Y48","1"], + ["line","W48",48,1], + ["clear","W49","hole49"], + ["add","W49","Y49","1"], + ["line","W49",49,1], + ["clear","W50","hole50"], + ["add","W50","Y50","1"], + ["line","W50",50,1], + ["clear","W51","hole51"], + ["add","W51","Y51","1"], + ["line","W51",51,1], + ["clear","W52","hole52"], + ["add","W52","Y52","1"], + ["line","W52",52,1], + ["clear","W53","hole53"], + ["add","W53","Y53","1"], + ["line","W53",53,1], + ["clear","W54","hole54"], + ["add","W54","Y54","1"], + ["line","W54",54,1], + ["clear","W55","hole55"], + ["add","W55","Y55","1"], + ["line","W55",55,1], + ["clear","W56","hole56"], + ["add","W56","Y56","1"], + ["line","W56",56,1], + ["clear","W57","hole57"], + ["add","W57","Y57","1"], + ["line","W57",57,1], + ["clear","W58","hole58"], + ["add","W58","Y58","1"], + ["line","W58",58,1], + ["clear","W59","hole59"], + ["add","W59","Y59","1"], + ["line","W59",59,1], + ["clear","W60","hole60"], + ["add","W60","Y60","1"], + ["line","W60",60,1], + ["clear","W61","hole61"], + ["add","W61","Y61","1"], + ["line","W61",61,1], + ["clear","W62","hole62"], + ["add","W62","Y62","1"], + ["line","W62",62,1], + ["clear","W63","hole63"], + ["add","W63","Y63","1"], + ["line","W63",63,1], + ["clear","W64","hole64"], + ["add","W64","Y64","1"], + ["line","W64",64,1], + ["clear","W65","hole65"], + ["add","W65","Y65","1"], + ["line","W65",65,1], + ["clear","W66","hole66"], + ["add","W66","Y66","1"], + ["line","W66",66,1], + ["clear","W67","hole67"], + ["add","W67","Y67","1"], + ["line","W67",67,1], + ["clear","W68","hole68"], + ["add","W68","Y68","1"], + ["line","W68",68,1], + ["clear","W69","hole69"], + ["add","W69","Y69","1"], + ["line","W69",69,1], + ["clear","W70","hole70"], + ["add","W70","Y70","1"], + ["line","W70",70,1], + ["clear","W71","hole71"], + ["add","W71","Y71","1"], + ["line","W71",71,1], + ["clear","W72","hole72"], + ["add","W72","Y72","1"], + ["line","W72",72,1], + ["clear","W73","hole73"], + ["add","W73","Y73","1"], + ["line","W73",73,1], + ["clear","W74","hole74"], + ["add","W74","Y74","1"], + ["line","W74",74,1], + ["clear","W75","hole75"], + ["add","W75","Y75","1"], + ["line","W75",75,1], + ["clear","W76","hole76"], + ["add","W76","Y76","1"], + ["line","W76",76,1], + ["clear","W77","hole77"], + ["add","W77","Y77","1"], + ["line","W77",77,1], + ["clear","W78","hole78"], + ["add","W78","Y78","1"], + ["line","W78",78,1], + ["clear","W79","hole79"], + ["add","W79","Y79","1"], + ["line","W79",79,1], + ["clear","W80","hole80"], + ["add","W80","Y80","1"], + ["line","W80",80,1], + ["clear","W81","hole81"], + ["add","W81","Y81","1"], + ["line","W81",81,1], + ["clear","W82","hole82"], + ["add","W82","Y82","1"], + ["line","W82",82,1], + ["clear","W83","hole83"], + ["add","W83","Y83","1"], + ["line","W83",83,1], + ["clear","W84","hole84"], + ["add","W84","Y84","1"], + ["line","W84",84,1], + ["clear","W85","hole85"], + ["add","W85","Y85","1"], + ["line","W85",85,1], + ["clear","W86","hole86"], + ["add","W86","Y86","1"], + ["line","W86",86,1], + ["clear","W87","hole87"], + ["add","W87","Y87","1"], + ["line","W87",87,1], + ["clear","W88","hole88"], + ["add","W88","Y88","1"], + ["line","W88",88,1], + ["clear","W89","hole89"], + ["add","W89","Y89","1"], + ["line","W89",89,1], + ["clear","W90","hole90"], + ["add","W90","Y90","1"], + ["line","W90",90,1], + ["clear","W91","hole91"], + ["add","W91","Y91","1"], + ["line","W91",91,1], + ["clear","W92","hole92"], + ["add","W92","Y92","1"], + ["line","W92",92,1], + ["clear","W93","hole93"], + ["add","W93","Y93","1"], + ["line","W93",93,1], + ["clear","W94","hole94"], + ["add","W94","Y94","1"], + ["line","W94",94,1], + ["clear","W95","hole95"], + ["add","W95","Y95","1"], + ["line","W95",95,1], + ["clear","W96","hole96"], + ["add","W96","Y96","1"], + ["line","W96",96,1], + ["clear","W97","hole97"], + ["add","W97","Y97","1"], + ["line","W97",97,1], + ["clear","W98","hole98"], + ["add","W98","Y98","1"], + ["line","W98",98,1], + ["clear","W99","hole99"], + ["add","W99","Y99","1"], + ["line","W99",99,1], + ["clear","W100","hole100"], + ["add","W100","Y100","1"], + ["line","W100",100,1], + ["clear","W101","hole101"], + ["add","W101","Y101","1"], + ["line","W101",101,1], + ["clear","W102","hole102"], + ["add","W102","Y102","1"], + ["line","W102",102,1], + ["clear","W103","hole103"], + ["add","W103","Y103","1"], + ["line","W103",103,1], + ["clear","W104","hole104"], + ["add","W104","Y104","1"], + ["line","W104",104,1], + ["clear","W105","hole105"], + ["add","W105","Y105","1"], + ["line","W105",105,1], + ["clear","W106","hole106"], + ["add","W106","Y106","1"], + ["line","W106",106,1], + ["clear","W107","hole107"], + ["add","W107","Y107","1"], + ["line","W107",107,1], + ["clear","W108","hole108"], + ["add","W108","Y108","1"], + ["line","W108",108,1], + ["clear","W109","hole109"], + ["add","W109","Y109","1"], + ["line","W109",109,1], + ["clear","W110","hole110"], + ["add","W110","Y110","1"], + ["line","W110",110,1], + ["clear","W111","hole111"], + ["add","W111","Y111","1"], + ["line","W111",111,1], + ["map","W0",1,0,false], + ["map","W1",1,1,false], + ["map","W2",1,2,false], + ["map","W3",1,3,false], + ["map","W4",1,4,false], + ["map","W5",1,5,false], + ["map","W6",1,6,false], + ["map","W7",1,7,false], + ["map","W8",1,8,false], + ["map","W9",1,9,false], + ["map","W10",1,10,false], + ["map","W11",1,11,false], + ["map","W12",1,12,false], + ["map","W13",1,13,false], + ["map","W14",1,14,false], + ["map","W15",1,15,false], + ["map","W16",1,16,false], + ["map","W17",1,17,false], + ["map","W18",1,18,false], + ["map","W19",1,19,false], + ["map","W20",1,20,false], + ["map","W21",1,21,false], + ["map","W22",1,22,false], + ["map","W23",1,23,false], + ["map","W24",1,24,false], + ["map","W25",1,25,false], + ["map","W26",1,26,false], + ["map","W27",1,27,false], + ["map","W28",1,28,false], + ["map","W29",1,29,false], + ["map","W30",1,30,false], + ["map","W31",1,31,false], + ["map","W32",1,32,false], + ["map","W33",1,33,false], + ["map","W34",1,34,false], + ["map","W35",1,35,false], + ["map","W36",1,36,false], + ["map","W37",1,37,false], + ["map","W38",1,38,false], + ["map","W39",1,39,false], + ["map","W40",1,40,false], + ["map","W41",1,41,false], + ["map","W42",1,42,false], + ["map","W43",1,43,false], + ["map","W44",1,44,false], + ["map","W45",1,45,false], + ["map","W46",1,46,false], + ["map","W47",1,47,false], + ["map","W48",1,48,false], + ["map","W49",1,49,false], + ["map","W50",1,50,false], + ["map","W51",1,51,false], + ["map","W52",1,52,false], + ["map","W53",1,53,false], + ["map","W54",1,54,false], + ["map","W55",1,55,false], + ["map","W56",1,56,false], + ["map","W57",1,57,false], + ["map","W58",1,58,false], + ["map","W59",1,59,false], + ["map","W60",1,60,false], + ["map","W61",1,61,false], + ["map","W62",1,62,false], + ["map","W63",1,63,false], + ["map","W64",1,64,false], + ["map","W65",1,65,false], + ["map","W66",1,66,false], + ["map","W67",1,67,false], + ["map","W68",1,68,false], + ["map","W69",1,69,false], + ["map","W70",1,70,false], + ["map","W71",1,71,false], + ["map","W72",1,72,false], + ["map","W73",1,73,false], + ["map","W74",1,74,false], + ["map","W75",1,75,false], + ["map","W76",1,76,false], + ["map","W77",1,77,false], + ["map","W78",1,78,false], + ["map","W79",1,79,false], + ["map","W80",1,80,false], + ["map","W81",1,81,false], + ["map","W82",1,82,false], + ["map","W83",1,83,false], + ["map","W84",1,84,false], + ["map","W85",1,85,false], + ["map","W86",1,86,false], + ["map","W87",1,87,false], + ["map","W88",1,88,false], + ["map","W89",1,89,false], + ["map","W90",1,90,false], + ["map","W91",1,91,false], + ["map","W92",1,92,false], + ["map","W93",1,93,false], + ["map","W94",1,94,false], + ["map","W95",1,95,false], + ["map","W96",1,96,false], + ["map","W97",1,97,false], + ["map","W98",1,98,false], + ["map","W99",1,99,false], + ["map","W100",1,100,false], + ["map","W101",1,101,false], + ["map","W102",1,102,false], + ["map","W103",1,103,false], + ["map","W104",1,104,false], + ["map","W105",1,105,false], + ["map","W106",1,106,false], + ["map","W107",1,107,false], + ["map","W108",1,108,false], + ["map","W109",1,109,false], + ["map","W110",1,110,false], + ["map","W111",1,111,false], + ["begin","B1_current_query",8], + ["clear","F0","wide"], + ["add","F0","W0","1"], + ["add","F0","W2","1"], + ["add","F0","W7","1"], + ["add","F0","W9","1"], + ["add","F0","W10","1"], + ["add","F0","W11","1"], + ["add","F0","W12","1"], + ["add","F0","W17","1"], + ["add","F0","W18","1"], + ["add","F0","W19","1"], + ["add","F0","W22","1"], + ["add","F0","W23","1"], + ["add","F0","W24","1"], + ["add","F0","W25","1"], + ["add","F0","W27","1"], + ["add","F0","W31","1"], + ["add","F0","W32","1"], + ["add","F0","W33","1"], + ["add","F0","W34","1"], + ["add","F0","W35","1"], + ["add","F0","W38","1"], + ["add","F0","W39","1"], + ["add","F0","W40","1"], + ["add","F0","W45","1"], + ["add","F0","W48","1"], + ["add","F0","W49","1"], + ["add","F0","W50","1"], + ["add","F0","W54","1"], + ["add","F0","W55","1"], + ["add","F0","W56","1"], + ["add","F0","W57","1"], + ["add","F0","W61","1"], + ["add","F0","W62","1"], + ["add","F0","W63","1"], + ["add","F0","W70","1"], + ["add","F0","W71","1"], + ["add","F0","W72","1"], + ["add","F0","W76","1"], + ["add","F0","W77","1"], + ["add","F0","W79","1"], + ["add","F0","W81","1"], + ["add","F0","W85","1"], + ["add","F0","W87","1"], + ["add","F0","W89","1"], + ["add","F0","W90","1"], + ["add","F0","W91","1"], + ["add","F0","W92","1"], + ["add","F0","W94","1"], + ["add","F0","W98","1"], + ["add","F0","W100","1"], + ["add","F0","W101","1"], + ["add","F0","W102","1"], + ["add","F0","W103","1"], + ["add","F0","W107","1"], + ["add","F0","W108","1"], + ["add","F0","W109","1"], + ["clear","F1","wide"], + ["add","F1","W0","1"], + ["add","F1","W1","1"], + ["add","F1","W2","1"], + ["add","F1","W3","1"], + ["add","F1","W4","1"], + ["add","F1","W5","1"], + ["add","F1","W6","1"], + ["add","F1","W7","-1"], + ["add","F1","W8","1"], + ["add","F1","W9","-1"], + ["add","F1","W10","-1"], + ["add","F1","W11","-1"], + ["add","F1","W25","1"], + ["add","F1","W26","1"], + ["add","F1","W27","1"], + ["add","F1","W28","1"], + ["add","F1","W29","1"], + ["add","F1","W30","1"], + ["add","F1","W57","-1"], + ["add","F1","W58","1"], + ["add","F1","W59","1"], + ["add","F1","W60","1"], + ["add","F1","W61","-1"], + ["add","F1","W62","-1"], + ["add","F1","W63","-1"], + ["add","F1","W64","1"], + ["add","F1","W65","1"], + ["add","F1","W66","1"], + ["add","F1","W67","1"], + ["add","F1","W68","1"], + ["add","F1","W69","1"], + ["add","F1","W70","1"], + ["add","F1","W71","1"], + ["add","F1","W72","1"], + ["add","F1","W73","1"], + ["add","F1","W74","1"], + ["add","F1","W75","1"], + ["add","F1","W76","1"], + ["add","F1","W79","-1"], + ["add","F1","W80","1"], + ["add","F1","W81","-1"], + ["add","F1","W82","1"], + ["add","F1","W83","1"], + ["add","F1","W84","1"], + ["add","F1","W86","1"], + ["add","F1","W87","1"], + ["add","F1","W88","1"], + ["add","F1","W89","1"], + ["add","F1","W90","1"], + ["add","F1","W91","1"], + ["add","F1","W92","-1"], + ["add","F1","W93","1"], + ["add","F1","W94","-1"], + ["add","F1","W95","1"], + ["add","F1","W96","1"], + ["add","F1","W97","1"], + ["clear","F2","wide"], + ["add","F2","W0","1"], + ["add","F2","W1","1"], + ["add","F2","W6","1"], + ["add","F2","W7","-1"], + ["add","F2","W12","1"], + ["add","F2","W13","1"], + ["add","F2","W14","1"], + ["add","F2","W15","1"], + ["add","F2","W16","1"], + ["add","F2","W17","-1"], + ["add","F2","W18","-1"], + ["add","F2","W19","-1"], + ["add","F2","W27","-1"], + ["add","F2","W28","-1"], + ["add","F2","W29","-1"], + ["add","F2","W30","-1"], + ["add","F2","W31","1"], + ["add","F2","W38","-1"], + ["add","F2","W39","-1"], + ["add","F2","W40","-1"], + ["add","F2","W41","1"], + ["add","F2","W42","1"], + ["add","F2","W43","1"], + ["add","F2","W44","1"], + ["add","F2","W51","1"], + ["add","F2","W52","1"], + ["add","F2","W53","1"], + ["add","F2","W54","1"], + ["add","F2","W55","1"], + ["add","F2","W56","1"], + ["add","F2","W57","1"], + ["add","F2","W58","-1"], + ["add","F2","W59","-1"], + ["add","F2","W60","-1"], + ["add","F2","W73","1"], + ["add","F2","W74","1"], + ["add","F2","W75","1"], + ["add","F2","W76","1"], + ["add","F2","W77","-1"], + ["add","F2","W78","1"], + ["add","F2","W81","-1"], + ["add","F2","W82","1"], + ["add","F2","W83","1"], + ["add","F2","W84","1"], + ["add","F2","W86","-1"], + ["add","F2","W87","-1"], + ["add","F2","W92","1"], + ["add","F2","W93","-1"], + ["add","F2","W99","1"], + ["add","F2","W100","1"], + ["add","F2","W101","1"], + ["add","F2","W102","1"], + ["add","F2","W103","-1"], + ["add","F2","W104","1"], + ["add","F2","W105","1"], + ["add","F2","W106","1"], + ["clear","F3","wide"], + ["add","F3","W0","1"], + ["add","F3","W3","1"], + ["add","F3","W4","1"], + ["add","F3","W5","1"], + ["add","F3","W7","1"], + ["add","F3","W8","-1"], + ["add","F3","W13","1"], + ["add","F3","W14","1"], + ["add","F3","W15","1"], + ["add","F3","W16","-1"], + ["add","F3","W22","-1"], + ["add","F3","W23","-1"], + ["add","F3","W24","-1"], + ["add","F3","W26","-1"], + ["add","F3","W27","-1"], + ["add","F3","W32","1"], + ["add","F3","W33","1"], + ["add","F3","W34","1"], + ["add","F3","W35","-1"], + ["add","F3","W41","-1"], + ["add","F3","W42","-1"], + ["add","F3","W43","-1"], + ["add","F3","W44","-1"], + ["add","F3","W45","-1"], + ["add","F3","W48","1"], + ["add","F3","W49","1"], + ["add","F3","W50","1"], + ["add","F3","W51","1"], + ["add","F3","W52","1"], + ["add","F3","W53","1"], + ["add","F3","W57","-1"], + ["add","F3","W64","-1"], + ["add","F3","W65","-1"], + ["add","F3","W66","-1"], + ["add","F3","W67","1"], + ["add","F3","W68","1"], + ["add","F3","W69","1"], + ["add","F3","W76","-1"], + ["add","F3","W78","1"], + ["add","F3","W80","1"], + ["add","F3","W81","-1"], + ["add","F3","W85","1"], + ["add","F3","W87","1"], + ["add","F3","W88","1"], + ["add","F3","W92","1"], + ["add","F3","W95","-1"], + ["add","F3","W96","-1"], + ["add","F3","W97","-1"], + ["add","F3","W98","1"], + ["add","F3","W99","1"], + ["add","F3","W104","-1"], + ["add","F3","W105","-1"], + ["add","F3","W106","-1"], + ["add","F3","W107","-1"], + ["add","F3","W108","-1"], + ["add","F3","W109","-1"], + ["clear","F4","wide"], + ["add","F4","W1","-1"], + ["add","F4","W3","-1"], + ["add","F4","W6","1"], + ["add","F4","W8","1"], + ["add","F4","W10","-1"], + ["add","F4","W11","-1"], + ["add","F4","W12","1"], + ["add","F4","W14","1"], + ["add","F4","W15","1"], + ["add","F4","W17","1"], + ["add","F4","W20","1"], + ["add","F4","W21","1"], + ["add","F4","W24","-1"], + ["add","F4","W26","-1"], + ["add","F4","W28","-1"], + ["add","F4","W31","-1"], + ["add","F4","W32","-1"], + ["add","F4","W35","-1"], + ["add","F4","W36","1"], + ["add","F4","W37","1"], + ["add","F4","W38","-1"], + ["add","F4","W41","1"], + ["add","F4","W42","1"], + ["add","F4","W45","1"], + ["add","F4","W46","1"], + ["add","F4","W47","1"], + ["add","F4","W48","1"], + ["add","F4","W52","-1"], + ["add","F4","W53","-1"], + ["add","F4","W56","-1"], + ["add","F4","W58","1"], + ["add","F4","W62","1"], + ["add","F4","W63","1"], + ["add","F4","W66","-1"], + ["add","F4","W67","1"], + ["add","F4","W70","1"], + ["add","F4","W71","1"], + ["add","F4","W75","-1"], + ["add","F4","W77","-1"], + ["add","F4","W80","1"], + ["add","F4","W82","1"], + ["add","F4","W85","-1"], + ["add","F4","W86","-1"], + ["add","F4","W88","-1"], + ["add","F4","W90","-1"], + ["add","F4","W91","-1"], + ["add","F4","W93","1"], + ["add","F4","W95","1"], + ["add","F4","W98","1"], + ["add","F4","W100","1"], + ["add","F4","W103","1"], + ["add","F4","W105","-1"], + ["add","F4","W106","-1"], + ["add","F4","W107","1"], + ["add","F4","W110","1"], + ["add","F4","W111","1"], + ["clear","F5","wide"], + ["add","F5","W4","-1"], + ["add","F5","W5","1"], + ["add","F5","W10","1"], + ["add","F5","W11","-1"], + ["add","F5","W14","-1"], + ["add","F5","W15","1"], + ["add","F5","W18","1"], + ["add","F5","W19","-1"], + ["add","F5","W20","-1"], + ["add","F5","W21","1"], + ["add","F5","W22","1"], + ["add","F5","W23","-1"], + ["add","F5","W29","-1"], + ["add","F5","W30","1"], + ["add","F5","W33","-1"], + ["add","F5","W34","1"], + ["add","F5","W36","1"], + ["add","F5","W37","-1"], + ["add","F5","W39","-1"], + ["add","F5","W40","1"], + ["add","F5","W41","1"], + ["add","F5","W42","-1"], + ["add","F5","W46","-1"], + ["add","F5","W47","1"], + ["add","F5","W49","1"], + ["add","F5","W50","-1"], + ["add","F5","W52","1"], + ["add","F5","W53","-1"], + ["add","F5","W54","1"], + ["add","F5","W55","-1"], + ["add","F5","W59","1"], + ["add","F5","W60","-1"], + ["add","F5","W62","-1"], + ["add","F5","W63","1"], + ["add","F5","W64","1"], + ["add","F5","W65","-1"], + ["add","F5","W68","1"], + ["add","F5","W69","-1"], + ["add","F5","W70","1"], + ["add","F5","W71","-1"], + ["add","F5","W73","1"], + ["add","F5","W74","-1"], + ["add","F5","W83","1"], + ["add","F5","W84","-1"], + ["add","F5","W90","1"], + ["add","F5","W91","-1"], + ["add","F5","W96","1"], + ["add","F5","W97","-1"], + ["add","F5","W101","1"], + ["add","F5","W102","-1"], + ["add","F5","W105","1"], + ["add","F5","W106","-1"], + ["add","F5","W108","1"], + ["add","F5","W109","-1"], + ["add","F5","W110","-1"], + ["add","F5","W111","1"], + ["clear","F6","wide"], + ["add","F6","W2","1"], + ["add","F6","W3","1"], + ["add","F6","W8","1"], + ["add","F6","W9","-1"], + ["add","F6","W12","1"], + ["add","F6","W13","1"], + ["add","F6","W16","1"], + ["add","F6","W17","-1"], + ["add","F6","W20","1"], + ["add","F6","W21","1"], + ["add","F6","W22","-1"], + ["add","F6","W23","-1"], + ["add","F6","W25","-1"], + ["add","F6","W26","-1"], + ["add","F6","W29","-1"], + ["add","F6","W30","-1"], + ["add","F6","W31","-1"], + ["add","F6","W33","-1"], + ["add","F6","W34","-1"], + ["add","F6","W36","1"], + ["add","F6","W37","1"], + ["add","F6","W38","1"], + ["add","F6","W43","1"], + ["add","F6","W44","-1"], + ["add","F6","W46","-1"], + ["add","F6","W47","-1"], + ["add","F6","W49","1"], + ["add","F6","W50","1"], + ["add","F6","W51","-1"], + ["add","F6","W56","1"], + ["add","F6","W59","1"], + ["add","F6","W60","1"], + ["add","F6","W61","1"], + ["add","F6","W66","1"], + ["add","F6","W67","-1"], + ["add","F6","W72","1"], + ["add","F6","W73","-1"], + ["add","F6","W74","-1"], + ["add","F6","W77","-1"], + ["add","F6","W78","1"], + ["add","F6","W79","-1"], + ["add","F6","W80","1"], + ["add","F6","W83","1"], + ["add","F6","W84","1"], + ["add","F6","W88","-1"], + ["add","F6","W89","-1"], + ["add","F6","W94","1"], + ["add","F6","W95","-1"], + ["add","F6","W99","-1"], + ["add","F6","W100","-1"], + ["add","F6","W103","1"], + ["add","F6","W104","-1"], + ["add","F6","W108","1"], + ["add","F6","W109","1"], + ["add","F6","W110","-1"], + ["add","F6","W111","-1"], + ["clear","F7","wide"], + ["add","F7","W1","-1"], + ["add","F7","W2","-1"], + ["add","F7","W4","-1"], + ["add","F7","W5","-1"], + ["add","F7","W6","1"], + ["add","F7","W9","-1"], + ["add","F7","W13","1"], + ["add","F7","W16","-1"], + ["add","F7","W18","1"], + ["add","F7","W19","1"], + ["add","F7","W20","-1"], + ["add","F7","W21","-1"], + ["add","F7","W24","1"], + ["add","F7","W25","1"], + ["add","F7","W28","1"], + ["add","F7","W32","1"], + ["add","F7","W35","-1"], + ["add","F7","W36","1"], + ["add","F7","W37","1"], + ["add","F7","W39","-1"], + ["add","F7","W40","-1"], + ["add","F7","W43","1"], + ["add","F7","W44","1"], + ["add","F7","W45","1"], + ["add","F7","W46","1"], + ["add","F7","W47","1"], + ["add","F7","W48","-1"], + ["add","F7","W51","-1"], + ["add","F7","W54","-1"], + ["add","F7","W55","-1"], + ["add","F7","W58","-1"], + ["add","F7","W61","1"], + ["add","F7","W64","-1"], + ["add","F7","W65","-1"], + ["add","F7","W68","1"], + ["add","F7","W69","1"], + ["add","F7","W72","1"], + ["add","F7","W75","1"], + ["add","F7","W78","-1"], + ["add","F7","W79","1"], + ["add","F7","W82","-1"], + ["add","F7","W85","-1"], + ["add","F7","W86","-1"], + ["add","F7","W89","-1"], + ["add","F7","W93","1"], + ["add","F7","W94","-1"], + ["add","F7","W96","1"], + ["add","F7","W97","1"], + ["add","F7","W98","1"], + ["add","F7","W99","1"], + ["add","F7","W101","1"], + ["add","F7","W102","1"], + ["add","F7","W104","-1"], + ["add","F7","W107","-1"], + ["add","F7","W110","-1"], + ["add","F7","W111","-1"], + ["add","W1","F1","-1/4"], + ["add","W1","F2","-1/4"], + ["add","W1","F4","1/4"], + ["add","W1","F7","1/4"], + ["add","W2","F0","-1/4"], + ["add","W2","F1","-1/4"], + ["add","W2","F6","-1/4"], + ["add","W2","F7","1/4"], + ["add","W3","F1","-1/4"], + ["add","W3","F3","-1/4"], + ["add","W3","F4","1/4"], + ["add","W3","F6","-1/4"], + ["add","W4","F1","-1/4"], + ["add","W4","F3","-1/4"], + ["add","W4","F5","1/4"], + ["add","W4","F7","1/4"], + ["add","W5","F1","-1/4"], + ["add","W5","F3","-1/4"], + ["add","W5","F5","-1/4"], + ["add","W5","F7","1/4"], + ["add","W6","F1","-1/4"], + ["add","W6","F2","-1/4"], + ["add","W6","F4","-1/4"], + ["add","W6","F7","-1/4"], + ["add","W8","F1","-1/4"], + ["add","W8","F3","1/4"], + ["add","W8","F4","-1/4"], + ["add","W8","F6","-1/4"], + ["add","W9","F0","-1/4"], + ["add","W9","F1","1/4"], + ["add","W9","F6","1/4"], + ["add","W9","F7","1/4"], + ["add","W10","F0","-1/4"], + ["add","W10","F1","1/4"], + ["add","W10","F4","1/4"], + ["add","W10","F5","-1/4"], + ["add","W11","F0","-1/4"], + ["add","W11","F1","1/4"], + ["add","W11","F4","1/4"], + ["add","W11","F5","1/4"], + ["add","W12","F0","-1/4"], + ["add","W12","F2","-1/4"], + ["add","W12","F4","-1/4"], + ["add","W12","F6","-1/4"], + ["add","W13","F2","-1/4"], + ["add","W13","F3","-1/4"], + ["add","W13","F6","-1/4"], + ["add","W13","F7","-1/4"], + ["add","W14","F2","-1/4"], + ["add","W14","F3","-1/4"], + ["add","W14","F4","-1/4"], + ["add","W14","F5","1/4"], + ["add","W15","F2","-1/4"], + ["add","W15","F3","-1/4"], + ["add","W15","F4","-1/4"], + ["add","W15","F5","-1/4"], + ["add","W16","F2","-1/4"], + ["add","W16","F3","1/4"], + ["add","W16","F6","-1/4"], + ["add","W16","F7","1/4"], + ["add","W17","F0","-1/4"], + ["add","W17","F2","1/4"], + ["add","W17","F4","-1/4"], + ["add","W17","F6","1/4"], + ["add","W18","F0","-1/4"], + ["add","W18","F2","1/4"], + ["add","W18","F5","-1/4"], + ["add","W18","F7","-1/4"], + ["add","W19","F0","-1/4"], + ["add","W19","F2","1/4"], + ["add","W19","F5","1/4"], + ["add","W19","F7","-1/4"], + ["add","W22","F0","-1/4"], + ["add","W22","F3","1/4"], + ["add","W22","F5","-1/4"], + ["add","W22","F6","1/4"], + ["add","W23","F0","-1/4"], + ["add","W23","F3","1/4"], + ["add","W23","F5","1/4"], + ["add","W23","F6","1/4"], + ["add","W24","F0","-1/4"], + ["add","W24","F3","1/4"], + ["add","W24","F4","1/4"], + ["add","W24","F7","-1/4"], + ["add","W25","F0","-1/4"], + ["add","W25","F1","-1/4"], + ["add","W25","F6","1/4"], + ["add","W25","F7","-1/4"], + ["add","W26","F1","-1/4"], + ["add","W26","F3","1/4"], + ["add","W26","F4","1/4"], + ["add","W26","F6","1/4"], + ["add","W28","F1","-1/4"], + ["add","W28","F2","1/4"], + ["add","W28","F4","1/4"], + ["add","W28","F7","-1/4"], + ["add","W29","F1","-1/4"], + ["add","W29","F2","1/4"], + ["add","W29","F5","1/4"], + ["add","W29","F6","1/4"], + ["add","W30","F1","-1/4"], + ["add","W30","F2","1/4"], + ["add","W30","F5","-1/4"], + ["add","W30","F6","1/4"], + ["add","W31","F0","-1/4"], + ["add","W31","F2","-1/4"], + ["add","W31","F4","1/4"], + ["add","W31","F6","1/4"], + ["add","W32","F0","-1/4"], + ["add","W32","F3","-1/4"], + ["add","W32","F4","1/4"], + ["add","W32","F7","-1/4"], + ["add","W33","F0","-1/4"], + ["add","W33","F3","-1/4"], + ["add","W33","F5","1/4"], + ["add","W33","F6","1/4"], + ["add","W34","F0","-1/4"], + ["add","W34","F3","-1/4"], + ["add","W34","F5","-1/4"], + ["add","W34","F6","1/4"], + ["add","W35","F0","-1/4"], + ["add","W35","F3","1/4"], + ["add","W35","F4","1/4"], + ["add","W35","F7","1/4"], + ["add","W38","F0","-1/4"], + ["add","W38","F2","1/4"], + ["add","W38","F4","1/4"], + ["add","W38","F6","-1/4"], + ["add","W39","F0","-1/4"], + ["add","W39","F2","1/4"], + ["add","W39","F5","1/4"], + ["add","W39","F7","1/4"], + ["add","W40","F0","-1/4"], + ["add","W40","F2","1/4"], + ["add","W40","F5","-1/4"], + ["add","W40","F7","1/4"], + ["add","W41","F2","-1/4"], + ["add","W41","F3","1/4"], + ["add","W41","F4","-1/4"], + ["add","W41","F5","-1/4"], + ["add","W42","F2","-1/4"], + ["add","W42","F3","1/4"], + ["add","W42","F4","-1/4"], + ["add","W42","F5","1/4"], + ["add","W43","F2","-1/4"], + ["add","W43","F3","1/4"], + ["add","W43","F6","-1/4"], + ["add","W43","F7","-1/4"], + ["add","W44","F2","-1/4"], + ["add","W44","F3","1/4"], + ["add","W44","F6","1/4"], + ["add","W44","F7","-1/4"], + ["add","W45","F0","-1/4"], + ["add","W45","F3","1/4"], + ["add","W45","F4","-1/4"], + ["add","W45","F7","-1/4"], + ["add","W48","F0","-1/4"], + ["add","W48","F3","-1/4"], + ["add","W48","F4","-1/4"], + ["add","W48","F7","1/4"], + ["add","W49","F0","-1/4"], + ["add","W49","F3","-1/4"], + ["add","W49","F5","-1/4"], + ["add","W49","F6","-1/4"], + ["add","W50","F0","-1/4"], + ["add","W50","F3","-1/4"], + ["add","W50","F5","1/4"], + ["add","W50","F6","-1/4"], + ["add","W51","F2","-1/4"], + ["add","W51","F3","-1/4"], + ["add","W51","F6","1/4"], + ["add","W51","F7","1/4"], + ["add","W52","F2","-1/4"], + ["add","W52","F3","-1/4"], + ["add","W52","F4","1/4"], + ["add","W52","F5","-1/4"], + ["add","W53","F2","-1/4"], + ["add","W53","F3","-1/4"], + ["add","W53","F4","1/4"], + ["add","W53","F5","1/4"], + ["add","W54","F0","-1/4"], + ["add","W54","F2","-1/4"], + ["add","W54","F5","-1/4"], + ["add","W54","F7","1/4"], + ["add","W55","F0","-1/4"], + ["add","W55","F2","-1/4"], + ["add","W55","F5","1/4"], + ["add","W55","F7","1/4"], + ["add","W56","F0","-1/4"], + ["add","W56","F2","-1/4"], + ["add","W56","F4","1/4"], + ["add","W56","F6","-1/4"], + ["add","W58","F1","-1/4"], + ["add","W58","F2","1/4"], + ["add","W58","F4","-1/4"], + ["add","W58","F7","1/4"], + ["add","W59","F1","-1/4"], + ["add","W59","F2","1/4"], + ["add","W59","F5","-1/4"], + ["add","W59","F6","-1/4"], + ["add","W60","F1","-1/4"], + ["add","W60","F2","1/4"], + ["add","W60","F5","1/4"], + ["add","W60","F6","-1/4"], + ["add","W61","F0","-1/4"], + ["add","W61","F1","1/4"], + ["add","W61","F6","-1/4"], + ["add","W61","F7","-1/4"], + ["add","W62","F0","-1/4"], + ["add","W62","F1","1/4"], + ["add","W62","F4","-1/4"], + ["add","W62","F5","1/4"], + ["add","W63","F0","-1/4"], + ["add","W63","F1","1/4"], + ["add","W63","F4","-1/4"], + ["add","W63","F5","-1/4"], + ["add","W64","F1","-1/4"], + ["add","W64","F3","1/4"], + ["add","W64","F5","-1/4"], + ["add","W64","F7","1/4"], + ["add","W65","F1","-1/4"], + ["add","W65","F3","1/4"], + ["add","W65","F5","1/4"], + ["add","W65","F7","1/4"], + ["add","W66","F1","-1/4"], + ["add","W66","F3","1/4"], + ["add","W66","F4","1/4"], + ["add","W66","F6","-1/4"], + ["add","W67","F1","-1/4"], + ["add","W67","F3","-1/4"], + ["add","W67","F4","-1/4"], + ["add","W67","F6","1/4"], + ["add","W68","F1","-1/4"], + ["add","W68","F3","-1/4"], + ["add","W68","F5","-1/4"], + ["add","W68","F7","-1/4"], + ["add","W69","F1","-1/4"], + ["add","W69","F3","-1/4"], + ["add","W69","F5","1/4"], + ["add","W69","F7","-1/4"], + ["add","W70","F0","-1/4"], + ["add","W70","F1","-1/4"], + ["add","W70","F4","-1/4"], + ["add","W70","F5","-1/4"], + ["add","W71","F0","-1/4"], + ["add","W71","F1","-1/4"], + ["add","W71","F4","-1/4"], + ["add","W71","F5","1/4"], + ["add","W72","F0","-1/4"], + ["add","W72","F1","-1/4"], + ["add","W72","F6","-1/4"], + ["add","W72","F7","-1/4"], + ["add","W73","F1","-1/4"], + ["add","W73","F2","-1/4"], + ["add","W73","F5","-1/4"], + ["add","W73","F6","1/4"], + ["add","W74","F1","-1/4"], + ["add","W74","F2","-1/4"], + ["add","W74","F5","1/4"], + ["add","W74","F6","1/4"], + ["add","W75","F1","-1/4"], + ["add","W75","F2","-1/4"], + ["add","W75","F4","1/4"], + ["add","W75","F7","-1/4"], + ["add","W77","F0","-1/4"], + ["add","W77","F2","1/4"], + ["add","W77","F4","1/4"], + ["add","W77","F6","1/4"], + ["add","W78","F2","-1/4"], + ["add","W78","F3","-1/4"], + ["add","W78","F6","-1/4"], + ["add","W78","F7","1/4"], + ["add","W79","F0","-1/4"], + ["add","W79","F1","1/4"], + ["add","W79","F6","1/4"], + ["add","W79","F7","-1/4"], + ["add","W80","F1","-1/4"], + ["add","W80","F3","-1/4"], + ["add","W80","F4","-1/4"], + ["add","W80","F6","-1/4"], + ["add","W82","F1","-1/4"], + ["add","W82","F2","-1/4"], + ["add","W82","F4","-1/4"], + ["add","W82","F7","1/4"], + ["add","W83","F1","-1/4"], + ["add","W83","F2","-1/4"], + ["add","W83","F5","-1/4"], + ["add","W83","F6","-1/4"], + ["add","W84","F1","-1/4"], + ["add","W84","F2","-1/4"], + ["add","W84","F5","1/4"], + ["add","W84","F6","-1/4"], + ["add","W85","F0","-1/4"], + ["add","W85","F3","-1/4"], + ["add","W85","F4","1/4"], + ["add","W85","F7","1/4"], + ["add","W86","F1","-1/4"], + ["add","W86","F2","1/4"], + ["add","W86","F4","1/4"], + ["add","W86","F7","1/4"], + ["add","W88","F1","-1/4"], + ["add","W88","F3","-1/4"], + ["add","W88","F4","1/4"], + ["add","W88","F6","1/4"], + ["add","W89","F0","-1/4"], + ["add","W89","F1","-1/4"], + ["add","W89","F6","1/4"], + ["add","W89","F7","1/4"], + ["add","W90","F0","-1/4"], + ["add","W90","F1","-1/4"], + ["add","W90","F4","1/4"], + ["add","W90","F5","-1/4"], + ["add","W91","F0","-1/4"], + ["add","W91","F1","-1/4"], + ["add","W91","F4","1/4"], + ["add","W91","F5","1/4"], + ["add","W93","F1","-1/4"], + ["add","W93","F2","1/4"], + ["add","W93","F4","-1/4"], + ["add","W93","F7","-1/4"], + ["add","W94","F0","-1/4"], + ["add","W94","F1","1/4"], + ["add","W94","F6","-1/4"], + ["add","W94","F7","1/4"], + ["add","W95","F1","-1/4"], + ["add","W95","F3","1/4"], + ["add","W95","F4","-1/4"], + ["add","W95","F6","1/4"], + ["add","W96","F1","-1/4"], + ["add","W96","F3","1/4"], + ["add","W96","F5","-1/4"], + ["add","W96","F7","-1/4"], + ["add","W97","F1","-1/4"], + ["add","W97","F3","1/4"], + ["add","W97","F5","1/4"], + ["add","W97","F7","-1/4"], + ["add","W98","F0","-1/4"], + ["add","W98","F3","-1/4"], + ["add","W98","F4","-1/4"], + ["add","W98","F7","-1/4"], + ["add","W99","F2","-1/4"], + ["add","W99","F3","-1/4"], + ["add","W99","F6","1/4"], + ["add","W99","F7","-1/4"], + ["add","W100","F0","-1/4"], + ["add","W100","F2","-1/4"], + ["add","W100","F4","-1/4"], + ["add","W100","F6","1/4"], + ["add","W101","F0","-1/4"], + ["add","W101","F2","-1/4"], + ["add","W101","F5","-1/4"], + ["add","W101","F7","-1/4"], + ["add","W102","F0","-1/4"], + ["add","W102","F2","-1/4"], + ["add","W102","F5","1/4"], + ["add","W102","F7","-1/4"], + ["add","W103","F0","-1/4"], + ["add","W103","F2","1/4"], + ["add","W103","F4","-1/4"], + ["add","W103","F6","-1/4"], + ["add","W104","F2","-1/4"], + ["add","W104","F3","1/4"], + ["add","W104","F6","1/4"], + ["add","W104","F7","1/4"], + ["add","W105","F2","-1/4"], + ["add","W105","F3","1/4"], + ["add","W105","F4","1/4"], + ["add","W105","F5","-1/4"], + ["add","W106","F2","-1/4"], + ["add","W106","F3","1/4"], + ["add","W106","F4","1/4"], + ["add","W106","F5","1/4"], + ["add","W107","F0","-1/4"], + ["add","W107","F3","1/4"], + ["add","W107","F4","-1/4"], + ["add","W107","F7","1/4"], + ["add","W108","F0","-1/4"], + ["add","W108","F3","1/4"], + ["add","W108","F5","-1/4"], + ["add","W108","F6","-1/4"], + ["add","W109","F0","-1/4"], + ["add","W109","F3","1/4"], + ["add","W109","F5","1/4"], + ["add","W109","F6","-1/4"], + ["clear","F0","identity"], + ["clear","F1","identity"], + ["clear","F2","identity"], + ["clear","F3","identity"], + ["clear","F4","identity"], + ["clear","F5","identity"], + ["clear","F6","identity"], + ["clear","F7","identity"], + ["end","B1_current_query",8], + ["map","W1",1,1,true], + ["map","W2",1,2,true], + ["map","W3",1,3,true], + ["map","W4",1,4,true], + ["map","W5",1,5,true], + ["map","W6",1,6,true], + ["map","W8",1,8,true], + ["map","W9",1,9,true], + ["map","W10",1,10,true], + ["map","W11",1,11,true], + ["map","W12",1,12,true], + ["map","W13",1,13,true], + ["map","W14",1,14,true], + ["map","W15",1,15,true], + ["map","W16",1,16,true], + ["map","W17",1,17,true], + ["map","W18",1,18,true], + ["map","W19",1,19,true], + ["map","W22",1,22,true], + ["map","W23",1,23,true], + ["map","W24",1,24,true], + ["map","W25",1,25,true], + ["map","W26",1,26,true], + ["map","W28",1,28,true], + ["map","W29",1,29,true], + ["map","W30",1,30,true], + ["map","W31",1,31,true], + ["map","W32",1,32,true], + ["map","W33",1,33,true], + ["map","W34",1,34,true], + ["map","W35",1,35,true], + ["map","W38",1,38,true], + ["map","W39",1,39,true], + ["map","W40",1,40,true], + ["map","W41",1,41,true], + ["map","W42",1,42,true], + ["map","W43",1,43,true], + ["map","W44",1,44,true], + ["map","W45",1,45,true], + ["map","W48",1,48,true], + ["map","W49",1,49,true], + ["map","W50",1,50,true], + ["map","W51",1,51,true], + ["map","W52",1,52,true], + ["map","W53",1,53,true], + ["map","W54",1,54,true], + ["map","W55",1,55,true], + ["map","W56",1,56,true], + ["map","W58",1,58,true], + ["map","W59",1,59,true], + ["map","W60",1,60,true], + ["map","W61",1,61,true], + ["map","W62",1,62,true], + ["map","W63",1,63,true], + ["map","W64",1,64,true], + ["map","W65",1,65,true], + ["map","W66",1,66,true], + ["map","W67",1,67,true], + ["map","W68",1,68,true], + ["map","W69",1,69,true], + ["map","W70",1,70,true], + ["map","W71",1,71,true], + ["map","W72",1,72,true], + ["map","W73",1,73,true], + ["map","W74",1,74,true], + ["map","W75",1,75,true], + ["map","W77",1,77,true], + ["map","W78",1,78,true], + ["map","W79",1,79,true], + ["map","W80",1,80,true], + ["map","W82",1,82,true], + ["map","W83",1,83,true], + ["map","W84",1,84,true], + ["map","W85",1,85,true], + ["map","W86",1,86,true], + ["map","W88",1,88,true], + ["map","W89",1,89,true], + ["map","W90",1,90,true], + ["map","W91",1,91,true], + ["map","W93",1,93,true], + ["map","W94",1,94,true], + ["map","W95",1,95,true], + ["map","W96",1,96,true], + ["map","W97",1,97,true], + ["map","W98",1,98,true], + ["map","W99",1,99,true], + ["map","W100",1,100,true], + ["map","W101",1,101,true], + ["map","W102",1,102,true], + ["map","W103",1,103,true], + ["map","W104",1,104,true], + ["map","W105",1,105,true], + ["map","W106",1,106,true], + ["map","W107",1,107,true], + ["map","W108",1,108,true], + ["map","W109",1,109,true], + ["clear","W0","identity"], + ["clear","W7","identity"], + ["clear","W20","identity"], + ["clear","W27","identity"], + ["clear","W36","identity"], + ["clear","W46","identity"], + ["clear","W57","identity"], + ["clear","W111","identity"], + ["clear","W21","identity"], + ["clear","W37","identity"], + ["clear","W47","identity"], + ["clear","W76","identity"], + ["clear","W81","identity"], + ["clear","W87","identity"], + ["clear","W92","identity"], + ["clear","W110","identity"] +] diff --git a/research/qq16-f17-demand-projection/budget.py b/research/qq16-f17-demand-projection/budget.py new file mode 100644 index 0000000000..156ee76b2f --- /dev/null +++ b/research/qq16-f17-demand-projection/budget.py @@ -0,0 +1,136 @@ +#!/usr/bin/env python3 +"""Rational arithmetic reused from Clear1nsight PR3946, head 8dec5c663ace6285aeee49ec3f8eeae9a8bc9a58. + +Chris R / Clear1nsight, with substantial OpenAI assistance. Apache-2.0. +No predecessor executable is imported. See PROOF.md for the interval argument. +""" +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache + +M, W, R = 73, Q(896, 9), 51 +GRID = 1 << 80 + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def outward(lo, hi): + return Q((lo.numerator * GRID) // lo.denominator, GRID), Q(-((-hi.numerator * GRID) // hi.denominator), GRID) + + +@lru_cache(None) +def integral_log(y, panels=1024): + """Midpoint lower / trapezoid upper for integral_1^y 1/t dt.""" + y = Q(y) + need(1 <= y <= 2 and type(panels) is int and panels > 0, 'quadrature domain') + if y == 1: + return Q(0), Q(0) + h = (y - 1) / panels + lo = h * sum(1 / (1 + (Q(j) + Q(1, 2)) * h) for j in range(panels)) + hi = h * ((1 + 1 / y) / 2 + sum(1 / (1 + j * h) for j in range(1, panels))) + return outward(lo, hi) + + +@lru_cache(None) +def logarithm(x): + x = Q(x) + need(x >= 1, 'logarithm domain') + powers = 0 + while x > 2: + x /= 2 + powers += 1 + lo, hi = integral_log(x) + two_lo, two_hi = integral_log(Q(2)) + return outward(lo + powers * two_lo, hi + powers * two_hi) + + +def exponential(lo, hi, degree=6): + need(0 <= lo <= hi <= Q(1, 2), 'exponential domain') + need(type(degree) is int and degree >= 1, 'exponential degree') + lsum = usum = lterm = uterm = Q(1) + for j in range(1, degree + 1): + lterm *= lo / j + uterm *= hi / j + lsum += lterm + usum += uterm + first = uterm * hi / (degree + 1) + tail = first / (1 - hi / (degree + 2)) + return outward(lsum, usum + tail) + + +@lru_cache(None) +def cost(rank, a): + need(type(rank) is int and 0 < rank < M and a >= 0, 'child domain') + lo, hi = logarithm(Q(M, rank)) + lo, hi = exponential(a * lo, a * hi) + return outward(Q(rank, M) * lo, Q(rank, M) * hi) + +def expand(packet, name): + events = [] + + def visit(sequence): + for event in sequence: + tag = event[0] + if tag == 'retained_core': + need(event[1] in ('forward', 'backward'), 'core orientation') + visit(packet['core_words'][event[1]]) + elif tag in ('private_sweep', 'cover_sweep'): + visit(event[2]) + else: + need(tag in ('scalar', 'climb', 'adapter', 'residual_adapter', + 'phase', 'native_line', 'cover_map'), 'unknown event') + events.append(event) + + visit(packet['programs'][name]) + return events + + +def profile(packet, events): + out = Counter() + for event in events: + if event[0] == 'climb': + rank = event[5] + elif event[0] == 'native_line': + record = packet['native_line_recipes'][event[2]] + rank = record['rank'] + need(record['recipe']['rank'] == rank, 'wrapper recipe rank') + else: + continue + need(type(rank) is int and 0 < rank < M, 'literal child rank') + out[rank] += 1 + return dict(sorted(out.items())) + + +def moment(base, decoder_pair, centre, rank8, a, idle_rank=R): + need(all(type(r) is int and 0 < r < M and Q(n) >= 0 for r,n in base.items()), 'local profile domain') + need(2 * idle_rank**2 < M**2 and idle_rank >= max(base), 'halving / relaxation rank') + need(Q(decoder_pair) >= 0 and Q(centre) >= 0, 'negative budget charge') + local = {r: Q(n) for r, n in base.items()} + local[1] += Q(decoder_pair, 2) + if rank8: + local[8] = Q(8) + total = (M - 1) * W + centre + paid = sum(r * n for r, n in local.items()) + idle = total - paid + need(idle >= 0, 'negative idle mass') + lo = hi = Q(0) + for rank, number in local.items(): + clo, chi = cost(rank, a) + lo += number * clo + hi += number * chi + clo, chi = cost(idle_rank, a) + return outward((lo + idle / idle_rank * clo) / W, + (hi + idle / idle_rank * chi) / W) + + +def decimal_interval(pair, digits=12): + scale = 10**digits + lo, hi = pair + l = lo.numerator * scale // lo.denominator + u = -((-hi.numerator * scale) // hi.denominator) + return {'lower': str(Q(l, scale)), 'upper': str(Q(u, scale)), + 'decimal_lower': f'{l // scale}.{l % scale:0{digits}d}', + 'decimal_upper': f'{u // scale}.{u % scale:0{digits}d}'} diff --git a/research/qq16-f17-demand-projection/replay.py b/research/qq16-f17-demand-projection/replay.py new file mode 100644 index 0000000000..64c88d797d --- /dev/null +++ b/research/qq16-f17-demand-projection/replay.py @@ -0,0 +1,63 @@ +"""Demand-only replay adapted from ywz65 PR2707, using Arham Tahir PR2681 primitives. +Modified ownership/output/cleanup contract: Chris R / Clear1nsight with OpenAI. +Apache-2.0. See PREDECESSORS.json for exact retained source and modifications. +""" +from collections import Counter +from fractions import Fraction as Q +def replay(P, w, routes, labels, x2, y2, expected): + owned = {'W' + str(p) for p in range(112)} + rows = {name: {(name, P.AXES): Q(1)} for name in owned}; frames = {name: () for name in owned} + for side, bank in (('Y', y2),): + for p in range(112): + name = side + str(p); rows[name] = bank[p] + frames[name] = P.F17 + (((labels[p], -1),) if side == 'Y' else ()) + borrowed = {n: dict(r) for n, r in rows.items() if n[0] in ('X', 'Y')} + borrowed_frames = {n: frames[n] for n in borrowed} + active = set(); counts = Counter() + for index, e in enumerate(w): + op = e[0]; counts[op] += 1 + if op == 'begin': + P.need(not active, 'overlapping private sweeps') + active = {'F' + str(k) for k in range(8)} + P.need(e[2] == len(active), 'private scratch count') + for name in active: rows[name], frames[name] = {(name, P.AXES): Q(1)}, () + elif op == 'end': + P.need(len(active) == e[2], 'private boundary') + P.need(all(not rows[n] and P.phase(frames[n]) == P.phase(()) for n in active), 'scratch leak') + for name in active: del rows[name], frames[name] + active = set() + elif op == 'clear': + _, name, f = e; P.need(name in owned | active, 'clear borrowed input'); rows[name] = {} + frames[name] = {'wide': P.F17, 'current': P.F17, 'identity': ()}.get(f) + if f.startswith('hole'): frames[name] = P.F17 + ((labels[int(f[4:])], -1),) + P.need(frames[name] is not None, 'unknown clear frame') + elif op == 'add': + _, dst, src, q = e + P.need(dst in owned | active and dst != src, 'ADD ownership/alias') + P.need(dst in rows and src in rows, 'nonlive ADD role') + P.need(P.phase(frames[dst]) == P.phase(frames[src]), 'ADD frame mismatch ' + str(index)) + q = Q(q); P.need(abs(q) in (1, Q(1, 4)), 'unpriced coefficient') + rows[dst] = P.add(rows[dst], rows[src], q) + counts['unit_ADD' if abs(q) == 1 else 'quarter_ADD'] += 1 + elif op == 'line': + _, name, p, sign = e + P.need(not active and name in owned and sign in (-1, 1), 'line boundary') + frames[name] += ((labels[p], sign),) + elif op == 'map': + _, name, stage, p, inverse = e[:5] + P.need(not active and name in owned and stage == 1, 'map inside private sweep') + g = routes[stage][p]; b = P.alignment(g, P.F17) + if inverse: b = P.act(g, b) + if len(e) > 5 and e[5] == 'omit_shift': b = 0 + frames[name] = P.move(frames[name], g, b); rows[name] = P.routed(g, rows[name]) + else: raise ValueError('unknown event') + P.need(not active, 'unterminated private sweep') + for p in P.U: + name = 'W' + str(p) + P.need(rows[name] == expected[p], 'wrong demanded output ' + name) + P.need(P.phase(frames[name]) == P.phase(P.F17), 'wrong demanded output frame') + for p in P.V: + name = 'W' + str(p) + P.need(not rows[name] and P.phase(frames[name]) == P.phase(()), 'temporary leak') + P.need(all(rows[n] == r and frames[n] == borrowed_frames[n] for n, r in borrowed.items()), 'borrowed restoration') + return counts diff --git a/research/qq16-f17-demand-projection/test_verify.py b/research/qq16-f17-demand-projection/test_verify.py new file mode 100644 index 0000000000..790ea42974 --- /dev/null +++ b/research/qq16-f17-demand-projection/test_verify.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +"""Boundary checks for the changed consumer. Chris R / Clear1nsight, OpenAI; Apache-2.0.""" +import hashlib +import importlib.util +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + + +def imported(): + spec=importlib.util.spec_from_file_location('demand_verify',HERE/'verify.py') + v=importlib.util.module_from_spec(spec);spec.loader.exec_module(v) + return v + + +def inventory(root): + return {p.relative_to(root).as_posix():hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob('*') if p.is_file()} + + +class Boundaries(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.v=imported();cls.actual=cls.v.calculate() + + def export(self): + temp=tempfile.TemporaryDirectory();self.addCleanup(temp.cleanup) + root=Path(temp.name);pkg=root/'research'/HERE.name + shutil.copytree(HERE,pkg,ignore=shutil.ignore_patterns('__pycache__')) + for pin in json.loads((HERE/'SOURCES.json').read_bytes())['files']: + if pin['usage']=='input': + target=root/pin['path'];target.parent.mkdir(parents=True,exist_ok=True) + shutil.copy2(ROOT/pin['path'],target) + return root,pkg + + def run_export(self,pkg): + return subprocess.run([sys.executable,'-I','-O','-Werror','-B',str(pkg/'verify.py')], + text=True,capture_output=True,timeout=180) + + def test_complete_source_word_and_receipt(self): + self.assertEqual(self.v.canonical(self.actual),self.v.canonical(self.v.decode((HERE/'RESULT.json').read_bytes()))) + P,_,_,_,source=self.v.load(self.v.authenticate()) + self.assertEqual(self.v.projection(P,source),self.v.decode((HERE/'WORD.json').read_bytes())) + self.assertEqual(len(self.actual['controls']),9) + + def test_budget_conclusion_changes_with_rank8_premise(self): + b=self.actual['budget'] + from fractions import Fraction as Q + self.assertGreater(Q(b['centre64_retaining_eight_rank8']['lower']),1) + self.assertLess(Q(b['centre64_waiving_eight_rank8']['upper']),1) + self.assertEqual(b['pair_call_reduction_still_required_with_rank8_retained'],51) + + def test_git_free_read_only_export(self): + root,pkg=self.export();before=inventory(root) + paths=list(root.rglob('*')) + try: + for p in paths:p.chmod(0o555 if p.is_dir() else 0o444) + root.chmod(0o555) + result=self.run_export(pkg) + self.assertEqual(result.returncode,0,result.stderr) + self.assertIn('PASS_QQ16_F17_DEMAND_PROJECTION',result.stdout) + self.assertEqual(inventory(root),before) + finally: + root.chmod(0o755) + for p in paths:p.chmod(0o755 if p.is_dir() else 0o644) + + def test_source_rejected_before_execution(self): + root,pkg=self.export() + path=root/'research/qq16-line-normalized-decoder/verify.py' + path.write_text("raise RuntimeError('EXECUTED_CORRUPT_SOURCE')\n") + result=self.run_export(pkg) + self.assertNotEqual(result.returncode,0) + self.assertIn('source SHA256:',result.stderr) + self.assertNotIn('RuntimeError: EXECUTED_CORRUPT_SOURCE',result.stderr) + + def test_type_sensitive_receipt_rejection(self): + _,pkg=self.export();p=pkg/'RESULT.json';r=json.loads(p.read_bytes()) + r['invoice']['rank_one_children']='112';p.write_text(json.dumps(r)) + result=self.run_export(pkg) + self.assertNotEqual(result.returncode,0);self.assertIn('complete RESULT mismatch',result.stderr) + + def test_missing_cleanup_word_rejection(self): + _,pkg=self.export();p=pkg/'WORD.json';w=json.loads(p.read_bytes());w.pop();p.write_text(json.dumps(w)) + result=self.run_export(pkg) + self.assertNotEqual(result.returncode,0);self.assertIn('complete WORD mismatch',result.stderr) + + def test_missing_receipt_is_not_regenerated(self): + _,pkg=self.export();p=pkg/'RESULT.json';p.unlink() + result=self.run_export(pkg) + self.assertNotEqual(result.returncode,0);self.assertFalse(p.exists()) + + +if __name__=='__main__':unittest.main() diff --git a/research/qq16-f17-demand-projection/verify.py b/research/qq16-f17-demand-projection/verify.py new file mode 100644 index 0000000000..365ac9adec --- /dev/null +++ b/research/qq16-f17-demand-projection/verify.py @@ -0,0 +1,200 @@ +#!/usr/bin/env python3 +"""F17 demand projection. Chris R / Clear1nsight, OpenAI assistance; Apache-2.0. + +Source/operator primitives: ywz65 PR2707 and Arham Tahir PR2681. Source bytes +are authenticated before execution. This is a scoped changed-consumer audit. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import types + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +DEC='research/qq16-line-normalized-decoder/' + + +def need(ok, why): + if not ok: raise ValueError(why) + + +def decode(raw): + def unique(pairs): + out={} + for k,v in pairs: + need(k not in out,'duplicate JSON key'); out[k]=v + return out + return json.loads(raw,object_pairs_hook=unique) + + +def canonical(obj): + return json.dumps(obj,sort_keys=True,separators=(',',':')).encode() + + +def module(path, raw=None): + out=types.ModuleType(path.stem); out.__file__=str(path) + exec(compile(path.read_bytes() if raw is None else raw,str(path),'exec'),out.__dict__) + return out + + +def authenticate(): + raw={} + for pin in decode((HERE/'SOURCES.json').read_bytes())['files']: + if pin['usage']!='input': continue + data=(ROOT/pin['path']).read_bytes() + need(hashlib.sha256(data).hexdigest()==pin['sha256'],'source SHA256: '+pin['path']) + need(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest()==pin['git_blob'],'source Git blob') + raw[pin['path']]=data + return raw + + +def load(raw): + L=module(ROOT/DEC/'verify.py',raw[DEC+'verify.py']) + P,R,routes,labels,_=L.load_source() + source=decode(raw[DEC+'WORD.json']) + need(source==L.lower(P,R),'complete source word regeneration') + return P,R,routes,labels,source + + +def projection(P,source): + result=[] + for e in source: + # No stage-2 line/map is needed on U: logger writes only selected A. + if (e[0]=='line' and e[3]==-1) or (e[0]=='map' and e[2]==2): break + op=e[0] + if op in ('begin','end') or (op=='clear' and e[1].startswith('F')): + result.append(e.copy()) + elif op=='add': + dst,src=e[1:3] + if dst.startswith('F') or (dst.startswith('W') and src.startswith('Y')) or ( + dst.startswith('W') and int(dst[1:]) in P.U and src.startswith('F')): + result.append(e.copy()) + elif op in ('clear','line','map') and e[1].startswith('W'): + p=int(e[1][1:]) + if op=='clear' and e[2]=='wide': continue + if op=='map' and e[4] and p not in P.U: continue + result.append(e.copy()) + for p in P.V: result.append(['clear','W'+str(p),'identity']) + return result + + +def demand(P,R,routes,y2): + q=P.query(R,routes,1,y2,range(112)); correction=P.inject(R,routes,1,q,P.U) + return [P.add(y2[p],correction[p],-1) for p in range(112)] + + +def native(P,labels): + columns=0 + for q in labels: + pivot=(q & -q).bit_length()-1 + basis=(q,)+tuple(1<1 and waived[1]<1,'budget split') + need(B.moment(base,61,64,True,a)[1]<1