diff --git a/research/p104-two-handoffs/LITERAL-CHANGES.diff b/research/p104-two-handoffs/LITERAL-CHANGES.diff new file mode 100644 index 0000000000..d2e0fcf73d --- /dev/null +++ b/research/p104-two-handoffs/LITERAL-CHANGES.diff @@ -0,0 +1,114 @@ +--- closure/research/p104-productive-controller/local.py ++++ p104-two-handoffs/local.py +@@ -107,19 +107,19 @@ + program.append(['INIT' if op == 'private_init' else 'CLEAR', e['register'], frame(e['frame'])]) + else: + program.append([{'add':'ADD', 'scale':'SCALE', 'private_copy':'COPY'}[op], *e['registers'], e['coefficient'], frame(e['frame'])]) +- return {'schema':'p104-productive-source/1', 'public':735, 'live':live, 'ports':built['ports'], ++ return {'schema':'p104-productive-source/1', 'public':737, 'live':live, 'ports':built['ports'], + 'frames':frames, 'initial':initial, 'final':final, 'program':program} + + + def replay(w): + need(len(w['program']) < 26000, 'Fixed operation bound') + frames = [span(x) for x in w['frames']] +- rows = [{r:Q(1)} for r in range(743)] ++ rows = [{r:Q(1)} for r in range(745)] + current = list(w['initial']) + [None]*8 + paid, scalar, live_owned, peak = Counter(), 0, set(), 0 + for e in w['program']: + op, r = e[:2] +- need(0 <= r < 743, 'Role index') ++ need(0 <= r < 745, 'Role index') + if op == 'MOVE': + _, r, a, b, private = e + need(current[r] == a and (r in live_owned) == private, 'Transport source and ownership') +@@ -127,7 +127,7 @@ + paid[abs(len(w['frames'][b])-len(w['frames'][a]))] += 1 + current[r] = b + elif op == 'INIT': +- need(r >= 735 and r not in live_owned, 'Owned initialization') ++ need(r >= 737 and r not in live_owned, 'Owned initialization') + live_owned.add(r) + peak = max(peak, len(live_owned)) + rows[r] = {} +@@ -151,7 +151,7 @@ + scalar += 2*(abs(n.bit_length()-d.bit_length()) + int(q < 0)) + else: + s = e[2] +- need(s != r and 0 <= s < 743 and current[s] == f, 'Common scalar chart') ++ need(s != r and 0 <= s < 745 and current[s] == f, 'Common scalar chart') + if op == 'COPY': + need(r in live_owned and not rows[r], 'COPY into cleared owned field') + rows[r] = {k:q*x for k,x in rows[s].items()} +@@ -159,23 +159,23 @@ + need(op == 'ADD', 'Scalar opcode') + add(rows[r], rows[s], q) + scalar += 2*(3+n.bit_length()-1+n.bit_count()+d.bit_length()-1) +- need(not live_owned and peak == 1 and current[:735] == w['final'], 'All public and owned exits') ++ need(not live_owned and peak == 1 and current[:737] == w['final'], 'All public and owned exits') + live = set(w['live']) + for r,row in enumerate(rows): +- expected = {r:Q(1)} if r < 735 else {} ++ expected = {r:Q(1)} if r < 737 else {} + if r-112 in live: + expected[r-112] = Q(1) +- need(row == expected, 'All 743 public and owned rows') ++ need(row == expected, 'All 745 public and owned rows') + main = live | {r+112 for r in live} +- helpers = Counter(len(w['frames'][w['final'][r]])-len(w['frames'][w['initial'][r]]) for r in range(735) if r not in main) ++ helpers = Counter(len(w['frames'][w['final'][r]])-len(w['frames'][w['initial'][r]]) for r in range(737) if r not in main) + need(len(live) == len(w['ports']) == 104 and len(main) == 208 and min(helpers) > 0, 'Independent productive inputs') +- return {'paid':dict(paid), 'helpers':dict(helpers), 'public_inputs':735, 'owned_lifetimes':8, +- 'peak_owned_fields':peak, 'real_scalar_allowance':scalar, 'endpoint_coefficients':743*743} ++ return {'paid':dict(paid), 'helpers':dict(helpers), 'public_inputs':737, 'owned_lifetimes':8, ++ 'peak_owned_fields':peak, 'real_scalar_allowance':scalar, 'endpoint_coefficients':745*745} + + + def reverse_columns(w): + """Check the transpose with dense dyadic rows and the reverse chronology.""" +- n = 743 ++ n = 745 + rows = [[int(i == j) for j in range(n)] for i in range(n)] + exponents = [0]*n + for e in reversed(w['program']): +@@ -206,7 +206,7 @@ + exponents[r] -= 1 + for r,row in enumerate(rows): + expected = [0]*n +- if r < 735: ++ if r < 737: + expected[r] = 1 << exponents[r] + if r in w['live']: + expected[r+112] = 1 << exponents[r] +@@ -234,7 +234,7 @@ + check(e[2],e[3]) + main = set(w['live']) | {r+112 for r in w['live']} + helper_profile = Counter() +- for r in range(735): ++ for r in range(737): + if r not in main: + helper_profile[check(w['initial'][r],w['final'][r])['rank']] += 1 + adapters = [] +--- p104-joint-contact/pricing.py (PR5551) ++++ p104-two-handoffs/pricing.py +@@ -11,8 +11,8 @@ + from fractions import Fraction as Q + import local as L + +-KAPPA, TESTED = Q('.00304153'), Q('.0030415305') +-PREVIOUS = Q('.00304117') ++KAPPA, TESTED = Q('.00304282'), Q('.0030428205') ++PREVIOUS = Q('.00304153') + + + def encode(x): +@@ -61,7 +61,7 @@ + second_p[8*(j+1)] += 208 + L.need((targets,paid) == (second_t,second_p), 'Independent full invoice') + L.need(max(targets) == 145 and max(paid) == 72, 'Maximum recursive ranks') +- L.need(sum(targets.values()) == 12814 and sum(paid.values()) == 69912, 'Complete field and call counts') ++ L.need(sum(targets.values()) == 12850 and sum(paid.values()) == 69912, 'Complete field and call counts') + L.need(sum(r*n for r,n in targets.items())-sum(r*n for r,n in paid.items()) == 760, 'Complete rank surplus') + return targets,paid,counts + diff --git a/research/p104-two-handoffs/README.md b/research/p104-two-handoffs/README.md new file mode 100644 index 0000000000..eecf35927c --- /dev/null +++ b/research/p104-two-handoffs/README.md @@ -0,0 +1,45 @@ +# Two successor hand-offs on the P104 word (conditional kappa .0030428242) + +Complete conditional kappa **.0030428242** (**+1.29e-6** over +[PR5551](https://github.com/CrocSwap/integer-mult-bounds/pull/5551)'s .0030415312). The claim is +tested at .0030428205; the exact raw crossing lies in +(76070606559/25000000000000, 304282426237/100000000000000) = +(.00304282426236, .00304282426237). + +**Conditional on** (a) the five framework assumptions retained by PR5544/5545/5551; (b) the validity of +PR5551, which is unreproduced at the time of writing; (c) admissibility of a fresh helper that +starts at a non-canonical mid frame. For (c): "Variant A" below passes the **unmodified** PR5545 +`local.py`, and the canonical start-frame rule exists only in the #4610 compact-width verifier. The +selected record is not changed; no independent human or proof-kernel acceptance is claimed. + +## Mechanism +Helper 473 (event 13725) and helper 531 (event 13941) finish their first rank-1 climb at a dim-2 +frame (608, 613) and then idle; no other register holds their symbol. Following the successor +hand-off pattern of PR5472, the rest of each helper's life moves to a fresh helper that starts at +that frame: 473 climbs 8 as 1+7, 531 climbs 7 as 1+6. This is a pure rename: the same 25,310 events, +no extra ADD, identical paid profile (69,912 calls, rank-mass surplus 760). Only the helper targets change (12,814 -> 12,850 productive fields, the extra rank-1 spectators being +moment-neutral): at each of the 18 calls a rank-8 climb becomes 1+7 and a rank-7 climb 1+6, and by +subadditivity the concave moment gains 1-(8^t-7^t) resp. 1-(7^t-6^t), i.e. +6.6e-7 and +6.3e-7 in kappa. + +## Files +- `handoff.py` derives `WORD.json.gz` (and Variant A `WORD-VARIANT-A.json.gz`) from PR5551's pinned word `inputs/pr5551-WORD.json.gz` (sha256 48f8734c...). +- `local.py`, `pricing.py` are PR5545/5551's files with ONLY literal changes: 735->737 public inputs, 743->745 rows, targets 12814->12850, kappa constants. See `LITERAL-CHANGES.diff`; `verify.py` re-applies the substitutions and checks byte equality. +- Variant A: the two helpers' leading MOVE is deleted and they start at frames 608/613 (public stays 735). It passes the unmodified `local.py`/native/caller; only the call-count literal in pricing changes (69,912 -> 69,876), and the crossing is identical. +- `verify.py` / `verify.sh` (stdlib, Python 3.12, a few minutes): both words, replay, transpose, native maps, physical caller, pricing with both moment engines, all 54 strict + 4 functional outer checks, exact crossing interval. `--write` refreshes `RESULT.json`. +- `inputs/pr5545-source-closure.tar.gz` is PR5551's byte-pinned capsule (`SOURCES.json`). + +## Independent audit +An internal AI audit (separate read-only Claude agent, own builder and pipeline) found the literal +edits identical, the word byte-equal, extra targets double-count free, and reproduced the crossing +.003042824262. It rated legality of the mid-frame start as unresolved, which is why this is conditional. + +## Credits +Builds on PR5551 (thu-nmrc), the successor hand-off pattern of PR5472 (GamingPuzzled), and the P104 +word line of PR5544/5545 (aliromman; lineage PR2305/2152/2219). All predecessor credit is retained. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. + +## Open next questions + +- Is a fresh helper starting at a non-canonical mid frame admissible? The gain depends on it; Variant A passes the unmodified PR5545 `local.py`, and the canonical-start rule exists only in the #4610 compact-width verifier. +- Independent reproduction of PR5551, on which this package builds. diff --git a/research/p104-two-handoffs/RESULT.json b/research/p104-two-handoffs/RESULT.json new file mode 100644 index 0000000000..6aff82c1a4 --- /dev/null +++ b/research/p104-two-handoffs/RESULT.json @@ -0,0 +1,453 @@ +{ + "conditions": [ + "The five framework assumptions retained by PR5544/5545/5551.", + "PR5551's validity (unreproduced at time of writing).", + "Admissibility of a fresh helper starting at a non-canonical mid frame (Variant A passes the unmodified local.py; canonical-start rule exists only in the #4610 compact-width verifier)." + ], + "crossing_kappa_decimal": ".0030428242", + "crossing_kappa_interval": [ + "76070606559/25000000000000", + "304282426237/100000000000000" + ], + "handoff_complete_cost": { + "compiler": { + "H": 690116000000000, + "N": "2^690116000000000", + "eta": { + "lower": "0.000000183730781889947982672870", + "upper": "0.000000183730781889947982672871" + }, + "gap": "1/14000000000", + "integer_test_exponent": 49294, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "21299743/7000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "129/100000000", + "kappa": "152141/50000000", + "kappa_decimal": ".00304153", + "margin_at_previous": { + "lower": "0.321204501865110839011132155185", + "upper": "0.321204501865110839011132155186" + }, + "negative_controls": { + "old_BIT": "Rejected by outer inequalities", + "old_cutoff": "Rejected by completion-tail ratio greater than one" + }, + "nonrecursive": { + "fixed_scalar_growth_bound": "At most 2^(16*26000) before native factors; a declared constant, not an attained norm.", + "local_routes": 5338000, + "local_scalar": 217428, + "peak_owned_fields": 1, + "raw_budget": 1000000000, + "raw_scalar_upper": 184647552, + "tensor_native_growth_bound": "Each rank-r Gaussian has row l1 norm at most 2^(rf); sum of local ranks is 5894." + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "3485999999253/3500000000000", + "fixed_halo_explicit_metadata_branch": "269500000001/3500000000", + "new_BIT_row_stock_sublinear_in_active_group": "13957999997009/14000000000000", + "new_semantic_group_guard": "3/14000000000" + }, + "margins": { + "boundary_algebraic_matrix": "596392775957400517/196000000000000000000", + "fused_gaussian": "596392775872201551/196000000000000000000", + "global_coordinate_router": "10649871/3500000000", + "group_bit_router": "149098197468050387/49000000000000000000", + "group_scans": "6999999999/7000000000", + "main_transform": "596392761957400517/196000000000000000000", + "microbox_face_corrections": "269500000001/3500000000", + "polynomial_products": "13999999999/14000000000", + "sparse_union_movement": "80221392775957400517/196000000000000000000" + }, + "parameters": { + "a": "10649871/3500000000", + "b": "8519897/2800000000", + "beta": "13999999997/14000000000", + "bit_saving": "17/5000", + "cap_xi": "178221392761957400517/196000000000000000000", + "complex_uniform_saving": "21299743/7000000000", + "d": "1/14000000000", + "epsilon": "13999999999/14000000000", + "kappa": "152141/50000000", + "lambda_": "3987828719/4000000000", + "lambda_prime": "13957400517/14000000000", + "layout": "1/14000000000", + "q": "42599483/14000000000", + "r0": "1/140000000000", + "stop": "1/14000000000", + "tested_saving": "6085641/2000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "1250129/3500000000", + "actual_logarithmic_gamma_guard": "1/14000000000", + "actual_logarithmic_group_guard": "17778607259042599483/98000000000000000000", + "alpha_logarithm_absorption": "1/140000000000", + "boundary_algebraic_matrix_above_kappa": "55957400517/196000000000000000000", + "cap_above_band": "80221392761957400517/196000000000000000000", + "cap_below_cell": "17778607224042599483/196000000000000000000", + "cap_below_phase_cell_power": "213778607238042599483/196000000000000000000", + "complex_above_effective": "1/14000000000", + "complex_below_one_over_32": "78980103/2800000000", + "complex_endpoint": "1/7000000000", + "epsilon_below_one": "1/14000000000", + "epsilon_positive": "13999999999/14000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "55872201551/196000000000000000000", + "gaussian_above_main": "6957400517/98000000000000000000", + "global_coordinate_router_above_kappa": "1/3500000000", + "global_gamma_power_slack": "9/140000000000", + "group_below_dimension": "1/7000000000", + "group_bit_router_above_kappa": "17468050387/49000000000000000000", + "group_gauge_power_slack": "17778607258342599483/98000000000000000000", + "group_key_fits_record": "1/7000000000", + "group_positive": "13999999997/14000000000", + "group_scans_above_kappa": "6978700259/7000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "655924790400418148631/500000000000000000000000", + "lambda_above_internal": "1/28000000000", + "lambda_above_sigma": "3/28000000000", + "lambda_above_tau": "1/28000000000", + "lambda_prime_above_lambda": "1/28000000000", + "lambda_prime_above_leaf": "5591480103/39200000000000000000", + "leaf_saving_above_effective": "2791480103/39200000000000000000", + "main_transform_above_kappa": "41957400517/196000000000000000000", + "membership_arithmetic_fits_record": "1/14000000000", + "microbox_face_corrections_above_kappa": "269489350131/3500000000", + "microbox_halo_volume": "1106000000003/14000000000", + "new_complex_uniform_saving_above_b": "1/14000000000", + "new_semantic_guard_with_C1_one": "1/14000000000", + "polynomial_products_above_kappa": "13957400519/14000000000", + "positive_layout_slack": "1/14000000000", + "q_below_effective": "1/14000000000", + "q_below_internal": "1/14000000000", + "q_below_leaf": "5591480103/39200000000000000000", + "q_positive": "42599483/14000000000", + "short_record_fallback": "2791480103/2800000000", + "source_axis_superpolynomial": "1/14000000000", + "sparse_union_movement_above_kappa": "79625000055957400517/196000000000000000000", + "stop_below_one": "13999999999/14000000000", + "stop_positive": "1/14000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/14000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/14000000000", + "union_tag_work_per_visit_fits_record": "3/14000000000" + } + }, + "paid": { + "1": 45300, + "16": 416, + "2": 9972, + "24": 416, + "3": 7020, + "32": 416, + "4": 1998, + "40": 416, + "48": 416, + "5": 1944, + "56": 416, + "6": 306, + "64": 416, + "7": 234, + "72": 208, + "9": 18 + }, + "paid_calls": 69912, + "previous_open_pr5545": "304153/100000000", + "productive_fields": 12850, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "106559/25000000000000", + "426237/100000000000000" + ], + "raw_root_interval": [ + "76070606559/25000000000000", + "304282426237/100000000000000" + ], + "relative_gain_percent": "12900/304153", + "strictification": { + "alpha": { + "lower": "0.999999996066382069189398021044", + "upper": "0.999999996066382069189398021045" + }, + "cutoff": 17, + "delta": { + "lower": "0.966061214261917464730975868956", + "upper": "0.966061214261917464730975868957" + }, + "floor": 18, + "gamma": { + "lower": "0.965230662617852758922870305982", + "upper": "0.965230662617852758922870305983" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "6085641/2000000000" + }, + "targets": { + "1": 36, + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "4": 918, + "41": 416, + "49": 416, + "5": 648, + "57": 416, + "6": 18, + "65": 416, + "7": 432, + "73": 208, + "8": 2178, + "9": 5292 + }, + "whole_idle_jobs": 3120 + }, + "helpers_local": { + "1": 2, + "4": 51, + "5": 36, + "6": 1, + "7": 24, + "8": 121, + "9": 294 + }, + "kappa_claimed": ".00304282", + "paid_local": { + "1": 2430, + "2": 554, + "3": 390, + "4": 111, + "5": 108, + "6": 17, + "7": 13, + "9": 1 + }, + "previous_pr5551": ".00304153", + "status": "PASS_P104_TWO_HANDOFFS_CONDITIONAL_KAPPA_0030428242", + "variant_a_complete_cost": { + "compiler": { + "H": 690116000000000, + "N": "2^690116000000000", + "eta": { + "lower": "0.000000183730781889947982672870", + "upper": "0.000000183730781889947982672871" + }, + "gap": "1/14000000000", + "integer_test_exponent": 49294, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "21299743/7000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "129/100000000", + "kappa": "152141/50000000", + "kappa_decimal": ".00304153", + "margin_at_previous": { + "lower": "0.321204501865110839011132155185", + "upper": "0.321204501865110839011132155186" + }, + "negative_controls": { + "old_BIT": "Rejected by outer inequalities", + "old_cutoff": "Rejected by completion-tail ratio greater than one" + }, + "nonrecursive": { + "fixed_scalar_growth_bound": "At most 2^(16*26000) before native factors; a declared constant, not an attained norm.", + "local_routes": 5332000, + "local_scalar": 217428, + "peak_owned_fields": 1, + "raw_budget": 1000000000, + "raw_scalar_upper": 184647552, + "tensor_native_growth_bound": "Each rank-r Gaussian has row l1 norm at most 2^(rf); sum of local ranks is 5894." + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "3485999999253/3500000000000", + "fixed_halo_explicit_metadata_branch": "269500000001/3500000000", + "new_BIT_row_stock_sublinear_in_active_group": "13957999997009/14000000000000", + "new_semantic_group_guard": "3/14000000000" + }, + "margins": { + "boundary_algebraic_matrix": "596392775957400517/196000000000000000000", + "fused_gaussian": "596392775872201551/196000000000000000000", + "global_coordinate_router": "10649871/3500000000", + "group_bit_router": "149098197468050387/49000000000000000000", + "group_scans": "6999999999/7000000000", + "main_transform": "596392761957400517/196000000000000000000", + "microbox_face_corrections": "269500000001/3500000000", + "polynomial_products": "13999999999/14000000000", + "sparse_union_movement": "80221392775957400517/196000000000000000000" + }, + "parameters": { + "a": "10649871/3500000000", + "b": "8519897/2800000000", + "beta": "13999999997/14000000000", + "bit_saving": "17/5000", + "cap_xi": "178221392761957400517/196000000000000000000", + "complex_uniform_saving": "21299743/7000000000", + "d": "1/14000000000", + "epsilon": "13999999999/14000000000", + "kappa": "152141/50000000", + "lambda_": "3987828719/4000000000", + "lambda_prime": "13957400517/14000000000", + "layout": "1/14000000000", + "q": "42599483/14000000000", + "r0": "1/140000000000", + "stop": "1/14000000000", + "tested_saving": "6085641/2000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "1250129/3500000000", + "actual_logarithmic_gamma_guard": "1/14000000000", + "actual_logarithmic_group_guard": "17778607259042599483/98000000000000000000", + "alpha_logarithm_absorption": "1/140000000000", + "boundary_algebraic_matrix_above_kappa": "55957400517/196000000000000000000", + "cap_above_band": "80221392761957400517/196000000000000000000", + "cap_below_cell": "17778607224042599483/196000000000000000000", + "cap_below_phase_cell_power": "213778607238042599483/196000000000000000000", + "complex_above_effective": "1/14000000000", + "complex_below_one_over_32": "78980103/2800000000", + "complex_endpoint": "1/7000000000", + "epsilon_below_one": "1/14000000000", + "epsilon_positive": "13999999999/14000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "55872201551/196000000000000000000", + "gaussian_above_main": "6957400517/98000000000000000000", + "global_coordinate_router_above_kappa": "1/3500000000", + "global_gamma_power_slack": "9/140000000000", + "group_below_dimension": "1/7000000000", + "group_bit_router_above_kappa": "17468050387/49000000000000000000", + "group_gauge_power_slack": "17778607258342599483/98000000000000000000", + "group_key_fits_record": "1/7000000000", + "group_positive": "13999999997/14000000000", + "group_scans_above_kappa": "6978700259/7000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "655924790400418148631/500000000000000000000000", + "lambda_above_internal": "1/28000000000", + "lambda_above_sigma": "3/28000000000", + "lambda_above_tau": "1/28000000000", + "lambda_prime_above_lambda": "1/28000000000", + "lambda_prime_above_leaf": "5591480103/39200000000000000000", + "leaf_saving_above_effective": "2791480103/39200000000000000000", + "main_transform_above_kappa": "41957400517/196000000000000000000", + "membership_arithmetic_fits_record": "1/14000000000", + "microbox_face_corrections_above_kappa": "269489350131/3500000000", + "microbox_halo_volume": "1106000000003/14000000000", + "new_complex_uniform_saving_above_b": "1/14000000000", + "new_semantic_guard_with_C1_one": "1/14000000000", + "polynomial_products_above_kappa": "13957400519/14000000000", + "positive_layout_slack": "1/14000000000", + "q_below_effective": "1/14000000000", + "q_below_internal": "1/14000000000", + "q_below_leaf": "5591480103/39200000000000000000", + "q_positive": "42599483/14000000000", + "short_record_fallback": "2791480103/2800000000", + "source_axis_superpolynomial": "1/14000000000", + "sparse_union_movement_above_kappa": "79625000055957400517/196000000000000000000", + "stop_below_one": "13999999999/14000000000", + "stop_positive": "1/14000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/14000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/14000000000", + "union_tag_work_per_visit_fits_record": "3/14000000000" + } + }, + "paid": { + "1": 45264, + "16": 416, + "2": 9972, + "24": 416, + "3": 7020, + "32": 416, + "4": 1998, + "40": 416, + "48": 416, + "5": 1944, + "56": 416, + "6": 306, + "64": 416, + "7": 234, + "72": 208, + "9": 18 + }, + "paid_calls": 69876, + "previous_open_pr5545": "304153/100000000", + "productive_fields": 12814, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "106559/25000000000000", + "426237/100000000000000" + ], + "raw_root_interval": [ + "76070606559/25000000000000", + "304282426237/100000000000000" + ], + "relative_gain_percent": "12900/304153", + "strictification": { + "alpha": { + "lower": "0.999999996065785400023736094415", + "upper": "0.999999996065785400023736094416" + }, + "cutoff": 17, + "delta": { + "lower": "0.963500865319358472081773388657", + "upper": "0.963500865319358472081773388658" + }, + "floor": 18, + "gamma": { + "lower": "0.965291003254181696228005813681", + "upper": "0.965291003254181696228005813682" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "6085641/2000000000" + }, + "targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "4": 918, + "41": 416, + "49": 416, + "5": 648, + "57": 416, + "6": 18, + "65": 416, + "7": 432, + "73": 208, + "8": 2178, + "9": 5292 + }, + "whole_idle_jobs": 3120 + } +} diff --git a/research/p104-two-handoffs/SOURCES.json b/research/p104-two-handoffs/SOURCES.json new file mode 100644 index 0000000000..97b6a6a322 --- /dev/null +++ b/research/p104-two-handoffs/SOURCES.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + } + ], + "retained_source": { + "path": "research/p104-two-handoffs/inputs/pr5545-source-closure.tar.gz", + "sha256": "59768da554e11b11fae52d07f520f50684cc7a9ee0bec2873edbcd6b63814837", + "export_manifest_sha256": "0a20358f9c089be1f5606c78077314e30a72998fb3c5123848d921a8d1814e76", + "commit": "18968423711fd902aaee1099979497d55603e1dc", + "files": 33, + "source_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5545", + "note": "Byte-identical copy of the capsule retained by PR5551; used unmodified except for the literal changes in LITERAL-CHANGES.diff." + }, + "pinned_word": { + "path": "research/p104-two-handoffs/inputs/pr5551-WORD.json.gz", + "sha256": "48f8734ca9c5adf5d60ded3a5fefbc24894d2c358ed7cb30fcc0d71718599446", + "source_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5551", + "source_head": "1123635a6f63f23638df9459c994160e5e649d30", + "source_path": "research/p104-joint-contact/WORD.json.gz" + }, + "pinned_pricing": { + "path": "research/p104-two-handoffs/inputs/pr5551-pricing.py", + "source_path": "research/p104-joint-contact/pricing.py at PR5551 head" + } +} diff --git a/research/p104-two-handoffs/TASK.json b/research/p104-two-handoffs/TASK.json new file mode 100644 index 0000000000..c975e0fa24 --- /dev/null +++ b/research/p104-two-handoffs/TASK.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "actual_scope": "On PR5551's pinned P104 word, split helper 473 (8 -> 1+7, frame 608) and helper 531 (7 -> 1+6, frame 613) with the successor hand-off pattern of PR5472; pure rename, no new ADD, paid profile identical; certify the changed complete conditional moment.", + "bottleneck_link": "Each successor hand-off replaces one rank-8 (resp. rank-7) helper climb by a rank-1 plus a rank-7 (rank-6) climb at all 18 calls; by subadditivity the concave moment drops.", + "stop_rule": "Retain the conditional kappa only after exact scalar/native replay, physical caller, both moment engines and all 54 strict + 4 functional outer checks pass.", + "outcome": "completed", + "author": "DreamingOfClouds, with Claude Opus 5.5 (Anthropic), via Claude Code", + "ai_assistance": "Claude Opus 5.5 via Claude Code; an internal AI audit reproduced the result independently. No independent human or proof-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "Is a fresh helper starting at a non-canonical mid frame admissible?", + "why_it_matters": "The gain depends on it; Variant A passes the unmodified PR5545 local.py, the canonical-start rule exists only in the #4610 compact-width verifier.", + "blocked_by": "Maintainer or swarm review.", + "first_step": "Review whether verify_buffers/native admit fresh helper identity rows at a non-canonical start frame in the P104 caller; Variant A (start at 608/613, unmodified PR5545 local.py) is the test case." + } + ], + "scope_status": "changed", + "scope_change_reason": "The scalar-to-moment card asks about scalar A2 contractions on the retained word; this package instead applies two successor hand-offs (PR5472 pattern) to PR5551's P104 word, a different construction on a newer word. Recorded as changed; the card's own object is not pursued.", + "evidence": "verify.py regenerates both words from PR5551's pinned word, checks local.py/pricing.py are literal-only edits (LITERAL-CHANGES.diff), replays scalar/native/physical caller, runs both moment engines and all 54 strict + 4 functional outer checks, and certifies the exact crossing interval (76070606559/25000000000000, 304282426237/100000000000000) for the hand-off word and for Variant A on the unmodified PR5545 local.py.", + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "scalar-to-moment", + "question": "Can a changed frame itinerary remove a paid transition beyond the already covered scalar A2 contractions?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-a2-graph-rewrite/README.md", + "research/staged544-separated-a2/README.md", + "research/staged544-a2-composition-audit/README.md", + "research/staged544-a1858-contraction-audit/README.md" + ], + "methods": [ + "Derive the changed legal frame itinerary and exact child histogram.", + "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract." + ], + "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the A2 and separated-A2 constructions and their composition/contraction audits. Scalar contractions can preserve the complete recursive histogram; fewer ADDs alone do not justify further scans.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Identify an actual paid transition to remove and construct a legal replacement frame itinerary, charging restoration, source windows and changed helpers. Compare complete before/after histograms. Stop if only scalar count changes; report that benefit honestly, without expanding the same scalar-only census.", + "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.", + "allowed_variations": [ + "One existing scalar simplification and one proposed frame-path change." + ], + "scope_change_triggers": [ + "Submitting only another scalar count as completion of a paid-profile task." + ], + "overlap_terms": [ + "scalar simplification", + "paid profile", + "R439", + "3998", + "4019", + "4112", + "4152", + "staged544-a2-graph-rewrite", + "staged544-separated-a2", + "staged544-a2-composition-audit", + "staged544-a1858-contraction-audit" + ], + "existing_checks": [ + { + "scope": "PR #3998: consecutive A2 scalar contraction", + "evidence": "research/staged544-a2-graph-rewrite/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4019: separated A2 sites with unchanged recursive histogram", + "evidence": "research/staged544-separated-a2/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "f408e09df300b575235f7f77f81948071397e16d", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4112: composition audit", + "evidence": "research/staged544-a2-composition-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "205b7380656ba4b6316a8a493b1a3c679b8f7a0e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4152: A1858 contraction audit", + "evidence": "research/staged544-a1858-contraction-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "caaa14cde5962adc372fdca71f63d0f29e73c8b2", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + } +} diff --git a/research/p104-two-handoffs/VERIFY.json b/research/p104-two-handoffs/VERIFY.json new file mode 100644 index 0000000000..d3bc44466e --- /dev/null +++ b/research/p104-two-handoffs/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "handoff" + ], + "timeout_seconds": 600, + "checks": "Main claim: regenerate both words from PR5551's pinned word; literal-only local.py/pricing.py edits; replay, transpose, native, physical caller, both moment engines, 54 strict + 4 functional outer checks, exact crossing interval for the hand-off word." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "variant-a" + ], + "timeout_seconds": 600, + "checks": "Supporting: Variant A (helpers start at 608/613) on the UNMODIFIED PR5545 local.py gives the same exact crossing interval and all outer checks." + } + ] +} diff --git a/research/p104-two-handoffs/WORD-VARIANT-A.json.gz b/research/p104-two-handoffs/WORD-VARIANT-A.json.gz new file mode 100644 index 0000000000..f3db5ee533 Binary files /dev/null and b/research/p104-two-handoffs/WORD-VARIANT-A.json.gz differ diff --git a/research/p104-two-handoffs/WORD.json.gz b/research/p104-two-handoffs/WORD.json.gz new file mode 100644 index 0000000000..b1c80d27f5 Binary files /dev/null and b/research/p104-two-handoffs/WORD.json.gz differ diff --git a/research/p104-two-handoffs/common.py b/research/p104-two-handoffs/common.py new file mode 100644 index 0000000000..4c32746826 --- /dev/null +++ b/research/p104-two-handoffs/common.py @@ -0,0 +1,47 @@ +"""Open the byte-pinned PR5545 source closure (same pins as PR5551); Apache-2.0. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. +Mechanism and all predecessor credit: see README.md. +""" +from contextlib import contextmanager +from hashlib import sha256 +from io import BytesIO +from pathlib import Path,PurePosixPath +import gzip,importlib.util,json,sys,tarfile,tempfile + +HERE=Path(__file__).resolve().parent +def need(ok,why): + if not ok: + raise ValueError(why) + +def read(path): + raw=Path(path).read_bytes() + return json.loads(gzip.decompress(raw) if str(path).endswith('.gz') else raw) + +def load(path,name): + spec=importlib.util.spec_from_file_location(name,path) + mod=importlib.util.module_from_spec(spec);sys.modules[name]=mod;spec.loader.exec_module(mod);return mod + +@contextmanager +def closure(): + pins=json.loads((HERE/'SOURCES.json').read_bytes())['retained_source'] + raw=(HERE/'inputs'/Path(pins['path']).name).read_bytes() + need(sha256(raw).hexdigest()==pins['sha256'],'Retained PR5545 capsule byte pin') + with tempfile.TemporaryDirectory(prefix='p104-two-handoffs-')as tmp: + root=Path(tmp) + with tarfile.open(fileobj=BytesIO(gzip.decompress(raw)),mode='r:')as archive: + members=archive.getmembers();names=[m.name for m in members] + need(len(names)==len(set(names)),'Unique retained source paths') + for m in members: + n=PurePosixPath(m.name) + need(m.isfile()and not n.is_absolute()and '..'not in n.parts,'Regular retained source path') + t=root/m.name;t.parent.mkdir(parents=True,exist_ok=True);t.write_bytes(archive.extractfile(m).read()) + mraw=(root/'.research-export.json').read_bytes() + need(sha256(mraw).hexdigest()==pins['export_manifest_sha256'],'Exact export inventory') + man=json.loads(mraw) + need(man['commit']==pins['commit']and len(man['files'])==pins['files']==33,'Exact predecessor closure') + need(set(names)=={'.research-export.json'}|{r['path']for r in man['files']},'No omitted or extra file') + for r in man['files']: + b=(root/r['path']).read_bytes() + need(len(b)==r['size']and sha256(b).hexdigest()==r['sha256'],'Source file '+r['path']) + yield root diff --git a/research/p104-two-handoffs/handoff.py b/research/p104-two-handoffs/handoff.py new file mode 100644 index 0000000000..b0a5151dc5 --- /dev/null +++ b/research/p104-two-handoffs/handoff.py @@ -0,0 +1,73 @@ +"""Derive the two-hand-off word from PR5551's pinned word. Apache-2.0. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. + +Helper 473 (event 13725) and helper 531 (event 13941) each end their first +rank-1 climb at a dim-2 frame F and are then idle; no other register holds +their symbol. The successor hand-off rewrites the rest of the helper's life +onto a fresh helper that starts at F. Pure rename: same 25,310 events, no new +ADD, identical paid profile. Scratch registers 735..742 shift to 737..744. + + default : old helper ends at F; fresh helper starts at F and keeps the old final frame. + --variant-a: no old/fresh split; the helper's leading MOVE is deleted and the + helper starts at F (public stays 735, program shorter by 2). +""" +import gzip,json,sys +from pathlib import Path +HERE=Path(__file__).resolve().parent +SPLITS=((473,13725),(531,13941)) # (helper, index of the MOVE reaching F) + +def source(): + return json.load(gzip.open(HERE/'inputs'/'pr5551-WORD.json.gz')) + +def need(ok,why): + if not ok: raise ValueError(why) + +def regs(e): + return (1,) if e[0] in('MOVE','INIT','CLEAR','SCALE') else (1,2) + +def check_leading(P,h,j): + uses=[i for i,e in enumerate(P) if any(e[k]==h for k in regs(e))] + need(uses[0]==j and P[j][0]=='MOVE',f'helper {h} first event is the climb to F') + return uses + +def handoff(w): + w=json.loads(json.dumps(w));P=w['program'] + need(w['public']==735 and len(w['initial'])==735,'pinned PR5551 shape') + new={h:735+i for i,(h,_) in enumerate(SPLITS)} + shift=lambda x:x+2 if 735<=x<743 else x + out=[];done={} + for i,e in enumerate(P): + e=list(e) + for k in regs(e): + x=e[k] + e[k]=done.get(x,x) if x<735 else shift(x) + out.append(e) + for h,j in SPLITS: + if i==j: + need(e[:2]==['MOVE',h],'split event');F=e[3] + check_leading(P,h,j) + done[h]=new[h] + w['program']=out;w['public']=737 + for h,j in SPLITS: + F=P[j][3] + w['initial'].append(F);w['final'].append(w['final'][h]);w['final'][h]=F + return w + +def variant_a(w): + w=json.loads(json.dumps(w));P=w['program'];drop=set() + for h,j in SPLITS: + check_leading(P,h,j);need(P[j][2]==w['initial'][h],'climb starts at the initial frame') + w['initial'][h]=P[j][3];drop.add(j) + w['program']=[e for i,e in enumerate(P) if i not in drop] + return w + +def dump(w,path): + raw=json.dumps(w,sort_keys=True,separators=(',',':')).encode() + with open(path,'wb') as f: + with gzip.GzipFile(fileobj=f,mode='wb',mtime=0) as g: g.write(raw) + +if __name__=='__main__': + w=source() + dump(handoff(w),HERE/'WORD.json.gz');dump(variant_a(w),HERE/'WORD-VARIANT-A.json.gz') + print('wrote WORD.json.gz and WORD-VARIANT-A.json.gz') diff --git a/research/p104-two-handoffs/inputs/pr5545-source-closure.tar.gz b/research/p104-two-handoffs/inputs/pr5545-source-closure.tar.gz new file mode 100644 index 0000000000..3084088544 Binary files /dev/null and b/research/p104-two-handoffs/inputs/pr5545-source-closure.tar.gz differ diff --git a/research/p104-two-handoffs/inputs/pr5551-WORD.json.gz b/research/p104-two-handoffs/inputs/pr5551-WORD.json.gz new file mode 100644 index 0000000000..c04a815c26 Binary files /dev/null and b/research/p104-two-handoffs/inputs/pr5551-WORD.json.gz differ diff --git a/research/p104-two-handoffs/inputs/pr5551-pricing.py b/research/p104-two-handoffs/inputs/pr5551-pricing.py new file mode 100644 index 0000000000..ef78de99ff --- /dev/null +++ b/research/p104-two-handoffs/inputs/pr5551-pricing.py @@ -0,0 +1,156 @@ +"""Complete mixed-target price, compiler and outer transfer. + +The interval and compiler bounds follow zxv and Cao Yifan. The productive +recursion is by Jacob Alan Sussman. The controller is by Cinna Davis. +Adapted from Ali Romman's PR5544/5545 for the two coupled contact changes. +Successor choices prepared for thu-nmrc with substantial OpenAI Codex assistance. +Ali Romman's complete caller/price proof and all predecessor credit are retained. +Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +import local as L + +KAPPA, TESTED = Q('.00304153'), Q('.0030415305') +PREVIOUS = Q('.00304117') + + +def encode(x): + if isinstance(x,Q): + return str(x) + if isinstance(x,dict): + return {str(k):encode(v) for k,v in x.items()} + if isinstance(x,(list,tuple)): + return [encode(v) for v in x] + return x + + +def assemble(local, native, word, physical): + paid, targets = Counter(), Counter() + counts = Counter() + L.need(local['helpers'] == native['helpers'], 'Every productive helper has a native target') + for e in word['physical_events']: + counts[e[0]] += 1 + if e[0] == 'LOCAL': + L.need(e[3] is False, 'Every source invocation is forward') + paid.update(local['paid']) + targets.update(local['helpers']) + elif e[0] == 'QUERY_SHEAR': + paid[1] += 104 + elif e[0] == 'IDLE': + paid[8*len(e[2])] += 208 + main = Counter() + idle = Counter({8*len(e[2]):0 for e in word['physical_events'] if e[0] == 'IDLE'}) + for e in word['physical_events']: + if e[0] == 'IDLE': + idle[8*len(e[2])] += 208 + L.need(idle == physical['whole_idle_jobs'], 'Every whole idle has a native Gaussian and full rank') + for term in word['diagonal']: + main[1+8*sum(term[1:])] += 104 + L.need(main == physical['main_targets'], 'Every main target has its full native phase') + targets.update(main) + L.need(counts['LOCAL'] == 18 and counts['QUERY_SHEAR'] == counts['IDLE'] == 15, 'Complete call census') + # Recount by the two path lengths, without using emitted main diagonals. + second_t = Counter({r:18*n for r,n in local['helpers'].items()}) + second_p = Counter({r:18*n for r,n in local['paid'].items()}) + second_t[145] += 208 + second_p[1] += 15*104 + for length in (7,8): + for j in range(1,length+1): + second_t[1+8*(j+1)] += 208 + second_p[8*(j+1)] += 208 + L.need((targets,paid) == (second_t,second_p), 'Independent full invoice') + L.need(max(targets) == 145 and max(paid) == 72, 'Maximum recursive ranks') + L.need(sum(targets.values()) == 12814 and sum(paid.values()) == 69912, 'Complete field and call counts') + L.need(sum(r*n for r,n in targets.items())-sum(r*n for r,n in paid.items()) == 760, 'Complete rank surplus') + return targets,paid,counts + + +def run(local,native,word,physical): + T,P,counts = assemble(local,native,word,physical) + E = L.load(L.ROOT/'research/higher-moment-strictification/verify.py','p104_productive_intervals') + other = L.load(L.ROOT/'research/kappa-rebuild/architecture/mixed_target_probe.py','p104_productive_second_intervals') + def margin(k): + a,b = E.moment(T,1-k), E.moment(P,1-k) + return a[0]-b[1],a[1]-b[0] + lo,hi,grid = 0,10**12,10**14 + while hi-lo > 1: + m=(lo+hi)//2 + if margin(Q(m,grid))[0] > 0: + lo=m + else: + hi=m + lower,upper = Q(lo,grid),Q(hi,grid) + L.need(margin(lower)[0] > 0 and margin(upper)[1] < 0, 'Strict rational crossing enclosure') + L.need(PREVIOUS < KAPPA < TESTED < lower and margin(PREVIOUS)[0] > 0, 'Changed complete bill improves selected kappa') + t,u,v,c,b = 1-TESTED,Q(1,5),1024,17,18 + target,paid = E.moment(T,t),E.moment(P,t) + tl,th = other.moment(T,TESTED) + pl,ph = other.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') + alpha = E.divide(paid,target) + gamma = E.divide(E.moment(P,t+u),E.mul(E.power(c,u),target)) + delta = E.divide((Q(sum(T.values())*b),)*2,E.mul(E.power(c,TESTED),target)) + reserve,decay = Q(1,10**10),Q(97,100) + L.need(alpha[1] < 1-reserve and gamma[1] < decay and delta[1] < decay, 'All three charged tail ratios') + L.need(decay**128 < Q(1,16), 'Both tail decay blocks') + normalized = 1/(1+v*reserve)+Q(4,2**32) + L.need(normalized < 1 and c**64 < b**63, 'Full completion, splitting and rounding charges') + theta,power = Q(63,64),1000 + eta = E.scale(E.power(145,-v*TESTED),t) + L.need(2*(c**v)**64 <= (145**v)**63 and eta[0] > theta**power, 'Shifted exits and complement capacity') + L.need(E.power(145,v*TESTED)[1] < 2**power, 'Compiler initial range') + gap = (TESTED-KAPPA)/7 + L.need(gap.numerator == 1, 'Exact compiler integer grid') + step = gap.denominator + def wins(j): + return (step*j+1)**power < 2**j + left,right=1,2 + while not wins(right): + left,right=right,2*right + while right-left > 1: + m=(left+right)//2 + if wins(m): + right=m + else: + left=m + H=step*right + L.need(H > 8*v and wins(right) and not wins(right-1), 'Finite uniform threshold with predecessor rejection') + local_routes = (sum(local['paid'].values())+native['helper_normalizers']+native['main_adapters']+4*104+4*local['owned_lifetimes'])*1000 + L.need(local['real_scalar_allowance']+local_routes < 10**7, 'Every local scalar, route and owned operation is funded') + boundary = sum(len(word['boundaries'][side+'_program']) for side in ('left','right')) + raw = 18*10**7 + 15*1664 + 32*104*(len(word['physical_events'])+boundary) + raw += 32*104*(26+1000) + L.need(raw < 10**9, 'Complete nonrecursive raw bound') + bit = L.read(L.ROOT/'research/query-thinned-controllers/RESULT.json')['ordinary_BIT'] + atom = Q(bit['atom']) + ordinary=(1-atom)*Q(bit['after_cover'])+atom*Q('.0000384599') + admitted=Q(bit['admitted']) + L.need(atom > ordinary > admitted > TESTED and atom < 1-ordinary, 'Retained BIT admission and stock') + outer_module=L.load(L.ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py','p104_productive_outer') + params={'kappa':KAPPA,'tested_saving':TESTED,'complex_uniform_saving':KAPPA+6*gap, + 'b':KAPPA+5*gap,'a':KAPPA+4*gap,'q':KAPPA+3*gap,'bit_saving':admitted, + 'epsilon':1-gap,'beta':1-3*gap,'r0':gap/10,'stop':gap,'layout':gap,'d':gap} + outer=outer_module.ledger(params) + outer['functional_checks']['actual_new_BIT_stock_sublinear']=params['beta']*(1-atom) + L.need(len(outer['strict_checks']) == 54 and len(outer['functional_checks']) == 4, 'Complete outer predicate inventory') + L.need(all(x > 0 for key in ('strict_checks','functional_checks') for x in outer[key].values()), 'All outer inequalities strict') + wrong_cutoff = E.divide((Q(sum(T.values())*21),)*2,E.mul(E.power(20,TESTED),target)) + L.need(wrong_cutoff[0] > 1, 'Old cutoff fails with this helper inventory') + bad=outer_module.ledger(dict(params,bit_saving=Q('.0027'))) + L.need(any(x <= 0 for x in bad['strict_checks'].values()), 'Insufficient BIT contract rejected') + return encode({'kappa':KAPPA,'kappa_decimal':'.00304153','previous_open_pr5545':PREVIOUS,'gain':KAPPA-PREVIOUS, + 'relative_gain_percent':100*(KAPPA/PREVIOUS-1),'raw_root_interval':[lower,upper], + 'raw_headroom':[lower-KAPPA,upper-KAPPA],'margin_at_previous':E.display(margin(PREVIOUS)), + 'targets':T,'paid':P,'productive_fields':sum(T.values()),'paid_calls':sum(P.values()), + 'rank_mass_surplus':760,'full_forward_calls':18,'query_shears':15,'whole_idle_jobs':3120, + 'strictification':{'tested':TESTED,'power':v,'cutoff':c,'floor':b,'tail_offset':u,'reserve':reserve, + 'alpha':E.display(alpha),'gamma':E.display(gamma),'delta':E.display(delta),'normalized_paid_upper':normalized}, + 'compiler':{'theta':theta,'logarithm_power':power,'eta':E.display(eta),'gap':gap,'H':H,'N':'2^'+str(H), + 'integer_test_exponent':right,'uniform_saving':params['complex_uniform_saving'],'word_materialized':False}, + 'nonrecursive':{'local_scalar':local['real_scalar_allowance'],'local_routes':local_routes, + 'raw_scalar_upper':raw,'raw_budget':10**9,'peak_owned_fields':1, + 'fixed_scalar_growth_bound':'At most 2^(16*26000) before native factors; a declared constant, not an attained norm.', + 'tensor_native_growth_bound':'Each rank-r Gaussian has row l1 norm at most 2^(rf); sum of local ranks is 5894.'}, + 'ordinary_BIT':bit,'outer':outer, + 'negative_controls':{'old_cutoff':'Rejected by completion-tail ratio greater than one','old_BIT':'Rejected by outer inequalities'}}) diff --git a/research/p104-two-handoffs/local.py b/research/p104-two-handoffs/local.py new file mode 100644 index 0000000000..69ead9f46d --- /dev/null +++ b/research/p104-two-handoffs/local.py @@ -0,0 +1,264 @@ +"""Replay the credited P104 word and its complete native interfaces. + +David Arias supplied the coalesced word. Cinna Davis supplied private reuse. +Gareth Davidson supplied their composition. Ali Romman prepared this caller +with substantial OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +from hashlib import sha256 +from pathlib import Path +import gzip +import importlib.util +import json +import sys +import tarfile +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PREFIX = 'research/p104-coalesced-private-reuse/' +GEOMETRY = ('research/complex-block-rank-optimum/inputs/selected.json.gz', + 'research/frame-sa504/inputs/hamming/PROTOTYPE.json', + 'research/p104-native-channel/inputs/P104-FIXTURE.json') + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def add(dst, src, q): + for k, v in tuple(src.items()): + value = dst.get(k, 0) + q*v + if value: + dst[k] = value + else: + dst.pop(k, None) + + +def span(basis): + out = {0} + for v in basis: + need(type(v) is int and 0 < v < 512 and v not in out, 'Independent binary basis') + out |= {x ^ v for x in tuple(out)} + return frozenset(out) + + +def construct(): + """Rebuild the published source without its obsolete owner-price engine.""" + manifest = read(ROOT / (PREFIX+'SOURCES.json')) + archive, = manifest['archives'] + raw = (ROOT / (PREFIX+'predecessor2152.tar.gz')).read_bytes() + need(sha256(raw).hexdigest() == archive['sha256'], 'Exact predecessor archive') + pins = {x['path']: x for x in archive['members']} + with tempfile.TemporaryDirectory(prefix='p104-source-') as tmp: + root = Path(tmp) + with tarfile.open(ROOT / (PREFIX+'predecessor2152.tar.gz')) as data: + members = data.getmembers() + need(len(members) == len(pins) == 11 and {m.name for m in members} == set(pins), 'Archive inventory') + for m in members: + need(m.isfile() and not Path(m.name).is_absolute() and '..' not in Path(m.name).parts, 'Archive file') + raw = data.extractfile(m).read() + need(sha256(raw).hexdigest() == pins[m.name]['sha256'], 'Archive member pin') + path = root/m.name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(raw) + for path in GEOMETRY: + target = root/path + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes((ROOT/path).read_bytes()) + C = load(root/'research/p104-interleaved-search/coalesced.py', 'productive_p104_coalesced') + A = load(ROOT/(PREFIX+'compose.py'), 'productive_p104_composition') + built = A.construct(C, C.construct()) + need(built['report'] == read(ROOT/(PREFIX+'RESULT.json'))['composition'], 'Published complete source report') + frames, numbers = [], {} + def frame(basis): + key = tuple(basis) + if key not in numbers: + numbers[key] = len(frames) + frames.append(list(key)) + return numbers[key] + initial = [frame(C.F.basis(x)) for x in built['initial']] + final = [frame(C.F.basis(x)) for x in built['final']] + live = [r for r in range(112) if len(built['initial'][r]) == 2] + edges = built['transport_edges'] + program = [] + for e in built['scalar_operations']: + op = e['kind'] + if op == 'transport': + edge = edges[e['occurrence']] + program.append(['MOVE', edge['register'], frame(edge['source_frame']), frame(edge['target_frame']), edge['private']]) + elif op in ('private_init', 'private_discard'): + program.append(['INIT' if op == 'private_init' else 'CLEAR', e['register'], frame(e['frame'])]) + else: + program.append([{'add':'ADD', 'scale':'SCALE', 'private_copy':'COPY'}[op], *e['registers'], e['coefficient'], frame(e['frame'])]) + return {'schema':'p104-productive-source/1', 'public':737, 'live':live, 'ports':built['ports'], + 'frames':frames, 'initial':initial, 'final':final, 'program':program} + + +def replay(w): + need(len(w['program']) < 26000, 'Fixed operation bound') + frames = [span(x) for x in w['frames']] + rows = [{r:Q(1)} for r in range(745)] + current = list(w['initial']) + [None]*8 + paid, scalar, live_owned, peak = Counter(), 0, set(), 0 + for e in w['program']: + op, r = e[:2] + need(0 <= r < 745, 'Role index') + if op == 'MOVE': + _, r, a, b, private = e + need(current[r] == a and (r in live_owned) == private, 'Transport source and ownership') + need(frames[b] < frames[a] if private else frames[a] < frames[b], 'Nested chronological transport') + paid[abs(len(w['frames'][b])-len(w['frames'][a]))] += 1 + current[r] = b + elif op == 'INIT': + need(r >= 737 and r not in live_owned, 'Owned initialization') + live_owned.add(r) + peak = max(peak, len(live_owned)) + rows[r] = {} + current[r] = e[2] + scalar += 2 + elif op == 'CLEAR': + need(r in live_owned and current[r] == e[2], 'Owned erasure at declared frame') + rows[r] = {} + current[r] = None + live_owned.remove(r) + scalar += 2 + else: + q, f = Q(e[-2]), e[-1] + need(q and current[r] == f, 'Scalar destination and coefficient') + n, d = abs(q.numerator), q.denominator + need(d & (d-1) == 0, 'Dyadic scalar coefficient') + need(abs(q)+1 < 2**16, 'Fixed scalar growth bound') + if op == 'SCALE': + need(n & (n-1) == 0, 'Dyadic unit SCALE') + rows[r] = {k:q*x for k,x in rows[r].items()} + scalar += 2*(abs(n.bit_length()-d.bit_length()) + int(q < 0)) + else: + s = e[2] + need(s != r and 0 <= s < 745 and current[s] == f, 'Common scalar chart') + if op == 'COPY': + need(r in live_owned and not rows[r], 'COPY into cleared owned field') + rows[r] = {k:q*x for k,x in rows[s].items()} + else: + need(op == 'ADD', 'Scalar opcode') + add(rows[r], rows[s], q) + scalar += 2*(3+n.bit_length()-1+n.bit_count()+d.bit_length()-1) + need(not live_owned and peak == 1 and current[:737] == w['final'], 'All public and owned exits') + live = set(w['live']) + for r,row in enumerate(rows): + expected = {r:Q(1)} if r < 737 else {} + if r-112 in live: + expected[r-112] = Q(1) + need(row == expected, 'All 745 public and owned rows') + main = live | {r+112 for r in live} + helpers = Counter(len(w['frames'][w['final'][r]])-len(w['frames'][w['initial'][r]]) for r in range(737) if r not in main) + need(len(live) == len(w['ports']) == 104 and len(main) == 208 and min(helpers) > 0, 'Independent productive inputs') + return {'paid':dict(paid), 'helpers':dict(helpers), 'public_inputs':737, 'owned_lifetimes':8, + 'peak_owned_fields':peak, 'real_scalar_allowance':scalar, 'endpoint_coefficients':745*745} + + +def reverse_columns(w): + """Check the transpose with dense dyadic rows and the reverse chronology.""" + n = 745 + rows = [[int(i == j) for j in range(n)] for i in range(n)] + exponents = [0]*n + for e in reversed(w['program']): + op,r = e[:2] + if op == 'MOVE': + continue + if op in ('INIT','CLEAR'): + rows[r] = [0]*n + exponents[r] = 0 + continue + q = Q(e[-2]) + qe = q.denominator.bit_length()-1 + if op == 'SCALE': + rows[r] = [q.numerator*x for x in rows[r]] + exponents[r] += qe + else: + s = e[2] + level = max(exponents[s], exponents[r]+qe) + a, b = 1 << (level-exponents[s]), q.numerator << (level-exponents[r]-qe) + rows[s] = [a*x+b*y for x,y in zip(rows[s],rows[r])] + exponents[s] = level + if op == 'COPY': + rows[r] = [0]*n + exponents[r] = 0 + r = s + while exponents[r] and not any(x & 1 for x in rows[r]): + rows[r] = [x//2 for x in rows[r]] + exponents[r] -= 1 + for r,row in enumerate(rows): + expected = [0]*n + if r < 737: + expected[r] = 1 << exponents[r] + if r in w['live']: + expected[r+112] = 1 << exponents[r] + need(row == expected, 'Independent dense transpose columns') + return {'columns':n, 'coefficients':n*n, 'arithmetic':'Dense integer rows with binary denominators; reverse chronology'} + + +def native(w): + C = load(ROOT/'research/p104-native-channel/vendor/clifford_exact.py', 'p104_productive_clifford') + V = load(ROOT/'research/p104-native-channel/vendor/native_verify.py', 'p104_productive_gaussian') + @lru_cache(None) + def chart(i): + return C.canonical_frame(9, tuple(w['frames'][i])) + recipes = {} + def check(a,b): + if (a,b) not in recipes: + recipe,_ = C.lower_child(chart(a).adjoint().then(chart(b))) + expected = V.adjoint(V.frame(w['frames'][a],9)) + V.frame(w['frames'][b],9) + V.equal(V.recipe(recipe),expected,'Native chart change and exact global phase') + need(recipe['rank'] == abs(len(w['frames'][a])-len(w['frames'][b])), 'Native boundary rank') + recipes[a,b] = recipe + return recipes[a,b] + for e in w['program']: + if e[0] == 'MOVE': + check(e[2],e[3]) + main = set(w['live']) | {r+112 for r in w['live']} + helper_profile = Counter() + for r in range(737): + if r not in main: + helper_profile[check(w['initial'][r],w['final'][r])['rank']] += 1 + adapters = [] + for r,q in zip(w['live'],w['ports']): + need(w['frames'][w['initial'][r]] == [q], 'Literal central port') + need(span(w['frames'][w['final'][r+112]]) == frozenset(x for x in range(512) if not (x&q).bit_count()%2), 'Literal output hyperplane') + tests = [ + (C.cgate(9,q,1).adjoint().then(chart(w['initial'][r])), V.adjoint((('C',q,1),))+V.frame(w['frames'][w['initial'][r]],9)), + (chart(w['final'][r+112]).adjoint().then(C.cgate(9,q,-1).then(C.fourier(9))), V.adjoint(V.frame(w['frames'][w['final'][r+112]],9))+(('C',q,-1),)+V.fourier(9))] + for actual,expected in tests: + recipe,_ = C.lower_child(actual) + need(recipe['rank'] == 0, 'Free intrinsic main adapter') + V.equal(V.recipe(recipe),expected,'Main endpoint phase') + adapters.append(recipe) + bad = json.loads(json.dumps(next(iter(recipes.values())))) + bad['left']['phase'] = (bad['left']['phase']+1)%4 + a,b = next(iter(recipes)) + try: + V.equal(V.recipe(bad),V.adjoint(V.frame(w['frames'][a],9))+V.frame(w['frames'][b],9),'Wrong phase control') + except ValueError: + pass + else: + raise ValueError('Wrong native phase accepted') + payload = [[a,b,recipes[a,b]] for a,b in sorted(recipes)] + adapters + return {'distinct_maps':len(recipes),'main_adapters':len(adapters),'helper_normalizers':2*sum(helper_profile.values()), + 'helpers':dict(helper_profile),'recipe_payload_sha256':sha256(json.dumps(payload,sort_keys=True,separators=(',',':')).encode()).hexdigest(), + 'wrong_phase_rejected':True, 'proof':'Every signed Pauli image and exact global phase; frame induction at every positive tensor width'} diff --git a/research/p104-two-handoffs/pricing.py b/research/p104-two-handoffs/pricing.py new file mode 100644 index 0000000000..e7708a6ac1 --- /dev/null +++ b/research/p104-two-handoffs/pricing.py @@ -0,0 +1,156 @@ +"""Complete mixed-target price, compiler and outer transfer. + +The interval and compiler bounds follow zxv and Cao Yifan. The productive +recursion is by Jacob Alan Sussman. The controller is by Cinna Davis. +Adapted from Ali Romman's PR5544/5545 for the two coupled contact changes. +Successor choices prepared for thu-nmrc with substantial OpenAI Codex assistance. +Ali Romman's complete caller/price proof and all predecessor credit are retained. +Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +import local as L + +KAPPA, TESTED = Q('.00304282'), Q('.0030428205') +PREVIOUS = Q('.00304153') + + +def encode(x): + if isinstance(x,Q): + return str(x) + if isinstance(x,dict): + return {str(k):encode(v) for k,v in x.items()} + if isinstance(x,(list,tuple)): + return [encode(v) for v in x] + return x + + +def assemble(local, native, word, physical): + paid, targets = Counter(), Counter() + counts = Counter() + L.need(local['helpers'] == native['helpers'], 'Every productive helper has a native target') + for e in word['physical_events']: + counts[e[0]] += 1 + if e[0] == 'LOCAL': + L.need(e[3] is False, 'Every source invocation is forward') + paid.update(local['paid']) + targets.update(local['helpers']) + elif e[0] == 'QUERY_SHEAR': + paid[1] += 104 + elif e[0] == 'IDLE': + paid[8*len(e[2])] += 208 + main = Counter() + idle = Counter({8*len(e[2]):0 for e in word['physical_events'] if e[0] == 'IDLE'}) + for e in word['physical_events']: + if e[0] == 'IDLE': + idle[8*len(e[2])] += 208 + L.need(idle == physical['whole_idle_jobs'], 'Every whole idle has a native Gaussian and full rank') + for term in word['diagonal']: + main[1+8*sum(term[1:])] += 104 + L.need(main == physical['main_targets'], 'Every main target has its full native phase') + targets.update(main) + L.need(counts['LOCAL'] == 18 and counts['QUERY_SHEAR'] == counts['IDLE'] == 15, 'Complete call census') + # Recount by the two path lengths, without using emitted main diagonals. + second_t = Counter({r:18*n for r,n in local['helpers'].items()}) + second_p = Counter({r:18*n for r,n in local['paid'].items()}) + second_t[145] += 208 + second_p[1] += 15*104 + for length in (7,8): + for j in range(1,length+1): + second_t[1+8*(j+1)] += 208 + second_p[8*(j+1)] += 208 + L.need((targets,paid) == (second_t,second_p), 'Independent full invoice') + L.need(max(targets) == 145 and max(paid) == 72, 'Maximum recursive ranks') + L.need(sum(targets.values()) == 12850 and sum(paid.values()) == 69912, 'Complete field and call counts') + L.need(sum(r*n for r,n in targets.items())-sum(r*n for r,n in paid.items()) == 760, 'Complete rank surplus') + return targets,paid,counts + + +def run(local,native,word,physical): + T,P,counts = assemble(local,native,word,physical) + E = L.load(L.ROOT/'research/higher-moment-strictification/verify.py','p104_productive_intervals') + other = L.load(L.ROOT/'research/kappa-rebuild/architecture/mixed_target_probe.py','p104_productive_second_intervals') + def margin(k): + a,b = E.moment(T,1-k), E.moment(P,1-k) + return a[0]-b[1],a[1]-b[0] + lo,hi,grid = 0,10**12,10**14 + while hi-lo > 1: + m=(lo+hi)//2 + if margin(Q(m,grid))[0] > 0: + lo=m + else: + hi=m + lower,upper = Q(lo,grid),Q(hi,grid) + L.need(margin(lower)[0] > 0 and margin(upper)[1] < 0, 'Strict rational crossing enclosure') + L.need(PREVIOUS < KAPPA < TESTED < lower and margin(PREVIOUS)[0] > 0, 'Changed complete bill improves selected kappa') + t,u,v,c,b = 1-TESTED,Q(1,5),1024,17,18 + target,paid = E.moment(T,t),E.moment(P,t) + tl,th = other.moment(T,TESTED) + pl,ph = other.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') + alpha = E.divide(paid,target) + gamma = E.divide(E.moment(P,t+u),E.mul(E.power(c,u),target)) + delta = E.divide((Q(sum(T.values())*b),)*2,E.mul(E.power(c,TESTED),target)) + reserve,decay = Q(1,10**10),Q(97,100) + L.need(alpha[1] < 1-reserve and gamma[1] < decay and delta[1] < decay, 'All three charged tail ratios') + L.need(decay**128 < Q(1,16), 'Both tail decay blocks') + normalized = 1/(1+v*reserve)+Q(4,2**32) + L.need(normalized < 1 and c**64 < b**63, 'Full completion, splitting and rounding charges') + theta,power = Q(63,64),1000 + eta = E.scale(E.power(145,-v*TESTED),t) + L.need(2*(c**v)**64 <= (145**v)**63 and eta[0] > theta**power, 'Shifted exits and complement capacity') + L.need(E.power(145,v*TESTED)[1] < 2**power, 'Compiler initial range') + gap = (TESTED-KAPPA)/7 + L.need(gap.numerator == 1, 'Exact compiler integer grid') + step = gap.denominator + def wins(j): + return (step*j+1)**power < 2**j + left,right=1,2 + while not wins(right): + left,right=right,2*right + while right-left > 1: + m=(left+right)//2 + if wins(m): + right=m + else: + left=m + H=step*right + L.need(H > 8*v and wins(right) and not wins(right-1), 'Finite uniform threshold with predecessor rejection') + local_routes = (sum(local['paid'].values())+native['helper_normalizers']+native['main_adapters']+4*104+4*local['owned_lifetimes'])*1000 + L.need(local['real_scalar_allowance']+local_routes < 10**7, 'Every local scalar, route and owned operation is funded') + boundary = sum(len(word['boundaries'][side+'_program']) for side in ('left','right')) + raw = 18*10**7 + 15*1664 + 32*104*(len(word['physical_events'])+boundary) + raw += 32*104*(26+1000) + L.need(raw < 10**9, 'Complete nonrecursive raw bound') + bit = L.read(L.ROOT/'research/query-thinned-controllers/RESULT.json')['ordinary_BIT'] + atom = Q(bit['atom']) + ordinary=(1-atom)*Q(bit['after_cover'])+atom*Q('.0000384599') + admitted=Q(bit['admitted']) + L.need(atom > ordinary > admitted > TESTED and atom < 1-ordinary, 'Retained BIT admission and stock') + outer_module=L.load(L.ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py','p104_productive_outer') + params={'kappa':KAPPA,'tested_saving':TESTED,'complex_uniform_saving':KAPPA+6*gap, + 'b':KAPPA+5*gap,'a':KAPPA+4*gap,'q':KAPPA+3*gap,'bit_saving':admitted, + 'epsilon':1-gap,'beta':1-3*gap,'r0':gap/10,'stop':gap,'layout':gap,'d':gap} + outer=outer_module.ledger(params) + outer['functional_checks']['actual_new_BIT_stock_sublinear']=params['beta']*(1-atom) + L.need(len(outer['strict_checks']) == 54 and len(outer['functional_checks']) == 4, 'Complete outer predicate inventory') + L.need(all(x > 0 for key in ('strict_checks','functional_checks') for x in outer[key].values()), 'All outer inequalities strict') + wrong_cutoff = E.divide((Q(sum(T.values())*21),)*2,E.mul(E.power(20,TESTED),target)) + L.need(wrong_cutoff[0] > 1, 'Old cutoff fails with this helper inventory') + bad=outer_module.ledger(dict(params,bit_saving=Q('.0027'))) + L.need(any(x <= 0 for x in bad['strict_checks'].values()), 'Insufficient BIT contract rejected') + return encode({'kappa':KAPPA,'kappa_decimal':'.00304153','previous_open_pr5545':PREVIOUS,'gain':KAPPA-PREVIOUS, + 'relative_gain_percent':100*(KAPPA/PREVIOUS-1),'raw_root_interval':[lower,upper], + 'raw_headroom':[lower-KAPPA,upper-KAPPA],'margin_at_previous':E.display(margin(PREVIOUS)), + 'targets':T,'paid':P,'productive_fields':sum(T.values()),'paid_calls':sum(P.values()), + 'rank_mass_surplus':760,'full_forward_calls':18,'query_shears':15,'whole_idle_jobs':3120, + 'strictification':{'tested':TESTED,'power':v,'cutoff':c,'floor':b,'tail_offset':u,'reserve':reserve, + 'alpha':E.display(alpha),'gamma':E.display(gamma),'delta':E.display(delta),'normalized_paid_upper':normalized}, + 'compiler':{'theta':theta,'logarithm_power':power,'eta':E.display(eta),'gap':gap,'H':H,'N':'2^'+str(H), + 'integer_test_exponent':right,'uniform_saving':params['complex_uniform_saving'],'word_materialized':False}, + 'nonrecursive':{'local_scalar':local['real_scalar_allowance'],'local_routes':local_routes, + 'raw_scalar_upper':raw,'raw_budget':10**9,'peak_owned_fields':1, + 'fixed_scalar_growth_bound':'At most 2^(16*26000) before native factors; a declared constant, not an attained norm.', + 'tensor_native_growth_bound':'Each rank-r Gaussian has row l1 norm at most 2^(rf); sum of local ranks is 5894.'}, + 'ordinary_BIT':bit,'outer':outer, + 'negative_controls':{'old_cutoff':'Rejected by completion-tail ratio greater than one','old_BIT':'Rejected by outer inequalities'}}) diff --git a/research/p104-two-handoffs/verify.py b/research/p104-two-handoffs/verify.py new file mode 100644 index 0000000000..09177f2897 --- /dev/null +++ b/research/p104-two-handoffs/verify.py @@ -0,0 +1,92 @@ +"""Reproduce the conditional kappa of the two successor hand-offs. Apache-2.0. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. +Runs the hand-off word through PR5551's own chain (replay, transpose, native maps, +physical caller, pricing with all 54 strict + 4 functional outer checks), then the +supporting Variant A through the UNMODIFIED PR5545 local.py. About 5-10 minutes. +""" +from fractions import Fraction +import difflib,gzip,json,sys +from pathlib import Path +sys.dont_write_bytecode=True +HERE=Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +from common import closure,need,load,read +import handoff + +LOCAL_LITERALS=[("'public':735","'public':737"),('range(743)','range(745)'),('0 <= r < 743','0 <= r < 745'), + ('r >= 735 and r not in live_owned','r >= 737 and r not in live_owned'),('0 <= s < 743','0 <= s < 745'), + ('current[:735]','current[:737]'),('if r < 735 else','if r < 737 else'),('All 743 public','All 745 public'), + ('for r in range(735) if r not in main','for r in range(737) if r not in main'),("'public_inputs':735","'public_inputs':737"), + ('743*743','745*745'),('n = 743','n = 745'),('if r < 735:','if r < 737:'),('for r in range(735):','for r in range(737):')] +PRICING_LITERALS=[("Q('.00304153'), Q('.0030415305')","Q('.00304282'), Q('.0030428205')"),("PREVIOUS = Q('.00304117')","PREVIOUS = Q('.00304153')"), + ('sum(targets.values()) == 12814','sum(targets.values()) == 12850')] +INTERVAL=['76070606559/25000000000000','304282426237/100000000000000'] # raw crossing, kappa in (.00304282426236, .00304282426237) + +def patch(text,table): + for a,b in table: + need(text.count(a)>=1,'literal present: '+a);text=text.replace(a,b) + return text + +def chain(root,L,pricing_text,word,tag): + sys.modules['local']=L;L.ROOT=root + C=L.load(root/'research/p104-productive-controller/caller.py','p104_two_handoffs_caller_'+tag) + tmp=HERE/('.pricing-'+tag+'.py');tmp.write_text(pricing_text) + try: P=L.load(tmp,'p104_two_handoffs_pricing_'+tag) + finally: tmp.unlink() + loc=L.replay(word);col=L.reverse_columns(word) + print(tag,'PASS replay: paid',loc['paid'],'public',loc['public_inputs'],flush=True) + nat=L.native(word);print(tag,'PASS native maps',nat['distinct_maps'],'helpers',nat['helpers'],flush=True) + ctl=C.construct();need(ctl==read(root/'research/p104-productive-controller/CONTROLLER.json'),'Exact complete caller') + phys=C.physical(ctl,word);print(tag,'PASS physical caller',flush=True) + res=P.run(loc,nat,ctl,phys) + return loc,res + +def main(): + pinned=handoff.source() + word=handoff.handoff(pinned);wa=handoff.variant_a(pinned) + for name,w in(('WORD.json.gz',word),('WORD-VARIANT-A.json.gz',wa)): + need(read(HERE/name)==w,name+' regenerates from the pinned PR5551 word') + need(word['public']==737 and len(word['program'])==len(pinned['program']),'rename-only edit') + part=sys.argv[sys.argv.index('--part')+1] if '--part' in sys.argv else 'all' + need(part in('all','handoff','variant-a'),'--part must be handoff or variant-a') + out={} + with closure() as root: + orig_local=(root/'research/p104-productive-controller/local.py').read_text() + shipped=(HERE/'local.py').read_text() + need(patch(orig_local,LOCAL_LITERALS)==shipped,'shipped local.py = closure local.py + literal changes only') + pr_pricing=(HERE/'inputs/pr5551-pricing.py').read_text() + need(patch(pr_pricing,PRICING_LITERALS)==(HERE/'pricing.py').read_text(),'shipped pricing.py = PR5551 pricing.py + literal changes only') + # --- main claim: two successor hand-offs, patched local.py (737 public inputs) + if part in ('all', 'handoff'): + L=load(HERE/'local.py','local');L.ROOT=root + loc,res=chain(root,L,(HERE/'pricing.py').read_text(),word,'handoff') + need(res['raw_root_interval']==INTERVAL,'exact crossing interval') + need(res['productive_fields']==12850 and res['paid_calls']==69912 and res['rank_mass_surplus']==760,'invoice') + need(len(res['outer']['strict_checks'])==54 and len(res['outer']['functional_checks'])==4,'outer inventory') + need(all(Fraction(x)>0 for k in('strict_checks','functional_checks') for x in res['outer'][k].values()),'all outer checks strict') + out['handoff']=res;out['loc']=loc + # --- supporting Variant A: helpers start at frames 608/613, UNMODIFIED local.py (735 public inputs) + if part in ('all', 'variant-a'): + L0=load(root/'research/p104-productive-controller/local.py','local');L0.ROOT=root + need(Path(L0.__file__).read_text()==orig_local,'unmodified closure local.py') + ptxt=patch(pr_pricing,PRICING_LITERALS[:2]).replace('sum(paid.values()) == 69912','sum(paid.values()) == 69876') + locA,resA=chain(root,L0,ptxt,wa,'variantA') + need(resA['raw_root_interval']==INTERVAL,'Variant A: same exact crossing interval') + need(len(resA['outer']['strict_checks'])==54 and len(resA['outer']['functional_checks'])==4 and all(Fraction(x)>0 for k in('strict_checks','functional_checks') for x in resA['outer'][k].values()),'Variant A outer checks') + out['variant_a']=resA + lo,hi=[Fraction(x) for x in INTERVAL] + print('Crossing kappa in (%s, %s) = (%.14f, %.14f)'%(INTERVAL[0],INTERVAL[1],lo,hi)) + print('Conditional complete kappa 0.0030428242; PR5551 0.0030415312; gain +1.2931e-6 (float price)') + print('54 strict + 4 functional outer checks pass for: '+part) + if '--write' in sys.argv and part=='all': + loc=out['loc'] + (HERE/'RESULT.json').write_text(json.dumps({'status':'PASS_P104_TWO_HANDOFFS_CONDITIONAL_KAPPA_0030428242', + 'kappa_claimed':'.00304282','crossing_kappa_interval':INTERVAL,'crossing_kappa_decimal':'.0030428242', + 'previous_pr5551':'.00304153','paid_local':loc['paid'],'helpers_local':loc['helpers'], + 'handoff_complete_cost':out['handoff'],'variant_a_complete_cost':out['variant_a'], + 'conditions':['The five framework assumptions retained by PR5544/5545/5551.', + "PR5551's validity (unreproduced at time of writing).", + 'Admissibility of a fresh helper starting at a non-canonical mid frame (Variant A passes the unmodified local.py; canonical-start rule exists only in the #4610 compact-width verifier).']},indent=1,sort_keys=True,default=str)+'\n') + print('PASS P104_TWO_HANDOFFS') +main() diff --git a/research/p104-two-handoffs/verify.sh b/research/p104-two-handoffs/verify.sh new file mode 100755 index 0000000000..d7a4b8e1b5 --- /dev/null +++ b/research/p104-two-handoffs/verify.sh @@ -0,0 +1,3 @@ +#!/bin/sh +# usage: research/p104-two-handoffs/verify.sh (from repository root; Python 3.12, stdlib only) +exec python3 -B "$(dirname "$0")/verify.py" "$@" diff --git a/research/wordram-ntt-kernel/VERIFY.json b/research/wordram-ntt-kernel/VERIFY.json index 4ae0f65622..3e43a2b044 100644 --- a/research/wordram-ntt-kernel/VERIFY.json +++ b/research/wordram-ntt-kernel/VERIFY.json @@ -1,7 +1,7 @@ { "format": "standalone source-export research package", "inputs": [ - "MANIFEST.json" + "research/wordram-ntt-kernel/MANIFEST.json" ], "commands": [ [