diff --git a/research/bit-nine-owned-relations/PROOF.md b/research/bit-nine-owned-relations/PROOF.md new file mode 100644 index 0000000000..217cee7af0 --- /dev/null +++ b/research/bit-nine-owned-relations/PROOF.md @@ -0,0 +1,184 @@ +# Boundary proof and complete BIT cost + +## 1. Source and owned input code + +Use the PR589 word retained at the source commit in SOURCES.json. It has +111 X fields, 111 Y fields, 439 helpers and one owned COPY centre. The +logical main map is `(X,Y) -> (X,Y+X)` over GF(2). Each helper has the +identity logical endpoint. The source forward and reverse words have +this same logical map. + +Replay the source records in reverse order over the vector space with +661 independent input symbols. Each of its nine COPY entries is a +linear form in these symbols. Reduce these nine forms by helper columns. +The resulting pivot helpers are + +```text +222, 223, 224, 225, 226, 228, 230, 231, 233. +``` + +Each reduced form contains its own pivot and no other pivot. Every field +in its support has the full entrance frame. The relation rows are saved +in RESULT.json and are derived again from the source during every run. + +Own these nine helpers. Clear each at entry and XOR its other relation +terms into it. The nine forms are then zero. These operations use a +common frame and leave all 652 retained input fields unchanged. A +chronological replay of the original reverse word now proves that every +COPY value is zero. The copy centre stays zero. Nine rank-one moves are +also on zero values. Replace only these moves by zero frame changes. +Clear the nine owned helpers at exit, and return the centre to its empty +frame. This gives a map on arbitrary retained inputs with all owned exit +fields zero. The entry clears make the result independent of arbitrary +initial values in owned storage. + +The exact new local paid profile is + +```text +{1:1314, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:10}. +``` + +The productive helper profile is `{8:430}`. There are no new nonzero +native maps. The original rank-one and rank-seven jobs are removed in +nine pairs. Each pair loses one rank-eight target. The fixed field count +remains 662; no new physical field is required. + +## 2. Why one reverse word serves both directions + +The logical involution alone is insufficient. Check the physical address +maps as well. For a source port let P be its rank-one rational projector, +K=I-P, Q=D_P, S=D_K, and R=D_I. Here D denotes the source two-bank +interchange, with its fixed second-bank reversal included. These address +permutations commute, square to I, and satisfy QS=R. + +In this paragraph Q, S and R denote their induced data-permutation +operators. Let M be the two-field XOR shear, with block rows `(I,0)` +and `(I,I)`. The source forward physical operator is + +```text +diag(R,S) M diag(Q,I) = [[S,0],[R,S]]. +``` + +Its reverse physical operator is + +```text +diag(Q,I) M diag(R,S) = [[S,0],[R,S]]. +``` + +Both products therefore give the same physical endpoint. This endpoint +is an involution over GF(2), since RS+SR=0. Each retained helper has +endpoint D_I, also an involution. Thus the new reverse implementation +replaces either direction of the original local call with the same +caller port and role assignments. No new query, route or native map is +needed for this replacement. + +The verifier checks the source entrance line and exit complement for +every port. It checks the rational address identities `D_I D_P=D_K` +and `D_P^2=D_K^2=I`. These are identities of address matrices. The block +XOR calculation above is an identity of induced data operators; it does +not identify addition of address matrices with addition of data operators. + +## 3. Native interfaces and all column multiplicities + +All nonzero native transitions are retained source transitions. The +verifier rebuilds every source projector over the rationals and checks +both nesting products and the rank difference for each transition pair. +For each of the 111 ports it builds an exact complement basis and a +15-dimensional route. It checks that the route is an involution, fixes +the central line, and sends the local full projector to the required +line-plus-fresh-stage projector. + +For column multiplicity f, tensor each head-space projector and route +with I_f. The same products, inclusions and involutions hold. The entry +code consists of pointwise XORs and clears in a common full frame. Its +relations hold on arbitrary data arrays. The complete finite program +therefore has the same native boundary for every f under the inherited +all-column and owned-erasure premises. + +Apply the retained delayed-cover bridge only after the entire finite +program is compiled. Its one common external weight is the same for all +fresh roles. All pointwise XORs commute with that weight. The retained +whole-fibre routes preserve independent data. The new code adds no +right-route symbol, nonzero native map or denominator. This argument +retains the source compiler and native realization premises; the finite +rational tests alone do not prove them. + +## 4. Complete controller invoice + +Replay every physical event in the source p16/a7 BIT controller over the +GF(2) group ring. Verify its literal scalar boundaries and all 32 +independent main inputs per port. There are eighteen full calls and +fifteen query shears. Replace every full call by the new word, using +Section 2. Leave each thin query and idle transform in place. + +Let P_old, T_old and P_new, T_new be the full paid and target histograms. +The exact differences are + +```text +P_new - P_old = -162 H1 -162 H7 +T_new - T_old = -162 H8. +``` + +Here Hr denotes one rank-r job or target. The new total is 57,231 paid +jobs and 11,292 productive fields. The paid rank mass is 215,457 and the +target rank mass is 216,210. The surplus is 753, as before. The verifier +reconstructs both complete invoices from the literal event list; it does +not subtract a proposed saving from a stored total. + +For every 00`. An equivalent certificate for the signed paid-minus- +target difference is the hinge sum `sum(delta_r*min(r,k))`: its values +at k=1,7,8 are -162,-162,0. All tail values are zero. This charges every +lost target and proves a strict improvement for the concave rank power. + +Two rational interval engines check the new moment. The raw moment has +a positive margin at 0.003472070044 and a negative margin at +0.003472070045. This is a certified crossing, not an optimum over other +words or controller classes. + +## 5. Compiler, cover and ordinary conversion + +The new tested saving is 0.0034678 and the uniform saving is 0.0034668. +Keep the source tensor power 1024, cutoff 17, floor 18, second-moment +parameter 1/5 and reserve 1/250000. The exact interval checks give the +charged first-moment ratio below `1-reserve`, the tail ratio below +31/32 and the rounding ratio below 19/20. Both decay bounds after 128 +steps are below 1/16. The completion surplus is positive, `17^64<18^63`, +and every target rank is below 256. RESULT.json records the exact H0 and +strict H1 thresholds. The winning uniform word is not materialized. + +Keep the source cover loss 0.000009. The saving after cover is 0.0034578. +Use an odd prime `q>2^26*N^5` that avoids all fixed denominators and rank +witnesses. Keep atom fraction 0.004 and old ordinary saving 0.0000384599. +The new ordinary saving is + +```text +(1-0.004)*0.0034578 + 0.004*0.0000384599 = 0.0034441226396. +``` + +The strict admitted endpoint is 0.00344412. At the same compiler gaps, +cover loss and atom fraction, the old word gives 0.0034363538396. The +matched gain is exactly 0.0000077688. This comparison does not credit the +new relations for the old source's unused conservative headroom. + +The new local word has 25,891 pointwise records. This is 1,568 more than +the source's 24,305 XORs and eighteen COPY entry/exit records. Add all +1,568 records to the inherited complete local allowance of 1,000,000. +The new local allowance is 1,001,568. With all eighteen calls, thin +queries, physical events and boundary operations, the complete raw +nonrecursive allowance is 19,170,192, below the retained 10^9 allowance. +The new code uses only unit XOR coefficients, adds no denominator and +no storage field, and retains the source tape and cover obligations. + +## 6. Complete multiplication scope + +Use the pinned PR5398 outer parameters and replace only their ordinary +BIT saving by 0.00344412. All 54 strict and four functional predicates +pass. The actual BIT stock exponent is positive and strictly below the +active group exponent, which is below one. The complete multiplication +endpoint remains 0.00302728823. The complex supplier still binds. + +This is a complete conditional BIT component improvement. It is not a +new complete multiplication bound, a selected-frontier change, a formal +proof, or an independent replay of the consumed complex construction. +All five inherited premise classes remain explicit in RESULT.json. diff --git a/research/bit-nine-owned-relations/README.md b/research/bit-nine-owned-relations/README.md new file mode 100644 index 0000000000..f2914f37b9 --- /dev/null +++ b/research/bit-nine-owned-relations/README.md @@ -0,0 +1,89 @@ +# Nine owned BIT helper relations + +This conditional construction raises the ordinary BIT saving from +**0.0034363538396 to 0.0034441226396** at matched compiler and cover +parameters. It admits the strict endpoint **0.00344412**. The complete +multiplication kappa does not increase: the complex supplier still binds. + +The reverse PR589 word has nine COPY values that are linear forms of its +initial full-frame fields. Own one helper for each independent form and +set all nine forms to zero. This removes nine rank-one transitions and +nine rank-seven COPY jobs per local call. It also removes nine rank-eight +productive helper targets. All 652 retained inputs remain independent. +The ten owned fields, including the old COPY centre, accept arbitrary +entry data and finish at zero. + +[PROOF.md](PROOF.md) gives the local boundary argument, the physical +involution that permits use at all eighteen full calls, the tensor lift, +and the complete cost. [RESULT.json](RESULT.json) contains the exact +receipt. [WORD.json.gz](WORD.json.gz) contains the emitted program. +[SOURCES.json](SOURCES.json) pins all thirteen live inputs at base +`d277c97824e50782da6adbc486ca3c76c8fc687e`. The selected record in that +manifest is historical provenance. This package does not change it. + +The complete p16/a7 controller has 57,231 paid jobs and 11,292 productive +fields. Its change is minus 162 rank-one jobs, minus 162 rank-seven jobs, +and minus 162 rank-eight targets. Its rank surplus remains 753. The raw +moment crossing lies strictly between 0.003472070044 and 0.003472070045. +The complete scalar and route allowance remains below 10^9. + +## Reproduce + +Use CPython 3.12 and its standard library. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/bit-nine-owned-relations +python3.12 -O -B research/bit-nine-owned-relations/verify.py +``` + +The verifier prints: + +```text +PASS_BIT_NINE_OWNED_RELATIONS_00344412_NO_NEW_MULTIPLICATION_KAPPA +``` + +It authenticates every live source, rebuilds the word, checks all symbolic +input rows, and replays each of the 662 input columns with separate +Boolean state. It checks rational projectors and all 111 port charts, +the literal controller, all targets and paid jobs, two exact moment +engines, the compiler tail, the cover loss, the ordinary BIT conversion, +and the unchanged outer arithmetic. It rejects missing entry or exit +clears, a changed relation, a nonzero free transition, a missing target +debit, and the old word at the new saving. + +## Scope + +The native all-column, owned-erasure, compiler, precision/tape, and +analytic-recovery premises remain conditional. The source delayed-cover +argument supplies the common weight and recursive interface. The finite +checks do not materialize the full GL cover, the winning uniform word, +or the complete integer multiplier. No Lean or proof-kernel check is +included. The outer arithmetic consumes the pinned PR5398 receipt; it +does not replay that complex construction. No global optimum is claimed. + +## Open next questions + +A further BIT gain needs a new relation space after all nine COPY jobs +are removed. Check active claims first, then charge each lost target +against the full word. The current full-history searches supply no such +additional gain. A complete multiplication gain needs a cheaper complex +supplier with a complete caller and cost. This package supplies neither. +[TASK.json](TASK.json) records the scope and these limits. + +## Credit + +DreamingOfClouds supplied [PR #589](https://github.com/CrocSwap/integer-mult-bounds/pull/589), +the retained two-transport word. eumemic supplied +[PR #555](https://github.com/CrocSwap/integer-mult-bounds/pull/555), the +punctured 111-port, 439-helper construction, from the credited earlier +word and port construction. Their source notices remain unchanged. +Cinna Davis supplied the query-thinned controller, the native BIT binding, +and the delayed-cover bridge. The exact compiler and tail work follows +zxv and the retained mixed-target recursion of Jacob Alan Sussman. +Ali Romman's [PR #5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383) +supplies the prior owned-helper method. The unchanged complex comparison +comes from [PR #5398](https://github.com/CrocSwap/integer-mult-bounds/pull/5398). +The exact consumed source paths and pins are in SOURCES.json. + +Prepared by Ali Romman with substantial OpenAI Codex assistance; no +subagents. New work is Apache-2.0. All predecessor notices are retained. diff --git a/research/bit-nine-owned-relations/RESULT.json b/research/bit-nine-owned-relations/RESULT.json new file mode 100644 index 0000000000..b3fd1f0fa2 --- /dev/null +++ b/research/bit-nine-owned-relations/RESULT.json @@ -0,0 +1,1962 @@ +{ + "complete_cost": { + "binding_constraint": "The complex supplier remains below this BIT saving.", + "budgets": { + "added_pointwise_records_per_call": 1568, + "complete_raw_nonrecursive": 19170192, + "inherited_source_local_upper": 1000000, + "local_complete_upper": 1001568, + "local_scalar": 25891, + "raw_allowance": 1000000000 + }, + "complete_multiplication_kappa_improvement": false, + "concave_order_certificate": { + "1": -162, + "7": -162, + "8": 0 + }, + "controller": { + "full_calls": 18, + "parent_inputs_per_port": 32, + "physical_events": 154, + "thin_calls": 15 + }, + "negative_controls": { + "missing_target_debit": "Every paid job and earned target must match the literal word", + "old_word_at_new_saving": "Rejected by the exact raw moment" + }, + "new_compiler": { + "H0": 3764063437, + "H1": 26102274310221, + "alpha": { + "lower": "0.999995697975360862052844540831", + "upper": "0.999995697975360862052844540832" + }, + "cutoff": 17, + "delta": { + "lower": "0.941917605188527740239545244446", + "upper": "0.941917605188527740239545244447" + }, + "floor": 18, + "gamma": { + "lower": "0.958354812695517905511855681272", + "upper": "0.958354812695517905511855681273" + }, + "normalized_surplus_lower": "68719461047/16845935476736", + "reserve": "1/250000", + "tensor_power": 1024, + "tested": "17339/5000000", + "uniform": "8667/2500000", + "uniform_N": "2^26102274310221", + "winning_word_materialized": false + }, + "new_raw_root": [ + "868017511/250000000000", + "694414009/200000000000" + ], + "old_compiler": { + "H0": 3755884544, + "H1": 25986965159937, + "alpha": { + "lower": "0.999995735238059506641600561767", + "upper": "0.999995735238059506641600561768" + }, + "cutoff": 17, + "delta": { + "lower": "0.949707924144871179442776557218", + "upper": "0.949707924144871179442776557219" + }, + "floor": 18, + "gamma": { + "lower": "0.957429821066420278606254392110", + "upper": "0.957429821066420278606254392111" + }, + "normalized_surplus_lower": "68719461047/16845935476736", + "reserve": "1/250000", + "tensor_power": 1024, + "tested": "173/50000", + "uniform": "3459/1000000", + "uniform_N": "2^25986965159937", + "winning_word_materialized": false + }, + "old_raw_root": [ + "866062243/250000000000", + "3464248973/1000000000000" + ], + "ordinary_BIT": { + "admitted": "86103/25000000", + "after_cover": "17289/5000000", + "atom": "1/250", + "gain_at_matched_parameters": "9711/1250000000", + "new_ordinary": "8610306599/2500000000000", + "old_ordinary": "8590884599/2500000000000", + "prime_rule": "Odd q > 2^26*N^5, avoiding all fixed denominators and rank witnesses" + }, + "outer_at_unchanged_complex_endpoint": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "174299999999253/175000000000000", + "fixed_halo_explicit_metadata_branch": "13475000000001/175000000000", + "new_BIT_row_stock_sublinear_in_active_group": "697899999997009/700000000000000", + "new_semantic_group_guard": "3/700000000000" + }, + "margins": { + "boundary_algebraic_matrix": "370842808874470224559/122500000000000000000000", + "fused_gaussian": "370842808873410673677/122500000000000000000000", + "global_coordinate_router": "423820353/140000000000", + "group_bit_router": "296674247238728538941/98000000000000000000000", + "group_scans": "349999999999/350000000000", + "main_transform": "370842808699470224559/122500000000000000000000", + "microbox_face_corrections": "13475000000001/175000000000", + "polynomial_products": "699999999999/700000000000", + "sparse_union_movement": "50136467808874470224559/122500000000000000000000" + }, + "parameters": { + "a": "423820353/140000000000", + "b": "1059550883/350000000000", + "beta": "699999999997/700000000000", + "bit_saving": "86103/25000000", + "cap_xi": "111386467808699470224559/122500000000000000000000", + "complex_uniform_saving": "2119101767/700000000000", + "d": "1/700000000000", + "epsilon": "699999999999/700000000000", + "kappa": "302728823/100000000000", + "lambda_": "199394542353/200000000000", + "lambda_prime": "174470224559/175000000000", + "layout": "1/700000000000", + "q": "529775441/175000000000", + "r0": "1/7000000000000", + "stop": "1/700000000000", + "tested_saving": "37841103/12500000000" + }, + "strict_checks": { + "actual_bit_above_effective": "58356447/140000000000", + "actual_logarithmic_gamma_guard": "1/700000000000", + "actual_logarithmic_group_guard": "11113532191563029775441/61250000000000000000000", + "alpha_logarithm_absorption": "1/7000000000000", + "boundary_algebraic_matrix_above_kappa": "699470224559/122500000000000000000000", + "cap_above_band": "50136467808699470224559/122500000000000000000000", + "cap_below_cell": "11113532191125529775441/122500000000000000000000", + "cap_below_phase_cell_power": "133613532191300529775441/122500000000000000000000", + "complex_above_effective": "1/700000000000", + "complex_below_one_over_32": "9877949117/350000000000", + "complex_endpoint": "1/350000000000", + "epsilon_below_one": "1/700000000000", + "epsilon_positive": "699999999999/700000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "698410673677/122500000000000000000000", + "gaussian_above_main": "86970224559/61250000000000000000000", + "global_coordinate_router_above_kappa": "1/175000000000", + "global_gamma_power_slack": "9/7000000000000", + "group_below_dimension": "1/350000000000", + "group_bit_router_above_kappa": "698728538941/98000000000000000000000", + "group_gauge_power_slack": "11113532191554279775441/61250000000000000000000", + "group_key_fits_record": "1/350000000000", + "group_positive": "699999999997/700000000000", + "group_scans_above_kappa": "697880898237/700000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "648158905400418148631/500000000000000000000000", + "lambda_above_internal": "1/1400000000000", + "lambda_above_sigma": "3/1400000000000", + "lambda_above_tau": "1/1400000000000", + "lambda_prime_above_lambda": "1/1400000000000", + "lambda_prime_above_leaf": "698940449117/245000000000000000000000", + "leaf_saving_above_effective": "348940449117/245000000000000000000000", + "main_transform_above_kappa": "524470224559/122500000000000000000000", + "membership_arithmetic_fits_record": "1/700000000000", + "microbox_face_corrections_above_kappa": "53897880898243/700000000000", + "microbox_halo_volume": "55300000000003/700000000000", + "new_complex_uniform_saving_above_b": "1/700000000000", + "new_semantic_guard_with_C1_one": "1/700000000000", + "polynomial_products_above_kappa": "348940449119/350000000000", + "positive_layout_slack": "1/700000000000", + "q_below_effective": "1/700000000000", + "q_below_internal": "1/700000000000", + "q_below_leaf": "698940449117/245000000000000000000000", + "q_positive": "529775441/175000000000", + "short_record_fallback": "348940449117/350000000000", + "source_axis_superpolynomial": "1/700000000000", + "sparse_union_movement_above_kappa": "49765625000699470224559/122500000000000000000000", + "stop_below_one": "699999999999/700000000000", + "stop_positive": "1/700000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/700000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/700000000000", + "union_tag_work_per_visit_fits_record": "3/700000000000" + } + }, + "paid": { + "1": 25317, + "14": 444, + "2": 24156, + "21": 444, + "28": 444, + "3": 1422, + "35": 444, + "4": 792, + "42": 444, + "49": 444, + "5": 1836, + "56": 444, + "6": 198, + "63": 222, + "7": 180 + }, + "paid_count": 57231, + "rank_bill": 215457, + "rank_credit": 216210, + "signed_delta": { + "1": -162, + "7": -162, + "8": 162 + }, + "target_count": 11292, + "targets": { + "127": 222, + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "43": 444, + "50": 444, + "57": 444, + "64": 222, + "8": 7740 + } + }, + "limits": [ + "The complex supplier still limits the complete multiplication bound.", + "Native all-column, owned-erasure, compiler, precision/tape and analytic recovery premises remain conditional.", + "The full GL cover, winning uniform word and complete integer multiplier are not materialized.", + "No Lean or proof-kernel check is included." + ], + "local": { + "arbitrary_owned_entries": 10, + "events": 28802, + "helpers": { + "8": 430 + }, + "maximum_binary_row_weight": 264, + "native": { + "all_f_rule": "Source projectors tensor I_f; the source address involutions and all GF(2) identities stay exact.", + "fresh_port_routes": 111, + "full_GL_cover_executed": false, + "main_involution_ports": 111, + "nested_transition_pairs": 2386, + "new_nonzero_native_maps": 0, + "rational_projectors": 636 + }, + "negative_controls": { + "changed_relation": "Only a zero value can change frame for free", + "missing_owned_entry_clear": "Only a zero value can change frame for free", + "missing_owned_exit_clear": "Every retained and arbitrary owned entry column", + "unearned_free_transition": "Only a zero value can change frame for free" + }, + "paid": { + "1": 1314, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 10 + }, + "relation_basis": { + "222": [ + 8, + 9, + 10, + 11, + 12, + 13, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 46, + 47, + 48, + 49, + 50, + 51, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 222, + 239, + 243, + 245, + 251, + 256, + 261, + 265, + 269, + 270, + 272, + 273, + 281, + 282, + 285, + 286, + 291, + 292, + 295, + 297, + 298, + 299, + 301, + 305, + 309, + 313, + 315, + 317, + 318, + 321, + 322, + 325, + 327, + 329, + 330, + 335, + 336, + 340, + 344, + 346, + 347, + 348, + 349, + 351, + 352, + 353, + 354, + 355, + 357, + 358, + 360, + 364, + 368, + 371, + 375, + 376, + 377, + 378, + 379, + 381, + 383, + 385, + 386, + 387, + 388, + 394, + 396, + 403, + 404, + 406, + 410, + 411, + 416, + 420, + 422, + 426, + 427, + 431, + 432, + 433, + 435, + 436, + 438, + 440, + 442, + 443, + 454, + 460, + 462, + 465, + 466, + 467, + 474, + 476, + 477, + 478, + 486, + 488, + 492, + 495, + 496, + 507, + 509, + 511, + 517, + 528, + 547, + 551, + 558, + 559, + 585, + 597, + 603, + 615, + 622, + 634, + 639, + 651, + 657 + ], + "223": [ + 0, + 3, + 5, + 6, + 14, + 16, + 18, + 20, + 22, + 23, + 26, + 27, + 31, + 33, + 35, + 37, + 40, + 41, + 44, + 45, + 47, + 48, + 50, + 53, + 54, + 55, + 56, + 60, + 61, + 63, + 65, + 69, + 70, + 71, + 72, + 74, + 76, + 77, + 79, + 82, + 83, + 84, + 85, + 88, + 90, + 93, + 95, + 96, + 97, + 102, + 104, + 105, + 107, + 110, + 223, + 240, + 241, + 246, + 247, + 249, + 250, + 251, + 258, + 260, + 266, + 268, + 269, + 274, + 276, + 278, + 280, + 282, + 284, + 285, + 291, + 292, + 297, + 298, + 301, + 305, + 307, + 313, + 317, + 321, + 322, + 327, + 330, + 331, + 332, + 334, + 336, + 338, + 340, + 341, + 342, + 347, + 348, + 349, + 352, + 354, + 357, + 360, + 365, + 368, + 369, + 376, + 378, + 381, + 385, + 387, + 388, + 392, + 394, + 403, + 406, + 408, + 410, + 411, + 416, + 417, + 419, + 420, + 421, + 422, + 423, + 425, + 432, + 435, + 436, + 437, + 438, + 439, + 440, + 449, + 460, + 462, + 464, + 466, + 467, + 472, + 473, + 476, + 478, + 484, + 492, + 495, + 496, + 499, + 504, + 511, + 517, + 528, + 547, + 551, + 558, + 559, + 585, + 597, + 603, + 615, + 622, + 634, + 639, + 651, + 657 + ], + "224": [ + 0, + 1, + 6, + 7, + 9, + 10, + 12, + 14, + 16, + 18, + 20, + 22, + 25, + 27, + 28, + 30, + 31, + 32, + 33, + 39, + 41, + 43, + 45, + 46, + 48, + 49, + 50, + 52, + 53, + 56, + 57, + 62, + 63, + 64, + 65, + 67, + 69, + 71, + 74, + 76, + 78, + 80, + 81, + 83, + 84, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 98, + 100, + 102, + 104, + 106, + 108, + 110, + 224, + 237, + 238, + 239, + 241, + 242, + 245, + 248, + 252, + 254, + 256, + 257, + 261, + 263, + 271, + 277, + 279, + 281, + 283, + 287, + 288, + 290, + 293, + 294, + 295, + 296, + 297, + 299, + 300, + 303, + 305, + 307, + 309, + 312, + 316, + 319, + 322, + 327, + 335, + 339, + 341, + 343, + 344, + 348, + 349, + 352, + 355, + 360, + 363, + 364, + 367, + 371, + 376, + 380, + 389, + 390, + 391, + 392, + 394, + 396, + 400, + 402, + 404, + 406, + 414, + 418, + 429, + 430, + 434, + 442, + 452, + 454, + 455, + 456, + 462, + 463, + 464, + 469, + 471, + 477, + 479, + 490, + 501, + 514, + 525, + 531, + 544, + 561, + 568, + 582, + 594, + 606, + 608, + 617, + 629, + 641, + 643, + 649 + ], + "225": [ + 1, + 2, + 5, + 6, + 11, + 12, + 13, + 14, + 16, + 19, + 21, + 24, + 25, + 26, + 27, + 30, + 32, + 35, + 37, + 40, + 41, + 42, + 43, + 47, + 48, + 49, + 51, + 53, + 54, + 55, + 56, + 59, + 60, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 75, + 77, + 79, + 82, + 83, + 86, + 87, + 88, + 90, + 92, + 94, + 98, + 99, + 102, + 103, + 106, + 107, + 110, + 225, + 227, + 240, + 243, + 247, + 249, + 250, + 259, + 266, + 267, + 268, + 276, + 278, + 282, + 288, + 297, + 304, + 305, + 307, + 308, + 320, + 328, + 331, + 332, + 334, + 338, + 341, + 342, + 347, + 351, + 353, + 354, + 356, + 357, + 360, + 368, + 371, + 377, + 379, + 381, + 391, + 392, + 393, + 394, + 401, + 403, + 405, + 408, + 410, + 413, + 416, + 417, + 423, + 424, + 425, + 427, + 435, + 437, + 440, + 443, + 447, + 449, + 451, + 455, + 457, + 458, + 461, + 466, + 467, + 472, + 476, + 484, + 486, + 492, + 499, + 504, + 511, + 517, + 528, + 547, + 551, + 558, + 559, + 585, + 597, + 603, + 615, + 622, + 634, + 639, + 651, + 657 + ], + "226": [ + 2, + 3, + 4, + 5, + 8, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 24, + 26, + 29, + 30, + 31, + 32, + 33, + 39, + 41, + 43, + 45, + 46, + 48, + 49, + 50, + 52, + 53, + 56, + 57, + 59, + 60, + 61, + 66, + 68, + 70, + 72, + 73, + 75, + 77, + 79, + 82, + 85, + 86, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 98, + 100, + 102, + 104, + 106, + 108, + 110, + 226, + 235, + 240, + 241, + 246, + 247, + 249, + 250, + 256, + 264, + 265, + 268, + 269, + 276, + 278, + 281, + 282, + 285, + 286, + 292, + 298, + 305, + 306, + 307, + 313, + 315, + 317, + 318, + 322, + 326, + 327, + 330, + 331, + 332, + 334, + 336, + 338, + 341, + 342, + 343, + 347, + 348, + 349, + 352, + 354, + 357, + 360, + 361, + 369, + 374, + 376, + 378, + 381, + 382, + 386, + 387, + 392, + 394, + 403, + 406, + 408, + 410, + 416, + 417, + 419, + 420, + 421, + 423, + 425, + 426, + 432, + 435, + 436, + 437, + 438, + 440, + 449, + 450, + 457, + 460, + 462, + 464, + 466, + 472, + 473, + 476, + 478, + 480, + 484, + 488, + 492, + 495, + 496, + 499, + 504, + 506, + 511, + 515, + 517, + 518, + 528, + 530, + 536, + 538, + 547, + 551, + 554, + 558, + 559, + 569, + 571, + 585, + 593, + 596, + 597, + 603, + 612, + 615, + 622, + 624, + 625, + 631, + 634, + 639, + 644, + 651, + 656, + 657 + ], + "228": [ + 0, + 3, + 5, + 6, + 8, + 10, + 12, + 13, + 14, + 15, + 20, + 21, + 22, + 24, + 27, + 29, + 32, + 33, + 34, + 35, + 39, + 41, + 42, + 44, + 46, + 47, + 48, + 53, + 55, + 57, + 59, + 60, + 64, + 65, + 68, + 69, + 72, + 75, + 76, + 79, + 80, + 83, + 85, + 87, + 88, + 89, + 92, + 93, + 96, + 98, + 100, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 228, + 239, + 240, + 243, + 245, + 247, + 251, + 256, + 261, + 265, + 266, + 268, + 269, + 270, + 273, + 276, + 278, + 281, + 282, + 285, + 286, + 288, + 291, + 292, + 295, + 297, + 299, + 301, + 304, + 305, + 308, + 309, + 313, + 315, + 317, + 318, + 321, + 322, + 325, + 327, + 329, + 330, + 332, + 334, + 335, + 336, + 338, + 340, + 342, + 344, + 347, + 348, + 349, + 351, + 352, + 353, + 354, + 355, + 364, + 368, + 371, + 375, + 376, + 377, + 378, + 379, + 383, + 386, + 387, + 388, + 391, + 393, + 394, + 396, + 401, + 403, + 404, + 405, + 406, + 410, + 411, + 413, + 416, + 417, + 420, + 422, + 423, + 425, + 426, + 427, + 431, + 432, + 435, + 436, + 437, + 438, + 440, + 442, + 443, + 447, + 451, + 454, + 455, + 457, + 460, + 461, + 462, + 465, + 466, + 467, + 472, + 474, + 476, + 477, + 478, + 484, + 486, + 488, + 492, + 495, + 496, + 499, + 504, + 507, + 509, + 511, + 517, + 528, + 547, + 551, + 558, + 559, + 585, + 597, + 603, + 615, + 622, + 634, + 639, + 651, + 657 + ], + "230": [ + 4, + 5, + 6, + 7, + 8, + 10, + 11, + 14, + 17, + 18, + 21, + 22, + 25, + 26, + 29, + 30, + 33, + 34, + 37, + 38, + 41, + 42, + 45, + 46, + 49, + 51, + 52, + 53, + 55, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 70, + 71, + 74, + 75, + 78, + 79, + 82, + 85, + 86, + 89, + 90, + 93, + 94, + 97, + 98, + 101, + 102, + 104, + 105, + 108, + 109, + 230, + 239, + 240, + 243, + 245, + 247, + 262, + 266, + 267, + 268, + 271, + 276, + 278, + 282, + 285, + 288, + 293, + 295, + 304, + 305, + 308, + 324, + 330, + 332, + 334, + 335, + 337, + 338, + 342, + 346, + 351, + 357, + 358, + 360, + 365, + 369, + 370, + 373, + 375, + 377, + 379, + 383, + 385, + 391, + 393, + 394, + 401, + 403, + 404, + 405, + 410, + 415, + 417, + 423, + 425, + 427, + 433, + 435, + 436, + 437, + 443, + 444, + 447, + 451, + 453, + 454, + 455, + 457, + 461, + 468, + 470, + 471, + 472, + 475, + 484, + 486, + 487, + 499, + 504, + 510, + 517, + 528, + 558, + 559, + 584, + 598, + 603, + 616, + 622, + 634, + 640, + 651, + 658 + ], + "231": [ + 4, + 5, + 6, + 7, + 8, + 10, + 11, + 15, + 16, + 19, + 20, + 23, + 24, + 27, + 28, + 30, + 33, + 34, + 37, + 38, + 41, + 42, + 45, + 47, + 48, + 50, + 54, + 56, + 57, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 70, + 71, + 73, + 76, + 77, + 80, + 81, + 83, + 84, + 87, + 89, + 90, + 93, + 94, + 97, + 98, + 101, + 102, + 103, + 106, + 107, + 110, + 231, + 237, + 239, + 240, + 243, + 245, + 247, + 249, + 250, + 251, + 254, + 256, + 261, + 266, + 268, + 269, + 276, + 278, + 281, + 282, + 283, + 285, + 288, + 291, + 292, + 295, + 299, + 300, + 301, + 304, + 308, + 309, + 313, + 317, + 321, + 322, + 325, + 327, + 330, + 331, + 332, + 334, + 335, + 336, + 338, + 339, + 342, + 343, + 344, + 347, + 348, + 349, + 351, + 352, + 353, + 354, + 357, + 360, + 364, + 368, + 371, + 376, + 377, + 378, + 379, + 380, + 381, + 387, + 388, + 390, + 391, + 393, + 396, + 400, + 401, + 403, + 404, + 405, + 406, + 408, + 410, + 411, + 413, + 414, + 416, + 417, + 418, + 420, + 422, + 423, + 425, + 427, + 432, + 435, + 436, + 437, + 438, + 440, + 441, + 442, + 443, + 447, + 449, + 451, + 454, + 455, + 456, + 457, + 459, + 460, + 461, + 462, + 466, + 467, + 472, + 476, + 477, + 478, + 484, + 486, + 492, + 495, + 496, + 499, + 504, + 511, + 517, + 528, + 547, + 551, + 558, + 559, + 585, + 597, + 603, + 615, + 622, + 634, + 639, + 651, + 657 + ], + "233": [ + 9, + 11, + 14, + 17, + 19, + 20, + 23, + 24, + 26, + 29, + 30, + 33, + 35, + 36, + 39, + 40, + 42, + 45, + 46, + 50, + 52, + 53, + 55, + 58, + 59, + 61, + 63, + 64, + 66, + 67, + 69, + 72, + 73, + 76, + 78, + 79, + 82, + 84, + 87, + 88, + 91, + 93, + 94, + 97, + 98, + 100, + 103, + 106, + 108, + 109, + 233, + 240, + 241, + 243, + 247, + 249, + 250, + 251, + 266, + 268, + 269, + 276, + 278, + 282, + 285, + 288, + 291, + 292, + 297, + 301, + 304, + 305, + 307, + 308, + 313, + 317, + 319, + 321, + 327, + 330, + 331, + 332, + 334, + 336, + 338, + 341, + 342, + 347, + 348, + 351, + 352, + 353, + 354, + 357, + 360, + 368, + 371, + 376, + 377, + 378, + 379, + 381, + 387, + 388, + 391, + 392, + 393, + 394, + 401, + 403, + 405, + 406, + 408, + 410, + 411, + 413, + 416, + 417, + 420, + 422, + 423, + 425, + 427, + 432, + 435, + 436, + 437, + 438, + 440, + 443, + 447, + 449, + 451, + 455, + 457, + 460, + 461, + 463, + 464, + 466, + 467, + 472, + 476, + 478, + 484, + 486, + 492, + 495, + 496, + 499, + 504, + 511, + 517, + 528, + 547, + 551, + 558, + 559, + 585, + 597, + 603, + 615, + 622, + 634, + 639, + 651, + 657 + ] + }, + "removed": [ + [ + 2398, + "MOVE", + 472, + 1 + ], + [ + 2405, + "MOVE", + 473, + 1 + ], + [ + 2412, + "MOVE", + 474, + 1 + ], + [ + 2419, + "MOVE", + 475, + 1 + ], + [ + 2426, + "MOVE", + 476, + 1 + ], + [ + 2433, + "MOVE", + 477, + 1 + ], + [ + 2440, + "MOVE", + 478, + 1 + ], + [ + 2447, + "MOVE", + 479, + 1 + ], + [ + 2454, + "MOVE", + 480, + 1 + ], + [ + 4873, + "COPY", + 480, + 7 + ], + [ + 4938, + "COPY", + 479, + 7 + ], + [ + 4995, + "COPY", + 478, + 7 + ], + [ + 5052, + "COPY", + 477, + 7 + ], + [ + 5117, + "COPY", + 476, + 7 + ], + [ + 5182, + "COPY", + 475, + 7 + ], + [ + 5239, + "COPY", + 474, + 7 + ], + [ + 5296, + "COPY", + 473, + 7 + ], + [ + 5353, + "COPY", + 472, + 7 + ] + ], + "retained_inputs": 652, + "scalar_events": 25891, + "word_sha256": "265c58356ced52b4d4345b5872aa225db373e96739de6c8d90b087a900db3588" + }, + "separate_columns": { + "columns": 662, + "method": "One Boolean input at a time; bytearray state; no symbolic row algebra" + }, + "source_inputs_authenticated": 13, + "status": "PASS_BIT_NINE_OWNED_RELATIONS_00344412_NO_NEW_MULTIPLICATION_KAPPA" +} diff --git a/research/bit-nine-owned-relations/SOURCES.json b/research/bit-nine-owned-relations/SOURCES.json new file mode 100644 index 0000000000..ff523a2966 --- /dev/null +++ b/research/bit-nine-owned-relations/SOURCES.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "base_commit": "d277c97824e50782da6adbc486ca3c76c8fc687e", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b288ae44032fd84dd5564243422836cbcd29835e", + "sha256": "f9ed52bb642cd1e1486cf2743557ac5fa23cf1514a3277d786a644e39a565038" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/higher-moment-strictification/verify.py", + "usage": "input", + "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699", + "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "usage": "input", + "git_blob": "8b40135a84e7f0f0cd44bed69655801310b916a7", + "sha256": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85" + }, + { + "path": "research/kappa-backward-controller-20261023/RESULT.json", + "usage": "input", + "git_blob": "32b2b214ae108046bb68a507939ecb8c28c4ba92", + "sha256": "9b65013f63f616f12f4bb4d96ac75429452fad8680cada4bfd570e001fcd9a34" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "usage": "input", + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + }, + { + "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "usage": "input", + "git_blob": "a58774e237c9362869a60a22bda35be09fb85872", + "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443" + }, + { + "path": "research/kappa-rebuild/bit/mixed_productive_bit.py", + "usage": "input", + "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96", + "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e" + }, + { + "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/records/249-records.bin", + "usage": "input", + "git_blob": "bdf9ab4ca0fd74cde6837f95f5f4e88133704e0e", + "sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a" + }, + { + "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/records/frames.json", + "usage": "input", + "git_blob": "a9a932b9268da28af9ba4bccdab205c5bcd50ad3", + "sha256": "d006b3bfe0c04afecfea7aecfa59dfe4298b99501c70da3938e40289bc2f5010" + }, + { + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "usage": "input", + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15" + }, + { + "path": "research/query-thinned-controllers/BIT-CONTROLLER.json", + "usage": "input", + "git_blob": "89c400d5970024b3debe870c36ce43889beed001", + "sha256": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d" + }, + { + "path": "research/query-thinned-controllers/PROOF.md", + "usage": "input", + "git_blob": "9068f429896112082664455ab00bab083c99d1d8", + "sha256": "5ade59641f2ed70d045d6f60e89db7d979b1d1e9967f3acbe5c56eac81312841" + }, + { + "path": "research/query-thinned-controllers/verify.py", + "usage": "input", + "git_blob": "f1114036fff66f57014e5c1256141fb78ff4c4a9", + "sha256": "07dea601d6bbaa4d90e576f20c8607c37fb01e8778c798d919fa9df435049950" + } + ] +} diff --git a/research/bit-nine-owned-relations/TASK.json b/research/bit-nine-owned-relations/TASK.json new file mode 100644 index 0000000000..742ca9f9c7 --- /dev/null +++ b/research/bit-nine-owned-relations/TASK.json @@ -0,0 +1,71 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "d277c97824e50782da6adbc486ca3c76c8fc687e", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Own nine initial BIT helper relations in the PR589 reverse word; remove nine rank-one transitions and nine rank-seven COPY jobs; debit nine rank-eight helper targets; admit the complete BIT component at 0.00344412. The complete multiplication kappa does not increase.", + "scope_change_reason": "The user asked to generalize the owned-helper relation method. This applies the method to the current retained BIT supplier and keeps every retained helper autonomous. It does not change the abstract H2/K operation alphabet.", + "bottleneck_link": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19154639", + "budget_minutes": 120, + "stop_rule": "Stop this package after the exact local endpoint, both source directions, complete BIT cost and source-bound replay pass. Do not claim a complete multiplication improvement from extra BIT headroom.", + "outcome": "completed", + "evidence": "RESULT.json, WORD.json.gz, exact row and separate column replays, rational native charts, full compiler/cover and outer arithmetic.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents.", + "open_questions": [ + { + "question": "Can a different BIT relation space remove more paid work after all nine COPY jobs are zero?", + "why_it_matters": "A smaller BIT bill can support a future stronger complex supplier.", + "first_step": "Check active claims, then derive a new relation space from the emitted word and charge each lost target.", + "blocked_by": "The current nine COPY jobs are already removed; no additional saving is proved." + }, + { + "question": "Can a complete complex supplier exceed the new BIT endpoint?", + "why_it_matters": "The complex side still limits the complete multiplication exponent.", + "first_step": "Use a source-bound complex word with a complete caller and native bill.", + "blocked_by": "No such improvement is supplied by this package." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19154639", + "distinct_scope": "BIT local helper relations; does not take the coupled complex caller in Discussion 4930." + } +} diff --git a/research/bit-nine-owned-relations/VERIFY.json b/research/bit-nine-owned-relations/VERIFY.json new file mode 100644 index 0000000000..ed003ddfa0 --- /dev/null +++ b/research/bit-nine-owned-relations/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/higher-moment-strictification/verify.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "research/kappa-backward-controller-20261023/RESULT.json", + "research/kappa-rebuild/architecture/mixed_target_probe.py", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "research/kappa-rebuild/bit/mixed_productive_bit.py", + "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz", + "research/kappa-rebuild/bit/sources/pr589-regenerated/records/249-records.bin", + "research/kappa-rebuild/bit/sources/pr589-regenerated/records/frames.json", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "research/query-thinned-controllers/BIT-CONTROLLER.json", + "research/query-thinned-controllers/PROOF.md", + "research/query-thinned-controllers/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticate exact sources; rebuild the owned program; check all symbolic rows and all 662 Boolean input columns; check rational frames and port routes; replay the p16 controller; verify both complete invoices, two exact moment engines, compiler, cover, ordinary BIT and unchanged outer endpoint; reject semantic mutations." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Repeat the same complete checks with Python assertions disabled." + } + ] +} diff --git a/research/bit-nine-owned-relations/WORD.json.gz b/research/bit-nine-owned-relations/WORD.json.gz new file mode 100644 index 0000000000..19caa85e45 Binary files /dev/null and b/research/bit-nine-owned-relations/WORD.json.gz differ diff --git a/research/bit-nine-owned-relations/local.py b/research/bit-nine-owned-relations/local.py new file mode 100644 index 0000000000..8fb7f48ebd --- /dev/null +++ b/research/bit-nine-owned-relations/local.py @@ -0,0 +1,249 @@ +"""Own nine BIT helper relations and check all input columns. + +The source word is due to DreamingOfClouds, eumemic and their predecessors. +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from pathlib import Path +import gzip +import importlib.util +import json +import struct +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / 'research/kappa-rebuild/bit/sources/pr589-regenerated' +SIZE, PORTS = 661, 111 +OLD_PAID = {1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19} +NEW_PAID = {1:1314, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:10} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, ROOT / path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def source(): + word = json.loads(gzip.decompress((SOURCE / 'WORD.json.gz').read_bytes())) + records = list(struct.iter_unpack('<6i', (SOURCE / 'records/249-records.bin').read_bytes())) + frames = json.loads((SOURCE / 'records/frames.json').read_text())['frames'] + return word, records, frames + + +def relations(word, records): + rows = [1 << i for i in range(SIZE)] + [0] + result = [] + for op, x, y, coefficient, frame, _ in reversed(records): + if op == 1 and coefficient & 1: + rows[x] ^= rows[y] + elif op == 3: + need(y == SIZE and rows[SIZE] == 0, 'Source COPY entrance') + result.append(rows[x]) + rows[SIZE] = rows[x] + elif op == 2: + need(y == SIZE and rows[x] == rows[SIZE], 'Source COPY exit') + rows[SIZE] = 0 + want = [(1 << i) ^ ((1 << (i-PORTS)) if PORTS <= i < 2*PORTS else 0) + for i in range(SIZE)] + [0] + need(rows == want and len(result) == 9, 'Source reverse identity and all nine COPY forms') + basis = {} + for row in result: + for pivot, value in sorted(basis.items()): + if row >> pivot & 1: + row ^= value + helpers = row >> (2*PORTS) + need(helpers != 0, 'Each relation has a new helper pivot') + pivot = 2*PORTS + (helpers & -helpers).bit_length()-1 + for old in list(basis): + if basis[old] >> pivot & 1: + basis[old] ^= row + basis[pivot] = row + need(len(basis) == 9, 'Nine independent helper relations') + pivots = sum(1 << i for i in basis) + for pivot, row in basis.items(): + need(row & pivots == 1 << pivot, 'Reduced helper basis') + need(all(word['final'][i] == 1 for i in range(SIZE) if row >> i & 1), + 'Every relation input has the full entrance frame') + return dict(sorted(basis.items())) + + +def construct(word, records, basis): + frames = list(word['final']) + [None] + rows = [1 << i for i in range(SIZE+1)] + program = [['CLEAR', SIZE, None]] + rows[SIZE] = 0 + for pivot, row in basis.items(): + program.append(['CLEAR', pivot, 1]) + rows[pivot] = 0 + for i in range(SIZE): + if i != pivot and row >> i & 1: + program.append(['ADD', pivot, i, 1]) + rows[pivot] ^= rows[i] + removed = [] + for index, (op, x, y, a, b, _) in enumerate(reversed(records)): + if op == 0: + old, new, rank = a, y, b + need(frames[x] == old, 'Source MOVE entrance') + if rows[x]: + program.append(['MOVE', x, old, new, rank]) + else: + program.append(['ZERO_MOVE', x, old, new]) + if rank: + removed.append([index, 'MOVE', x, rank]) + frames[x] = new + elif op == 1: + need(frames[x] == frames[y] == b, 'Source ADD frame') + if a & 1: + rows[x] ^= rows[y] + program.append(['ADD', x, y, b]) + elif op == 3: + need(y == SIZE and frames[x] == a and rows[x] == rows[SIZE] == 0, + 'All nine source COPY values are zero') + program.append(['CLEAR', SIZE, b]) + frames[SIZE] = b + removed.append([index, 'COPY', x, 7]) + else: + need(op == 2 and y == SIZE and rows[x] == rows[SIZE] == 0, + 'Zero COPY close') + program.append(['CLEAR', SIZE, None]) + frames[SIZE] = None + for pivot in basis: + program.append(['CLEAR', pivot, word['start'][pivot]]) + return program, removed + + +def replay(word, program, basis): + owned = set(basis) | {SIZE} + rows = [1 << i for i in range(SIZE+1)] + frames = list(word['final']) + [None] + paid = Counter() + largest_row = 1 + for event in program: + op, role = event[:2] + if op == 'CLEAR': + need(role in owned, 'Only an owned field can be cleared') + rows[role], frames[role] = 0, event[2] + elif op == 'ADD': + _, dst, src, frame = event + need(dst != src and frames[dst] == frames[src] == frame, 'Common-frame XOR') + rows[dst] ^= rows[src] + largest_row = max(largest_row, rows[dst].bit_count()) + elif op in ('MOVE', 'ZERO_MOVE'): + _, role, old, new, *rank = event + need(frames[role] == old, 'Native MOVE entrance') + if op == 'ZERO_MOVE': + need(rows[role] == 0, 'Only a zero value can change frame for free') + elif rank[0]: + paid[rank[0]] += 1 + frames[role] = new + else: + raise ValueError('Unknown local operation') + for i, row in enumerate(rows): + expected = 0 if i in owned else (1 << i) ^ ((1 << (i-PORTS)) if PORTS <= i < 2*PORTS else 0) + need(row == expected, 'Every retained and arbitrary owned entry column') + need(frames[:SIZE] == word['start'] and frames[SIZE] is None, 'All exit frames') + need(dict(paid) == NEW_PAID, 'Exact changed local paid profile') + return {'paid': dict(sorted(paid.items())), 'helpers': {8:439-len(basis)}, + 'retained_inputs': SIZE-len(basis), 'arbitrary_owned_entries': len(owned), + 'events': len(program), 'scalar_events': sum(e[0] in ('ADD', 'CLEAR') for e in program), + 'maximum_binary_row_weight': largest_row, + 'word_sha256': sha256(json.dumps(program, separators=(',', ':')).encode()).hexdigest()} + + +def native(word, records, frame_data): + load('research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py', 'joint_pair_dag') + module = load('research/kappa-rebuild/bit/mixed_productive_bit.py', 'bit_source_geometry') + projectors = module.frame_projectors(frame_data) + dims = {int(f): row['dim'] for f, row in frame_data.items()} + pairs = {(e[2], e[3], e[4]) for e in records if e[0] == 0} + for a, b, rank in pairs: + p, q = projectors[a], projectors[b] + need(module.matrix_multiply(p, q) == p == module.matrix_multiply(q, p), 'Nested exact projectors') + need(dims[b]-dims[a] == rank, 'Every original and reversed child rank') + multiply = module.matrix_multiply + def eye(n): + return [[Fraction(i == j) for j in range(n)] for i in range(n)] + def swap(p): + return [[Fraction(int(i == j)-(p[i][j] if i < 8 and j < 8 else p[i-8][j-8]) + if (i < 8) == (j < 8) else p[i][j-8] if i < 8 else p[i-8][j]) + for j in range(16)] for i in range(16)] + for port in range(PORTS): + p = projectors[word['start'][port]] + complement = [[Fraction(i == j)-p[i][j] for j in range(8)] for i in range(8)] + need(dims[word['start'][port]] == 1 and word['start'][port+PORTS] == 0, + 'Actual main entrance line and empty frame') + need(word['final'][port] == 1 and projectors[word['final'][port+PORTS]] == complement, + 'Actual main full frame and complement') + q = list(map(Fraction, word['lines'][port])) + need(sum(x*x for x in q) == 4 and p == [[x*y/4 for y in q] for x in q], + 'Source root and actual entrance projector') + u = [Fraction(i == 0)-q[i]/2 for i in range(8)] + norm = sum(x*x for x in u) + g = eye(8) if norm == 0 else [[Fraction(i == j)-2*u[i]*u[j]/norm for j in range(8)] for i in range(8)] + a = [row[1:] for row in g] + at = list(map(list, zip(*a))) + need(multiply(at,a) == eye(7) and multiply(a,at) == complement, 'Fresh exact complement basis') + rho = [p[i]+a[i] for i in range(8)] + [row+[Fraction(0)]*7 for row in at] + full = [[Fraction(i == j and i < 8) for j in range(15)] for i in range(15)] + active = [[p[i][j] if i < 8 and j < 8 else Fraction(i == j and i >= 8) for j in range(15)] for i in range(15)] + central = [[p[i][j] if i < 8 and j < 8 else Fraction(0) for j in range(15)] for i in range(15)] + need(multiply(rho,rho) == eye(15), 'Fresh port route is an involution') + need(multiply(multiply(rho,full),rho) == active, 'Every port route maps the full local projector to the next active block') + need(multiply(multiply(rho,central),rho) == central, 'Every route fixes the central query projector') + need(multiply(swap(eye(8)),swap(p)) == swap(complement), 'Exact address map D_I D_P equals D_K') + need(multiply(swap(p),swap(p)) == eye(16) and multiply(swap(complement),swap(complement)) == eye(16), + 'Both physical address factors are involutions') + need(all(word['start'][i] == 0 and word['final'][i] == 1 for i in range(2*PORTS, SIZE)), + 'Every retained helper has a rank-eight target') + return {'rational_projectors': len(projectors), 'nested_transition_pairs': len(pairs), + 'main_involution_ports': PORTS, 'fresh_port_routes': PORTS, 'new_nonzero_native_maps': 0, + 'all_f_rule': 'Source projectors tensor I_f; the source address involutions and all GF(2) identities stay exact.', + 'full_GL_cover_executed': False} + + +def controls(word, program, basis): + bad = json.loads(json.dumps(program)) + bad.pop(next(i for i, e in enumerate(bad) if e[0] == 'CLEAR' and e[1] in basis)) + variants = {'missing_owned_entry_clear': bad} + bad = json.loads(json.dumps(program)) + bad.pop(next(i for i, e in enumerate(bad) if e[0] == 'ADD' and e[1] in basis)) + variants['changed_relation'] = bad + bad = json.loads(json.dumps(program)) + bad.pop(max(i for i, e in enumerate(bad) if e[0] == 'CLEAR' and e[1] in basis)) + variants['missing_owned_exit_clear'] = bad + bad = json.loads(json.dumps(program)) + i = next(i for i, e in enumerate(bad) if e[0] == 'MOVE' and e[-1] > 0) + bad[i] = ['ZERO_MOVE'] + bad[i][1:4] + variants['unearned_free_transition'] = bad + failures = {} + for name, bad in variants.items(): + try: + replay(word, bad, basis) + except ValueError as error: + failures[name] = str(error) + else: + raise ValueError('Accepted local mutation: ' + name) + return failures + + +def run(): + word, records, frames = source() + basis = relations(word, records) + program, removed = construct(word, records, basis) + result = replay(word, program, basis) + need(Counter(e[-1] for e in removed) == {1:9, 7:9}, 'All removed jobs and no others') + result.update({'relation_basis': {str(p): [i for i in range(SIZE) if row >> i & 1] for p, row in basis.items()}, + 'removed': removed, 'native': native(word, records, frames), + 'negative_controls': controls(word, program, basis)}) + return result, program diff --git a/research/bit-nine-owned-relations/price.py b/research/bit-nine-owned-relations/price.py new file mode 100644 index 0000000000..7257ce9112 --- /dev/null +++ b/research/bit-nine-owned-relations/price.py @@ -0,0 +1,232 @@ +"""Price the complete BIT controller, cover and compiler. + +The controller and tail proof follow Cinna Davis, zxv and the retained +mixed-target work of Jacob Alan Sussman. Apache-2.0. +Ali Romman with substantial OpenAI Codex assistance. +""" +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path +import json +import local as L + +TESTED, UNIFORM = Q('.0034678'), Q('.0034668') +AFTER, ATOM, OLD_ORDINARY = Q('.0034578'), Q('.004'), Q('.0000384599') +ADMITTED = Q('.00344412') + + +def encode(value): + if isinstance(value, Q): + return str(value) + if isinstance(value, dict): + return {str(k):encode(v) for k,v in value.items()} + if isinstance(value, (tuple, list)): + return [encode(v) for v in value] + return value + + +def controller(word): + n = 2*word['pairs'] + L.need((word['kind'], n, word['prefix_pairs']) == ('bit', 32, 7), 'Source BIT p16/a7 controller') + def xor(dst, src): + for term, mask in src.items(): + value = dst.get(term, 0) ^ mask + if value: + dst[term] = value + else: + dst.pop(term, None) + def shifted(row, monomial): + return {term ^ monomial: mask for term, mask in row.items()} + def boundary(program): + rows = [1 << i for i in range(n)] + for event in program: + op, a, b = event + if op == 'ADD': + rows[a] ^= rows[b] + else: + L.need(op == 'SWAP', 'Binary boundary operation') + rows[a], rows[b] = rows[b], rows[a] + return rows + for side in ('left', 'right'): + L.need(boundary(word['boundaries'][side+'_program']) == word['boundaries'][side+'_rows'], + 'Every binary boundary coefficient') + rows = [{0:mask} for mask in word['boundaries']['right_rows']] + for event in word['physical_events']: + op = event[0] + if op in ('LOCAL', 'QUERY_SHEAR'): + _, stage, pair, reverse = event + x, y = 2*pair, 2*pair+1 + if reverse: + x, y = y, x + xor(rows[y], shifted(rows[x], 1)) + if op == 'LOCAL': + for role in (x, y): + rows[role] = shifted(rows[role], 1 << (stage+1)) + elif op == 'IDLE': + _, pair, stages = event + monomial = sum(1 << (stage+1) for stage in stages) + for role in (2*pair, 2*pair+1): + rows[role] = shifted(rows[role], monomial) + elif op == 'ADD': + xor(rows[event[1]], rows[event[2]]) + else: + L.need(op == 'SWAP', 'Physical controller operation') + rows[event[1]], rows[event[2]] = rows[event[2]], rows[event[1]] + result = [] + for mask in word['boundaries']['left_rows']: + row = {} + for i in range(n): + if mask >> i & 1: + xor(row, rows[i]) + result.append(row) + L.need(result == [{term:1 << i} for i,term in enumerate(word['diagonal'])], + 'Complete controller endpoint on all binary monomials') + return {'parent_inputs_per_port': n, 'physical_events': len(word['physical_events']), + 'full_calls': sum(e[0] == 'LOCAL' for e in word['physical_events']), + 'thin_calls': sum(e[0] == 'QUERY_SHEAR' for e in word['physical_events'])} + + +def invoice(word, paid, helpers): + targets, children = Counter(), Counter() + for event in word['physical_events']: + if event[0] == 'LOCAL': + targets.update(helpers) + children.update(paid) + elif event[0] == 'QUERY_SHEAR': + children[1] += L.PORTS + elif event[0] == 'IDLE': + children[7*len(event[2])] += 2*L.PORTS + for term in word['diagonal']: + L.need(term & 1, 'Every main target retains its central direction') + targets[1+7*(term >> 1).bit_count()] += L.PORTS + return targets, children + + +def tail(E, T, P, tested, uniform): + t, u, v, cutoff, floor = 1-tested, Q(1, 5), 1024, 17, 18 + target, paid = E.moment(T, t), E.moment(P, t) + alpha = E.divide(paid, target) + second = L.load('research/kappa-rebuild/architecture/mixed_target_probe.py', 'bit_relation_second_moments') + tl, th = second.moment(T, tested) + pl, ph = second.moment(P, tested) + L.need(tl > ph and max(tl, target[0]) <= min(th, target[1]) + and max(pl, paid[0]) <= min(ph, paid[1]), 'Two exact moment engines agree') + gamma = E.divide(E.moment(P, t+u), E.mul(E.power(cutoff, u), target)) + delta = E.divide((Q(sum(T.values())*floor),)*2, E.mul(E.power(cutoff, tested), target)) + reserve = Q(1, 250000) + L.need(alpha[1] < 1-reserve and gamma[1] < Q(31, 32) and delta[1] < Q(19, 20), + 'All three charged compiler ratios') + L.need(Q(31,32)**128 < Q(1,16) and Q(19,20)**128 < Q(1,16), 'Strict tail decay blocks') + surplus = 1-Q(1)/(1+v*reserve)-Q(4, 2**32) + L.need(surplus > 0 and cutoff**64 < floor**63 and max(T) < 256, + 'Completion, splitting and rounding surplus') + h = Q(1,64) + z, z0 = 1-uniform, (t+1-uniform)/2 + gap = z0-t + B, debt = (5+8*h)*v, 1+8*v*(1-z0) + x = (gap*B+debt)/(h*gap) + H0 = -((-x.numerator)//x.denominator) + x = H0*(1-z0)/(z-z0) + H1 = x.numerator//x.denominator+1 + L.need(H0 >= 8*v and H0*h*gap >= gap*B+debt and (H0-1)*h*gap < gap*B+debt, + 'Exact first compiler threshold') + L.need(H1*(z-z0) > H0*(1-z0) >= (H1-1)*(z-z0), 'Exact strict uniform threshold') + return {'tested': tested, 'uniform': uniform, 'alpha': E.display(alpha), + 'gamma': E.display(gamma), 'delta': E.display(delta), 'reserve': reserve, + 'tensor_power': v, 'cutoff': cutoff, 'floor': floor, + 'normalized_surplus_lower': surplus, 'H0': H0, 'H1': H1, + 'uniform_N': '2^'+str(H1), 'winning_word_materialized': False} + + +def root(E, T, P): + def margin(kappa): + a, b = E.moment(T, 1-kappa), E.moment(P, 1-kappa) + return a[0]-b[1], a[1]-b[0] + lo, hi, grid = 0, 10**10, 10**12 + while hi-lo > 1: + mid = (lo+hi)//2 + if margin(Q(mid,grid))[0] > 0: + lo = mid + else: + hi = mid + L.need(margin(Q(lo,grid))[0] > 0 > margin(Q(hi,grid))[1], 'Exact raw moment crossing') + return [Q(lo,grid), Q(hi,grid)] + + +def run(local): + word = json.loads((L.ROOT/'research/query-thinned-controllers/BIT-CONTROLLER.json').read_text()) + replay = controller(word) + L.need((replay['full_calls'], replay['thin_calls']) == (18,15), 'All full and thin calls counted') + T, P = invoice(word, local['paid'], local['helpers']) + oldT, oldP = invoice(word, L.OLD_PAID, {8:439}) + old_invoice = word['invoice'] + L.need(oldT == Counter({int(k):v for k,v in old_invoice['targets'].items()}) + and oldP == Counter({int(k):v for k,v in old_invoice['paid'].items()}), + 'Independent reconstruction of the complete predecessor invoice') + L.need(oldP-P == {1:162,7:162} and oldT-T == {8:162}, 'All eighteen local exchanges and target debits') + difference = {r:(P[r]-T[r])-(oldP[r]-oldT[r]) for r in set(P)|set(T)|set(oldP)|set(oldT)} + difference = {r:n for r,n in difference.items() if n} + concave = {k:sum(n*min(r,k) for r,n in difference.items()) for k in sorted(difference)} + L.need(all(v <= 0 for v in concave.values()) and min(concave.values()) < 0, + 'Exact uniform improvement for every strict concave rank power') + E = L.load('research/higher-moment-strictification/verify.py', 'bit_relation_exact_moments') + new_tail = tail(E, T, P, TESTED, UNIFORM) + old_tail = tail(E, oldT, oldP, Q('.00346'), Q('.003459')) + old_root, new_root = root(E, oldT, oldP), root(E, T, P) + L.need(new_root[0] > old_root[1] and TESTED < new_root[0], 'Changed raw ceiling and compiler headroom') + ordinary = (1-ATOM)*AFTER+ATOM*OLD_ORDINARY + old_ordinary = (1-ATOM)*Q('.00345')+ATOM*OLD_ORDINARY + L.need(UNIFORM-AFTER == Q('.003459')-Q('.00345') and 2**26 > 256/(UNIFORM-AFTER), + 'Same funded cover loss and finite prime rule') + L.need(ATOM > ordinary > ADMITTED > old_ordinary and ATOM < 1-ordinary, + 'Strict ordinary BIT admission and stock') + source_local_upper = 10**6 + source_scalar_events = 24305+2*9 + added_pointwise = local['scalar_events']-source_scalar_events + L.need(added_pointwise == 1568, 'All added pointwise XOR and CLEAR records') + local_bound = source_local_upper+added_pointwise + boundary = word['boundaries']['boundary_unit_ADDs_per_port'] + raw_bound = 18*local_bound+15*111*16+32*111*(len(word['physical_events'])+boundary) + L.need(raw_bound < 10**9, 'Retained source allowance plus every added record fits') + def complete_census(targets, children): + expected_targets, expected_paid = invoice(word, local['paid'], local['helpers']) + L.need(targets == expected_targets and children == expected_paid, 'Every paid job and earned target must match the literal word') + controls = {} + try: + complete_census(oldT, P) + except ValueError as error: + controls['missing_target_debit'] = str(error) + else: + raise ValueError('Accepted unearned helper targets') + a, b = E.moment(oldT,1-TESTED), E.moment(oldP,1-TESTED) + L.need(a[1] < b[0], 'The old complete bill fails at the new tested saving') + controls['old_word_at_new_saving'] = 'Rejected by the exact raw moment' + complex_receipt = json.loads((L.ROOT/'research/kappa-backward-controller-20261023/RESULT.json').read_text())['arithmetic'] + params = {k:Q(v) for k,v in complex_receipt['outer']['parameters'].items()} + params['bit_saving'] = ADMITTED + engine = L.load('research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py', 'bit_relation_complete_outer') + outer = engine.ledger(params) + outer['functional_checks']['actual_new_BIT_stock_sublinear'] = params['beta']*(1-ATOM) + L.need(0 < params['beta']*(1-ATOM) < params['beta'] < 1, + 'The actual BIT row stock is sublinear in its active group') + L.need(len(outer['strict_checks']) == 54 and len(outer['functional_checks']) == 4, 'All outer predicates are present') + L.need(all(v > 0 for group in ('strict_checks','functional_checks') for v in outer[group].values()), + 'The complete unchanged multiplication endpoint still passes') + L.need(params['kappa'] == Q('.00302728823'), 'No new multiplication kappa is claimed') + return encode({'controller': replay, 'targets': T, 'paid': P, + 'target_count': sum(T.values()), 'paid_count': sum(P.values()), + 'rank_credit': sum(r*n for r,n in T.items()), 'rank_bill': sum(r*n for r,n in P.items()), + 'signed_delta': difference, 'concave_order_certificate': concave, + 'old_raw_root': old_root, 'new_raw_root': new_root, + 'old_compiler': old_tail, 'new_compiler': new_tail, + 'ordinary_BIT': {'old_ordinary':old_ordinary, 'new_ordinary':ordinary, + 'gain_at_matched_parameters':ordinary-old_ordinary, + 'admitted':ADMITTED, 'atom':ATOM, 'after_cover':AFTER, + 'prime_rule':'Odd q > 2^26*N^5, avoiding all fixed denominators and rank witnesses'}, + 'budgets':{'inherited_source_local_upper':source_local_upper, + 'added_pointwise_records_per_call':added_pointwise, + 'local_scalar':local['scalar_events'], 'local_complete_upper':local_bound, + 'complete_raw_nonrecursive':raw_bound,'raw_allowance':10**9}, + 'negative_controls':controls, 'outer_at_unchanged_complex_endpoint':outer, + 'complete_multiplication_kappa_improvement':False, + 'binding_constraint':'The complex supplier remains below this BIT saving.'}) diff --git a/research/bit-nine-owned-relations/verify.py b/research/bit-nine-owned-relations/verify.py new file mode 100644 index 0000000000..19adda84c1 --- /dev/null +++ b/research/bit-nine-owned-relations/verify.py @@ -0,0 +1,92 @@ +"""Check the nine-relation BIT supplier and its complete conditional cost. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from hashlib import sha1, sha256 +from pathlib import Path +import gzip +import json +import sys + +sys.dont_write_bytecode = True +import local as L +import price as P + + +def authenticate(): + count = 0 + for row in json.loads((L.HERE/'SOURCES.json').read_text())['files']: + if row['usage'] != 'input': + continue + raw = (L.ROOT/row['path']).read_bytes() + L.need(sha256(raw).hexdigest() == row['sha256'], 'Changed source: '+row['path']) + L.need(sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'], + 'Changed source Git object: '+row['path']) + count += 1 + return count + + +def columns(program, pivots): + owned = set(pivots) | {L.SIZE} + for column in range(L.SIZE+1): + state = bytearray(L.SIZE+1) + state[column] = 1 + for event in program: + op = event[0] + if op == 'CLEAR': + state[event[1]] = 0 + elif op == 'ADD': + state[event[1]] ^= state[event[2]] + elif op == 'ZERO_MOVE': + L.need(state[event[1]] == 0, 'Separate column replay: zero transport') + else: + L.need(op == 'MOVE', 'Separate column replay: known operation') + expected = bytearray(L.SIZE+1) + if column not in owned: + expected[column] = 1 + if column < L.PORTS: + expected[column+L.PORTS] = 1 + L.need(state == expected, 'Separate Boolean replay of every retained and owned column') + return {'columns': L.SIZE+1, 'method':'One Boolean input at a time; bytearray state; no symbolic row algebra'} + + +def run(): + pins = authenticate() + local, program = L.run() + column_check = columns(program, map(int, local['relation_basis'])) + price = P.run(local) + result = {'status':'PASS_BIT_NINE_OWNED_RELATIONS_00344412_NO_NEW_MULTIPLICATION_KAPPA', + 'source_inputs_authenticated':pins, 'local':local, 'separate_columns':column_check, + 'complete_cost':price, + 'limits':['The complex supplier still limits the complete multiplication bound.', + 'Native all-column, owned-erasure, compiler, precision/tape and analytic recovery premises remain conditional.', + 'The full GL cover, winning uniform word and complete integer multiplier are not materialized.', + 'No Lean or proof-kernel check is included.']} + artifact = {'schema':'bit-nine-owned-relations/1', 'source_word_sha256':L.sha256((L.SOURCE/'WORD.json.gz').read_bytes()).hexdigest(), + 'owned':sorted([int(p) for p in local['relation_basis']]+[L.SIZE]), + 'program':program} + return P.encode(result), artifact + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result, artifact = run() + if args.write: + (L.HERE/'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + (L.HERE/'WORD.json.gz').write_bytes(gzip.compress(json.dumps(artifact, separators=(',',':')).encode(), mtime=0)) + else: + L.need(json.loads((L.HERE/'RESULT.json').read_text()) == result, 'Frozen complete result') + L.need(json.loads(gzip.decompress((L.HERE/'WORD.json.gz').read_bytes())) == artifact, 'Frozen emitted word payload') + print(result['status']) + print(json.dumps({'retained_inputs':result['local']['retained_inputs'], + 'owned_entries':result['local']['arbitrary_owned_entries'], + 'paid_calls':result['complete_cost']['paid_count'], + 'productive_fields':result['complete_cost']['target_count'], + 'ordinary_BIT':result['complete_cost']['ordinary_BIT']}, sort_keys=True)) + + +if __name__ == '__main__': + main()