diff --git a/research/p104-helper468-rung-removal/EDIT.json.gz b/research/p104-helper468-rung-removal/EDIT.json.gz new file mode 100644 index 0000000000..af21a8fbea Binary files /dev/null and b/research/p104-helper468-rung-removal/EDIT.json.gz differ diff --git a/research/p104-helper468-rung-removal/EXPECT.json b/research/p104-helper468-rung-removal/EXPECT.json new file mode 100644 index 0000000000..c6b2545b2e --- /dev/null +++ b/research/p104-helper468-rung-removal/EXPECT.json @@ -0,0 +1,38 @@ +{ + "interval": [ + "78132227471/25000000000000", + "62505781977/20000000000000" + ], + "paid_calls": 66852, + "productive_fields": 13444, + "rank_mass_surplus": 760, + "events": 25998, + "inventory": [ + 770, + 29, + 31, + 13 + ], + "paid_delta": { + "1": -4, + "4": 1, + "6": 1, + "7": 1 + }, + "helper_delta": { + "1": -3, + "3": 1, + "6": 1, + "7": 1 + }, + "control_sites": { + "add21": 21, + "add27": 27 + }, + "sign_sites": { + "add21": 21, + "add27": 27 + }, + "base_commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "status": "PASS_P104_BASE5827_EDIT_KAPPA_312528200" +} diff --git a/research/p104-helper468-rung-removal/PRICING-EDITS.json b/research/p104-helper468-rung-removal/PRICING-EDITS.json new file mode 100644 index 0000000000..fdde68e1a3 --- /dev/null +++ b/research/p104-helper468-rung-removal/PRICING-EDITS.json @@ -0,0 +1,18 @@ +[ + [ + "KAPPA, TESTED = Q('0.00312476680'), Q('0.003124766805')", + "KAPPA, TESTED = Q('0.003125282'), Q('0.0031252870')" + ], + [ + "PREVIOUS = Q('0.00312418633064')", + "PREVIOUS = Q('0.00312476680')" + ], + [ + "sum(targets.values()) == 13444 and sum(paid.values()) == 66870", + "sum(targets.values()) == 13444 and sum(paid.values()) == 66852" + ], + [ + "'kappa_decimal':'0.00312476680','previous_pr5811':PREVIOUS", + "'kappa_decimal':'0.003125282','previous_pr5827':PREVIOUS" + ] +] diff --git a/research/p104-helper468-rung-removal/README.md b/research/p104-helper468-rung-removal/README.md new file mode 100644 index 0000000000..8072f8fa04 --- /dev/null +++ b/research/p104-helper468-rung-removal/README.md @@ -0,0 +1,65 @@ +# Conditional kappa 0.003125282: remove helper 468's frame-593 rung with rerouted reads + +This package edits the word of [PR #5827](https://github.com/CrocSwap/integer-mult-bounds/pull/5827) +(aliromman, head `05cd36e5af06d7a3790e30ce3f449fa89b853768`, conditional kappa 0.00312476680) and re-certifies it with PR #5827's own chain. The complete +conditional kappa is **0.003125282**, tested at 0.0031252870; the exact raw crossing lies in +(0.00312528909884, 0.00312528909885) = (78132227471/25000000000000, 62505781977/20000000000000), +which is +5.223e-07 above PR #5827's raw crossing (.00312476681507). The paid bill falls to +**66852 calls** (PR #5827: 66,870) at an unchanged 13444 productive targets and rank-mass surplus +760. Public inputs, owned fields, owned lifetimes and peak occupancy (770, 29, 31, 13) are unchanged; +the word has 25998 events (retained cap 26,000). + +## The edit + +The edit removes helper 468's rung at frame 593: its itinerary 3 -> 593 -> 712 becomes 3 -> 712. Helper 703's +chain 593 -> 859 -> 127 now runs 593 -> 712 -> 127. Three one-hop helpers are retargeted: helper 455 goes from +3 -> 105 to 3 -> 925, helper 557 from 3 -> 105 to 105 -> 925, and helper 765 from 245 -> 127 to 263 -> 742. Their +helper spans rise (1 to 7, 6 and 3), which moves paid ranks as listed below. Every other change is the induced +rewrite of read and write windows: about 650 registers carry a different event sequence, with 1 MOVE fewer and +15 ADDs more (SCALE, COPY, INIT and CLEAR counts are equal). + +Boundary charts changed by the edit: initial 557: 3 -> 105; initial 765: 245 -> 263; final 455: 105 -> 925; final 557: 105 -> 925; final 765: 127 -> 742. Paid-profile change vs PR #5827: rank 1: -4, rank 4: +1, rank 6: +1, rank 7: +1. +Every public input column, every signed native map and the physical caller are re-checked in full (see Verification). + +`EDIT.json.gz` is the explicit edit list: boundary changes plus the new event list as copy segments of +PR #5827's program and literal events. `construct.py` (standard library only) applies it to PR #5827's word, taken from +the pinned archive, and regenerates `WORD.json.gz` byte for byte: + +```sh +python3.12 -I -B research/p104-helper468-rung-removal/construct.py +``` + +## Verification + +```sh +python3.12 -I -B research/p104-helper468-rung-removal/verify.py +``` + +`verify.py` authenticates the pinned PR #5827 package (`inputs/pr5827-source.tar`, per-file SHA256 and Git blob) and its seven-deep source +chain, asserts that the shipped `pricing.py` equals PR #5827's `pricing.py` plus the literal edits in `PRICING-EDITS.json` (claim, +previous claim, the paid-call count and two labels), regenerates the word, and runs PR #5827's chain unchanged: exact replay and storage +inventory, all 799 input columns with a separate transpose, every signed native map (2,921), 208 main adapters, 1,124 helper +normalizers, the exact physical caller, the complete invoice, both interval engines, compiler and 54 strict plus 4 functional outer +checks, rejection controls, and the committed `RESULT.json`. `--part build` runs the authentication, regeneration and replay only. + +## Conditions inherited + +The five framework assumptions retained by the P104 line (native all-column implementation, owned erasure, uniform compiler closure, +precision and fixed-tape costs, claim accounting) and PR #5827's own checker are inherited unchanged. Author checks are not +independent human acceptance. The finite local word is materialized; the large uniform word and rounded multiplier are not. No merge, +closure or selected-frontier change is requested. + +## Credits + +The base word and verifier are Ali Romman's (aliromman, PR #5827, with substantial OpenAI Codex assistance), built on PR #5811 +(Mason Hale), PR #5786 and the earlier lineage back to PR #5565 (Pierre-Loic Doulcet), with all retained source notices in the pinned +archive. This package contributes only the edit above and its packaging. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. + +## Open next questions + +- Does an independent reviewer confirm the edit list, the regenerated word and the full chain? First step: run `construct.py` and + `verify.py` as above, then compare the changed boundary charts with PR #5827's. +- Do other helpers with the same rung structure admit the same removal, and does any combination fit the 25998-of-26,000 + event cap? First step: list helpers whose itinerary passes through a frame used by no other reader, then compare event counts. diff --git a/research/p104-helper468-rung-removal/RESULT.json b/research/p104-helper468-rung-removal/RESULT.json new file mode 100644 index 0000000000..21a900ef8a --- /dev/null +++ b/research/p104-helper468-rung-removal/RESULT.json @@ -0,0 +1,387 @@ +{ + "base_commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "base_margin_upper_at_new_claim": "-195320222899522377925999803745422919897273526173986946657/1569275433846670190958947355801916604025588861116008628224", + "complete_cost": { + "compiler": { + "H": 65807000000000, + "N": "2^65807000000000", + "eta": { + "lower": "0.000000120677907870429700134975", + "upper": "0.000000120677907870429700134976" + }, + "gap": "1/1400000000", + "integer_test_exponent": 47005, + "logarithm_power": 1024, + "theta": "63/64", + "uniform_saving": "5469251/1750000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "161/312500000", + "kappa": "1562641/500000000", + "kappa_decimal": "0.003125282", + "margin_at_previous": { + "lower": "0.126162874283923634451386973763", + "upper": "0.126162874283923634451386973764" + }, + "negative_controls": { + "old_BIT": "Rejected by outer inequalities", + "old_cutoff": "Rejected by completion-tail ratio greater than one", + "source_completion": "Rejected at cutoff17, floor18 and decay39/40", + "source_offset": "Rejected at cutoff16 with tail offset1/5" + }, + "nonrecursive": { + "fixed_scalar_growth_bound": "At most 2^(16*26000) before native factors; a declared constant, not an attained norm.", + "local_paid_rank_mass": 5947, + "local_routes": 5326000, + "local_scalar": 228664, + "peak_owned_fields": 13, + "raw_budget": 1000000000, + "raw_scalar_upper": 184647552, + "tensor_native_growth_bound": "Each rank-r Gaussian has row l1 norm at most 2^(rf); use local_paid_rank_mass for the whole word." + }, + "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": "348599999253/350000000000", + "fixed_halo_explicit_metadata_branch": "26950000001/350000000", + "new_BIT_row_stock_sublinear_in_active_group": "1395799997009/1400000000000", + "new_semantic_group_guard": "3/1400000000" + }, + "margins": { + "boundary_algebraic_matrix": "30627791578123011/9800000000000000000", + "fused_gaussian": "30627791534369033/9800000000000000000", + "global_coordinate_router": "10938497/3500000000", + "group_bit_router": "15313899267184509/4900000000000000000", + "group_scans": "699999999/700000000", + "main_transform": "30627784578123011/9800000000000000000", + "microbox_face_corrections": "26950000001/350000000", + "polynomial_products": "1399999999/1400000000", + "sparse_union_movement": "4011877791578123011/9800000000000000000" + }, + "parameters": { + "a": "10938497/3500000000", + "b": "21876999/7000000000", + "beta": "1399999997/1400000000", + "bit_saving": "17/5000", + "cap_xi": "8911877784578123011/9800000000000000000", + "complex_uniform_saving": "5469251/1750000000", + "d": "1/1400000000", + "epsilon": "1399999999/1400000000", + "kappa": "1562641/500000000", + "lambda_": "1993749431/2000000000", + "lambda_prime": "6978123011/7000000000", + "layout": "1/1400000000", + "q": "21876989/7000000000", + "r0": "1/14000000000", + "stop": "1/1400000000", + "tested_saving": "3125287/1000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "961503/3500000000", + "actual_logarithmic_gamma_guard": "1/1400000000", + "actual_logarithmic_group_guard": "888122225921876989/4900000000000000000", + "alpha_logarithm_absorption": "1/14000000000", + "boundary_algebraic_matrix_above_kappa": "27978123011/9800000000000000000", + "cap_above_band": "4011877784578123011/9800000000000000000", + "cap_below_cell": "888122208421876989/9800000000000000000", + "cap_below_phase_cell_power": "10688122215421876989/9800000000000000000", + "complex_above_effective": "1/1400000000", + "complex_below_one_over_32": "196873001/7000000000", + "complex_endpoint": "1/700000000", + "epsilon_below_one": "1/1400000000", + "epsilon_positive": "1399999999/1400000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "27934369033/9800000000000000000", + "gaussian_above_main": "3478123011/4900000000000000000", + "global_coordinate_router_above_kappa": "1/350000000", + "global_gamma_power_slack": "9/14000000000", + "group_below_dimension": "1/700000000", + "group_bit_router_above_kappa": "17467184509/4900000000000000000", + "group_gauge_power_slack": "888122225571876989/4900000000000000000", + "group_key_fits_record": "1/700000000", + "group_positive": "1399999997/1400000000", + "group_scans_above_kappa": "872265377/875000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "697155790400418148631/500000000000000000000000", + "lambda_above_internal": "1/2800000000", + "lambda_above_sigma": "3/2800000000", + "lambda_above_tau": "1/2800000000", + "lambda_prime_above_lambda": "1/2800000000", + "lambda_prime_above_leaf": "13978123001/9800000000000000000", + "leaf_saving_above_effective": "6978123001/9800000000000000000", + "main_transform_above_kappa": "20978123011/9800000000000000000", + "membership_arithmetic_fits_record": "1/1400000000", + "microbox_face_corrections_above_kappa": "269489061523/3500000000", + "microbox_halo_volume": "110600000003/1400000000", + "new_complex_uniform_saving_above_b": "1/1400000000", + "new_semantic_guard_with_C1_one": "1/1400000000", + "polynomial_products_above_kappa": "6978123021/7000000000", + "positive_layout_slack": "1/1400000000", + "q_below_effective": "1/1400000000", + "q_below_internal": "1/1400000000", + "q_below_leaf": "13978123001/9800000000000000000", + "q_positive": "21876989/7000000000", + "short_record_fallback": "6978123001/7000000000", + "source_axis_superpolynomial": "1/1400000000", + "sparse_union_movement_above_kappa": "3981250027978123011/9800000000000000000", + "stop_below_one": "1399999999/1400000000", + "stop_positive": "1/1400000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/1400000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/1400000000", + "union_tag_work_per_visit_fits_record": "3/1400000000" + } + }, + "paid": { + "1": 41538, + "16": 416, + "2": 8208, + "24": 416, + "3": 8964, + "32": 416, + "4": 1782, + "40": 416, + "48": 416, + "5": 2934, + "56": 416, + "6": 180, + "64": 416, + "7": 126, + "72": 208 + }, + "paid_calls": 66852, + "previous_pr5827": "7811917/2500000000", + "productive_fields": 13444, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_ceiling": { + "derivative_upper": "-91967583976429127709300459493881349289345588519386446349058305/392318858461667547739736838950479151006397215279002157056", + "interval": [ + "0", + "17/5000" + ] + }, + "raw_headroom": [ + "177471/25000000000000", + "141977/20000000000000" + ], + "raw_root_interval": [ + "78132227471/25000000000000", + "62505781977/20000000000000" + ], + "relative_gain_percent": "128800/7811917", + "strictification": { + "alpha": { + "lower": "0.999999997872095508862174217650", + "upper": "0.999999997872095508862174217651" + }, + "cutoff": 16, + "delta": { + "lower": "0.950984762414878072613274872891", + "upper": "0.950984762414878072613274872892" + }, + "floor": 17, + "gamma": { + "lower": "0.975557689499641750208313531528", + "upper": "0.975557689499641750208313531529" + }, + "normalized_paid_upper": "1048576000976562501/1048576001073741824", + "power": 1024, + "reserve": "1/1000000000000", + "tail_block": 128, + "tail_decay": "125/128", + "tail_offset": "1/7", + "tested": "3125287/1000000000" + }, + "targets": { + "1": 270, + "145": 208, + "17": 416, + "2": 126, + "25": 416, + "3": 90, + "33": 416, + "4": 1926, + "41": 416, + "49": 416, + "5": 252, + "57": 416, + "6": 18, + "65": 416, + "7": 180, + "73": 208, + "8": 324, + "9": 6930 + }, + "whole_idle_jobs": 3120 + }, + "controls": { + "damaged_source_LOCAL-EDITS.json": "Exact source SHA256: research/p104-unread-path-resynthesis/LOCAL-EDITS.json", + "damaged_source_NOTICE": "Exact source SHA256: research/p104-unread-path-resynthesis/NOTICE", + "damaged_source_PLAN.json": "Exact source SHA256: research/p104-unread-path-resynthesis/PLAN.json", + "extra_target_credit": "Every productive helper has a native target", + "missing_add21": "All public and owned rows", + "missing_add27": "All public and owned rows", + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "unpaid_query": "Complete field and call counts", + "wrong_sign_add21": "All public and owned rows", + "wrong_sign_add27": "All public and owned rows" + }, + "limits": [ + "All five inherited framework assumptions remain.", + "The large uniform word and rounded multiplier are not materialized.", + "Author checks do not establish independent acceptance.", + "The selected frontier is unchanged." + ], + "local": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 15, + "2": 7, + "3": 5, + "4": 107, + "5": 14, + "6": 1, + "7": 10, + "8": 18, + "9": 385 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid": { + "1": 2221, + "2": 456, + "3": 498, + "4": 99, + "5": 163, + "6": 10, + "7": 7 + }, + "paid_rank_mass": 5947, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 228664 + }, + "native": { + "distinct_maps": 2921, + "helper_normalizers": 1124, + "helpers": { + "1": 15, + "2": 7, + "3": 5, + "4": 107, + "5": 14, + "6": 1, + "7": 10, + "8": 18, + "9": 385 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "d6f5096016d605200d47ad85c1ea8d46b6582468e08ce79d087de32e4b1e2f45", + "wrong_phase_rejected": true + }, + "paid_delta": { + "1": -4, + "4": 1, + "6": 1, + "7": 1 + }, + "physical_caller": { + "central_square_columns": 53248, + "full_calls": 18, + "main_targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208 + }, + "new_paid_jobs": 0, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "7f4f0ca768ffbc4f93dcff575592c4c67411f46b4289e45b73f715a2ad47b142", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "wrapper_sites": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "separate_columns": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 638401, + "columns": 799 + }, + "source_local": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 18, + "2": 7, + "3": 4, + "4": 107, + "5": 14, + "7": 9, + "8": 18, + "9": 385 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid": { + "1": 2225, + "2": 456, + "3": 498, + "4": 98, + "5": 163, + "6": 9, + "7": 6 + }, + "paid_rank_mass": 5934, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 225046 + }, + "status": "PASS_P104_BASE5827_EDIT_KAPPA_312528200", + "target_delta": { + "1": -3, + "3": 1, + "6": 1, + "7": 1 + } +} diff --git a/research/p104-helper468-rung-removal/SOURCES.json b/research/p104-helper468-rung-removal/SOURCES.json new file mode 100644 index 0000000000..945b167044 --- /dev/null +++ b/research/p104-helper468-rung-removal/SOURCES.json @@ -0,0 +1,189 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ], + "source_archive": { + "local_path": "inputs/pr5827-source.tar", + "sha256": "7af5908a4d83e83e28f59523fd7494841f669b7295311cfdbc3027fa65c5826d", + "files": 23, + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "pr": 5827, + "package": "research/p104-unread-path-resynthesis" + }, + "archived_files": [ + { + "path": "research/p104-unread-path-resynthesis/LOCAL-EDITS.json", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 59, + "sha256": "c4d195bcf17209a129bacf5b8ebd311d475c44405feb040683f096858f87a987", + "git_blob": "f725d2bb87b3322512cb76eefbe3a9b26ece7176" + }, + { + "path": "research/p104-unread-path-resynthesis/NOTICE", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 6714, + "sha256": "fe02063ca48bf070303ac05f613ab1e6e4dd9ee62141f7e7012d855faf7b0c78", + "git_blob": "8fc3f76cc0d66f19c9abd7c7111ec69c73c0434d" + }, + { + "path": "research/p104-unread-path-resynthesis/PLAN.json", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 1030, + "sha256": "46bada733d461d7d5154ba5ede7d32697eaa00ab7380a0ceaf53324b9084d1a8", + "git_blob": "dc269304a438d39c9aa60256eb33c4d439fb378a" + }, + { + "path": "research/p104-unread-path-resynthesis/PRICING-EDITS.json", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 437, + "sha256": "7cec40c77056d30d879ff6752bf785ce1773c11e6c959cc8f33c351b828e3c8a", + "git_blob": "205de2990148e83bdac27aea49de593ffbefee0a" + }, + { + "path": "research/p104-unread-path-resynthesis/PROOF.md", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 6614, + "sha256": "16b1ba9b9468b097796d900ac04f9a278e09cba5ec9e08436b6e06ee066b385b", + "git_blob": "eae2e1b895284155a1485f240a0ad43a4b52c0aa" + }, + { + "path": "research/p104-unread-path-resynthesis/README.md", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 4574, + "sha256": "5f5026b41eb3f822652d4b41b5f4f81c4a285ac77d7ec34f41fabdbdad4b0252", + "git_blob": "e663d069442adfb224de108031f80b603180d873" + }, + { + "path": "research/p104-unread-path-resynthesis/RESULT.json", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 13257, + "sha256": "e437dd9fc7368de705cef8a9d27c6161f1b246f36e320e5c155dde89f88e16e2", + "git_blob": "e2e078df445d6c1b988cf926fed3bc7570a88237" + }, + { + "path": "research/p104-unread-path-resynthesis/SOURCES.json", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 8164, + "sha256": "b6aa6b569e76a7ab07f59e3d3c1204dad485bc9d6638211907a3f619073b6e33", + "git_blob": "4531538f264f4aaf9bd5e0d6be74758578fab749" + }, + { + "path": "research/p104-unread-path-resynthesis/TASK.json", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 7801, + "sha256": "2548bea7e62ee5d8b988c72988c7f8cf69ed623994e662929639ff857620942f", + "git_blob": "1b7c6ccdb6a32e89b11f70163e1b4b409f5693d6" + }, + { + "path": "research/p104-unread-path-resynthesis/VALIDATION.md", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 1790, + "sha256": "593470975c818bd86d3af813d86d8a6c17ef51c0e7e437e14a0c94de1286112c", + "git_blob": "1a3fa30e394a9837ec6d57adc019144ac323ea67" + }, + { + "path": "research/p104-unread-path-resynthesis/VERIFY.json", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 677, + "sha256": "c0c2995e2961dcad87e5f78fac22b519c629a1da77e661f924fa5101a87fde4d", + "git_blob": "988b0541663f9bddf08d3c80ff09cacd87d9ab4c" + }, + { + "path": "research/p104-unread-path-resynthesis/WITNESS.json", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 677, + "sha256": "6f9bb837e47c5b10f6d008d57a87415c7013e2076f3313fde1848d27b3314e67", + "git_blob": "969ff0c9b474bc9d2df2eec8482e17cfb75c1fbe" + }, + { + "path": "research/p104-unread-path-resynthesis/WORD.json.gz", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 122919, + "sha256": "5d50e5654910c9535e9025de0f644bb2dece2396e799b4a766110363448fd0b0", + "git_blob": "6341a49f717bd64ef2a5b7c440bd86d5513425dc" + }, + { + "path": "research/p104-unread-path-resynthesis/construct.py", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 2371, + "sha256": "e23a70d1fa000c05c6e05a6d8c909cd47b8aabc6c7505f925fc0235575076c9c", + "git_blob": "7d33cb8646ea7492131853070e97afd5935521da" + }, + { + "path": "research/p104-unread-path-resynthesis/inputs/pr5786-source.tar", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 3788800, + "sha256": "9ca76daeb8db6b623d7329628248fae114946f35fb036c3171fcdba868131dc2", + "git_blob": "a1f7e63c7dd3b5ef4cde70b96e8ad6aa30cdc684" + }, + { + "path": "research/p104-unread-path-resynthesis/inputs/pr5811-NOTICE", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 1027, + "sha256": "2f87017c7497194392d41c8ae80e5e1cfcf14651627cea2f918c1c8924c9858d", + "git_blob": "bd91106cde0cc8c201329bedc2d45af65c582b57" + }, + { + "path": "research/p104-unread-path-resynthesis/inputs/pr5811-PROOF.md", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 12191, + "sha256": "87756328c812a9076a55d5ebe1b9ea81d8fdcb166608cb39b0b43cca2cdc8593", + "git_blob": "71a8c020a59e8469cd547511766db92fa79480c4" + }, + { + "path": "research/p104-unread-path-resynthesis/inputs/pr5811-RESULT.json", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 19496, + "sha256": "2ba9ec0c06ce0c2683cdd704cacb63e6bb9afeb90a07a16fb63ec9e55696c488", + "git_blob": "2e73d97bdd2b2c13e05e66299722e0aa30c2d050" + }, + { + "path": "research/p104-unread-path-resynthesis/inputs/pr5811-WORD.json.gz", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 122915, + "sha256": "690656bfca9c6f0366527d158ca4edb14f83c410604d647953c20c7c94bea2e8", + "git_blob": "3633d78556932b1d66285c19d888fcd7c62cdbf1" + }, + { + "path": "research/p104-unread-path-resynthesis/local.py", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 9394, + "sha256": "7201df8e32f5c99f7403150e8664042322037906088bc754c67293a241368597", + "git_blob": "b7be846b10c4c54a4e1558d7b563bc8c3a170223" + }, + { + "path": "research/p104-unread-path-resynthesis/pricing.py", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 11028, + "sha256": "04b36429147f2809468d9ff037e26eaa70e66a5180e4b5c71a060bd5d14ffd9c", + "git_blob": "f2882694610b9bb49ddd7b6d99ccd628ae58be37" + }, + { + "path": "research/p104-unread-path-resynthesis/sources.py", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 2488, + "sha256": "f96de7d80f369c12f6f904b7935610979d59617ed0d49963841e86b9a2b45557", + "git_blob": "3b4c60838a43cb849707292bac144f14ad7fc8f1" + }, + { + "path": "research/p104-unread-path-resynthesis/verify.py", + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "size": 7142, + "sha256": "41f71fff49c041d44048652228c901221555762f7ff3e11a088aa270ce6820a7", + "git_blob": "2a4d91891374a872dbee92b86bd21ebfb305c029" + } + ] +} diff --git a/research/p104-helper468-rung-removal/TASK.json b/research/p104-helper468-rung-removal/TASK.json new file mode 100644 index 0000000000..ba6c250917 --- /dev/null +++ b/research/p104-helper468-rung-removal/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Edit the word of PR5827 (one helper rung removed, three helpers retargeted) and re-certify the complete conditional claim with PR5827's own chain.", + "scope_change_reason": "The card asks for joint helper bases and a legal causal split; this package changes the itinerary of helpers in PR5827's word instead, with productive targets fixed. Recorded as changed.", + "bottleneck_link": "The edit moves paid ranks (rank 1: -4, rank 4: +1, rank 6: +1, rank 7: +1) and lowers the paid bill from 66,870 to 66852 at fixed productive targets, so the exact crossing rises from .00312476681507 to 0.00312528909884.", + "budget_minutes": null, + "stop_rule": "Retain the claim only after the word regenerates byte for byte from the pinned PR5827 word and the edit list, pricing equals PR5827 pricing plus the declared literal edits, and the complete chain passes with the exact crossing interval.", + "outcome": "completed", + "evidence": "construct.py, verify.py, EDIT.json.gz, WORD.json.gz and RESULT.json", + "author": "DreamingOfClouds, with Claude Opus 5.5 (Anthropic), via Claude Code", + "ai_assistance": "Claude Opus 5.5 via Claude Code for the edit packaging and checks; all checks are author-side. Predecessor work: PR5827 aliromman (with substantial OpenAI Codex assistance) and its lineage, retained in the pinned archive.", + "open_questions": [ + { + "question": "Does an independent reviewer confirm the edit list, the regenerated word and the full chain?", + "why_it_matters": "Author checks do not establish independent acceptance.", + "blocked_by": "Independent review and the five framework assumptions remain open.", + "first_step": "Run construct.py and verify.py, then compare the changed boundary charts with the base word." + }, + { + "question": "Do other helpers with the same rung structure admit the same removal within the event cap?", + "why_it_matters": "Each further removal would lower the paid bill again.", + "blocked_by": "The retained cap of 26,000 events leaves little slack.", + "first_step": "List helpers whose itinerary passes through a frame no other helper reads and compare event counts." + } + ] +} diff --git a/research/p104-helper468-rung-removal/VERIFY.json b/research/p104-helper468-rung-removal/VERIFY.json new file mode 100644 index 0000000000..2e08a282a5 --- /dev/null +++ b/research/p104-helper468-rung-removal/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper468-rung-removal/EDIT.json.gz", + "research/p104-helper468-rung-removal/EXPECT.json", + "research/p104-helper468-rung-removal/PRICING-EDITS.json", + "research/p104-helper468-rung-removal/SOURCES.json", + "research/p104-helper468-rung-removal/WORD.json.gz", + "research/p104-helper468-rung-removal/construct.py", + "research/p104-helper468-rung-removal/inputs/pr5827-source.tar", + "research/p104-helper468-rung-removal/pricing.py", + "research/p104-helper468-rung-removal/sources.py", + "research/p104-helper468-rung-removal/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticate the pinned PR5827 package and source chain; assert pricing.py = PR5827 pricing.py + declared edits; regenerate WORD.json.gz from the edit list; replay, all input columns, native maps, physical caller, complete price, two interval engines, compiler, outer checks, controls and the committed receipt." + } + ] +} diff --git a/research/p104-helper468-rung-removal/WORD.json.gz b/research/p104-helper468-rung-removal/WORD.json.gz new file mode 100644 index 0000000000..7ffe7b500b Binary files /dev/null and b/research/p104-helper468-rung-removal/WORD.json.gz differ diff --git a/research/p104-helper468-rung-removal/construct.py b/research/p104-helper468-rung-removal/construct.py new file mode 100644 index 0000000000..87c578494c --- /dev/null +++ b/research/p104-helper468-rung-removal/construct.py @@ -0,0 +1,78 @@ +"""Regenerate WORD.json.gz from PR5827's pinned word and the explicit edit list in EDIT.json.gz. Apache-2.0. + +Standard library only; no solver and no dependence on any other tooling. The edit list is data: + initial / final : {register: [old, new]} changes to the public boundary charts, + program : the new event list as segments; [a, b] copies PR5827's program[a:b] unchanged and any + other entry is a literal event. +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. +Predecessor credit (PR5827 aliromman and its lineage): see README.md. +""" +from collections import Counter +from copy import deepcopy +from hashlib import sha256 +from pathlib import Path +import gzip, json, sys + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def read(path): + raw = Path(path).read_bytes() + return json.loads(gzip.decompress(raw) if str(path).endswith('.gz') else raw) + + +def digest(value): + return sha256(json.dumps(value, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + + +def dump(value): + return gzip.compress((json.dumps(value, sort_keys=True, indent=2) + '\n').encode(), mtime=0) + + +def construct(base, edit): + """Return the edited word. `base` is PR5827's WORD.json.gz payload, `edit` is EDIT.json.gz.""" + need(digest(base) == edit['base_word_sha256'], 'Edit applies to the pinned PR5827 word') + word = deepcopy(base) + for key in ('initial', 'final'): + for register, (old, new) in edit[key].items(): + need(base[key][int(register)] == old, 'Declared old boundary value: ' + key + ' ' + register) + word[key][int(register)] = new + program, source = [], base['program'] + for step in edit['program']: + if isinstance(step[0], int): + a, b = step + need(0 <= a < b <= len(source), 'Copy segment inside the base program') + program.extend(deepcopy(source[a:b])) + else: + program.append(list(step)) + word['program'] = program + need(word.keys() == base.keys(), 'Same word fields') + for key in base: + if key not in ('program', 'initial', 'final'): + need(word[key] == base[key], 'Unchanged word field: ' + key) + removed = Counter(e[0] for e in source) - Counter(e[0] for e in program) + added = Counter(e[0] for e in program) - Counter(e[0] for e in source) + need({'added': dict(added), 'removed': dict(removed)} == edit['operation_delta'], 'Declared operation delta') + return word + + +def pinned_base(): + """PR5827's word, read from the pinned source archive (digest-checked again in construct).""" + import io, tarfile + pins = read(HERE / 'SOURCES.json')['source_archive'] + with tarfile.open(HERE / pins['local_path'], 'r:') as bundle: + raw = bundle.extractfile(pins['package'] + '/WORD.json.gz').read() + return json.loads(gzip.decompress(raw)) + + +if __name__ == '__main__': + word = construct(pinned_base(), read(HERE / 'EDIT.json.gz')) + if '--write' in sys.argv: + (HERE / 'WORD.json.gz').write_bytes(dump(word)) + print('constructed', len(word['program']), 'events,', word['public'], 'public', + '(matches shipped WORD.json.gz)' if (HERE / 'WORD.json.gz').read_bytes() == dump(word) else '(differs from shipped)') diff --git a/research/p104-helper468-rung-removal/inputs/pr5827-source.tar b/research/p104-helper468-rung-removal/inputs/pr5827-source.tar new file mode 100644 index 0000000000..1e10936044 Binary files /dev/null and b/research/p104-helper468-rung-removal/inputs/pr5827-source.tar differ diff --git a/research/p104-helper468-rung-removal/pricing.py b/research/p104-helper468-rung-removal/pricing.py new file mode 100644 index 0000000000..0863b7e753 --- /dev/null +++ b/research/p104-helper468-rung-removal/pricing.py @@ -0,0 +1,184 @@ +"""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 were prepared for thu-nmrc with OpenAI Codex assistance. +Helper-subspace targets were added by Ali Romman with OpenAI Codex assistance. +The source commuting-contact construction is by Pierre-Loic Doulcet (hexapode) in PR5565. +The source coupled-frame change is by Ali Romman with OpenAI Codex in PR5601. +Five fixed boundary relations are from Ali Romman's PR5602. +The shared and delayed relays are from flyingviper's PR5605 and PR5612. The preparation is from +Scratch-net's PR5606. Their costs and target debit are included. +Ali Romman's complete caller/price proof and all predecessor credit are retained. +The paid A2 change is from zxv PR5643. The three helper relations are from +Ali Romman PR5644. The four-gate change is by Ali Romman with Codex assistance. +The four interior basis changes are by Ali Romman with Codex assistance. +Paid intermediate meetings: Ali Romman with substantial OpenAI Codex assistance. +Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +import local as L + +KAPPA, TESTED = Q('0.003125282'), Q('0.0031252870') +PREVIOUS = Q('0.00312476680') + + +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()) == 13444 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) + signed = Counter(T) + signed.subtract(P) + cap = Q('.0034') + derivative_upper = Q(0) + for rank, count in signed.items(): + logarithm = E.log_bounds(rank) + low = E.mul(E.power(rank, 1-cap), logarithm)[0] + high = rank*logarithm[1] + derivative_upper -= count*(low if count >= 0 else high) + L.need(derivative_upper < 0, 'Unique raw crossing below the retained BIT cap') + 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 the source claim') + t,u,v,c,b = 1-TESTED,Q(1,7),1024,16,17 + 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**12),Q(125,128) + 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),1024 + 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') + old_completion = E.divide((Q(sum(T.values())*18),)*2,E.mul(E.power(17,TESTED),target)) + L.need(old_completion[0] > Q(39,40), 'PR5718 completion-tail bound fails with the new target count') + old_offset = E.divide(E.moment(P,t+Q(1,5)),E.mul(E.power(16,Q(1,5)),target)) + L.need(old_offset[0] > decay, 'The old tail offset fails at the new cutoff') + 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':'0.003125282','previous_pr5827':PREVIOUS,'gain':KAPPA-PREVIOUS, + 'relative_gain_percent':100*(KAPPA/PREVIOUS-1),'raw_root_interval':[lower,upper], + 'raw_headroom':[lower-KAPPA,upper-KAPPA], + 'raw_ceiling':{'interval':[Q(0),cap],'derivative_upper':derivative_upper},'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,'tail_decay':decay,'tail_block':128, + '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':local['peak_owned_fields'], + 'fixed_scalar_growth_bound':'At most 2^(16*26000) before native factors; a declared constant, not an attained norm.', + 'local_paid_rank_mass':local['paid_rank_mass'], + 'tensor_native_growth_bound':'Each rank-r Gaussian has row l1 norm at most 2^(rf); use local_paid_rank_mass for the whole word.'}, + 'ordinary_BIT':bit,'outer':outer, + 'negative_controls':{'source_completion':'Rejected at cutoff17, floor18 and decay39/40', + 'source_offset':'Rejected at cutoff16 with tail offset1/5', + 'old_cutoff':'Rejected by completion-tail ratio greater than one','old_BIT':'Rejected by outer inequalities'}}) diff --git a/research/p104-helper468-rung-removal/sources.py b/research/p104-helper468-rung-removal/sources.py new file mode 100644 index 0000000000..d9199b5302 --- /dev/null +++ b/research/p104-helper468-rung-removal/sources.py @@ -0,0 +1,70 @@ +"""Authenticate and open PR5827's published package before importing any of its code. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. Apache-2.0. +The archive format and per-file checks follow PR5827's own sources.py (Ali Romman, OpenAI Codex assistance). +""" +from contextlib import contextmanager +from hashlib import sha1, sha256 +from pathlib import Path, PurePosixPath +import importlib.util +import json +import sys +import tarfile +import tempfile + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def read(path): + import gzip + 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) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def authenticate(raw, pin): + need(len(raw) == pin['size'], 'Exact source size: ' + pin['path']) + need(sha256(raw).hexdigest() == pin['sha256'], 'Exact source SHA256: ' + pin['path']) + need(sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == pin['git_blob'], + 'Exact source Git blob: ' + pin['path']) + + +@contextmanager +def sources(): + """Yield the directory of PR5827's extracted package (every file authenticated).""" + pins = json.loads((HERE / 'SOURCES.json').read_bytes()) + archive = pins['source_archive'] + path = HERE / archive['local_path'] + need(sha256(path.read_bytes()).hexdigest() == archive['sha256'], 'Exact source archive') + members = {p['path']: p for p in pins['archived_files']} + need(len(members) == len(pins['archived_files']) == archive['files'], 'Exact source inventory') + with tempfile.TemporaryDirectory(prefix='p104-base-source-') as directory: + root = Path(directory) + with tarfile.open(path, 'r:') as bundle: + seen = set() + for member in bundle.getmembers(): + name = PurePosixPath(member.name) + need(member.isfile() and not name.is_absolute() and '..' not in name.parts + and '\\' not in member.name and ':' not in member.name, + 'Regular relative source file') + need(member.name in members and member.name not in seen, 'Unique declared source file') + seen.add(member.name) + raw = bundle.extractfile(member).read() + authenticate(raw, members[member.name]) + target = root.joinpath(*name.parts) + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(raw) + need(seen == set(members), 'Complete source archive') + yield root / archive['package'] diff --git a/research/p104-helper468-rung-removal/verify.py b/research/p104-helper468-rung-removal/verify.py new file mode 100644 index 0000000000..4101470277 --- /dev/null +++ b/research/p104-helper468-rung-removal/verify.py @@ -0,0 +1,146 @@ +"""Verify the edited PR5827 word with PR5827's own chain. Apache-2.0. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. The chain below is +PR5827's own verifier (its package is authenticated from inputs/ and loaded unmodified, apart from +pricing.py whose declared literal edits are in PRICING-EDITS.json); the word is regenerated by +construct.py from PR5827's word and the explicit edit list. +Parts: --part build (authentication, regeneration, exact replay and storage inventory), + --part chain (the complete chain; includes build). Default: chain. +""" +from collections import Counter +from contextlib import ExitStack +from copy import deepcopy +from fractions import Fraction as Q +from pathlib import Path +import json, sys, tempfile +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from sources import sources, load, need, read, authenticate +from construct import construct, dump + +EXPECT = read(HERE / 'EXPECT.json') + + +def reject(action): + try: + action() + except ValueError as error: + return str(error) + raise ValueError('Invalid control accepted') + + +def delta(after, before): + value = Counter(after) + value.subtract(before) + return {str(r): n for r, n in sorted(value.items()) if n} + + +def run(part): + with ExitStack() as contexts: + parent = contexts.enter_context(sources()) # PR5827's extracted package + cursor = contexts.enter_context(load(parent / 'sources.py', 'base_source_top').sources()) + for depth in range(7): # PR5827's own seven-deep source chain + module = load(cursor / 'sources.py', 'base_source_' + str(depth)) + cursor, root = contexts.enter_context(module.sources()) + text = (parent / 'pricing.py').read_text(encoding='utf-8') + for old, new in read(HERE / 'PRICING-EDITS.json'): + need(text.count(old) == 1, 'Unique declared pricing edit') + text = text.replace(old, new) + need(text == (HERE / 'pricing.py').read_text(encoding='utf-8'), 'Shipped pricing.py = PR5827 pricing.py + declared edits only') + L = load(parent / 'local.py', 'local') + L.ROOT = root + source = read(parent / 'WORD.json.gz') + word = construct(source, read(HERE / 'EDIT.json.gz')) + need((HERE / 'WORD.json.gz').read_bytes() == dump(word), 'Entire regenerated WORD.json.gz, byte for byte') + need(all(type(e[4]) is bool for e in word['program'] if e[0] == 'MOVE'), 'Canonical MOVE private flags') + baseline, local = L.replay(source), L.replay(word) + need((local['public_inputs'], local['owned_fields'], local['owned_lifetimes'], local['peak_owned_fields']) == + (baseline['public_inputs'], baseline['owned_fields'], baseline['owned_lifetimes'], baseline['peak_owned_fields']) + == tuple(EXPECT['inventory']), 'Unchanged storage inventory') + need(len(word['program']) == EXPECT['events'] <= 26000, 'Event count within the retained bound') + need(delta(local['paid'], baseline['paid']) == EXPECT['paid_delta'], 'Exact paid-profile delta') + need(delta(local['helpers'], baseline['helpers']) == EXPECT['helper_delta'], 'Exact productive-target delta') + print('PASS regenerated WORD.json.gz, exact replay, storage inventory, paid delta', EXPECT['paid_delta'], flush=True) + if part == 'build': + print(EXPECT['status'] + '_BUILD'); return None + columns = L.reverse_columns(word) + need(columns['columns'] == 799, 'All input columns') + print('PASS all input columns and separate transpose', flush=True) + native = L.native(word) + C = load(root / 'research/p104-productive-controller/caller.py', 'base_caller') + caller = C.construct() + need(caller == read(root / 'research/p104-productive-controller/CONTROLLER.json'), 'Exact physical caller') + physical = C.physical(caller, word) + print('PASS native maps, absolute phases, adapters and complete physical caller', flush=True) + P = load(HERE / 'pricing.py', 'edit_price') + price = P.run(local, native, caller, physical) + need(price['raw_root_interval'] == EXPECT['interval'], 'Exact crossing interval') + need((price['paid_calls'], price['productive_fields'], price['rank_mass_surplus']) == + (EXPECT['paid_calls'], EXPECT['productive_fields'], EXPECT['rank_mass_surplus']), 'Invoice') + need(len(price['outer']['strict_checks']) == 54 and len(price['outer']['functional_checks']) == 4, 'Outer inventory') + # the base word's profile, scaled as in the invoice, must fail at the new claim + E = L.load(root / 'research/higher-moment-strictification/verify.py', 'base_price_engine') + old_p = {int(r): n for r, n in price['paid'].items()} + old_t = {int(r): n for r, n in price['targets'].items()} + for r, n in baseline['paid'].items(): + old_p[r] += 18 * (n - local['paid'].get(r, 0)) + for r in set(baseline['helpers']) | set(local['helpers']): + old_t[r] += 18 * (baseline['helpers'].get(r, 0) - local['helpers'].get(r, 0)) + margin = E.moment(old_t, 1 - P.KAPPA)[1] - E.moment(old_p, 1 - P.KAPPA)[0] + need(margin < 0, 'PR5827 full profile fails at the new claim') + print('PASS both rational engines, completion, compiler and all outer costs', price['raw_root_interval'], flush=True) + + controls = C.controls(caller) + for label, make in EXPECT_CONTROLS(word, source): + controls[label] = reject(make) + bad = deepcopy(local); bad['paid'][1] -= 1 + controls['unpaid_query'] = reject(lambda: P.assemble(bad, native, caller, physical)) + bad = deepcopy(local); bad['helpers'][9] += 1 + controls['extra_target_credit'] = reject(lambda: P.assemble(bad, native, caller, physical)) + for pin in read(HERE / 'SOURCES.json')['archived_files'][:3]: + raw = (parent / Path(pin['path']).relative_to(read(HERE / 'SOURCES.json')['source_archive']['package'])).read_bytes() + controls['damaged_source_' + Path(pin['path']).name] = reject( + lambda raw=raw, pin=pin: authenticate(bytes([raw[0] ^ 1]) + raw[1:], pin)) + result = dict(status=EXPECT['status'], base_commit=EXPECT['base_commit'], source_local=baseline, local=local, + paid_delta=EXPECT['paid_delta'], target_delta=EXPECT['helper_delta'], separate_columns=columns, + native=native, physical_caller=physical, complete_cost=price, + base_margin_upper_at_new_claim=margin, controls=controls, + limits=['All five inherited framework assumptions remain.', + 'The large uniform word and rounded multiplier are not materialized.', + 'Author checks do not establish independent acceptance.', + 'The selected frontier is unchanged.']) + return P.encode(result) + + +def EXPECT_CONTROLS(word, source): + """Corruptions of the edited word that the exact replay must reject.""" + L = sys.modules['local'] + out = [] + for label, index in EXPECT['control_sites'].items(): + bad = deepcopy(word); bad['program'].pop(index) + out.append(('missing_' + label, lambda bad=bad: L.replay(bad))) + for label, index in EXPECT['sign_sites'].items(): + bad = deepcopy(word); q = Q(bad['program'][index][-2]); bad['program'][index][-2] = str(-q) + out.append(('wrong_sign_' + label, lambda bad=bad: L.replay(bad))) + return out + + +def main(): + part = sys.argv[sys.argv.index('--part') + 1] if '--part' in sys.argv else 'chain' + need(part in ('build', 'chain'), '--part must be build or chain') + with tempfile.TemporaryDirectory(prefix='p104-edit-bytecode-') as cache: + sys.pycache_prefix = cache + result = run(part) + if result is None: + return + path = HERE / 'RESULT.json' + if '--write' in sys.argv: + path.write_bytes((json.dumps(result, sort_keys=True, indent=2) + '\n').encode()) + else: + need(read(path) == result, 'Exact retained output: RESULT.json') + print(EXPECT['status'], flush=True) + + +if __name__ == '__main__': + main()