diff --git a/research/p104-free-endpoint-retime/LITERAL-CHANGES.diff b/research/p104-free-endpoint-retime/LITERAL-CHANGES.diff new file mode 100644 index 0000000000..fa9154b209 --- /dev/null +++ b/research/p104-free-endpoint-retime/LITERAL-CHANGES.diff @@ -0,0 +1,58 @@ +--- inputs/pr5551-pricing.py (PR5551 head 1123635a) ++++ pricing.py (headline) +@@ -11,7 +11,7 @@ + from fractions import Fraction as Q + import local as L + +-KAPPA, TESTED = Q('.00304153'), Q('.0030415305') ++KAPPA, TESTED = Q('.00308142'), Q('.0030814205') + PREVIOUS = Q('.00304117') + + +@@ -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()) == 12814 and sum(paid.values()) == 66852, '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 + +@@ -139,7 +139,7 @@ + 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, ++ return encode({'kappa':KAPPA,'kappa_decimal':'.00308142','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()), +--- inputs/pr5551-pricing.py (PR5551 head 1123635a) ++++ pricing-starts-only.py (supporting) +@@ -11,7 +11,7 @@ + from fractions import Fraction as Q + import local as L + +-KAPPA, TESTED = Q('.00304153'), Q('.0030415305') ++KAPPA, TESTED = Q('.003076879'), Q('.0030768795') + PREVIOUS = Q('.00304117') + + +@@ -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()) == 12814 and sum(paid.values()) == 67374, '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 + +@@ -139,7 +139,7 @@ + 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, ++ return encode({'kappa':KAPPA,'kappa_decimal':'.003076879','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()), diff --git a/research/p104-free-endpoint-retime/README.md b/research/p104-free-endpoint-retime/README.md new file mode 100644 index 0000000000..e8c177c6b7 --- /dev/null +++ b/research/p104-free-endpoint-retime/README.md @@ -0,0 +1,74 @@ +# Free helper endpoints on the P104 word (conditional kappa .0030814243) + +Complete conditional kappa **.0030814243** (**+3.99e-5**, +1.31% over +[PR5551](https://github.com/CrocSwap/integer-mult-bounds/pull/5551)'s .0030415312). The claim is +tested at .0030814205; the exact raw crossing lies in +(15407121669/5000000000000, 308142433381/100000000000000) = (.00308142433380, .00308142433381). +A supporting word that needs only free helper *start* frames reaches **.0030768801** (+3.54e-5); +its exact crossing lies in (76922002003/25000000000000, 307688008013/100000000000000) = (.00307688008012, .00307688008013), tested at .0030768795. + +**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) **free helper START frames and free +helper FINAL frames**. For (c): the verifier checks only that each helper's initial frame is strictly +nested in its final frame and that the native boundary map has rank equal to the dimension gap; only +the X-initial and Y-final frames are literal (the 104 ports). The canonical-start rule exists only +in the #4610 compact-width verifier. Unmodified PR5544/5545 already has mid-frame helper starts +(23 distinct start frames, dimensions 0, 1, 4, 5) and mixed finals (18 distinct, dimensions 4, 5, 8, 9). +The headline word needs both (c)-starts and (c)-finals; the supporting word needs (c)-starts only. The +selected record is not changed; no independent human or proof-kernel acceptance is claimed. + +## What the edit is (and is not) +This is **not** an unchanged circuit. Relative to PR5551's pinned word (`inputs/pr5551-WORD.json.gz`): +- The scalar program is identical: the same 21,686 ADD/COPY/SCALE/INIT/CLEAR events in the same order + with the same registers and coefficients (no register merge or reordering). +- Only frame labels and MOVE stops change. The solve chose the subspace at every ADD-chart cluster + subject to the verifier's nesting laws (an exact-lattice CP-SAT retime), and **170 stops became + redundant and are deleted** (3,624 -> 3,454 MOVEs; 25,310 -> 25,140 events). The supporting word + deletes 141 stops (3,483 MOVEs). +- Headline word: 168 helper start spans and 23 helper final spans differ from PR5551's (22 of the + finals move from dimension 8 to 9); 607 scalar-event frame labels and 607 kept MOVE stops are + relabelled (149 of those stops belong to main registers, whose intermediate frames move together with a + helper in a shared ADD chart). Supporting word: 169 helper starts differ, 0 finals. +- All 208 main registers (104 X sources, 104 Y targets) keep identical initial and final spans, so the + literal ports, the caller and the controller are untouched. +- Productive fields stay 12,814 and the rank-mass surplus stays 760; the credited helper profile moves + (rank 9: 294 -> 425, rank 8: 122 -> 14, rank 7: 24 -> 0) and paid calls fall 69,912 -> 66,852 + (headline) / 67,374 (supporting). + +## Files +- `WORD.json.gz` (headline, free starts + finals) and `WORD-STARTS-ONLY.json.gz` (supporting). +- `retime.py`: the CP-SAT solve is multi-worker and not byte-reproducible, so instead of a generator + this exact stdlib checker proves a candidate is a legal retime of the pinned word: identical scalar + program, MOVEs a subsequence of the pinned MOVEs, all 208 main endpoint spans unchanged, 104 ports + and live list equal. Nesting, ownership, the common-chart frame law and rank = dimension gap are then + enforced by the unmodified PR5545 `local.py` replay and `native()`. +- `pricing.py`, `pricing-starts-only.py`: PR5551's `pricing.py` (`inputs/pr5551-pricing.py`) with ONLY + literal changes: the KAPPA/TESTED claim line, the call census 69912 -> 66852 / 67374, and the + `kappa_decimal` label. `LITERAL-CHANGES.diff` shows them; `verify.py` re-applies the substitutions + and checks byte equality. No `local.py` change is needed (735 public inputs), so the unmodified + PR5545 `local.py` from the byte-pinned capsule is used. +- `verify.py` / `verify.sh` (stdlib, Python 3.12): `--part headline` and `--part starts-only`, each + about 6 minutes: retime legality, replay, transposed columns, native maps, physical caller, pricing + with both moment engines, all 54 strict + 4 functional outer checks, exact crossing interval. +- `inputs/pr5545-source-closure.tar.gz`, `inputs/pr5551-WORD.json.gz`, `inputs/pr5551-pricing.py`: + PR5551's byte-pinned inputs (`SOURCES.json`). + +## Independent audit +An internal AI audit (separate read-only Claude agent) reproduced an earlier version of this retime on +PR5545's word through the real replay/native/pricing stack, found helper credit and main endpoints +sound, and rated maintainer intent for free helper frames as unresolved, which is why this is +conditional. The PR5551-based words here are checked by `verify.py`; they have not had a separate audit. + +## Credits +Builds on PR5551 (thu-nmrc) and the P104 word line of PR5544/5545 (aliromman; lineage +PR2305/2152/2219). The idea of a fresh helper starting at a non-canonical frame follows the +hand-off precedent of PR5472 (GamingPuzzled). All predecessor credit is retained. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. + +## Open next questions + +- Are free helper start frames (non-canonical, mid-frame) admissible in the P104 caller contract? Both words depend on it; the supporting word depends on nothing else. +- Are free helper final frames admissible? The finals-free gain is the difference between the two words (.0030814243 vs .0030768801). +- Can the retime be reproduced by a deterministic single-threaded solve, so a generator can replace the checker? +- Independent reproduction of PR5551, on which this package builds. Interaction with hand-off words such as PR5553 is not tested here. diff --git a/research/p104-free-endpoint-retime/RESULT.json b/research/p104-free-endpoint-retime/RESULT.json new file mode 100644 index 0000000000..a953f0a60a --- /dev/null +++ b/research/p104-free-endpoint-retime/RESULT.json @@ -0,0 +1,416 @@ +{ + "headline": { + "compiler": { + "H": 690116000000000, + "N": "2^690116000000000", + "eta": { + "lower": "0.000000150915557284809901282836", + "upper": "0.000000150915557284809901282837" + }, + "gap": "1/14000000000", + "integer_test_exponent": 49294, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "21569943/7000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "161/4000000", + "kappa": "154071/50000000", + "kappa_decimal": ".00308142", + "margin_at_previous": { + "lower": "9.863889227373890942015545303213", + "upper": "9.863889227373890942015545303214" + }, + "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": 5164000, + "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": "603958375956860117/196000000000000000000", + "fused_gaussian": "603958375870580351/196000000000000000000", + "global_coordinate_router": "10784971/3500000000", + "group_bit_router": "150989597467645087/49000000000000000000", + "group_scans": "6999999999/7000000000", + "main_transform": "603958361956860117/196000000000000000000", + "microbox_face_corrections": "269500000001/3500000000", + "polynomial_products": "13999999999/14000000000", + "sparse_union_movement": "80228958375956860117/196000000000000000000" + }, + "parameters": { + "a": "10784971/3500000000", + "b": "8627977/2800000000", + "beta": "13999999997/14000000000", + "bit_saving": "17/5000", + "cap_xi": "178228958361956860117/196000000000000000000", + "complex_uniform_saving": "21569943/7000000000", + "d": "1/14000000000", + "epsilon": "13999999999/14000000000", + "kappa": "154071/50000000", + "lambda_": "3987674319/4000000000", + "lambda_prime": "13956860117/14000000000", + "layout": "1/14000000000", + "q": "43139883/14000000000", + "r0": "1/140000000000", + "stop": "1/14000000000", + "tested_saving": "6162841/2000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "1115029/3500000000", + "actual_logarithmic_gamma_guard": "1/14000000000", + "actual_logarithmic_group_guard": "17771041659043139883/98000000000000000000", + "alpha_logarithm_absorption": "1/140000000000", + "boundary_algebraic_matrix_above_kappa": "55956860117/196000000000000000000", + "cap_above_band": "80228958361956860117/196000000000000000000", + "cap_below_cell": "17771041624043139883/196000000000000000000", + "cap_below_phase_cell_power": "213771041638043139883/196000000000000000000", + "complex_above_effective": "1/14000000000", + "complex_below_one_over_32": "78872023/2800000000", + "complex_endpoint": "1/7000000000", + "epsilon_below_one": "1/14000000000", + "epsilon_positive": "13999999999/14000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "55870580351/196000000000000000000", + "gaussian_above_main": "6956860117/98000000000000000000", + "global_coordinate_router_above_kappa": "1/3500000000", + "global_gamma_power_slack": "9/140000000000", + "group_below_dimension": "1/7000000000", + "group_bit_router_above_kappa": "17467645087/49000000000000000000", + "group_gauge_power_slack": "17771041658343139883/98000000000000000000", + "group_key_fits_record": "1/7000000000", + "group_positive": "13999999997/14000000000", + "group_scans_above_kappa": "6978430059/7000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "675224790400418148631/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": "5591372023/39200000000000000000", + "leaf_saving_above_effective": "2791372023/39200000000000000000", + "main_transform_above_kappa": "41956860117/196000000000000000000", + "membership_arithmetic_fits_record": "1/14000000000", + "microbox_face_corrections_above_kappa": "269489215031/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": "13956860119/14000000000", + "positive_layout_slack": "1/14000000000", + "q_below_effective": "1/14000000000", + "q_below_internal": "1/14000000000", + "q_below_leaf": "5591372023/39200000000000000000", + "q_positive": "43139883/14000000000", + "short_record_fallback": "2791372023/2800000000", + "source_axis_superpolynomial": "1/14000000000", + "sparse_union_movement_above_kappa": "79625000055956860117/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": 41340, + "16": 416, + "2": 8262, + "24": 416, + "3": 8928, + "32": 416, + "4": 1674, + "40": 416, + "48": 416, + "5": 2952, + "56": 416, + "6": 324, + "64": 416, + "7": 252, + "72": 208 + }, + "paid_calls": 66852, + "previous_open_pr5545": "304117/100000000", + "productive_fields": 12814, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "21669/5000000000000", + "433381/100000000000000" + ], + "raw_root_interval": [ + "15407121669/5000000000000", + "308142433381/100000000000000" + ], + "relative_gain_percent": "402500/304117", + "strictification": { + "alpha": { + "lower": "0.999999996077490279252156945261", + "upper": "0.999999996077490279252156945262" + }, + "cutoff": 17, + "delta": { + "lower": "0.954776932282871740517530812724", + "upper": "0.954776932282871740517530812725" + }, + "floor": 18, + "gamma": { + "lower": "0.967371300368832148444639574582", + "upper": "0.967371300368832148444639574583" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "6162841/2000000000" + }, + "targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "4": 1494, + "41": 416, + "49": 416, + "5": 90, + "57": 416, + "65": 416, + "73": 208, + "8": 252, + "9": 7650 + }, + "whole_idle_jobs": 3120 + }, + "starts_only": { + "compiler": { + "H": 690116000000000, + "N": "2^690116000000000", + "eta": { + "lower": "0.000000154449432404612929595969", + "upper": "0.000000154449432404612929595970" + }, + "gap": "1/14000000000", + "integer_test_exponent": 49294, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "5384539/1750000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "35709/1000000000", + "kappa": "3076879/1000000000", + "kappa_decimal": ".003076879", + "margin_at_previous": { + "lower": "8.763458055403927069103933159568", + "upper": "8.763458055403927069103933159569" + }, + "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": 5193000, + "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": "603068339956923691/196000000000000000000", + "fused_gaussian": "603068339870771073/196000000000000000000", + "global_coordinate_router": "4307631/1400000000", + "group_bit_router": "60306835387077107/19600000000000000000", + "group_scans": "6999999999/7000000000", + "main_transform": "603068325956923691/196000000000000000000", + "microbox_face_corrections": "269500000001/3500000000", + "polynomial_products": "13999999999/14000000000", + "sparse_union_movement": "80228068339956923691/196000000000000000000" + }, + "parameters": { + "a": "4307631/1400000000", + "b": "43076311/14000000000", + "beta": "13999999997/14000000000", + "bit_saving": "17/5000", + "cap_xi": "178228068325956923691/196000000000000000000", + "complex_uniform_saving": "5384539/1750000000", + "d": "1/14000000000", + "epsilon": "13999999999/14000000000", + "kappa": "3076879/1000000000", + "lambda_": "3987692483/4000000000", + "lambda_prime": "13956923691/14000000000", + "layout": "1/14000000000", + "q": "43076309/14000000000", + "r0": "1/140000000000", + "stop": "1/14000000000", + "tested_saving": "6153759/2000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "452369/1400000000", + "actual_logarithmic_gamma_guard": "1/14000000000", + "actual_logarithmic_group_guard": "17771931695043076309/98000000000000000000", + "alpha_logarithm_absorption": "1/140000000000", + "boundary_algebraic_matrix_above_kappa": "55956923691/196000000000000000000", + "cap_above_band": "80228068325956923691/196000000000000000000", + "cap_below_cell": "17771931660043076309/196000000000000000000", + "cap_below_phase_cell_power": "213771931674043076309/196000000000000000000", + "complex_above_effective": "1/14000000000", + "complex_below_one_over_32": "394423689/14000000000", + "complex_endpoint": "1/7000000000", + "epsilon_below_one": "1/14000000000", + "epsilon_positive": "13999999999/14000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "55870771073/196000000000000000000", + "gaussian_above_main": "6956923691/98000000000000000000", + "global_coordinate_router_above_kappa": "1/3500000000", + "global_gamma_power_slack": "9/140000000000", + "group_below_dimension": "1/7000000000", + "group_bit_router_above_kappa": "6987077107/19600000000000000000", + "group_gauge_power_slack": "17771931694343076309/98000000000000000000", + "group_key_fits_record": "1/7000000000", + "group_positive": "13999999997/14000000000", + "group_scans_above_kappa": "3489230923/3500000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "672954290400418148631/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": "27956923689/196000000000000000000", + "leaf_saving_above_effective": "13956923689/196000000000000000000", + "main_transform_above_kappa": "41956923691/196000000000000000000", + "membership_arithmetic_fits_record": "1/14000000000", + "microbox_face_corrections_above_kappa": "538978461849/7000000000", + "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": "13956923693/14000000000", + "positive_layout_slack": "1/14000000000", + "q_below_effective": "1/14000000000", + "q_below_internal": "1/14000000000", + "q_below_leaf": "27956923689/196000000000000000000", + "q_positive": "43076309/14000000000", + "short_record_fallback": "13956923689/14000000000", + "source_axis_superpolynomial": "1/14000000000", + "sparse_union_movement_above_kappa": "79625000055956923691/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": 42204, + "16": 416, + "2": 8442, + "24": 416, + "3": 8442, + "32": 416, + "4": 1638, + "40": 416, + "48": 416, + "5": 2970, + "56": 416, + "6": 306, + "64": 416, + "7": 252, + "72": 208 + }, + "paid_calls": 67374, + "previous_open_pr5545": "304117/100000000", + "productive_fields": 12814, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "27003/25000000000000", + "108013/100000000000000" + ], + "raw_root_interval": [ + "76922002003/25000000000000", + "307688008013/100000000000000" + ], + "relative_gain_percent": "357090/304117", + "strictification": { + "alpha": { + "lower": "0.999999999404592592047426513673", + "upper": "0.999999999404592592047426513674" + }, + "cutoff": 17, + "delta": { + "lower": "0.956340515100833390077946018407", + "upper": "0.956340515100833390077946018408" + }, + "floor": 18, + "gamma": { + "lower": "0.967169144621326622973846552884", + "upper": "0.967169144621326622973846552885" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "6153759/2000000000" + }, + "targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "4": 1494, + "41": 416, + "49": 416, + "5": 90, + "57": 416, + "65": 416, + "7": 18, + "73": 208, + "8": 612, + "9": 7272 + }, + "whole_idle_jobs": 3120 + }, + "status": "PASS_P104_FREE_ENDPOINT_RETIME_CONDITIONAL_KAPPA" +} diff --git a/research/p104-free-endpoint-retime/SOURCES.json b/research/p104-free-endpoint-retime/SOURCES.json new file mode 100644 index 0000000000..2fe44de014 --- /dev/null +++ b/research/p104-free-endpoint-retime/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-free-endpoint-retime/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 (no local.py edit is needed: the retimed words keep 735 public inputs)." + }, + "pinned_word": { + "path": "research/p104-free-endpoint-retime/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-free-endpoint-retime/inputs/pr5551-pricing.py", + "source_path": "research/p104-joint-contact/pricing.py at PR5551 head" + } +} diff --git a/research/p104-free-endpoint-retime/TASK.json b/research/p104-free-endpoint-retime/TASK.json new file mode 100644 index 0000000000..7a34be8497 --- /dev/null +++ b/research/p104-free-endpoint-retime/TASK.json @@ -0,0 +1,116 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "actual_scope": "On PR5551's pinned P104 word, retime the helper START and FINAL frames (and the intermediate frames of the shared ADD charts) with an exact-lattice CP-SAT solve, collapsing 170 now-redundant stops (141 for the starts-only variant); the 54 strict + 4 functional outer checks and the exact crossing are re-certified for the changed complete conditional moment.", + "bottleneck_link": "Free helper endpoints let credited helper rank move from many rank-8 climbs to rank-9 climbs and remove 170 rank-1 stops per call; at all 18 calls this lowers the paid profile (69,912 -> 66,852 calls) at unchanged rank-mass surplus 760, so the concave moment gap widens.", + "stop_rule": "Retain the conditional kappa only after retime.py proves each word a legal retime of PR5551's word and 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": "Are free helper START frames (non-canonical, mid-frame) admissible in the P104 caller contract?", + "why_it_matters": "Both words depend on it; the starts-only word depends on nothing else. The verifier checks only nesting and rank = dim gap for helpers; the canonical-start rule exists only in the #4610 verifier, and unmodified PR5544/5545 already has helper starts at dims 0,1,4,5.", + "blocked_by": "Maintainer or swarm review.", + "first_step": "Decide whether helper identity rows at arbitrary nested start frames are intended in the P104 caller; WORD-STARTS-ONLY.json.gz is the test case." + }, + { + "question": "Are free helper FINAL frames admissible?", + "why_it_matters": "The headline word changes 23 helper finals (mostly dim 8 -> 9); the extra gain from finals is the difference between the two words.", + "blocked_by": "Maintainer or swarm review.", + "first_step": "Compare the two words: the finals-free gain is the difference .0030814243 - .0030768801." + }, + { + "question": "Can the retime be reproduced byte-for-byte by a deterministic solver?", + "why_it_matters": "The words are checked, not generated; a deterministic generator would shorten review.", + "blocked_by": "None; the solve is a multi-worker CP-SAT run.", + "first_step": "Re-run the exact-lattice solve single-threaded with a fixed seed and compare against retime.py." + } + ], + "scope_status": "changed", + "scope_change_reason": "The scalar-to-moment card asks about scalar A2 contractions on the retained word; this package instead retimes helper endpoint and stop frames of 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 checks each word with retime.py (legal retime of PR5551's pinned word: identical scalar program, only stops deleted and frame labels changed, all 208 main endpoint spans unchanged), the unmodified PR5545 local.py replay/columns/native, the physical caller, PR5551's pricing with literal-only changes, both moment engines, all 54 strict + 4 functional outer checks, and the exact crossing interval for each word.", + "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-free-endpoint-retime/VERIFY.json b/research/p104-free-endpoint-retime/VERIFY.json new file mode 100644 index 0000000000..a4cfbef7c2 --- /dev/null +++ b/research/p104-free-endpoint-retime/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "headline" + ], + "timeout_seconds": 600, + "checks": "Main claim: retime.py legality of WORD.json.gz against PR5551's word; unmodified PR5545 replay, transposed columns, native maps, physical caller; literal-only pricing; both moment engines; 54 strict + 4 functional outer checks; exact crossing interval." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "starts-only" + ], + "timeout_seconds": 600, + "checks": "Supporting: the same chain for WORD-STARTS-ONLY.json.gz (helper finals unchanged), which needs only free helper start frames." + } + ] +} diff --git a/research/p104-free-endpoint-retime/WORD-STARTS-ONLY.json.gz b/research/p104-free-endpoint-retime/WORD-STARTS-ONLY.json.gz new file mode 100644 index 0000000000..b0c13f48e9 Binary files /dev/null and b/research/p104-free-endpoint-retime/WORD-STARTS-ONLY.json.gz differ diff --git a/research/p104-free-endpoint-retime/WORD.json.gz b/research/p104-free-endpoint-retime/WORD.json.gz new file mode 100644 index 0000000000..c367d865a1 Binary files /dev/null and b/research/p104-free-endpoint-retime/WORD.json.gz differ diff --git a/research/p104-free-endpoint-retime/common.py b/research/p104-free-endpoint-retime/common.py new file mode 100644 index 0000000000..b8368c7948 --- /dev/null +++ b/research/p104-free-endpoint-retime/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-free-endpoint-retime-')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-free-endpoint-retime/inputs/pr5545-source-closure.tar.gz b/research/p104-free-endpoint-retime/inputs/pr5545-source-closure.tar.gz new file mode 100644 index 0000000000..3084088544 Binary files /dev/null and b/research/p104-free-endpoint-retime/inputs/pr5545-source-closure.tar.gz differ diff --git a/research/p104-free-endpoint-retime/inputs/pr5551-WORD.json.gz b/research/p104-free-endpoint-retime/inputs/pr5551-WORD.json.gz new file mode 100644 index 0000000000..c04a815c26 Binary files /dev/null and b/research/p104-free-endpoint-retime/inputs/pr5551-WORD.json.gz differ diff --git a/research/p104-free-endpoint-retime/inputs/pr5551-pricing.py b/research/p104-free-endpoint-retime/inputs/pr5551-pricing.py new file mode 100644 index 0000000000..ef78de99ff --- /dev/null +++ b/research/p104-free-endpoint-retime/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-free-endpoint-retime/pricing-starts-only.py b/research/p104-free-endpoint-retime/pricing-starts-only.py new file mode 100644 index 0000000000..e32cbc0fe1 --- /dev/null +++ b/research/p104-free-endpoint-retime/pricing-starts-only.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('.003076879'), Q('.0030768795') +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()) == 67374, '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':'.003076879','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-free-endpoint-retime/pricing.py b/research/p104-free-endpoint-retime/pricing.py new file mode 100644 index 0000000000..8d3e006225 --- /dev/null +++ b/research/p104-free-endpoint-retime/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('.00308142'), Q('.0030814205') +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()) == 66852, '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':'.00308142','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-free-endpoint-retime/retime.py b/research/p104-free-endpoint-retime/retime.py new file mode 100644 index 0000000000..fa8b19a7ce --- /dev/null +++ b/research/p104-free-endpoint-retime/retime.py @@ -0,0 +1,88 @@ +"""Exact checker: a candidate word is a legal helper-endpoint retime of PR5551's pinned word. Apache-2.0. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. + +The two shipped words were found by an exact-lattice CP-SAT retiming (multi-worker, so +not byte-reproducible); this module is therefore a CHECKER, not a generator. It proves, with +stdlib only, that a candidate differs from the pinned word ONLY as follows: + 1. the non-MOVE scalar program (operation, registers, coefficient, order) is identical; + 2. the candidate's MOVEs are a subsequence of the pinned MOVEs (stops may be deleted, + none added, none reordered across scalar events, same register); + 3. frame labels may change, but all 208 MAIN registers (104 X sources, 104 Y targets) keep + the SAME SPAN at their initial and final frames (X-initial and Y-final are the literal + ports). Intermediate main frames may change where a shared ADD chart moves together + with a retimed helper; these are counted, not forbidden; + 4. the 104 ports, live list and public count are equal. +Nesting, ownership, rank = dimension gap and the frame law at every ADD/COPY/SCALE are then +enforced by the unmodified PR5544/5545 local.py replay and native() (see verify.py). +""" + +def rref(basis): + """Canonical form of the F2 span of integer bit-vectors (reduced row echelon, sorted).""" + rows=[] + for v in basis: + for r in rows: + if v^r0 for k in('strict_checks','functional_checks') for x in res['outer'][k].values()),'all outer checks strict') + lo,hi=[Fraction(x) for x in spec['interval']] + print(name,'crossing kappa in (%.14f, %.14f); 54 strict + 4 functional outer checks pass'%(lo,hi),flush=True) + out[name]=res + if '--write' in sys.argv and part=='all': + (HERE/'RESULT.json').write_text(json.dumps({'status':'PASS_P104_FREE_ENDPOINT_RETIME_CONDITIONAL_KAPPA','headline':out['headline'], + 'starts_only':out['starts-only']},indent=1,sort_keys=True,default=str)+'\n') + print('PASS P104_FREE_ENDPOINT_RETIME',part) +main() diff --git a/research/p104-free-endpoint-retime/verify.sh b/research/p104-free-endpoint-retime/verify.sh new file mode 100755 index 0000000000..d7a4b8e1b5 --- /dev/null +++ b/research/p104-free-endpoint-retime/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/p104-priced-handoff/LITERAL-CHANGES.diff b/research/p104-priced-handoff/LITERAL-CHANGES.diff new file mode 100644 index 0000000000..d89bdccc85 --- /dev/null +++ b/research/p104-priced-handoff/LITERAL-CHANGES.diff @@ -0,0 +1,20 @@ +--- inputs/pr5561-pricing.py (PR5561 head 452d27dd) ++++ pricing.py +@@ -11,7 +11,7 @@ + from fractions import Fraction as Q + import local as L + +-KAPPA, TESTED = Q('.00308142'), Q('.0030814205') ++KAPPA, TESTED = Q('.00308181'), Q('.0030818105') + PREVIOUS = Q('.00304117') + + +@@ -139,7 +139,7 @@ + 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':'.00308142','previous_open_pr5545':PREVIOUS,'gain':KAPPA-PREVIOUS, ++ return encode({'kappa':KAPPA,'kappa_decimal':'.00308181','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()), diff --git a/research/p104-priced-handoff/README.md b/research/p104-priced-handoff/README.md new file mode 100644 index 0000000000..81c5660a3c --- /dev/null +++ b/research/p104-priced-handoff/README.md @@ -0,0 +1,128 @@ +# One priced successor hand-off on PR5561's P104 word (conditional kappa .00308181) + +Complete conditional kappa **.00308181** (certified claim line; tested at .0030818105). The raw crossing is +.0030818185, which is **+3.94e-7** (+0.0128%) over the raw crossing .0030814243 of +[PR5561](https://github.com/CrocSwap/integer-mult-bounds/pull/5561) (claim line .00308142). The exact raw crossing lies in +(154090925761/50000000000000, 308181851523/100000000000000) = (.00308181851522, .00308181851523). + +**Conditional on** the same assumptions as PR5561: +(a) the five framework assumptions retained by PR5544/5545/5551; +(b) the validity of PR5551 and PR5561, neither independently reproduced at the time of writing; +(c) free helper FINAL frames. The edit lowers one helper final frame from dim 9 to dim 8, as PR5561's headline +word does for 23 helpers. It needs no new start frame. +The selected record is not changed. No independent human or proof-kernel acceptance is claimed. + +## Mechanism (successor hand-off with one co-framed partner) + +This is the successor hand-off of PR5472 with **co-framed cancellation** (R18 notation), priced with the +re-flagging cost of the R19 addendum. Helper 706 has initial dim 0 and final dim 9 in PR5561's headline word. +- **Last read.** Event 15443 (`ADD 121 += -2*706`, frame 549, dim 7) is its last read. From then on its row is + `706 + D`, and no other register holds symbol 706. +- **The only remaining use.** `MOVE 706 549->127` (rank 2), then the uncompute `ADD 706 += -1/2*173` at frame + 127 (dim 9). +- **The partner.** Main register 173 (Y target of port 61) sits at frame 559 (dim 8, 549 < 559 < 127) from event + 13089 until event 17248. Its row is constant after event 13097, so `-1/2*row(173) = -D` already holds at + event 15443. + +The successor hand-off at F = 559: +1. 706 climbs to F (`MOVE 549->559`, rank 1). +2. 706 cancels D against the co-framed partner (`ADD 706 += -1/2*173 @559`). +3. 706 retires at F. + +The successor would start at F and carry nothing up to dim 9. It would be a rank-1 spectator: one rank-1 target +and one rank-1 climb, which is moment-neutral, like PR5553's "Variant A". It is therefore omitted. The literal +edit (`handoff.py`) is: + +| | PR5561 headline word | this word | +|---|---|---| +| after event 15443 | (idle) | `MOVE 706 549->559`, `ADD 706 += -1/2*173 @559` | +| events 17251/17252 | `MOVE 706 549->127`, `ADD 706 += -1/2*173 @127` | deleted (moved) | +| `final[706]` | frame 127 (dim 9) | frame 559 (dim 8) | +| events / public inputs | 25,140 / 735 | 25,140 / 735 (same scalar events; one ADD moved and relabelled) | + +Per call, credited helper 706 drops from rank 9 to rank 8, and one paid rank-2 climb becomes rank 1. The +rank-mass surplus stays 760, productive fields stay 12,814 and paid calls stay 66,852. + +Seen as a hand-off, the gain is g(8,1) = f(8)+f(1)−f(9) = 0.009632 and the re-flagging cost (the helper's own +new stop 7->8->9) is g(1,1) = 0.004267. That leaves a net +0.005365 per call at f(x) = x^(1−C), C = .0030814, +which is strict at all 18 calls. + +## Exhaustive screen (tools/, outputs `tools/*.txt`) + +All screens run on PR5561's headline word and cover every non-main helper (527), every event and every mid frame +F with dim strictly between the helper's initial and final dims. + +| family | tool | result | +|---|---|---| +| free hand-off (helper pure, no other holder; PR5553's form) | `screen.py` | 0 on PR5561. Control: exactly PR5553's two (473 at ev 13725, 531 at ev 13941) on PR5551's word | +| co-framed span hand-off at existing frames | `screen2.py` | 0 (800 holder-co-framed points; span fails) | +| frame-independent mid-life pure windows | `windows.py` | 0: on this scalar program, free hand-offs are only endpoint retimes, which PR5561's free starts and finals already absorb | +| priced: all holders co-framed with lifts at any nested F, plus span closure over co-frameable registers | `lift21.py` | 589,992 (helper, event) points. 81 span-feasible with holders only: all net < 0 (best −0.00051; each needs a new stop on the helper, so cost ≥ gain). 24 more span-feasible after closure: exact frame-identity pricing leaves 1 net > 0 (this one) | +| priced single partner (row(j) ∝ carried D), every event and any nested F, both via chain frames and via generic F | `partner.py` | 1,086 matches; **1 net > 0** (706/173 at F = 559) | + +Scope of the screen: +- 2,832 points where an owned private scratch register (735..742) holds the helper symbol were skipped. +- Multi-partner closures are priced greedily (`lift21.py`), so they give an upper bound on the minimal-cost + closure. +- The same single candidate is also present on PR5561's starts-only word and on PR5551's word. PR5553 found only + the free ones. + +The orientation is forward only. The P104 caller invokes every source forward (`pricing.py` requires it). + +**Independent second check (outside the package).** The checker of PR5550 (Chris R / Clear1nsight) was patched +exactly as in PR5567 (Matarener: four literal input lines, temporary copy) and run on `WORD.json.gz` with this +package's invoice. It returns `PASS_SCOPED_CALLER_AND_TARGET_BINDING`: +- 66,852 paid / 12,814 productive; +- 527 helper normalizers and 274 exact signed-Pauli and phase anchors; +- all 10 controls reject; +- 124,232,680 ordinary passes ≤ 184,647,552. + +The unchanged PR5561 paid invoice is rejected on this word. PR5567 also argues that free helper endpoints are the +contract the unmodified P104 `local.py` implements, which bears on condition (c). + +## Files +- `handoff.py`: derives `WORD.json.gz` from `inputs/pr5561-WORD.json.gz`, with byte-exact regeneration checked. +- `pricing.py`: PR5561's `pricing.py` (`inputs/pr5561-pricing.py`) with only the KAPPA/TESTED claim line and the + `kappa_decimal` label changed (`LITERAL-CHANGES.diff`). The unmodified PR5545 `local.py` is used from the + byte-pinned capsule (735 public inputs). +- `verify.py` / `verify.sh` (stdlib, Python 3.12, about 4 minutes): + - input pins and regeneration; + - the edit inventory against PR5561's word; + - the exact hand-off condition (rational rows: sole holder, `row(706) = 706 + 1/2 row(173)`, partner row + constant until the original uncompute, frames 549 < 559 < 127); + - the unmodified PR5545 replay, transposed columns and native maps; + - the physical caller; + - both moment engines; + - all 54 strict + 4 functional outer checks; + - the exact crossing interval; + - four mutation controls, each rejected by `local.py`: no stop, wrong coefficient, final not lowered, and the + hand-off placed before the last read. +- `tools/`: the screens above, with `run_screens.sh` and the recorded outputs. +- `inputs/`: PR5561's headline word and pricing, and the PR5545 capsule. All are byte-pinned (`SOURCES.json`). + +## Reproduce +```sh +python3.12 -B scripts/research_package.py --package research/p104-priced-handoff +sh research/p104-priced-handoff/verify.sh # PASS P104_PRICED_HANDOFF +sh research/p104-priced-handoff/tools/run_screens.sh +``` + +## Credits +- DreamingOfClouds: PR5561 (free helper endpoints, the base word) and PR5553 (free hand-offs on PR5551). +- thu-nmrc: PR5551 (coupled P104 contacts). +- aliromman: PR5544/5545 (P104 word line, `local.py`). +- Lineage: PR2305/2152/2219. The credits in `local.py` (David Arias, Cinna Davis, Gareth Davidson) are retained. +- zxv: productive-helper paradigm #4359; PR5554 regime limits. +- Cao Yifan: #4610 native semantics. +- PR5472 (GamingPuzzled): the successor hand-off and its R18/R19 pricing. +All predecessor credit is retained. + +AI disclosure: Claude Opus 5.5 (Anthropic) via Claude Code, directed by Joel Pulikkan (GamingPuzzled). Apache-2.0. + +## Open next questions + +- Are free helper final frames admissible? This package inherits PR5561's condition (c). +- Do owned private scratch holders (registers 735..742) admit further priced hand-offs? The screen skipped 2,832 + such points. +- Can a joint retime and hand-off solve, in which PR5561's CP-SAT lattice also lets ADDs move within their idle + windows, find more co-framed partners? On the fixed PR5561 frames, only one net-positive hand-off exists. diff --git a/research/p104-priced-handoff/RESULT.json b/research/p104-priced-handoff/RESULT.json new file mode 100644 index 0000000000..a25ae8c11e --- /dev/null +++ b/research/p104-priced-handoff/RESULT.json @@ -0,0 +1,228 @@ +{ + "condition": { + "carried_symbols": 118, + "holders_of_706": 1, + "partner": "main register 173 (Y target of port register 61)" + }, + "controls": { + "final not lowered": "rejected: All public and owned exits", + "hand-off before the last read of 706": "rejected: Scalar destination and coefficient", + "no stop (ADD at 559 while 706 is at 549)": "rejected: Scalar destination and coefficient", + "wrong coefficient -1": "rejected: All 743 public and owned rows" + }, + "inventory": { + "changed_finals": [ + 706 + ], + "events": 25140, + "moved_add": "17252 -> 15445", + "stop": "706: 549 -> 559 (dim 7 -> 8) replaces 549 -> 127 (dim 7 -> 9)" + }, + "result": { + "compiler": { + "H": 690116000000000, + "N": "2^690116000000000", + "eta": { + "lower": "0.000000150615850302309784079917", + "upper": "0.000000150615850302309784079918" + }, + "gap": "1/14000000000", + "integer_test_exponent": 49294, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "21572673/7000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "127/3125000", + "kappa": "308181/100000000", + "kappa_decimal": ".00308181", + "margin_at_previous": { + "lower": "9.959205574848701606339600937574", + "upper": "9.959205574848701606339600937575" + }, + "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": 5164000, + "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": "604034815956854657/196000000000000000000", + "fused_gaussian": "604034815870563971/196000000000000000000", + "global_coordinate_router": "337073/109375000", + "group_bit_router": "4719022108363781/1531250000000000000", + "group_scans": "6999999999/7000000000", + "main_transform": "604034801956854657/196000000000000000000", + "microbox_face_corrections": "269500000001/3500000000", + "polynomial_products": "13999999999/14000000000", + "sparse_union_movement": "80229034815956854657/196000000000000000000" + }, + "parameters": { + "a": "337073/109375000", + "b": "8629069/2800000000", + "beta": "13999999997/14000000000", + "bit_saving": "17/5000", + "cap_xi": "178229034801956854657/196000000000000000000", + "complex_uniform_saving": "21572673/7000000000", + "d": "1/14000000000", + "epsilon": "13999999999/14000000000", + "kappa": "308181/100000000", + "lambda_": "3987672759/4000000000", + "lambda_prime": "13956854657/14000000000", + "layout": "1/14000000000", + "q": "43145343/14000000000", + "r0": "1/140000000000", + "stop": "1/14000000000", + "tested_saving": "6163621/2000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "17401/54687500", + "actual_logarithmic_gamma_guard": "1/14000000000", + "actual_logarithmic_group_guard": "17770965219043145343/98000000000000000000", + "alpha_logarithm_absorption": "1/140000000000", + "boundary_algebraic_matrix_above_kappa": "55956854657/196000000000000000000", + "cap_above_band": "80229034801956854657/196000000000000000000", + "cap_below_cell": "17770965184043145343/196000000000000000000", + "cap_below_phase_cell_power": "213770965198043145343/196000000000000000000", + "complex_above_effective": "1/14000000000", + "complex_below_one_over_32": "78870931/2800000000", + "complex_endpoint": "1/7000000000", + "epsilon_below_one": "1/14000000000", + "epsilon_positive": "13999999999/14000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "55870563971/196000000000000000000", + "gaussian_above_main": "6956854657/98000000000000000000", + "global_coordinate_router_above_kappa": "1/3500000000", + "global_gamma_power_slack": "9/140000000000", + "group_below_dimension": "1/7000000000", + "group_bit_router_above_kappa": "545863781/1531250000000000000", + "group_gauge_power_slack": "17770965218343145343/98000000000000000000", + "group_key_fits_record": "1/7000000000", + "group_positive": "13999999997/14000000000", + "group_scans_above_kappa": "6978427329/7000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "675419790400418148631/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": "5591370931/39200000000000000000", + "leaf_saving_above_effective": "2791370931/39200000000000000000", + "main_transform_above_kappa": "41956854657/196000000000000000000", + "membership_arithmetic_fits_record": "1/14000000000", + "microbox_face_corrections_above_kappa": "134744606833/1750000000", + "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": "13956854659/14000000000", + "positive_layout_slack": "1/14000000000", + "q_below_effective": "1/14000000000", + "q_below_internal": "1/14000000000", + "q_below_leaf": "5591370931/39200000000000000000", + "q_positive": "43145343/14000000000", + "short_record_fallback": "2791370931/2800000000", + "source_axis_superpolynomial": "1/14000000000", + "sparse_union_movement_above_kappa": "79625000055956854657/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": 41358, + "16": 416, + "2": 8244, + "24": 416, + "3": 8928, + "32": 416, + "4": 1674, + "40": 416, + "48": 416, + "5": 2952, + "56": 416, + "6": 324, + "64": 416, + "7": 252, + "72": 208 + }, + "paid_calls": 66852, + "previous_open_pr5545": "304117/100000000", + "productive_fields": 12814, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "425761/50000000000000", + "851523/100000000000000" + ], + "raw_root_interval": [ + "154090925761/50000000000000", + "308181851523/100000000000000" + ], + "relative_gain_percent": "406400/304117", + "strictification": { + "alpha": { + "lower": "0.999999991799751937818805906662", + "upper": "0.999999991799751937818805906663" + }, + "cutoff": 17, + "delta": { + "lower": "0.954848235883992924843231716007", + "upper": "0.954848235883992924843231716008" + }, + "floor": 18, + "gamma": { + "lower": "0.967388387929834548764409888758", + "upper": "0.967388387929834548764409888759" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "6163621/2000000000" + }, + "targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "4": 1494, + "41": 416, + "49": 416, + "5": 90, + "57": 416, + "65": 416, + "73": 208, + "8": 270, + "9": 7632 + }, + "whole_idle_jobs": 3120 + }, + "status": "PASS_P104_PRICED_HANDOFF_CONDITIONAL_KAPPA" +} diff --git a/research/p104-priced-handoff/SOURCES.json b/research/p104-priced-handoff/SOURCES.json new file mode 100644 index 0000000000..43360008e0 --- /dev/null +++ b/research/p104-priced-handoff/SOURCES.json @@ -0,0 +1,39 @@ +{ + "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-priced-handoff/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/PR5561; used UNMODIFIED (the hand-off word keeps 735 public inputs)." + }, + "pinned_word": { + "path": "research/p104-priced-handoff/inputs/pr5561-WORD.json.gz", + "sha256": "b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44", + "source_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5561", + "source_head": "452d27dde67ee9f772dbbd3be129db97a8ecb9c1", + "source_path": "research/p104-free-endpoint-retime/WORD.json.gz" + }, + "pinned_pricing": { + "path": "research/p104-priced-handoff/inputs/pr5561-pricing.py", + "sha256": "701f87ebf3742d55f21ccdb2fd13d04fc2019a6b6190d8542bb7f5d477c71de5", + "source_path": "research/p104-free-endpoint-retime/pricing.py at PR5561 head 452d27dd" + } +} diff --git a/research/p104-priced-handoff/TASK.json b/research/p104-priced-handoff/TASK.json new file mode 100644 index 0000000000..6be86275af --- /dev/null +++ b/research/p104-priced-handoff/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "actual_scope": "On PR5561's headline P104 word, one priced successor hand-off: helper 706 cancels its carried data against co-framed main register 173 at frame 559 (dim 8) right after its last read, instead of at frame 127 (dim 9) after a rank-2 climb. Found by an exhaustive screen of all helpers, events and mid frames (free, co-framed-span and single-partner priced families); the 54 strict + 4 functional outer checks and the exact crossing are re-certified.", + "bottleneck_link": "Successor hand-off (PR5472 pattern) splits the credited helper target 9 -> 8 + 1 (rank-1 spectator omitted) at the price of one extra stop 7 -> 8 -> 9 on the helper itself (paid rank 2 -> 1 after the spectator is dropped); net concave gain g(8,1) - g(1,1) > 0 at all 18 calls, rank-mass surplus 760 unchanged.", + "stop_rule": "Retain the conditional kappa only after verify.py proves the edit inventory, the exact hand-off condition, unmodified PR5545 replay/columns/native, physical caller, both moment engines, all 54 strict + 4 functional outer checks, the exact crossing, and that four mutation controls are rejected.", + "outcome": "completed", + "author": "Joel Pulikkan (GamingPuzzled), with Claude Opus 5.5 (Anthropic), via Claude Code", + "ai_assistance": "Claude Opus 5.5 (Anthropic) via Claude Code, directed by Joel Pulikkan (GamingPuzzled). No independent human or proof-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "Are free helper FINAL frames admissible in the P104 caller contract?", + "why_it_matters": "The hand-off lowers helper 706's final frame from dim 9 to dim 8, as PR5561's headline word does for 23 helpers.", + "blocked_by": "Maintainer or swarm review (same condition as PR5561).", + "first_step": "Decide PR5561's open question on free finals; this package inherits it." + }, + { + "question": "Do owned-scratch holders (registers 735..742) admit further hand-offs?", + "why_it_matters": "The screen skipped 2,832 (helper, event) points where an owned private register holds the helper symbol.", + "blocked_by": "Owned registers move privately downward; pricing their re-flagging needs a separate rule.", + "first_step": "Extend tools/partner.py to private chains." + } + ], + "scope_status": "changed", + "scope_change_reason": "The scalar-to-moment card asks about scalar A2 contractions; this package instead moves one helper uncompute ADD earlier (a successor hand-off) on PR5561's word, which changes the paid itinerary. Recorded as changed.", + "evidence": "verify.py: input pins, byte-exact regeneration by handoff.py, edit inventory against PR5561's word, exact hand-off condition, unmodified PR5545 local.py replay/columns/native, physical caller, PR5561 pricing with literal-only changes, both moment engines, 54 strict + 4 functional outer checks, exact crossing, four rejected mutation controls.", + "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-priced-handoff/VERIFY.json b/research/p104-priced-handoff/VERIFY.json new file mode 100644 index 0000000000..3e9655a2bf --- /dev/null +++ b/research/p104-priced-handoff/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Edit inventory and exact hand-off condition against PR5561's word; four mutation controls; unmodified PR5545 replay, transposed columns, native maps, physical caller; literal-only pricing; both moment engines; 54 strict + 4 functional outer checks; exact crossing interval." + } + ] +} diff --git a/research/p104-priced-handoff/WORD.json.gz b/research/p104-priced-handoff/WORD.json.gz new file mode 100644 index 0000000000..3f4eb4be87 Binary files /dev/null and b/research/p104-priced-handoff/WORD.json.gz differ diff --git a/research/p104-priced-handoff/common.py b/research/p104-priced-handoff/common.py new file mode 100644 index 0000000000..bd244313fc --- /dev/null +++ b/research/p104-priced-handoff/common.py @@ -0,0 +1,47 @@ +"""Open the byte-pinned PR5545 source closure (same pins as PR5551/PR5561); Apache-2.0. + +Copied from PR5561's research/p104-free-endpoint-retime/common.py (DreamingOfClouds), package path +renamed only. 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-priced-handoff-')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-priced-handoff/handoff.py b/research/p104-priced-handoff/handoff.py new file mode 100644 index 0000000000..ca1fba6980 --- /dev/null +++ b/research/p104-priced-handoff/handoff.py @@ -0,0 +1,60 @@ +"""Derive WORD.json.gz from PR5561's headline word by one priced successor hand-off. Apache-2.0. + +Prepared for Joel Pulikkan (GamingPuzzled) with Claude Opus 5.5 (Anthropic), via Claude Code. + +Helper 706 (initial dim 0, final dim 9) is last read at event 15443 (ADD 121 += -2*706, frame 549, +dim 7). From then on its row is 706 + D, and the only use left is the uncompute +ADD 706 += -1/2*173 at frame 127 (dim 9, event 17252) after the climb 549 -> 127 (event 17251). +Main register 173 sits at frame 559 (dim 8, 549 < 559 < 127) from event 13089 to event 17248, and its +row is constant after event 13097, so -1/2*row(173) = -D already at event 15443. + +Successor hand-off at F = 559 (PR5472 pattern, co-framed cancellation with one partner): +helper 706 climbs 549 -> 559, cancels D there, and ends at F. The successor would start at F and +carry no data to the old final frame, so it is a rank-1 spectator (moment-neutral, like PR5553's +"Variant A") and is omitted. The word therefore changes by: + * insert after event 15443: MOVE 706 549->559 ; ADD 706 += -1/2*173 @559 + * delete events 17251 (MOVE 706 549->127) and 17252 (ADD 706 += -1/2*173 @127) + * final[706]: 127 -> 559 +Same event count (25,140), same scalar events (one ADD moved and relabelled), 735 public inputs. +Paid per call: one rank-2 climb -> one rank-1 climb; credited helper 706: rank 9 -> 8. +""" +import gzip,json,sys +from pathlib import Path +HERE=Path(__file__).resolve().parent +H,J,T,F=706,173,15443,559 +OLD_MOVE=['MOVE',H,549,127,False] +OLD_ADD=['ADD',H,J,'-1/2',127] + +def need(ok,why): + if not ok: raise ValueError(why) + +def source(): + return json.loads(gzip.decompress((HERE/'inputs'/'pr5561-WORD.json.gz').read_bytes())) + +def positions(P): + iM=[i for i,e in enumerate(P) if e==OLD_MOVE]; iA=[i for i,e in enumerate(P) if e==OLD_ADD] + need(iM==[17251] and iA==[17252],'pinned uncompute events') + need(P[T]==['ADD',121,H,'-2',549],'last read of helper 706') + need(all(H not in e[1:3] for e in P[T+1:17251] if e[0] in('ADD','COPY')) and + all(e[1]!=H for e in P[T+1:17251]),'helper 706 idle between its last read and the uncompute') + return iM,iA + +def handoff(w,frame=F,coef='-1/2',stop=True,lower_final=True): + w=json.loads(json.dumps(w)); P=w['program'] + iM,iA=positions(P) + ins=([['MOVE',H,549,frame,False]] if stop else [])+[['ADD',H,J,coef,frame]] + w['program']=P[:T+1]+ins+[e for i,e in enumerate(P[T+1:],T+1) if i not in(iM[0],iA[0])] + if lower_final: w['final'][H]=frame + return w + +def dump(w,path): + Path(path).write_bytes(encoded(w)) + +def encoded(w): + import io + b=io.BytesIO() + with gzip.GzipFile(fileobj=b,mode='wb',mtime=0) as g: g.write(json.dumps(w,sort_keys=True,separators=(',',':')).encode()) + return b.getvalue() + +if __name__=='__main__': + dump(handoff(source()),HERE/'WORD.json.gz'); print('wrote WORD.json.gz') diff --git a/research/p104-priced-handoff/inputs/pr5545-source-closure.tar.gz b/research/p104-priced-handoff/inputs/pr5545-source-closure.tar.gz new file mode 100644 index 0000000000..3084088544 Binary files /dev/null and b/research/p104-priced-handoff/inputs/pr5545-source-closure.tar.gz differ diff --git a/research/p104-priced-handoff/inputs/pr5561-WORD.json.gz b/research/p104-priced-handoff/inputs/pr5561-WORD.json.gz new file mode 100644 index 0000000000..c367d865a1 Binary files /dev/null and b/research/p104-priced-handoff/inputs/pr5561-WORD.json.gz differ diff --git a/research/p104-priced-handoff/inputs/pr5561-pricing.py b/research/p104-priced-handoff/inputs/pr5561-pricing.py new file mode 100644 index 0000000000..8d3e006225 --- /dev/null +++ b/research/p104-priced-handoff/inputs/pr5561-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('.00308142'), Q('.0030814205') +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()) == 66852, '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':'.00308142','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-priced-handoff/pricing.py b/research/p104-priced-handoff/pricing.py new file mode 100644 index 0000000000..bb135338f1 --- /dev/null +++ b/research/p104-priced-handoff/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('.00308181'), Q('.0030818105') +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()) == 66852, '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':'.00308181','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-priced-handoff/tools/lift21.py b/research/p104-priced-handoff/tools/lift21.py new file mode 100644 index 0000000000..f39c593feb --- /dev/null +++ b/research/p104-priced-handoff/tools/lift21.py @@ -0,0 +1,248 @@ +"""Priced co-framed hand-off screen (frame-flexible) on a P104 word. +At each scalar-event boundary t and helper h (mid-life), S0 = holders(h) U {h}. +Necessary: h in span(rows of S) for S >= S0 (we try S0 then S0 + registers whose frames allow co-framing greedy). +Frame feasibility: each j in S between its last scalar frame A_j and next scalar frame B_j; F with sum A_j <= F <= cap B_j. +Price: gain = 18*[f(dF-d0)+f(d1-dF)-f(d1-d0)] ; cost = 18*sum_j [P-moment change of j's chain A_j->B_j forced through F].""" +import gzip,json,sys,math +from fractions import Fraction as Q +from collections import defaultdict,Counter +C=float(sys.argv[3]) if len(sys.argv)>3 else 0.0030814 +f=lambda x: x**(1-C) if x>0 else 0.0 +w=json.load(gzip.open(sys.argv[1])) +NP=w['public']; NR=NP+8 +FR=w['frames']; dim=[len(x) for x in FR] +def span_of(b): + out={0} + for v in b: out|={x^v for x in out} + return frozenset(out) +SP=[span_of(b) for b in FR] +def rrefb(basis): + rows=[] + for v in basis: + for r in rows: + if v^r>v&1 for v in basis) +live=set(w['live']); main=live|{r+112 for r in live} +P=w['program'] +# per-register timeline: list of (event index, frame) at scalar events; and chain of frames between them +cur=list(w['initial'])+[None]*8 +sev=defaultdict(list) # r -> list of (i, frame at i) +chains=defaultdict(list) # r -> list of chains: frames visited between consecutive scalar events +chain_now={r:[cur[r]] for r in range(NP)} +for i,e in enumerate(P): + op,r=e[:2] + if op=='MOVE': + cur[r]=e[3]; + if r=NP: continue + sev[x].append((i,cur[x])); chains[x].append(chain_now[x]); chain_now[x]=[cur[x]] +for r in range(NP): chains[r].append(chain_now[r]) # final chain to final frame +# chains[r][k] = frames from scalar event k-1 (or initial) to scalar event k (or final) +import bisect +sidx={r:[i for i,_ in sev[r]] for r in range(NP)} +def window(j,t): + """for boundary after event t: chain from last scalar event<=t to next >t""" + k=bisect.bisect_right(sidx[j],t) + return chains[j][k] +def pm(ch): # paid moment of chain + return sum(f(dim[b]-dim[a]) for a,b in zip(ch,ch[1:])) +def best_cost(ch,Fs): + """cost of forcing chain ch (A..B) through subspace Fs (frozenset), min over placements; returns (cost) or None""" + A,B=ch[0],ch[-1] + if not (SP[A]<=Fs<=SP[B]): return None + base=pm(ch) + best=None + # keep chain stops comparable with Fs: new chain = stops below Fs that are subsets, Fs, stops above that contain Fs + lo=[x for x in ch if SP[x]<=Fs]; hi=[x for x in ch if Fs<=SP[x]] + # chain is totally ordered; lo is a prefix, hi a suffix (possibly overlapping at Fs) + dl=[dim[x] for x in lo]; dh=[dim[x] for x in hi] + dF=len(Fs).bit_length()-1 + new=dl+[dF]+dh + nm=sum(f(b-a) for a,b in zip(new,new[1:]) if b>a) + return base-nm # positive = moment loss? we return P-moment increase as cost (new-old) +def cost(ch,Fs): + A,B=ch[0],ch[-1] + if not (SP[A]<=Fs<=SP[B]): return None + lo=[dim[x] for x in ch if SP[x]<=Fs]; hi=[dim[x] for x in ch if Fs<=SP[x]] + dF=len(Fs).bit_length()-1 + new=lo+[dF]+hi + return sum(f(b-a) for a,b in zip(new,new[1:]) if b>a)-pm(ch) +# replay rows +rows=[{r:Q(1)} for r in range(NR)] +holders=defaultdict(set) +for r in range(NR): holders[r].add(r) +def setrow(r,new): + for k in rows[r]: + if k not in new: holders[k].discard(r) + for k in new: holders[k].add(r) + rows[r]=new +def inspan(h,S): + piv={} + for j in S: + v=dict(rows[j]) + for p,rv in list(piv.items()): + c=v.get(p) + if c: + for k,x in rv.items(): + y=v.get(k,0)-c*x + if y: v[k]=y + else: v.pop(k,None) + if not v: continue + p=min(v); c=v[p]; v={k:x/c for k,x in v.items()} + for q,rv in piv.items(): + cc=rv.get(p) + if cc: + for k,x in v.items(): + y=rv.get(k,0)-cc*x + if y: rv[k]=y + else: rv.pop(k,None) + piv[p]=v + t={h:Q(1)} + for p,rv in piv.items(): + c=t.get(p) + if c: + for k,x in rv.items(): + y=t.get(k,0)-c*x + if y: t[k]=y + else: t.pop(k,None) + return t +PR=(1<<61)-1 +def inspanp(h,S): + piv={} + for j in S: + v={k:int(x.numerator*pow(x.denominator,-1,PR))%PR for k,x in rows[j].items()} + for p,rv in piv.items(): + c=v.get(p) + if c: + for k,x in rv.items(): + y=(v.get(k,0)-c*x)%PR + if y: v[k]=y + else: v.pop(k,None) + if not v: continue + p=min(v); ci=pow(v[p],-1,PR); v={k:x*ci%PR for k,x in v.items()} + for q,rv in piv.items(): + cc=rv.get(p) + if cc: + for k,x in v.items(): + y=(rv.get(k,0)-cc*x)%PR + if y: rv[k]=y + else: rv.pop(k,None) + piv[p]=v + t={h:1} + for p,rv in piv.items(): + c=t.get(p) + if c: + for k,x in rv.items(): + y=(t.get(k,0)-c*x)%PR + if y: t[k]=y + else: t.pop(k,None) + return t +first={r:sidx[r][0] for r in range(NP) if sidx[r]}; last={r:sidx[r][-1] for r in range(NP) if sidx[r]} +d0=[dim[w['initial'][r]] for r in range(NP)]; d1=[dim[w['final'][r]] for r in range(NP)] +stats=Counter(); best=[]; extpts=[] +def cur_at(j,i,lob,hiM): + ch=window(j,i) + return contains(EL[ch[-1]],lob) and (EL[ch[0]]|hiM)==hiM +seen=set() +for i,e in enumerate(P): + if i%2000==0: print('ev',i,dict(stats),flush=True) + op,r=e[:2] + if op=='MOVE': continue + touched=set(rows[r]) + if op in('INIT','CLEAR'): setrow(r,{}) + elif op=='SCALE': q=Q(e[-2]); setrow(r,{k:q*x for k,x in rows[r].items()}) + else: + q=Q(e[-2]); s=e[2] + if op=='COPY': setrow(r,{k:q*x for k,x in rows[s].items()}) + else: + new=dict(rows[r]) + for k,x in rows[s].items(): + v=new.get(k,0)+q*x + if v: new[k]=v + else: new.pop(k,None) + setrow(r,new) + touched|=set(rows[r])|{r} + if op in('ADD','COPY'): touched|=set(rows[e[2]])|{e[2]} + for h in touched: + if not(h=NP for j in S): stats['owned_holder']+=1; continue + chh=window(h,i) + if not (dim[chh[0]]d0[h] and max(dim[chh[0]],d0[h]+1)<=min(dim[chh[-1]],d1[h]-1)): + stats['own_window_no_mid']+=1; continue + wins={j:window(j,i) for j in S} + hiM=EL[chh[-1]]; loB=list(FR[chh[0]]) + for j,ch in wins.items(): + hiM&=EL[ch[-1]]; loB+=FR[ch[0]] + lob=rrefb(loB); dlo=len(lob); dhi=hiM.bit_count().bit_length()-1 + if not all((EL[ch[-1]]>>0) and contains(EL[ch[-1]],lob) for ch in wins.values()): + stats['frame_infeasible']+=1; continue + if max(dlo,d0[h]+1)>min(dhi,d1[h]-1): stats['no_mid_dim']+=1; continue + if inspanp(h,S): + stats['span_fail']+=1 + hiS=frozenset(x for x in range(512) if hiM>>x&1) + ext=[j for j in range(NP) if j not in S and cur_at(j,i,lob,hiM)] + if inspanp(h,list(S)+ext): stats['span_fail_ext']+=1; continue + stats['span_ok_ext']+=1 + g=lambda a,b: f(a)+f(b)-f(a+b) if a>0 and b>0 else 0.0 + W={j:window(j,i) for j in list(S)+ext} + Fc={x for ch in W.values() for x in ch if contains(EL[x],lob) and (EL[x]|hiM)==hiM and d0[h]=gain: continue + cs=sorted((c,j) for j in ext for c in [cj(j)] if c is not None) + T=[] + ok=not inspanp(h,list(S)) + for c,j in cs: + if ok or base+sum(cj(x) for x in T)+c>=gain: break + T.append(j); ok=not inspanp(h,list(S)+T) + if not ok: continue + for j in sorted(T,key=lambda x:-cj(x)): + T2=[x for x in T if x!=j] + if not inspanp(h,list(S)+T2): T=T2 + cost=base+sum(cj(x) for x in T) + extpts.append((gain-cost,gain,cost,h,i,k,F,len(S),T)) + continue + stats['span_ok']+=1 + g=lambda a,b: f(a)+f(b)-f(a+b) if a>0 and b>0 else 0.0 + for k in range(max(dlo,d0[h]+1),min(dhi,d1[h]-1)+1): + gain=g(k-d0[h],d1[h]-k) + opts=[] + for Fk in (('lo',) if k==dlo else ())+(('hi',) if k==dhi else ())+('gen',): + c=0.0 + for j,ch in wins.items(): + dA,dB=dim[ch[0]],dim[ch[-1]] + if Fk=='lo' and dA==dlo and EL[ch[0]].bit_count()==1<0',sum(x[0]>0 for x in extpts));[print(x) for x in extpts[:15]] +print(dict(stats)) +print('candidates',len(best),'net>0',sum(1 for b in best if b[0]>1e-15)) +for b in best[:25]: print(b) +json.dump(best[:5000],open(sys.argv[2],'w')) diff --git a/research/p104-priced-handoff/tools/lift21.txt b/research/p104-priced-handoff/tools/lift21.txt new file mode 100644 index 0000000000..88688b49aa --- /dev/null +++ b/research/p104-priced-handoff/tools/lift21.txt @@ -0,0 +1,29 @@ +extpts 1 net>0 1 +(0.005364915437549911, 0.009632084214207026, 0.004267168776657115, 706, 15443, 8, 559, 1, [173]) +{'points': 589992, 'own_window_no_mid': 383246, 'no_mid_dim': 75945, 'span_ok': 81, 'frame_infeasible': 127401, 'span_fail': 487, 'span_fail_ext': 463, 'owned_holder': 2832, 'span_ok_ext': 24} +candidates 81 net>0 0 +(-0.0005065368683023763, 0.009632084214207026, 0.010138621082509403, 557, 13606, 1, 'gen', 2) +(-0.0005065368683023763, 0.009632084214207026, 0.010138621082509403, 545, 13605, 1, 'gen', 2) +(-0.0005065368683023763, 0.009632084214207026, 0.010138621082509403, 544, 12799, 1, 'gen', 2) +(-0.0005065368683023763, 0.009632084214207026, 0.010138621082509403, 532, 13631, 1, 'gen', 2) +(-0.0005065368683023763, 0.009632084214207026, 0.010138621082509403, 521, 13602, 1, 'gen', 2) +(-0.0005065368683023763, 0.009632084214207026, 0.010138621082509403, 520, 13139, 1, 'gen', 2) +(-0.0005065368683023763, 0.009632084214207026, 0.010138621082509403, 509, 12594, 1, 'gen', 2) +(-0.0005065368683023763, 0.009632084214207026, 0.010138621082509403, 484, 12764, 1, 'gen', 2) +(-0.0005065368683023763, 0.009632084214207026, 0.010138621082509403, 472, 12781, 1, 'gen', 2) +(-0.0008890768991340892, 0.009249544183375313, 0.010138621082509403, 556, 13155, 1, 'gen', 2) +(-0.0008890768991340892, 0.009249544183375313, 0.010138621082509403, 533, 13604, 1, 'gen', 2) +(-0.0008890768991340892, 0.009249544183375313, 0.010138621082509403, 473, 13599, 2, 'gen', 2) +(-0.0015469298572003964, 0.009632084214207026, 0.011179014071407423, 508, 13620, 1, 'gen', 2) +(-0.0015469298572003964, 0.009632084214207026, 0.011179014071407423, 485, 13600, 1, 'gen', 2) +(-0.002110820397497548, 0.009632084214207026, 0.011742904611704574, 565, 9463, 1, 'gen', 2) +(-0.002110820397497548, 0.009632084214207026, 0.011742904611704574, 564, 9462, 1, 'gen', 2) +(-0.002110820397497548, 0.009632084214207026, 0.011742904611704574, 563, 9447, 1, 'gen', 2) +(-0.002110820397497548, 0.009632084214207026, 0.011742904611704574, 562, 9446, 1, 'gen', 2) +(-0.002110820397497548, 0.009632084214207026, 0.011742904611704574, 553, 9453, 1, 'gen', 2) +(-0.002110820397497548, 0.009632084214207026, 0.011742904611704574, 552, 9452, 1, 'gen', 2) +(-0.002110820397497548, 0.009632084214207026, 0.011742904611704574, 551, 9459, 1, 'gen', 2) +(-0.002110820397497548, 0.009632084214207026, 0.011742904611704574, 550, 9458, 1, 'gen', 2) +(-0.002110820397497548, 0.009632084214207026, 0.011742904611704574, 541, 9451, 1, 'gen', 2) +(-0.002110820397497548, 0.009632084214207026, 0.011742904611704574, 540, 9450, 1, 'gen', 2) +(-0.002110820397497548, 0.009632084214207026, 0.011742904611704574, 535, 9467, 1, 'gen', 2) diff --git a/research/p104-priced-handoff/tools/partner.py b/research/p104-priced-handoff/tools/partner.py new file mode 100644 index 0000000000..51634be046 --- /dev/null +++ b/research/p104-priced-handoff/tools/partner.py @@ -0,0 +1,132 @@ +"""Single-partner co-framed hand-off screen (exhaustive over time). +Helper h mid-life with holders(h)=={h}, row(h)=h+D (D!=0). Partner j with row(j)=c*D at time t. +Hand-off at frame F: h -= (1/c) j ; s += (1/c) j ; s replaces h afterwards. +Price: gain g(k-d0,d1-k); cost: for h and j, 0 if F in their window chain else g(split) (if nestable).""" +import gzip,json,sys,bisect +from fractions import Fraction as Q +from collections import defaultdict,Counter +C=float(sys.argv[3]) if len(sys.argv)>3 else 0.0030814 +f=lambda x: x**(1-C) if x>0 else 0.0 +g=lambda a,b: f(a)+f(b)-f(a+b) if a>0 and b>0 else 0.0 +w=json.load(gzip.open(sys.argv[1])); NP=w['public']; NR=NP+8; FR=w['frames']; dim=[len(x) for x in FR] +def elems(b): + out={0} + for v in b: out|={x^v for x in out} + return out +EL=[sum(1< helpers carrying it +carry={} # h -> key +def dkey(h): + if not(hbest[0]: best=r + # generic F of dim k between lo=A_h+A_j and hi=B_h & B_j + lo=rank(FR[chh[0]]+FR[chj[0]]); him=EL[chh[-1]]&EL[chj[-1]] + if all(him>>v&1 for v in rr(FR[chh[0]]+FR[chj[0]])): + dhi=him.bit_count().bit_length()-1 + for k in range(max(lo,d0[h]+1),min(dhi,d1[h]-1)+1): + cs=sum(g(k-dim[ch[0]],dim[ch[-1]]-k) for ch in (chh,chj)) + gain=g(k-d0[h],d1[h]-k) + rr_=(gain-cs,gain,cs,h,j,i,'gen',k,[dim[x] for x in chh],[dim[x] for x in chj]) + stats['generic']+=1 + if best is None or rr_[0]>best[0]: best=rr_ + if best: out.append(best) +for i,e in enumerate(P): + op,r=e[:2] + if op=='MOVE': continue + before=set(rows[r]) + if op in('INIT','CLEAR'): newrow={} + elif op=='SCALE': q=Q(e[-2]); newrow={k:q*x for k,x in rows[r].items()} + else: + q=Q(e[-2]); s=e[2] + if op=='COPY': newrow={k:q*x for k,x in rows[s].items()} + else: + newrow=dict(rows[r]) + for k,x in rows[s].items(): + v=newrow.get(k,0)+q*x + if v: newrow[k]=v + else: newrow.pop(k,None) + for k in rows[r]: + if k not in newrow: holders[k].discard(r) + for k in newrow: holders[k].add(r) + rows[r]=newrow + aff={k for k in before|set(newrow) if k0',sum(o[0]>0 for o in out)) +seen=set() +for o in out: + if o[0]>0 and (o[3],o[4]) not in seen: seen.add((o[3],o[4])); print(o) +json.dump(out,open(sys.argv[2],'w')) diff --git a/research/p104-priced-handoff/tools/partner.txt b/research/p104-priced-handoff/tools/partner.txt new file mode 100644 index 0000000000..26a4e6b256 --- /dev/null +++ b/research/p104-priced-handoff/tools/partner.txt @@ -0,0 +1,2 @@ +{'match2': 598, 'match': 488, 'generic': 8} priced 8 net>0 1 +(0.005364915437549911, 0.009632084214207026, 0.004267168776657115, 706, 173, 15443, 559, 8, [7, 9], [8, 9]) diff --git a/research/p104-priced-handoff/tools/run_screens.sh b/research/p104-priced-handoff/tools/run_screens.sh new file mode 100644 index 0000000000..32ac69dce8 --- /dev/null +++ b/research/p104-priced-handoff/tools/run_screens.sh @@ -0,0 +1,9 @@ +#!/bin/sh +# Exhaustive hand-off screens on PR5561's headline word (python3.12, stdlib). Writes tools/*.txt. +# usage: sh research/p104-priced-handoff/tools/run_screens.sh (from repository root; ~5 min) +D="$(dirname "$0")"; W="$D/../inputs/pr5561-WORD.json.gz"; O="${TMPDIR:-/tmp}" +python3 -B "$D/screen.py" "$W" "$O/r21-screen.json" > "$D/screen.txt" +python3 -B "$D/screen2.py" "$W" "$O/r21-screen2.json" > "$D/screen2.txt" +python3 -B "$D/windows.py" "$W" > "$D/windows.txt" +python3 -B "$D/partner.py" "$W" "$O/r21-partner.json" > "$D/partner.txt" +python3 -B "$D/lift21.py" "$W" "$O/r21-lift.json" | grep -v '^ev ' > "$D/lift21.txt" diff --git a/research/p104-priced-handoff/tools/screen.py b/research/p104-priced-handoff/tools/screen.py new file mode 100644 index 0000000000..b3d4b0f6b0 --- /dev/null +++ b/research/p104-priced-handoff/tools/screen.py @@ -0,0 +1,59 @@ +"""Free successor hand-off screen on a P104 word (local.py replay semantics).""" +import gzip,json,sys +from fractions import Fraction as Q +from collections import defaultdict +w=json.load(gzip.open(sys.argv[1])) +NP=w['public']; NR=NP+8 +dim=[len(f) for f in w['frames']] +live=set(w['live']); main=live|{r+112 for r in live} +rows=[{r:Q(1)} for r in range(NR)] +holders=defaultdict(set) +for r in range(NR): holders[r].add(r) +cur=list(w['initial'])+[None]*8 +def setrow(r,new): + old=rows[r] + for k in old: + if k not in new: holders[k].discard(r) + for k in new: holders[k].add(r) + rows[r]=new +def free(h): + return rows[h]=={h:Q(1)} and holders[h]=={h} +pts=defaultdict(list) # helper -> list of (event index after which, frame) +helpers=[r for r in range(NP) if r not in main] +for i,e in enumerate(w['program']): + op,r=e[:2] + if op=='MOVE': + cur[r]=e[3] + if r in main: continue + # after a climb: check freeness + if free(r): pts[r].append((i,e[3])) + continue + if op in('INIT','CLEAR'): + setrow(r,{}); cur[r]=e[2] if op=='INIT' else None; continue + q=Q(e[-2]) + if op=='SCALE': setrow(r,{k:q*x for k,x in rows[r].items()}); continue + s=e[2] + if op=='COPY': setrow(r,{k:q*x for k,x in rows[s].items()}) + else: + new=dict(rows[r]) + for k,x in rows[s].items(): + v=new.get(k,0)+q*x + if v: new[k]=v + else: new.pop(k,None) + setrow(r,new) + # after ADD, both r and other symbols: re-check helpers whose freeness may change at current frame + for h in (r,)+tuple(k for k in rows[s] if k row + for j in atF[F]: + v=dict(rows[j]) + for p,rv in piv.items(): + c=v.get(p) + if c: + for k,x in rv.items(): + y=v.get(k,0)-c*x + if y: v[k]=y + else: v.pop(k,None) + if not v: continue + p=min(v); c=v[p]; v={k:x/c for k,x in v.items()} + for q,rv in piv.items(): + cc=rv.get(p) + if cc: + for k,x in v.items(): + y=rv.get(k,0)-cc*x + if y: rv[k]=y + else: rv.pop(k,None) + piv[p]=v + t={h:Q(1)} + for p,rv in piv.items(): + c=t.get(p) + if c: + for k,x in rv.items(): + y=t.get(k,0)-c*x + if y: t[k]=y + else: t.pop(k,None) + return not t +found=defaultdict(dict) # h -> {F: first event} +nc2=0;ntest=0 +def test(h,i): + global nc2,ntest + F=cur[h] + if F is None or not (d0[h] 559, + replacing the MOVE 706 549->127 by MOVE 706 549->559, and final[706] 127 -> 559; + all other events, frames, ports, live list and endpoints (all 208 main registers) are equal; + (3) the exact hand-off condition (exact rationals): after event 15443 no register but 706 holds + symbol 706, row(706) = 706 + D with D = 1/2*row(173), row(173) is constant until event 17252, + and 706 / 173 are idle at frames 549 < 559 (nested) at the insertion point; + (4) UNMODIFIED PR5545 local.py replay, transposed columns, native maps; physical caller; + PR5561's pricing.py with only the KAPPA/TESTED claim line and kappa_decimal label changed + (LITERAL-CHANGES.diff); both moment engines; 54 strict + 4 functional outer checks; exact crossing; + (5) mutation controls, each must be rejected by the unmodified local.py replay: + no stop (ADD at 559 while 706 is still at 549), wrong coefficient, final not lowered, + hand-off one event before the last read of 706. +""" +from fractions import Fraction as Q +from hashlib import sha256 +import 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 as HO + +INTERVAL=['154090925761/50000000000000','308181851523/100000000000000'] +PINS={'inputs/pr5561-WORD.json.gz':'b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44', + 'inputs/pr5561-pricing.py':'701f87ebf3742d55f21ccdb2fd13d04fc2019a6b6190d8542bb7f5d477c71de5'} + +def patch(text): + for a,b in(("KAPPA, TESTED = Q('.00308142'), Q('.0030814205')","KAPPA, TESTED = Q('.00308181'), Q('.0030818105')"), + ("'kappa_decimal':'.00308142'","'kappa_decimal':'.00308181'")): + need(text.count(a)==1,'pinned pricing literal present once: '+a); text=text.replace(a,b) + return text + +def inventory(base,w): + for k in('schema','public','live','ports','frames','initial'): need(base[k]==w[k],'unchanged '+k) + diff=[r for r in range(base['public']) if base['final'][r]!=w['final'][r]] + need(diff==[HO.H] and base['final'][HO.H]==127 and w['final'][HO.H]==HO.F,'only final[706] changes 127 -> 559') + B,W=base['program'],w['program'] + need(len(B)==len(W),'same event count') + need(W[:HO.T+1]==B[:HO.T+1],'prefix through event 15443 unchanged') + need(W[HO.T+1:HO.T+3]==[['MOVE',HO.H,549,HO.F,False],['ADD',HO.H,HO.J,'-1/2',HO.F]],'inserted stop and moved ADD') + need(W[HO.T+3:17253]==B[HO.T+1:17251] and W[17253:]==B[17253:],'all other events unchanged and in order') + need(B[17251:17253]==[HO.OLD_MOVE,HO.OLD_ADD],'removed: MOVE 706 549->127 and its ADD @127') + fr=[frozenset(_span(x)) for x in w['frames']] + need(fr[549] 15445','stop':'706: 549 -> 559 (dim 7 -> 8) replaces 549 -> 127 (dim 7 -> 9)'} + +def _span(b): + out={0} + for v in b: out|={x^v for x in out} + return out + +def condition(w): + """Exact rows of the pinned PR5561 word at the hand-off point.""" + P=w['program']; NP=w['public'] + rows=[{r:Q(1)} for r in range(NP+8)]; cur=list(w['initial'])+[None]*8 + snap=None + for i,e in enumerate(P): + op,r=e[:2] + if op=='MOVE': cur[r]=e[3] + elif op in('INIT','CLEAR'): rows[r]={}; cur[r]=e[2] if op=='INIT' else None + elif op=='SCALE': rows[r]={k:Q(e[-2])*x for k,x in rows[r].items()} + else: + s=e[2];q=Q(e[-2]) + if op=='COPY': rows[r]={k:q*x for k,x in rows[s].items()} + else: + for k,x in rows[s].items(): + v=rows[r].get(k,0)+q*x + if v: rows[r][k]=v + else: rows[r].pop(k) + if i==HO.T: + hold=[j for j in range(NP+8) if HO.H in rows[j]] + need(hold==[HO.H],'no other holder of symbol 706 after its last read') + D={k:x for k,x in rows[HO.H].items() if k!=HO.H} + need(rows[HO.H].get(HO.H)==1 and D and D=={k:x/2 for k,x in rows[HO.J].items()},'row(706) = 706 + 1/2*row(173)') + need(cur[HO.H]==549 and cur[HO.J]==HO.F,'706 at 549 and 173 at 559 at the hand-off point') + snap=dict(rows[HO.J]) + if i==17251: + need(rows[HO.J]==snap and cur[HO.J]==127,'row(173) unchanged until the original uncompute') + return {'carried_symbols':len(D),'holders_of_706':1,'partner':'main register 173 (Y target of port register 61)'} + +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_priced_handoff_caller_'+tag) + tmp=HERE/('.pricing-'+tag+'.py');tmp.write_text(pricing_text) + try: P=L.load(tmp,'p104_priced_handoff_pricing_'+tag) + finally: tmp.unlink() + loc=L.replay(word);print(tag,'PASS replay: paid',loc['paid'],'helpers',loc['helpers'],flush=True) + L.reverse_columns(word);print(tag,'PASS transposed columns',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) + return loc,P.run(loc,nat,ctl,phys) + +def controls(L,base): + bad={'no stop (ADD at 559 while 706 is at 549)':HO.handoff(base,stop=False), + 'wrong coefficient -1':HO.handoff(base,coef='-1'), + 'final not lowered':HO.handoff(base,lower_final=False)} + early=HO.handoff(base); P=early['program'] + P.insert(HO.T,P.pop(HO.T+1)); P.insert(HO.T,P.pop(HO.T+2)) # stop and ADD before the last read + bad['hand-off before the last read of 706']=early + out={} + for name,w in bad.items(): + try: L.replay(w) + except ValueError as x: out[name]='rejected: '+str(x); print('control',name,'->',out[name],flush=True) + else: raise ValueError('control accepted: '+name) + return out + +def main(): + for p,h in PINS.items(): need(sha256((HERE/p).read_bytes()).hexdigest()==h,'input pin '+p) + base=read(HERE/'inputs/pr5561-WORD.json.gz'); word=read(HERE/'WORD.json.gz') + need(HO.encoded(HO.handoff(base))==(HERE/'WORD.json.gz').read_bytes(),'handoff.py regenerates WORD.json.gz byte for byte') + inv=inventory(base,word);print('PASS edit inventory',inv,flush=True) + cond=condition(base);print('PASS exact hand-off condition',cond,flush=True) + need((HERE/'pricing.py').read_text()==patch((HERE/'inputs/pr5561-pricing.py').read_text()),'pricing.py = PR5561 pricing.py + literal changes only') + with closure() as root: + L=load(root/'research/p104-productive-controller/local.py','local');L.ROOT=root + ctl=controls(L,base) + loc,res=chain(root,L,(HERE/'pricing.py').read_text(),word,'handoff') + print('raw crossing interval',res['raw_root_interval'],flush=True) + need(res['raw_root_interval']==INTERVAL,'exact crossing interval') + need(res['productive_fields']==12814 and res['paid_calls']==66852 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(Q(x)>0 for k in('strict_checks','functional_checks') for x in res['outer'][k].values()),'all outer checks strict') + lo,hi=[Q(x) for x in INTERVAL] + print('crossing kappa in (%.14f, %.14f); 54 strict + 4 functional outer checks pass'%(lo,hi),flush=True) + if '--write' in sys.argv: + (HERE/'RESULT.json').write_text(json.dumps({'status':'PASS_P104_PRICED_HANDOFF_CONDITIONAL_KAPPA','inventory':inv, + 'condition':cond,'controls':ctl,'result':res},indent=1,sort_keys=True,default=str)+'\n') + print('PASS P104_PRICED_HANDOFF') +main() diff --git a/research/p104-priced-handoff/verify.sh b/research/p104-priced-handoff/verify.sh new file mode 100644 index 0000000000..cd3a9370a0 --- /dev/null +++ b/research/p104-priced-handoff/verify.sh @@ -0,0 +1,3 @@ +#!/bin/sh +# usage: sh research/p104-priced-handoff/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": [ [