diff --git a/research/p104-helper470-twin-rung-removal/EDIT.json.gz b/research/p104-helper470-twin-rung-removal/EDIT.json.gz new file mode 100644 index 0000000000..7f2119f2b3 Binary files /dev/null and b/research/p104-helper470-twin-rung-removal/EDIT.json.gz differ diff --git a/research/p104-helper470-twin-rung-removal/EXPECT.json b/research/p104-helper470-twin-rung-removal/EXPECT.json new file mode 100644 index 0000000000..0e7201cef9 --- /dev/null +++ b/research/p104-helper470-twin-rung-removal/EXPECT.json @@ -0,0 +1,44 @@ +{ + "interval": [ + "312581155791/100000000000000", + "19536322237/6250000000000" + ], + "paid_calls": 66834, + "productive_fields": 13444, + "rank_mass_surplus": 760, + "events": 22803, + "inventory": [ + 770, + 29, + 31, + 13 + ], + "paid_delta": { + "1": -2, + "2": 1, + "3": -2, + "4": 1, + "6": 1, + "7": -1, + "8": 1 + }, + "helper_delta": { + "1": -1, + "2": 1, + "3": -1, + "6": 1, + "7": -1, + "8": 1 + }, + "control_sites": { + "add1": 1, + "add5": 5 + }, + "sign_sites": { + "add1": 1, + "add5": 5 + }, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "chain_commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "status": "PASS_P104_BASE5907_EDIT_KAPPA_312580400" +} diff --git a/research/p104-helper470-twin-rung-removal/PRICING-EDITS.json b/research/p104-helper470-twin-rung-removal/PRICING-EDITS.json new file mode 100644 index 0000000000..8e666b6c70 --- /dev/null +++ b/research/p104-helper470-twin-rung-removal/PRICING-EDITS.json @@ -0,0 +1,18 @@ +[ + [ + "KAPPA, TESTED = Q('0.00312476680'), Q('0.003124766805')", + "KAPPA, TESTED = Q('0.003125804'), Q('0.0031258090')" + ], + [ + "PREVIOUS = Q('0.00312418633064')", + "PREVIOUS = Q('0.003125282')" + ], + [ + "sum(targets.values()) == 13444 and sum(paid.values()) == 66870", + "sum(targets.values()) == 13444 and sum(paid.values()) == 66834" + ], + [ + "'kappa_decimal':'0.00312476680','previous_pr5811':PREVIOUS", + "'kappa_decimal':'0.003125804','previous_pr5907':PREVIOUS" + ] +] diff --git a/research/p104-helper470-twin-rung-removal/README.md b/research/p104-helper470-twin-rung-removal/README.md new file mode 100644 index 0000000000..725be51cbf --- /dev/null +++ b/research/p104-helper470-twin-rung-removal/README.md @@ -0,0 +1,75 @@ +# Conditional kappa 0.003125804: remove helper 470's frame-593 rung, the twin of PR5907's removal + +This package edits the word of [PR #5907](https://github.com/CrocSwap/integer-mult-bounds/pull/5907) +(DreamingOfClouds, merged on main, conditional kappa 0.003125282) and re-certifies it with the chain PR #5907 used: +PR #5827's own verifier (aliromman, head `05cd36e5af06d7a3790e30ce3f449fa89b853768`), loaded unmodified apart from the declared pricing literals. +The complete conditional kappa is **0.003125804**, tested at 0.0031258090; the exact raw crossing lies in +(0.00312581155791, 0.00312581155792) = (312581155791/100000000000000, 19536322237/6250000000000), +which is +5.225e-07 above PR #5907's raw crossing (0.00312528909884). The paid bill falls to +**66834 calls** (PR #5907: 66,852) 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 22,803 events (PR #5907: 25,998; retained cap 26,000). + +## The edit + +The edit removes helper 470's rung at frame 593: its itinerary 3 -> 593 -> 714 -> 875 -> 1001 -> 131 -> 127 becomes +3 -> 714 -> 875 -> 1001 -> 131 -> 127. Helper 704's chain 3 -> 593 -> 612 -> 127 now runs 3 -> 593 -> 714 -> 127, so helper 470 +takes its read of 704 at frame 714. This is the twin of PR #5907's removal (helper 468's frame-593 rung, with helper 703 moved to +frame 712). Helper 560 no longer reads 704 at frame 612; helper 268, which received that content through its frame-612 read +of 560, now reads 2ยท704 directly at frame 714. Four further itineraries change: helper 115 ends at frame 189 instead of 105, Y main 127's second chart is 595 +instead of 602, helper 713 starts at frame 76 instead of 3, and helper 736 starts at frame 749 instead of 424. +Every other change is a rewrite of the ordinary (ADD and SCALE) events. The INIT, CLEAR and COPY events are identical as a +multiset, every MOVE outside the six itineraries above is unchanged, and the chart list and every endpoint row are kept: the event list falls from 25,998 to 22,803 events (ADD 21,706 -> 18,404, +SCALE 753 -> 861, MOVE 3,454 -> 3,453), and about 795 registers carry a different event +sequence. + +Boundary charts changed by the edit: initial 713: 3 -> 76; initial 736: 424 -> 749; final 115: 105 -> 189. Paid-profile change vs PR #5907: rank 1: -2, rank 2: +1, rank 3: -2, rank 4: +1, rank 6: +1, rank 7: -1, rank 8: +1. +Credited helper-rank change: rank 1: -1, rank 2: +1, rank 3: -1, rank 6: +1, rank 7: -1, rank 8: +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 #5907's program and literal events. `construct.py` (standard library only) applies it to PR #5907's word, taken from +`inputs/pr5907-WORD.json.gz` (authenticated against main's `research/p104-helper468-rung-removal/WORD.json.gz`, Git blob and SHA256 in `SOURCES.json`), and regenerates +`WORD.json.gz` byte for byte: + +```sh +python3.12 -I -B research/p104-helper470-twin-rung-removal/construct.py +``` + +## Verification + +```sh +python3.12 -I -B research/p104-helper470-twin-rung-removal/verify.py +``` + +`verify.py` authenticates PR #5907's word and the pinned PR #5827 package (`inputs/pr5827-source.tar`, per-file SHA256 and Git blob; +byte-identical to the archive in PR #5907's package) 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 = PR #5907's, 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, 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, a check that PR #5907's full profile fails at the new claim, +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 is PR #5907's (DreamingOfClouds, helper 468's frame-593 rung removal), itself an edit of PR #5827's word. +The verifier chain is 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 itineraries with PR #5907's word. +- Helpers 469 and 471 have the same frame-593 rung shape as 468 and 470, but their frame-593 reads come from the same two sources + (703, 704) that the two removals now place at frames 712 and 714. Does any itinerary for 469 or 471 avoid frame 593 without a new + carrier of that content? First step: list the holders of 469's and 471's frame-593 read content at frames shared with 469 and 471. diff --git a/research/p104-helper470-twin-rung-removal/RESULT.json b/research/p104-helper470-twin-rung-removal/RESULT.json new file mode 100644 index 0000000000..e4a03118d5 --- /dev/null +++ b/research/p104-helper470-twin-rung-removal/RESULT.json @@ -0,0 +1,396 @@ +{ + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "base_margin_upper_at_new_claim": "-390359343452242794286352754590140865431940508358395458455/3138550867693340381917894711603833208051177722232017256448", + "complete_cost": { + "compiler": { + "H": 65807000000000, + "N": "2^65807000000000", + "eta": { + "lower": "0.000000120357243671228711011443", + "upper": "0.000000120357243671228711011444" + }, + "gap": "1/1400000000", + "integer_test_exponent": 47005, + "logarithm_power": 1024, + "theta": "63/64", + "uniform_saving": "10940329/3500000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "261/500000000", + "kappa": "781451/250000000", + "kappa_decimal": "0.003125804", + "margin_at_previous": { + "lower": "0.127894719171880023552284133066", + "upper": "0.127894719171880023552284133067" + }, + "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": 5952, + "local_routes": 5325000, + "local_scalar": 189428, + "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": "30632907178119357/9800000000000000000", + "fused_gaussian": "30632907134358071/9800000000000000000", + "global_coordinate_router": "2735081/875000000", + "group_bit_router": "3829114266794757/1225000000000000000", + "group_scans": "699999999/700000000", + "main_transform": "30632900178119357/9800000000000000000", + "microbox_face_corrections": "26950000001/350000000", + "polynomial_products": "1399999999/1400000000", + "sparse_union_movement": "4011882907178119357/9800000000000000000" + }, + "parameters": { + "a": "2735081/875000000", + "b": "21880653/7000000000", + "beta": "1399999997/1400000000", + "bit_saving": "17/5000", + "cap_xi": "8911882900178119357/9800000000000000000", + "complex_uniform_saving": "10940329/3500000000", + "d": "1/1400000000", + "epsilon": "1399999999/1400000000", + "kappa": "781451/250000000", + "lambda_": "1993748387/2000000000", + "lambda_prime": "6978119357/7000000000", + "layout": "1/1400000000", + "q": "21880643/7000000000", + "r0": "1/14000000000", + "stop": "1/1400000000", + "tested_saving": "3125809/1000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "239919/875000000", + "actual_logarithmic_gamma_guard": "1/1400000000", + "actual_logarithmic_group_guard": "888117110321880643/4900000000000000000", + "alpha_logarithm_absorption": "1/14000000000", + "boundary_algebraic_matrix_above_kappa": "27978119357/9800000000000000000", + "cap_above_band": "4011882900178119357/9800000000000000000", + "cap_below_cell": "888117092821880643/9800000000000000000", + "cap_below_phase_cell_power": "10688117099821880643/9800000000000000000", + "complex_above_effective": "1/1400000000", + "complex_below_one_over_32": "196869347/7000000000", + "complex_endpoint": "1/700000000", + "epsilon_below_one": "1/1400000000", + "epsilon_positive": "1399999999/1400000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "27934358071/9800000000000000000", + "gaussian_above_main": "3478119357/4900000000000000000", + "global_coordinate_router_above_kappa": "1/350000000", + "global_gamma_power_slack": "9/14000000000", + "group_below_dimension": "1/700000000", + "group_bit_router_above_kappa": "4366794757/1225000000000000000", + "group_gauge_power_slack": "888117109971880643/4900000000000000000", + "group_key_fits_record": "1/700000000", + "group_positive": "1399999997/1400000000", + "group_scans_above_kappa": "3489059681/3500000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "697416790400418148631/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": "13978119347/9800000000000000000", + "leaf_saving_above_effective": "6978119347/9800000000000000000", + "main_transform_above_kappa": "20978119357/9800000000000000000", + "membership_arithmetic_fits_record": "1/1400000000", + "microbox_face_corrections_above_kappa": "16843066231/218750000", + "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": "6978119367/7000000000", + "positive_layout_slack": "1/1400000000", + "q_below_effective": "1/1400000000", + "q_below_internal": "1/1400000000", + "q_below_leaf": "13978119347/9800000000000000000", + "q_positive": "21880643/7000000000", + "short_record_fallback": "6978119347/7000000000", + "source_axis_superpolynomial": "1/1400000000", + "sparse_union_movement_above_kappa": "3981250027978119357/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": 41502, + "16": 416, + "2": 8226, + "24": 416, + "3": 8928, + "32": 416, + "4": 1800, + "40": 416, + "48": 416, + "5": 2934, + "56": 416, + "6": 198, + "64": 416, + "7": 108, + "72": 208, + "8": 18 + }, + "paid_calls": 66834, + "previous_pr5907": "1562641/500000000", + "productive_fields": 13444, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_ceiling": { + "derivative_upper": "-367807535420800867201733748003152468614163818931415672397258381/1569275433846670190958947355801916604025588861116008628224", + "interval": [ + "0", + "17/5000" + ] + }, + "raw_headroom": [ + "755791/100000000000000", + "47237/6250000000000" + ], + "raw_root_interval": [ + "312581155791/100000000000000", + "19536322237/6250000000000" + ], + "relative_gain_percent": "26100/1562641", + "strictification": { + "alpha": { + "lower": "0.999999997408080181764198797100", + "upper": "0.999999997408080181764198797101" + }, + "cutoff": 16, + "delta": { + "lower": "0.950628642242169524414131100979", + "upper": "0.950628642242169524414131100980" + }, + "floor": 17, + "gamma": { + "lower": "0.975562351047467297857948799346", + "upper": "0.975562351047467297857948799347" + }, + "normalized_paid_upper": "1048576000976562501/1048576001073741824", + "power": 1024, + "reserve": "1/1000000000000", + "tail_block": 128, + "tail_decay": "125/128", + "tail_offset": "1/7", + "tested": "3125809/1000000000" + }, + "targets": { + "1": 252, + "145": 208, + "17": 416, + "2": 144, + "25": 416, + "3": 72, + "33": 416, + "4": 1926, + "41": 416, + "49": 416, + "5": 252, + "57": 416, + "6": 36, + "65": 416, + "7": 162, + "73": 208, + "8": 342, + "9": 6930 + }, + "whole_idle_jobs": 3120 + }, + "controls": { + "damaged_base_word": "Exact source SHA256: research/p104-helper468-rung-removal/WORD.json.gz", + "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_add1": "All public and owned rows", + "missing_add5": "All public and owned rows", + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "unpaid_query": "Complete field and call counts", + "wrong_sign_add1": "All public and owned rows", + "wrong_sign_add5": "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": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 2, + "7": 9, + "8": 19, + "9": 385 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid": { + "1": 2219, + "2": 457, + "3": 496, + "4": 100, + "5": 163, + "6": 11, + "7": 6, + "8": 1 + }, + "paid_rank_mass": 5952, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 189428 + }, + "native": { + "distinct_maps": 2922, + "helper_normalizers": 1124, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 2, + "7": 9, + "8": 19, + "9": 385 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "e22642923d5437c49e2d1dc79dd6b795503499d6f33615a1df3568f0b96164c1", + "wrong_phase_rejected": true + }, + "paid_delta": { + "1": -2, + "2": 1, + "3": -2, + "4": 1, + "6": 1, + "7": -1, + "8": 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": 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 + }, + "status": "PASS_P104_BASE5907_EDIT_KAPPA_312580400", + "target_delta": { + "1": -1, + "2": 1, + "3": -1, + "6": 1, + "7": -1, + "8": 1 + } +} diff --git a/research/p104-helper470-twin-rung-removal/SOURCES.json b/research/p104-helper470-twin-rung-removal/SOURCES.json new file mode 100644 index 0000000000..5042494d12 --- /dev/null +++ b/research/p104-helper470-twin-rung-removal/SOURCES.json @@ -0,0 +1,198 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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" + } + ], + "base_word": { + "local_path": "inputs/pr5907-WORD.json.gz", + "path": "research/p104-helper468-rung-removal/WORD.json.gz", + "commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "pr": 5907, + "size": 138258, + "sha256": "b69a9cb3a26d4f40aa7ad14f814b188fe16a782999f6f56292538e447d67b284", + "git_blob": "7ffe7b500b02b9d0de49a85ec53e36004f1a411f" + } +} diff --git a/research/p104-helper470-twin-rung-removal/TASK.json b/research/p104-helper470-twin-rung-removal/TASK.json new file mode 100644 index 0000000000..84e87fb351 --- /dev/null +++ b/research/p104-helper470-twin-rung-removal/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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 PR5907 (helper 470's frame-593 rung removed, helper 704 re-hosted to frame 714, four further itinerary changes) and re-certify the complete conditional claim with PR5827's own chain, as PR5907 did.", + "scope_change_reason": "The card asks for joint helper bases and a legal causal split; this package changes the itinerary of helpers in PR5907's word instead, with productive targets fixed. Recorded as changed.", + "bottleneck_link": "The edit moves paid ranks (rank 1: -2, rank 2: +1, rank 3: -2, rank 4: +1, rank 6: +1, rank 7: -1, rank 8: +1) and lowers the paid bill from 66,852 to 66834 at fixed productive targets, so the exact crossing rises from 0.00312528909884 to 0.00312581155791.", + "budget_minutes": null, + "stop_rule": "Retain the claim only after the word regenerates byte for byte from the pinned PR5907 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: PR5907 (DreamingOfClouds) and 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 itineraries with the PR5907 word." + }, + { + "question": "Can helpers 469 or 471 lose their frame-593 rung as well?", + "why_it_matters": "Each further removal would lower the paid bill again.", + "blocked_by": "Their frame-593 read content is held by sources 703/704, which the two removals now place at frames 712/714.", + "first_step": "List the holders of that content at frames shared with 469 and 471." + } + ] +} diff --git a/research/p104-helper470-twin-rung-removal/VERIFY.json b/research/p104-helper470-twin-rung-removal/VERIFY.json new file mode 100644 index 0000000000..625fba9abb --- /dev/null +++ b/research/p104-helper470-twin-rung-removal/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/EDIT.json.gz", + "research/p104-helper470-twin-rung-removal/EXPECT.json", + "research/p104-helper470-twin-rung-removal/PRICING-EDITS.json", + "research/p104-helper470-twin-rung-removal/SOURCES.json", + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-helper470-twin-rung-removal/construct.py", + "research/p104-helper470-twin-rung-removal/inputs/pr5827-source.tar", + "research/p104-helper470-twin-rung-removal/inputs/pr5907-WORD.json.gz", + "research/p104-helper470-twin-rung-removal/pricing.py", + "research/p104-helper470-twin-rung-removal/sources.py", + "research/p104-helper470-twin-rung-removal/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticate the pinned PR5907 word and the 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-helper470-twin-rung-removal/WORD.json.gz b/research/p104-helper470-twin-rung-removal/WORD.json.gz new file mode 100644 index 0000000000..22f9ab02d1 Binary files /dev/null and b/research/p104-helper470-twin-rung-removal/WORD.json.gz differ diff --git a/research/p104-helper470-twin-rung-removal/construct.py b/research/p104-helper470-twin-rung-removal/construct.py new file mode 100644 index 0000000000..b77ed74298 --- /dev/null +++ b/research/p104-helper470-twin-rung-removal/construct.py @@ -0,0 +1,76 @@ +"""Regenerate WORD.json.gz from PR5907'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 PR5907'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 (PR5907, 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 PR5907's WORD.json.gz payload, `edit` is EDIT.json.gz.""" + need(digest(base) == edit['base_word_sha256'], 'Edit applies to the pinned PR5907 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(): + """PR5907's word, authenticated against SOURCES.json (digest-checked again in construct).""" + sys.path.insert(0, str(HERE)) + from sources import base_word + return base_word() + + +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-helper470-twin-rung-removal/inputs/pr5827-source.tar b/research/p104-helper470-twin-rung-removal/inputs/pr5827-source.tar new file mode 100644 index 0000000000..1e10936044 Binary files /dev/null and b/research/p104-helper470-twin-rung-removal/inputs/pr5827-source.tar differ diff --git a/research/p104-helper470-twin-rung-removal/inputs/pr5907-WORD.json.gz b/research/p104-helper470-twin-rung-removal/inputs/pr5907-WORD.json.gz new file mode 100644 index 0000000000..7ffe7b500b Binary files /dev/null and b/research/p104-helper470-twin-rung-removal/inputs/pr5907-WORD.json.gz differ diff --git a/research/p104-helper470-twin-rung-removal/pricing.py b/research/p104-helper470-twin-rung-removal/pricing.py new file mode 100644 index 0000000000..65bb723f85 --- /dev/null +++ b/research/p104-helper470-twin-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.003125804'), Q('0.0031258090') +PREVIOUS = Q('0.003125282') + + +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()) == 66834, '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.003125804','previous_pr5907':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-helper470-twin-rung-removal/sources.py b/research/p104-helper470-twin-rung-removal/sources.py new file mode 100644 index 0000000000..227794adce --- /dev/null +++ b/research/p104-helper470-twin-rung-removal/sources.py @@ -0,0 +1,80 @@ +"""Authenticate PR5907's word (the base of the edit) and open PR5827's published package (the verifier chain) +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'] + + +def base_word(): + """PR5907's WORD.json.gz payload, authenticated against the main-branch pin in SOURCES.json.""" + import gzip + pin = json.loads((HERE / 'SOURCES.json').read_bytes())['base_word'] + raw = (HERE / pin['local_path']).read_bytes() + authenticate(raw, pin) + return json.loads(gzip.decompress(raw)) diff --git a/research/p104-helper470-twin-rung-removal/verify.py b/research/p104-helper470-twin-rung-removal/verify.py new file mode 100644 index 0000000000..624e36b1ca --- /dev/null +++ b/research/p104-helper470-twin-rung-removal/verify.py @@ -0,0 +1,148 @@ +"""Verify the edited PR5907 word with PR5827's own chain (the chain PR5907 used). 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 PR5907's word (authenticated against its main-branch pin) 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, base_word +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 = base_word() # PR5907's word, authenticated + 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 in set(baseline['paid']) | set(local['paid']): + old_p[r] = old_p.get(r, 0) + 18 * (baseline['paid'].get(r, 0) - local['paid'].get(r, 0)) + for r in set(baseline['helpers']) | set(local['helpers']): + old_t[r] = old_t.get(r, 0) + 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, 'PR5907 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)) + bw = read(HERE / 'SOURCES.json')['base_word']; raw = (HERE / bw['local_path']).read_bytes() + controls['damaged_base_word'] = reject(lambda: authenticate(bytes([raw[0] ^ 1]) + raw[1:], bw)) + 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()