diff --git a/research/p104-paid-interior-bases/NOTICE b/research/p104-paid-interior-bases/NOTICE new file mode 100644 index 0000000000..fa0bd1401f --- /dev/null +++ b/research/p104-paid-interior-bases/NOTICE @@ -0,0 +1,42 @@ +Four paid interior public-basis changes. +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +No subagents. + +The following exact notice is retained from PR5660. + +New helper-subspace construction, proof and replay: +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The same assistant performed the construction and author-side checks. + +Retained contributions: +flyingviper: PR5605 shared relay, PR5612 delayed relay, and the PR5608/PR5613 +relay/split compositions. +Scratch-net: PR5606 prepared-helper identities and target debit. +Pierre-Loic Doulcet (hexapode): PR5565 commuting-contact construction, used as the exact source. +Ali Romman: PR5602 fixed boundary relations, PR5601 three-contact frame +change, PR5580 contact step, +and PR5544/5545 complete P104 caller. +Joel Pulikkan (GamingPuzzled): PR5569 priced helper handoff. +DreamingOfClouds: PR5561 free helper endpoints and PR5568 search tools. +thu-nmrc: PR5551 contact improvements. +Gareth Davidson (bitplane): PR2305 source composition. +David Arias: PR2152 coalesced P104 word. +Cinna Davis: PR2219 private reuse and the controller lineage. +Jacob Alan Sussman: productive mixed-target recursion. +zxv and Cao Yifan: exact intervals, compiler and native/pricing lineage. +GamingPuzzled: PR5472 successor handoff, a predecessor to the split concept. +The retained source notices preserve earlier geometry, BIT and analytic credit. + +The elementary rank-one basis identity is not claimed as a new general +linear-algebra theorem. The contribution is its explicit independent-target +use on this P104 word and the complete conditional kappa improvement. + +New contribution: Ali Romman, with substantial OpenAI Codex assistance. +The four-gate source-version rewrite composes zxv PR5643 and Ali Romman PR5644. +The A2 method retains Chris R/Clear1nsight PR3998 and ToikY PR4019 credit. +The compensated triangle method retains Cinna Davis PR4692 credit. +No subagents were used for this contribution. Apache-2.0. + +Concurrent PR5650 by zxv publishes the PR5643/PR5644 composition. PR5651 by +Ali Romman corroborates it. This package credits that released composition +and contributes the further four-gate placement. diff --git a/research/p104-paid-interior-bases/PRICING-EDITS.json b/research/p104-paid-interior-bases/PRICING-EDITS.json new file mode 100644 index 0000000000..21f898d14e --- /dev/null +++ b/research/p104-paid-interior-bases/PRICING-EDITS.json @@ -0,0 +1,26 @@ +[ + [ + "Q('.00310676333'), Q('.003106763335')", + "Q('.00310815849'), Q('.003108158495')" + ], + [ + "PREVIOUS = Q('.00310644469')", + "PREVIOUS = Q('.00310676333')" + ], + [ + "== 66474", + "== 66402" + ], + [ + "'kappa_decimal':'.00310676333'", + "'kappa_decimal':'.00310815849'" + ], + [ + "previous_open_pr5651", + "previous_open_pr5660" + ], + [ + "Ali Romman PR5644. The four-gate change is by Ali Romman with Codex assistance.", + "Ali Romman PR5644. The four-gate change is by Ali Romman with Codex assistance.\nThe four interior basis changes are by Ali Romman with Codex assistance." + ] +] diff --git a/research/p104-paid-interior-bases/PROOF.md b/research/p104-paid-interior-bases/PROOF.md new file mode 100644 index 0000000000..77ef428c1a --- /dev/null +++ b/research/p104-paid-interior-bases/PROOF.md @@ -0,0 +1,111 @@ +# Exact construction and complete price + +## 1. One temporary basis + +Let `a` and `b` be distinct public registers. Set `R = I + c E_ab` for a +nonzero dyadic scalar `c`. Then `R^-1 = I - c E_ab`. + +Choose two internal cuts where both registers can reach one common chart. +Insert `R` at the first cut. Between the cuts, replace each scalar block +`M_j` by `R M_j R^-1`. Insert `R^-1` at the second cut. The complete interval +is unchanged: + +```text +R^-1 (R M_k R^-1) ... (R M_1 R^-1) R = M_k ... M_1. +``` + +A block that does not use either register commutes with `R`. The same is +true for each owned initialization and erasure, since `a` and `b` are public. +The checker requires one certificate for every affected block. It checks +the exact old event list and every rational matrix coefficient. It also +rejects extra certificates. Thus this is an identity for arbitrary inputs, +not a test on selected vectors. + +Each scalar block has one physical chart. The compiler moves each operand +to that chart before it is used. At every step, its physical value is the +declared native chart applied to its logical value. A scalar basis change +at a common chart therefore implements the same rational matrix `R`. +Native transport changes the chart and preserves the logical value. +The final basis removal restores the original logical interval. + +## 2. Fixed witnesses + +The four certificates are applied in the order in WITNESS.json. Block +indices refer to the complete word produced by the preceding step. + +| Public pair | Coefficient | Local paid delta | +| --- | ---: | --- | +| 438, 733 | -4 | `-H1-H2+H3` | +| 119, 125 | -1 | `-2H1+H2` | +| 125, 128 | -1 | `-2H1+H2` | +| 128, 139 | -1 | `-2H1+H2` | + +There are eight changed scalar blocks. Each certificate gives the full +before and after lists. The new contact graph permits four fewer local +native calls. The transport builder includes both meeting charts and all +remaining scalar contacts. It does not assign free movement to a basis +operation. All public paths remain nested. + +The separate endpoint checks cover 743 arbitrary public inputs and nine +owned register slots. There are eleven owned lifetimes and peak occupancy +two. Every owned instruction and transport stays in the same order. All +535 productive helper targets and all public boundary charts stay fixed. + +## 3. Native and caller binding + +The retained compiler lowers each chart change to a signed Gaussian-dyadic +recipe. A separate interpreter checks every signed Pauli image and the +global phase. It checks 2,918 distinct maps and 208 main endpoint adapters. +The helper normalizers retain the exact productive target profile. + +The p16/a7 caller is unchanged. Its physical binding checks all 7,488 +contacts and all 53,248 central-square columns. It has 18 full forward +calls, 15 thin query shears and 3,120 paid whole-idle jobs. The 3,328 main +targets and 9,630 helper targets give 12,958 productive fields. + +These exact finite identities use the retained factorwise tensor rule. +They do not add a new analytic or all-size admission assumption. The five +existing framework assumptions and helper endpoint contract remain. + +## 4. Complete cost + +For `H_r(t) = r^t` and `0 < t < 1`, the paid change per local call is + +```text +delta P = -7 H1 + 2 H2 + H3, +delta T = 0. +``` + +Strict concavity gives `1+2^t>3^t` and `2>2^t`. Thus the complete signed +moment increases by `18 * (7 - 2*2^t - 3^t) > 0` throughout that interval. +The new bill has 66,402 paid calls and rank surplus 760. The local paid rank +mass remains 5,986; the helper rank mass remains 4,266. Their difference is +the 1,664 main progress plus 56 owned descent debt. + +Two rational interval engines verify the full moment and put its unique +raw crossing in `(0.00310815850980, 0.00310815850981)`. The claim is +`0.00310815849`, and the tested saving is `0.003108158495`. + +All scalar changes are priced. The local scalar allowance is 220,290 and +the route allowance is 5,167,000. The retained complete raw ordinary bound +is 184,647,552, below its 1,000,000,000 budget. The power-1024 compiler, +cutoff 17, floor 18, tail parameter 1/5, reserve 10^-12 and decay 39/40 are +unchanged. All 54 strict and four functional outer conditions pass. + +## 5. Verification limits + +The full source archive is authenticated before any retained module is +loaded. The nested predecessor archive is authenticated again before its +local or native checker is loaded. The new checker verifies the source +word and every intermediate complete word. Its separate dense transpose +engine checks 565,504 entries. + +False basis signs, false block coefficients, a missing block certificate, +a missing native transport, a missing owned erasure, an unpaid query and +extra target credit are rejected. The inherited phase, caller and price +controls also run. + +The huge uniform word and rounded multiplier are algorithm-defined and +are not materialized. These are author checks, not independent scientific +acceptance or a proof-kernel theorem. The numerical improvement is small. +No large gain or global optimum is established. diff --git a/research/p104-paid-interior-bases/README.md b/research/p104-paid-interior-bases/README.md new file mode 100644 index 0000000000..4b3e17e186 --- /dev/null +++ b/research/p104-paid-interior-bases/README.md @@ -0,0 +1,81 @@ +# Paid interior bases for the P104 word + +Complete conditional kappa is **0.00310815849**, a gain of **0.00000139516** +(about **0.04491%**) over +[PR #5660](https://github.com/CrocSwap/integer-mult-bounds/pull/5660). +This is a small gain. A large improvement and a global optimum remain open. + +Four temporary changes of the public register basis remove paid contacts. +The basis changes occur at internal meeting charts. All transports to those +charts are included. The source and output interfaces stay fixed. +The complete local delta is `-7 H1 + 2 H2 + H3`. Across 18 full calls, this +removes 72 paid requests. The complete bill has **66,402 paid calls**, +**12,958 productive targets**, and rank surplus **760**. + +[PROOF.md](PROOF.md) states the identity and the complete cost. +[WITNESS.json](WITNESS.json) contains all eight scalar block certificates. +[RESULT.json](RESULT.json) is the full receipt. +[SOURCES.json](SOURCES.json) pins every consumed source. + +## Replay + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-paid-interior-bases +``` + +The hook runs normal and optimized checks. The expected final marker is: + +```text +PASS_P104_PAID_INTERIOR_BASES_KAPPA_00310815849 +``` + +The direct commands also work in a source export with no Git or network: + +```sh +python3.12 -I -B research/p104-paid-interior-bases/verify.py +python3.12 -I -O -B research/p104-paid-interior-bases/verify.py +``` + +The checks authenticate the 23-file PR5660 export and its 36-file predecessor +export before source imports. They check every exact block identity, all +565,504 transpose coefficients, 2,918 signed native maps, the physical caller, +both rational moment engines, all compiler costs, and all 58 outer conditions. +See [VALIDATION.md](VALIDATION.md) for the exact checks that ran. + +## Scope and limits + +The five inherited framework assumptions and the helper endpoint contract +remain. The huge uniform program and complete rounded multiplier are not +materialized. Author checks are not independent scientific acceptance. +The selected frontier is unchanged. + +The source is PR5660 at `3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa`. +The branch starts from canonical main `df0137efd35e11b4445734bf612bdd4c7ebc330c`, +priority revision 7. The complete source is retained, including all notices. + +## Open next questions + +1. Can an independent reviewer confirm the block identities and full bill? +2. Can a larger temporary basis or a different scalar schedule give a large + gain after all meeting transports and ordinary work are paid? +3. Can one of the inherited framework assumptions be resolved? + +The finite discovery searches do not prove a general obstruction. Further +work must check live Discussions and pin its complete input word. + +## Credit + +[PR #5660](https://github.com/CrocSwap/integer-mult-bounds/pull/5660) supplies +the complete input and the four-gate contact rewrite. It retains zxv's +[PR #5643](https://github.com/CrocSwap/integer-mult-bounds/pull/5643) A2 change, +the [PR #5644](https://github.com/CrocSwap/integer-mult-bounds/pull/5644) helper +relations, and the [PR #5650](https://github.com/CrocSwap/integer-mult-bounds/pull/5650) +composition. The source notices retain the P104, side-correction, helper, +native, caller, productive-recursion, interval and compiler authors. +The elementary change-of-basis identity is not claimed as a new theorem. + +The paid interior construction and this verification package are by +Ali Romman with substantial OpenAI Codex assistance. No subagents. +Apache-2.0. See [NOTICE](NOTICE) for the full retained attribution. diff --git a/research/p104-paid-interior-bases/RESULT.json b/research/p104-paid-interior-bases/RESULT.json new file mode 100644 index 0000000000..d5a73ee8ec --- /dev/null +++ b/research/p104-paid-interior-bases/RESULT.json @@ -0,0 +1,481 @@ +{ + "authenticated_nested_files": 36, + "authenticated_outer_files": 23, + "complete_cost": { + "compiler": { + "H": 80511200000000000, + "N": "2^80511200000000000", + "eta": { + "lower": "0.000000131687557081252595606387", + "upper": "0.000000131687557081252595606388" + }, + "gap": "1/1400000000000", + "integer_test_exponent": 57508, + "logarithm_power": 1024, + "theta": "63/64", + "uniform_saving": "1087855473/350000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "34879/25000000000", + "kappa": "310815849/100000000000", + "kappa_decimal": ".00310815849", + "margin_at_previous": { + "lower": "0.338879531362370820661965404439", + "upper": "0.338879531362370820661965404440" + }, + "negative_controls": { + "old_BIT": "Rejected by outer inequalities", + "old_cutoff": "Rejected by completion-tail ratio greater than one" + }, + "nonrecursive": { + "fixed_scalar_growth_bound": "At most 2^(16*26000) before native factors; a declared constant, not an attained norm.", + "local_paid_rank_mass": 5986, + "local_routes": 5167000, + "local_scalar": 220290, + "peak_owned_fields": 2, + "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": "348599999999253/350000000000000", + "fixed_halo_explicit_metadata_branch": "26950000000001/350000000000", + "new_BIT_row_stock_sublinear_in_active_group": "1395799999997009/1400000000000000", + "new_semantic_group_guard": "3/1400000000000" + }, + "margins": { + "boundary_algebraic_matrix": "6091990645995648578111/1960000000000000000000000", + "fused_gaussian": "6091990645986945734333/1960000000000000000000000", + "global_coordinate_router": "435142189/140000000000", + "group_bit_router": "609199064738694573433/196000000000000000000000", + "group_scans": "699999999999/700000000000", + "main_transform": "6091990644595648578111/1960000000000000000000000", + "microbox_face_corrections": "26950000000001/350000000000", + "polynomial_products": "1399999999999/1400000000000", + "sparse_union_movement": "802341990645995648578111/1960000000000000000000000" + }, + "parameters": { + "a": "435142189/140000000000", + "b": "4351421891/1400000000000", + "beta": "1399999999997/1400000000000", + "bit_saving": "17/5000", + "cap_xi": "1782341990644595648578111/1960000000000000000000000", + "complex_uniform_saving": "1087855473/350000000000", + "d": "1/1400000000000", + "epsilon": "1399999999999/1400000000000", + "kappa": "310815849/100000000000", + "lambda_": "398756736603/400000000000", + "lambda_prime": "1395648578111/1400000000000", + "layout": "1/1400000000000", + "q": "4351421889/1400000000000", + "r0": "1/14000000000000", + "stop": "1/1400000000000", + "tested_saving": "621631699/200000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "40857811/140000000000", + "actual_logarithmic_gamma_guard": "1/1400000000000", + "actual_logarithmic_group_guard": "177658009357504351421889/980000000000000000000000", + "alpha_logarithm_absorption": "1/14000000000000", + "boundary_algebraic_matrix_above_kappa": "5595648578111/1960000000000000000000000", + "cap_above_band": "802341990644595648578111/1960000000000000000000000", + "cap_below_cell": "177658009354004351421889/1960000000000000000000000", + "cap_below_phase_cell_power": "2137658009355404351421889/1960000000000000000000000", + "complex_above_effective": "1/1400000000000", + "complex_below_one_over_32": "39398578109/1400000000000", + "complex_endpoint": "1/700000000000", + "epsilon_below_one": "1/1400000000000", + "epsilon_positive": "1399999999999/1400000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "5586945734333/1960000000000000000000000", + "gaussian_above_main": "695648578111/980000000000000000000000", + "global_coordinate_router_above_kappa": "1/350000000000", + "global_gamma_power_slack": "9/14000000000000", + "group_below_dimension": "1/700000000000", + "group_bit_router_above_kappa": "698694573433/196000000000000000000000", + "group_gauge_power_slack": "177658009357434351421889/980000000000000000000000", + "group_key_fits_record": "1/700000000000", + "group_positive": "1399999999997/1400000000000", + "group_scans_above_kappa": "21807009033/21875000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "688594035400418148631/500000000000000000000000", + "lambda_above_internal": "1/2800000000000", + "lambda_above_sigma": "3/2800000000000", + "lambda_above_tau": "1/2800000000000", + "lambda_prime_above_lambda": "1/2800000000000", + "lambda_prime_above_leaf": "2795648578109/1960000000000000000000000", + "leaf_saving_above_effective": "1395648578109/1960000000000000000000000", + "main_transform_above_kappa": "4195648578111/1960000000000000000000000", + "membership_arithmetic_fits_record": "1/1400000000000", + "microbox_face_corrections_above_kappa": "53897824289059/700000000000", + "microbox_halo_volume": "110600000000003/1400000000000", + "new_complex_uniform_saving_above_b": "1/1400000000000", + "new_semantic_guard_with_C1_one": "1/1400000000000", + "polynomial_products_above_kappa": "1395648578113/1400000000000", + "positive_layout_slack": "1/1400000000000", + "q_below_effective": "1/1400000000000", + "q_below_internal": "1/1400000000000", + "q_below_leaf": "2795648578109/1960000000000000000000000", + "q_positive": "4351421889/1400000000000", + "short_record_fallback": "1395648578109/1400000000000", + "source_axis_superpolynomial": "1/1400000000000", + "sparse_union_movement_above_kappa": "796250000005595648578111/1960000000000000000000000", + "stop_below_one": "1399999999999/1400000000000", + "stop_positive": "1/1400000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/1400000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/1400000000000", + "union_tag_work_per_visit_fits_record": "3/1400000000000" + } + }, + "paid": { + "1": 40944, + "16": 416, + "2": 8280, + "24": 416, + "3": 8892, + "32": 416, + "4": 1638, + "40": 416, + "48": 416, + "5": 2862, + "56": 416, + "6": 396, + "64": 416, + "7": 270, + "72": 208 + }, + "paid_calls": 66402, + "previous_open_pr5660": "310676333/100000000000", + "productive_fields": 12958, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_ceiling": { + "derivative_upper": "-739773215192878821828754385468986974565929261970286747281917233/3138550867693340381917894711603833208051177722232017256448", + "interval": [ + "0", + "17/5000" + ] + }, + "raw_headroom": [ + "99/5000000000000", + "1981/100000000000000" + ], + "raw_root_interval": [ + "15540792549/5000000000000", + "310815850981/100000000000000" + ], + "relative_gain_percent": "13951600/310676333", + "strictification": { + "alpha": { + "lower": "0.999999999984953241363199004691", + "upper": "0.999999999984953241363199004692" + }, + "cutoff": 17, + "delta": { + "lower": "0.967532018342092943007295114144", + "upper": "0.967532018342092943007295114145" + }, + "floor": 18, + "gamma": { + "lower": "0.968220587948865237654067176469", + "upper": "0.968220587948865237654067176470" + }, + "normalized_paid_upper": "1048576000976562501/1048576001073741824", + "power": 1024, + "reserve": "1/1000000000000", + "tail_block": 128, + "tail_decay": "39/40", + "tail_offset": "1/5", + "tested": "621631699/200000000000" + }, + "targets": { + "1": 36, + "145": 208, + "17": 416, + "2": 72, + "25": 416, + "33": 416, + "4": 1638, + "41": 416, + "49": 416, + "5": 108, + "57": 416, + "65": 416, + "7": 90, + "73": 208, + "8": 288, + "9": 7398 + }, + "whole_idle_jobs": 3120 + }, + "limits": [ + "The five inherited assumptions and helper endpoint contract remain.", + "The huge uniform word and complete rounded multiplier are not materialized.", + "Author checks do not establish independent scientific acceptance.", + "This gain is small. The requested large gain and a global optimum remain unproved." + ], + "local": { + "endpoint_coefficients": 565504, + "helpers": { + "1": 2, + "2": 4, + "4": 91, + "5": 6, + "7": 5, + "8": 16, + "9": 411 + }, + "owned_fields": 9, + "owned_lifetimes": 11, + "paid": { + "1": 2188, + "2": 460, + "3": 494, + "4": 91, + "5": 159, + "6": 22, + "7": 15 + }, + "paid_rank_mass": 5986, + "peak_owned_fields": 2, + "public_inputs": 743, + "real_scalar_allowance": 220290 + }, + "local_helper_delta": {}, + "local_paid_delta": { + "1": -7, + "2": 2, + "3": 1 + }, + "native": { + "distinct_maps": 2918, + "helper_normalizers": 1070, + "helpers": { + "1": 2, + "2": 4, + "4": 91, + "5": 6, + "7": 5, + "8": 16, + "9": 411 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "b49a78ea62c2a3bae7f5d2d0ae02900ce52bb17870d488d7959dcc4b4f867915", + "wrong_phase_rejected": true + }, + "negative_controls": { + "extra_target": "Every productive helper has a native target", + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "missing_conjugated_block": "Every affected block has a certificate", + "missing_native_transport": "Scalar destination and coefficient", + "missing_owned_erasure": "All public and owned exits", + "unpaid_query": "Complete field and call counts", + "wrong_basis_sign": "Exact conjugation of the complete scalar block", + "wrong_scalar_block": "Exact conjugation of the complete scalar block" + }, + "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": 565504, + "columns": 752 + }, + "source_commit": "3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa", + "source_local": { + "endpoint_coefficients": 565504, + "helpers": { + "1": 2, + "2": 4, + "4": 91, + "5": 6, + "7": 5, + "8": 16, + "9": 411 + }, + "owned_fields": 9, + "owned_lifetimes": 11, + "paid": { + "1": 2195, + "2": 458, + "3": 493, + "4": 91, + "5": 159, + "6": 22, + "7": 15 + }, + "paid_rank_mass": 5986, + "peak_owned_fields": 2, + "public_inputs": 743, + "real_scalar_allowance": 220220 + }, + "status": "PASS_P104_PAID_INTERIOR_BASES_KAPPA_00310815849", + "steps": [ + { + "endpoint_coefficients": 565504, + "helpers": { + "1": 2, + "2": 4, + "4": 91, + "5": 6, + "7": 5, + "8": 16, + "9": 411 + }, + "owned_fields": 9, + "owned_lifetimes": 11, + "paid": { + "1": 2194, + "2": 457, + "3": 494, + "4": 91, + "5": 159, + "6": 22, + "7": 15 + }, + "paid_rank_mass": 5986, + "peak_owned_fields": 2, + "public_inputs": 743, + "real_scalar_allowance": 220224 + }, + { + "endpoint_coefficients": 565504, + "helpers": { + "1": 2, + "2": 4, + "4": 91, + "5": 6, + "7": 5, + "8": 16, + "9": 411 + }, + "owned_fields": 9, + "owned_lifetimes": 11, + "paid": { + "1": 2192, + "2": 458, + "3": 494, + "4": 91, + "5": 159, + "6": 22, + "7": 15 + }, + "paid_rank_mass": 5986, + "peak_owned_fields": 2, + "public_inputs": 743, + "real_scalar_allowance": 220246 + }, + { + "endpoint_coefficients": 565504, + "helpers": { + "1": 2, + "2": 4, + "4": 91, + "5": 6, + "7": 5, + "8": 16, + "9": 411 + }, + "owned_fields": 9, + "owned_lifetimes": 11, + "paid": { + "1": 2190, + "2": 459, + "3": 494, + "4": 91, + "5": 159, + "6": 22, + "7": 15 + }, + "paid_rank_mass": 5986, + "peak_owned_fields": 2, + "public_inputs": 743, + "real_scalar_allowance": 220268 + }, + { + "endpoint_coefficients": 565504, + "helpers": { + "1": 2, + "2": 4, + "4": 91, + "5": 6, + "7": 5, + "8": 16, + "9": 411 + }, + "owned_fields": 9, + "owned_lifetimes": 11, + "paid": { + "1": 2188, + "2": 460, + "3": 494, + "4": 91, + "5": 159, + "6": 22, + "7": 15 + }, + "paid_rank_mass": 5986, + "peak_owned_fields": 2, + "public_inputs": 743, + "real_scalar_allowance": 220290 + } + ] +} diff --git a/research/p104-paid-interior-bases/SOURCES.json b/research/p104-paid-interior-bases/SOURCES.json new file mode 100644 index 0000000000..5c13f25a07 --- /dev/null +++ b/research/p104-paid-interior-bases/SOURCES.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/p104-paid-interior-bases/inputs/pr5660-source.tar", + "usage": "input", + "pin": "head:89c7e069d6b93b7802f946d01886d92970303f86:research/p104-paid-interior-bases/inputs/pr5660-source.tar", + "git_blob": "5b84cf23231082376660b7295744b64655039d8c", + "sha256": "397b1f99061f670ed904198d0458808769c0a8693394bee0d9648f1f280d88d3" + } + ], + "source_export": { + "commit": "3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa", + "files": 23, + "git_blob": "5b84cf23231082376660b7295744b64655039d8c", + "sha256": "397b1f99061f670ed904198d0458808769c0a8693394bee0d9648f1f280d88d3", + "local_path": "inputs/pr5660-source.tar", + "package": "research/p104-contact-rewrite", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5660" + }, + "predecessors": { + "PR5627": "ed4dc88a09a7d201971f6603b8c2074e95dd9c32", + "PR5643": "a3ff5c628bfc8825553d62d913f3e91f75d6825f", + "PR5644": "c5871955d89bf73506fd68b0a5bf1cf2b3153c02", + "PR5650": "7916490124ac946704339a6a332bb76f06e5db5c", + "PR5651": "853192167b27d44aea0d4bc2b0d52d695fadc7c6", + "PR5660": "3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa" + }, + "attribution": "PR5660 supplies the complete input word and retains the P104, helper, scalar, native, caller and compiler source chain. Four paid interior basis changes and their exact certificates are new work by Ali Romman with substantial OpenAI Codex assistance. No subagents." +} diff --git a/research/p104-paid-interior-bases/TASK.json b/research/p104-paid-interior-bases/TASK.json new file mode 100644 index 0000000000..65842d6cff --- /dev/null +++ b/research/p104-paid-interior-bases/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Four temporary public basis changes at paid internal meeting charts improve the complete conditional kappa to .00310815849.", + "scope_change_reason": "Helper-only global bases and clean workspace tests gave no gain. Paid internal meeting points permit main/helper basis changes with an exact lower complete bill.", + "bottleneck_link": "The changed internal scalar graph changes the invoice. The inherited packing ceiling does not price this complete productive caller; its replacement bound is the exact complete signed moment.", + "budget_minutes": 240, + "stop_rule": "Verify and publish the fixed improved construction. Further searches must check live claims and a full new bill. Do not infer a large gain or global optimum.", + "outcome": "completed", + "evidence": "PROOF.md, WITNESS.json, RESULT.json and VALIDATION.md", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for algebra, exact scripts, source checks and writing. No subagents.", + "open_questions": [ + { + "question": "Can a reviewer verify the basis identity, native paths and complete price?", + "why_it_matters": "Author checks do not establish independent acceptance.", + "first_step": "Replay the exact publication commit and check the eight scalar block identities.", + "blocked_by": "No known technical blocker; independent review remains." + }, + { + "question": "Can a larger temporary basis or a different scalar schedule give a large gain?", + "why_it_matters": "The present complete gain is small.", + "first_step": "Check live claims and test a changed basis with every meeting transport and scalar operation charged.", + "blocked_by": "No positive large construction is known." + }, + { + "question": "Can the inherited framework assumptions be resolved?", + "why_it_matters": "The complete kappa remains conditional.", + "first_step": "Use the selected record to choose one named assumption and its proof review.", + "blocked_by": "The complete rounded multiplier and huge uniform word are not materialized." + } + ] +} diff --git a/research/p104-paid-interior-bases/VALIDATION.md b/research/p104-paid-interior-bases/VALIDATION.md new file mode 100644 index 0000000000..11b30c4ba1 --- /dev/null +++ b/research/p104-paid-interior-bases/VALIDATION.md @@ -0,0 +1,47 @@ +# Validation record + +The scientific package at `b90438ec9d51e7babc0b6b6cb9998a9df81c123d` passes +the following author checks with Python 3.12 and the standard library. + +```sh +python3.12 -B scripts/research_package.py --package research/p104-paid-interior-bases +python3.12 -B scripts/check_research_commit.py --package research/p104-paid-interior-bases +python3.12 -B scripts/export_research_package.py export --package research/p104-paid-interior-bases --ref HEAD --output /tmp/p104-interior-science.tar +python3.12 -B scripts/export_research_package.py check /tmp/p104-interior-science.tar +``` + +The registered hook runs both `-I -B` and `-I -O -B`. Both runs give +`PASS_P104_PAID_INTERIOR_BASES_KAPPA_00310815849`, followed by +`PASS_REGISTERED_RESEARCH_PACKAGE`. They check the source exports, the four +construction steps, all 565,504 transpose entries, 2,918 signed native maps, +the complete physical caller, both rational price engines, all compiler +terms, all 58 outer conditions, and the invalid-word controls in RESULT.json. + +All 16 package files match the scientific commit. The official export passes +its integrity check. Its 17 files include the export manifest. An isolated +optimized replay of this export passes in 89.70 seconds with an empty PATH, +no Git checkout, no network request, and read-only source files. Every file +hash and mode stays fixed. + +Separate temporary copies test archive-byte corruption, payload corruption +with a new outer digest, and a missing payload. Each case is tested on both +the outer export and the nested predecessor export, with and without `-O`. +All 12 cases reject before any retained research module is imported. These +are source-integrity tests; they do not replace the scientific replay. + +The complete conditional claim is `0.00310815849`. The tested saving is +`0.003108158495`, and the exact raw crossing is +`(0.00310815850980, 0.00310815850981)`. The source and final bills are checked +separately. Their difference is `18*(-7 H1 + 2 H2 + H3)` in paid requests, +with no change in productive targets. + +The branch starts from canonical main +`df0137efd35e11b4445734bf612bdd4c7ebc330c`. The source archive is retained in +its direct child `89c7e069d6b93b7802f946d01886d92970303f86`. Full-history +ancestry mode was not run because this checkout is shallow. + +Hosted CI and independent scientific review are separate statuses. The five +inherited assumptions and helper endpoint contract remain. The huge uniform +word and complete rounded multiplier are not materialized. The selected +frontier is unchanged. The numerical gain is small; no large improvement or +global optimum is claimed. diff --git a/research/p104-paid-interior-bases/VERIFY.json b/research/p104-paid-interior-bases/VERIFY.json new file mode 100644 index 0000000000..d1d1093b24 --- /dev/null +++ b/research/p104-paid-interior-bases/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-paid-interior-bases/inputs/pr5660-source.tar" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Both source exports, all four basis changes, every scalar row and transpose coefficient, native phases, the whole caller, two exact prices and controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Repeat the complete verification with assertions disabled." + } + ] +} diff --git a/research/p104-paid-interior-bases/WITNESS.json b/research/p104-paid-interior-bases/WITNESS.json new file mode 100644 index 0000000000..d3554cd80f --- /dev/null +++ b/research/p104-paid-interior-bases/WITNESS.json @@ -0,0 +1,501 @@ +[ + { + "a": 438, + "b": 733, + "coefficient": "-4", + "start_block": 1090, + "end_block": 1314, + "entry_frame": 794, + "exit_frame": 127, + "blocks": [ + { + "index": 1090, + "before": [ + [ + "ADD", + 140, + 733, + "2", + 794 + ], + [ + "ADD", + 140, + 438, + "-1/2", + 794 + ] + ], + "after": [ + [ + "ADD", + 140, + 438, + "-1/2", + 794 + ] + ] + }, + { + "index": 1313, + "before": [ + [ + "ADD", + 160, + 451, + "-1/2", + 911 + ], + [ + "ADD", + 144, + 733, + "2", + 911 + ], + [ + "ADD", + 144, + 438, + "-1/2", + 911 + ] + ], + "after": [ + [ + "ADD", + 160, + 451, + "-1/2", + 911 + ], + [ + "ADD", + 144, + 438, + "-1/2", + 911 + ] + ] + } + ] + }, + { + "a": 119, + "b": 125, + "coefficient": "-1", + "start_block": 703, + "end_block": 705, + "entry_frame": 3, + "exit_frame": 602, + "blocks": [ + { + "index": 703, + "before": [ + [ + "ADD", + 119, + 706, + "2", + 594 + ], + [ + "ADD", + 125, + 706, + "2", + 594 + ], + [ + "ADD", + 128, + 706, + "2", + 594 + ], + [ + "ADD", + 139, + 706, + "2", + 594 + ], + [ + "ADD", + 213, + 706, + "2", + 594 + ] + ], + "after": [ + [ + "ADD", + 213, + 706, + "2", + 594 + ], + [ + "ADD", + 139, + 706, + "2", + 594 + ], + [ + "ADD", + 128, + 706, + "2", + 594 + ], + [ + "ADD", + 125, + 706, + "2", + 594 + ] + ] + }, + { + "index": 704, + "before": [ + [ + "ADD", + 119, + 708, + "-2", + 602 + ], + [ + "ADD", + 125, + 708, + "2", + 602 + ], + [ + "ADD", + 127, + 708, + "2", + 602 + ], + [ + "ADD", + 128, + 708, + "-2", + 602 + ], + [ + "ADD", + 139, + 708, + "2", + 602 + ], + [ + "ADD", + 154, + 708, + "-2", + 602 + ] + ], + "after": [ + [ + "ADD", + 119, + 125, + "1", + 602 + ], + [ + "ADD", + 119, + 708, + "-2", + 602 + ], + [ + "ADD", + 125, + 708, + "2", + 602 + ], + [ + "ADD", + 127, + 708, + "2", + 602 + ], + [ + "ADD", + 128, + 708, + "-2", + 602 + ], + [ + "ADD", + 139, + 708, + "2", + 602 + ], + [ + "ADD", + 154, + 708, + "-2", + 602 + ], + [ + "ADD", + 119, + 125, + "-1", + 602 + ] + ] + } + ] + }, + { + "a": 125, + "b": 128, + "coefficient": "-1", + "start_block": 703, + "end_block": 705, + "entry_frame": 3, + "exit_frame": 602, + "blocks": [ + { + "index": 703, + "before": [ + [ + "ADD", + 119, + 125, + "-1", + 3 + ] + ], + "after": [ + [ + "ADD", + 125, + 128, + "1", + 3 + ], + [ + "ADD", + 119, + 125, + "-1", + 3 + ], + [ + "ADD", + 125, + 128, + "-1", + 3 + ] + ] + }, + { + "index": 704, + "before": [ + [ + "ADD", + 213, + 706, + "2", + 594 + ], + [ + "ADD", + 139, + 706, + "2", + 594 + ], + [ + "ADD", + 128, + 706, + "2", + 594 + ], + [ + "ADD", + 125, + 706, + "2", + 594 + ] + ], + "after": [ + [ + "ADD", + 213, + 706, + "2", + 594 + ], + [ + "ADD", + 139, + 706, + "2", + 594 + ], + [ + "ADD", + 128, + 706, + "2", + 594 + ] + ] + } + ] + }, + { + "a": 128, + "b": 139, + "coefficient": "-1", + "start_block": 703, + "end_block": 705, + "entry_frame": 3, + "exit_frame": 602, + "blocks": [ + { + "index": 703, + "before": [ + [ + "ADD", + 125, + 128, + "-1", + 3 + ], + [ + "ADD", + 125, + 128, + "1", + 3 + ], + [ + "ADD", + 119, + 125, + "-1", + 3 + ], + [ + "ADD", + 125, + 128, + "-1", + 3 + ] + ], + "after": [ + [ + "ADD", + 128, + 139, + "1", + 3 + ], + [ + "ADD", + 125, + 128, + "-1", + 3 + ], + [ + "ADD", + 125, + 128, + "1", + 3 + ], + [ + "ADD", + 119, + 125, + "-1", + 3 + ], + [ + "ADD", + 125, + 128, + "-1", + 3 + ], + [ + "ADD", + 128, + 139, + "-1", + 3 + ] + ] + }, + { + "index": 704, + "before": [ + [ + "ADD", + 213, + 706, + "2", + 594 + ], + [ + "ADD", + 139, + 706, + "2", + 594 + ], + [ + "ADD", + 128, + 706, + "2", + 594 + ] + ], + "after": [ + [ + "ADD", + 213, + 706, + "2", + 594 + ], + [ + "ADD", + 139, + 706, + "2", + 594 + ] + ] + } + ] + } +] diff --git a/research/p104-paid-interior-bases/WORD.json.gz b/research/p104-paid-interior-bases/WORD.json.gz new file mode 100644 index 0000000000..8be2b3e1c2 Binary files /dev/null and b/research/p104-paid-interior-bases/WORD.json.gz differ diff --git a/research/p104-paid-interior-bases/construct.py b/research/p104-paid-interior-bases/construct.py new file mode 100644 index 0000000000..ff4d7701fc --- /dev/null +++ b/research/p104-paid-interior-bases/construct.py @@ -0,0 +1,147 @@ +"""Apply four checked changes of the public register basis. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from copy import deepcopy +from fractions import Fraction as Q +from sources import need + + +def blocks(word): + result, block, frame = [], [], None + for event in word['program']: + if event[0] == 'MOVE': + continue + if event[0] in ('INIT', 'CLEAR'): + if block: + result.append(block) + result.append([event]) + block, frame = [], None + elif frame != event[-1]: + if block: + result.append(block) + block, frame = [event], event[-1] + else: + block.append(event) + if block: + result.append(block) + return result + + +def add(dst, src, coefficient): + for column, value in tuple(src.items()): + value = dst.get(column, Q(0)) + coefficient * value + if value: + dst[column] = value + else: + dst.pop(column, None) + + +def matrix(events, roles, frame): + rows = {r: {r: Q(1)} for r in roles} + for event in events: + op, r = event[:2] + need(op in ('ADD', 'SCALE') and event[-1] == frame, + 'One ordinary scalar block at one chart') + coefficient = Q(event[-2]) + need(r in roles and coefficient != 0, 'Declared scalar destination') + if op == 'SCALE': + rows[r] = {j: coefficient * value for j, value in rows[r].items()} + else: + need(event[2] in roles and event[2] != r, 'Declared scalar source') + add(rows[r], rows[event[2]], coefficient) + return rows + + +def protected(word): + n = word['public'] + return [e for e in word['program'] if e[1] >= n + or (e[0] in ('ADD', 'COPY') and e[2] >= n)] + + +def rebuild(word, scalar): + result = deepcopy(word) + frames = word['initial'][:] + [None] * word['owned_fields'] + program = [] + + def move(r, frame): + if frames[r] != frame: + need(frames[r] is not None, 'Live transport source') + program.append(['MOVE', r, frames[r], frame, r >= word['public']]) + frames[r] = frame + + for event in scalar: + op, r = event[:2] + if op == 'INIT': + need(frames[r] is None, 'Unused owned field') + frames[r] = event[2] + elif op == 'CLEAR': + move(r, event[2]) + frames[r] = None + else: + move(r, event[-1]) + if op in ('ADD', 'COPY'): + move(event[2], event[-1]) + program.append(event[:]) + for r in range(word['public']): + move(r, word['final'][r]) + result['program'] = program + return result + + +def step(word, witness, local): + source = blocks(word) + a, b, q = witness['a'], witness['b'], Q(witness['coefficient']) + start, end = witness['start_block'], witness['end_block'] + entry, exit_frame = witness['entry_frame'], witness['exit_frame'] + need(0 <= a < word['public'] and 0 <= b < word['public'] and a != b, + 'Two distinct public fields') + need(q and q.denominator & (q.denominator - 1) == 0, 'Nonzero dyadic basis') + need(0 < start < end < len(source), 'Internal interval of scalar blocks') + need(0 <= entry < len(word['frames']) and 0 <= exit_frame < len(word['frames']), + 'Declared basis charts') + replacements = {row['index']: row for row in witness['blocks']} + need(len(replacements) == len(witness['blocks']), 'Distinct replacement blocks') + expected = set() + scalar = [] + for index, block in enumerate(source): + if index == start: + scalar.append(['ADD', a, b, str(q), entry]) + roles = {e[1] for e in block} | { + e[2] for e in block if e[0] in ('ADD', 'COPY')} + if start <= index < end and roles & {a, b}: + expected.add(index) + need(index in replacements, 'Every affected block has a certificate') + row = replacements[index] + need(block == row['before'], 'Exact preceding scalar block') + frame = block[0][-1] + roles |= {a, b} + roles |= {e[1] for e in row['after']} | { + e[2] for e in row['after'] if e[0] == 'ADD'} + original = matrix(block, roles, frame) + # R = I + q E_ab. The two operations form R M R^-1. + add(original[a], original[b], q) + for vector in original.values(): + add(vector, {b: Q(1)}, -q * vector.get(a, 0)) + need(matrix(row['after'], roles, frame) == original, + 'Exact conjugation of the complete scalar block') + scalar.extend(row['after']) + else: + scalar.extend(block) + if index + 1 == end: + scalar.append(['ADD', a, b, str(-q), exit_frame]) + need(set(replacements) == expected, 'No extra replacement certificate') + result = rebuild(word, scalar) + need(protected(result) == protected(word), 'Every owned instruction and transport stays fixed') + need(result['initial'] == word['initial'] and result['final'] == word['final'], + 'All public boundaries stay fixed') + return result, local.replay(result) + + +def construct(source, witnesses, local): + word, receipts = source, [] + for witness in witnesses: + word, receipt = step(word, witness, local) + receipts.append(receipt) + word['schema'] = 'p104-paid-interior-bases/1' + return word, receipts diff --git a/research/p104-paid-interior-bases/inputs/pr5660-source.tar b/research/p104-paid-interior-bases/inputs/pr5660-source.tar new file mode 100644 index 0000000000..5b84cf2323 Binary files /dev/null and b/research/p104-paid-interior-bases/inputs/pr5660-source.tar differ diff --git a/research/p104-paid-interior-bases/pricing.py b/research/p104-paid-interior-bases/pricing.py new file mode 100644 index 0000000000..83e015643b --- /dev/null +++ b/research/p104-paid-interior-bases/pricing.py @@ -0,0 +1,177 @@ +"""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. +Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +import local as L + +KAPPA, TESTED = Q('.00310815849'), Q('.003108158495') +PREVIOUS = Q('.00310676333') + + +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()) == 12958 and sum(paid.values()) == 66402, '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,5),1024,17,18 + target,paid = E.moment(T,t),E.moment(P,t) + tl,th = other.moment(T,TESTED) + pl,ph = other.moment(P,TESTED) + L.need(tl > ph and max(tl,target[0]) <= min(th,target[1]) and max(pl,paid[0]) <= min(ph,paid[1]), 'Two exact moment engines') + alpha = E.divide(paid,target) + gamma = E.divide(E.moment(P,t+u),E.mul(E.power(c,u),target)) + delta = E.divide((Q(sum(T.values())*b),)*2,E.mul(E.power(c,TESTED),target)) + reserve,decay = Q(1,10**12),Q(39,40) + 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') + 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':'.00310815849','previous_open_pr5660':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':{'old_cutoff':'Rejected by completion-tail ratio greater than one','old_BIT':'Rejected by outer inequalities'}}) diff --git a/research/p104-paid-interior-bases/sources.py b/research/p104-paid-interior-bases/sources.py new file mode 100644 index 0000000000..108e075404 --- /dev/null +++ b/research/p104-paid-interior-bases/sources.py @@ -0,0 +1,61 @@ +"""Authenticate the retained PR5660 export before any source import. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The archive checks follow the repository exporter and flyingviper's PR5613. +""" +from contextlib import contextmanager +from hashlib import sha1, sha256 +from pathlib import Path, PurePosixPath +import importlib.util +import io +import json +import sys +import tarfile +import tempfile + +HERE = Path(__file__).resolve().parent + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +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 + + +@contextmanager +def sources(): + pin = json.loads((HERE/'SOURCES.json').read_bytes())['source_export'] + raw = (HERE/pin['local_path']).read_bytes() + need(sha256(raw).hexdigest() == pin['sha256'], 'Exact predecessor archive SHA256') + need(sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == pin['git_blob'], + 'Exact retained archive Git blob') + with tempfile.TemporaryDirectory(prefix='p104-interior-source-') as directory: + root, names = Path(directory), set() + with tarfile.open(fileobj=io.BytesIO(raw), mode='r:') as bundle: + for member in bundle.getmembers(): + path = PurePosixPath(member.name) + need(member.isfile() and not path.is_absolute() and '..' not in path.parts + and '\\' not in member.name and ':' not in member.name, + 'Regular relative source path') + need(member.name not in names, 'Unique source path') + names.add(member.name) + target = root.joinpath(*path.parts) + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(bundle.extractfile(member).read()) + manifest = json.loads((root/'.research-export.json').read_bytes()) + need(manifest['commit'] == pin['commit'] and manifest['package'] == pin['package'] + and len(manifest['files']) == pin['files'], 'Exact source commit and inventory') + need(names == {'.research-export.json'} | {r['path'] for r in manifest['files']}, + 'No missing or additional source payload') + for row in manifest['files']: + payload = (root/row['path']).read_bytes() + need(len(payload) == row['size'] and sha256(payload).hexdigest() == row['sha256'], + 'Authenticated payload: '+row['path']) + yield root/pin['package'], root diff --git a/research/p104-paid-interior-bases/verify.py b/research/p104-paid-interior-bases/verify.py new file mode 100644 index 0000000000..47d103c523 --- /dev/null +++ b/research/p104-paid-interior-bases/verify.py @@ -0,0 +1,131 @@ +"""Check the basis certificates and the complete conditional price. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from copy import deepcopy +import gzip +import json +from pathlib import Path +import sys +import tempfile + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from sources import sources, load, need +import construct + + +def rejected(action): + try: + action() + except ValueError as error: + return str(error) + raise ValueError('An invalid certificate was accepted') + + +def difference(after, before): + result = Counter(after) + result.subtract(before) + return {r: count for r, count in result.items() if count} + + +def run(): + witnesses = json.loads((HERE / 'WITNESS.json').read_bytes()) + need(len(witnesses) == 4, 'Four fixed basis changes') + with sources() as (parent, outer_root): + retained = load(parent / 'sources.py', 'interior_retained_sources') + with retained.sources() as (base, root): + L = load(base / 'local.py', 'local') + source = L.read(parent / 'WORD.json.gz') + old = L.replay(source) + word, steps = construct.construct(source, witnesses, L) + local = L.replay(word) + expected = [{1: -1, 2: -1, 3: 1}] + [{1: -2, 2: 1}] * 3 + previous = old + for receipt, delta in zip(steps, expected): + need(difference(receipt['paid'], previous['paid']) == delta, + 'Exact paid delta at each basis change') + need(receipt['helpers'] == old['helpers'], 'All productive targets retained') + previous = receipt + need(difference(local['paid'], old['paid']) == {1: -7, 2: 2, 3: 1}, + 'Complete local paid delta') + need((local['public_inputs'], local['owned_fields'], local['owned_lifetimes'], + local['peak_owned_fields']) == (743, 9, 11, 2), 'Public and owned inventories') + columns = L.reverse_columns(word) + print('PASS four basis changes, eight scalar blocks and all 565504 endpoint entries', flush=True) + native = L.native(word) + C = load(root / 'research/p104-productive-controller/caller.py', 'interior_caller') + caller = C.construct() + need(caller == L.read(root / 'research/p104-productive-controller/CONTROLLER.json'), + 'Same complete caller') + physical = C.physical(caller, word) + print('PASS all signed native maps and the complete physical caller', flush=True) + price_source = (parent / 'pricing.py').read_text() + for before, after in L.read(HERE / 'PRICING-EDITS.json'): + need(price_source.count(before) == 1, 'One declared price edit') + price_source = price_source.replace(before, after) + need(price_source == (HERE / 'pricing.py').read_text(), 'Only declared price edits') + P = load(HERE / 'pricing.py', 'interior_price') + price = P.run(local, native, caller, physical) + controls = C.controls(caller) + bad = deepcopy(witnesses[0]) + bad['coefficient'] = str(-L.Q(bad['coefficient'])) + controls['wrong_basis_sign'] = rejected(lambda: construct.step(source, bad, L)) + bad = deepcopy(witnesses[0]) + bad['blocks'][0]['after'][0][-2] = '17' + controls['wrong_scalar_block'] = rejected(lambda: construct.step(source, bad, L)) + bad = deepcopy(witnesses[0]) + bad['blocks'].pop() + controls['missing_conjugated_block'] = rejected(lambda: construct.step(source, bad, L)) + bad = deepcopy(word) + bad['program'].remove(next(e for e in bad['program'] if e[0] == 'MOVE')) + controls['missing_native_transport'] = rejected(lambda: L.replay(bad)) + bad = deepcopy(word) + bad['program'].pop(max(i for i, e in enumerate(bad['program']) if e[0] == 'CLEAR')) + controls['missing_owned_erasure'] = rejected(lambda: L.replay(bad)) + bad = deepcopy(local) + bad['paid'][1] -= 1 + controls['unpaid_query'] = rejected(lambda: P.assemble(bad, native, caller, physical)) + bad = deepcopy(local) + bad['helpers'][1] += 1 + controls['extra_target'] = rejected(lambda: P.assemble(bad, native, caller, physical)) + result = dict( + status='PASS_P104_PAID_INTERIOR_BASES_KAPPA_00310815849', + source_commit='3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa', + authenticated_outer_files=23, authenticated_nested_files=36, + source_local=old, steps=steps, local=local, separate_columns=columns, + local_paid_delta={1: -7, 2: 2, 3: 1}, local_helper_delta={}, + native=native, physical_caller=physical, complete_cost=price, + negative_controls=controls, + limits=[ + 'The five inherited assumptions and helper endpoint contract remain.', + 'The huge uniform word and complete rounded multiplier are not materialized.', + 'Author checks do not establish independent scientific acceptance.', + 'This gain is small. The requested large gain and a global optimum remain unproved.']) + return P.encode(result), word + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + with tempfile.TemporaryDirectory(prefix='p104-interior-bytecode-') as cache: + sys.pycache_prefix = cache + result, word = run() + for name, value in (('RESULT.json', result), ('WORD.json.gz', word)): + path = HERE / name + payload = (json.dumps(value, sort_keys=True, indent=2) + '\n').encode() + if args.write: + path.write_bytes(gzip.compress(payload, mtime=0) if name.endswith('.gz') else payload) + else: + raw = path.read_bytes() + need(json.loads(gzip.decompress(raw) if name.endswith('.gz') else raw) == value, + 'Exact retained output: ' + name) + print(result['status']) + + +if __name__ == '__main__': + main()