diff --git a/research/p104-two-boundary-helper-split/NOTICE b/research/p104-two-boundary-helper-split/NOTICE new file mode 100644 index 0000000000..f83cecccf5 --- /dev/null +++ b/research/p104-two-boundary-helper-split/NOTICE @@ -0,0 +1,47 @@ +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. + +New work: distributed scalar updates on an unobserved public field interval, the exact witness and complete conditional price. Prepared for Ali Romman with substantial OpenAI Codex assistance. No subagents. Apache-2.0. The source archive retains all predecessor notices. + +Two-boundary main-assisted helper split and early cleanup: flyingviper with substantial +OpenAI Codex assistance, including independent AI review agents. Apache-2.0. diff --git a/research/p104-two-boundary-helper-split/PRICING-EDITS.json b/research/p104-two-boundary-helper-split/PRICING-EDITS.json new file mode 100644 index 0000000000..43c33c00cc --- /dev/null +++ b/research/p104-two-boundary-helper-split/PRICING-EDITS.json @@ -0,0 +1,22 @@ +[ + [ + "sum(targets.values()) == 12958 and sum(paid.values()) == 66348", + "sum(targets.values()) == 12976 and sum(paid.values()) == 66348" + ], + [ + "KAPPA, TESTED = Q('155457611/50000000000'), Q('124366089/40000000000')", + "KAPPA, TESTED = Q('31102457/10000000000'), Q('622049141/200000000000')" + ], + [ + "PREVIOUS = Q('.00310871312')", + "PREVIOUS = Q('.00310915222')" + ], + [ + "'kappa_decimal':'0.00310915222'", + "'kappa_decimal':'0.00311024570'" + ], + [ + "'previous_open_pr5660'", + "'previous_open_pr5713'" + ] +] diff --git a/research/p104-two-boundary-helper-split/PROOF.md b/research/p104-two-boundary-helper-split/PROOF.md new file mode 100644 index 0000000000..0eeb4ce7ec --- /dev/null +++ b/research/p104-two-boundary-helper-split/PROOF.md @@ -0,0 +1,134 @@ +# Two boundary functionals for helper708 + +## Source and scope + +This construction starts from PR5713 head +`a5348f7143f95fe0046b92b96172e30763c7d731`, package +`p104-temporal-updates`, canonical word SHA256 +`32adce6656e49aa020d3e6317f1c45c11fccadeeb67a8d506172d101703d2138`. +Its source lineage and authors remain credited. The new construction changes +scalar dependencies and adds one independent public helper while retaining +every paid MOVE. It retains nine owned labels, eleven lifetimes and peak two. +All owned identifiers increase by one to make room for the new public field743. + +The resulting word has744 independent public fields and nine dirty owned input +columns. Its canonical SHA256 is +`a1c8277189a811546bdc7b147d72e6a594504ff9585c9bf59a5681aa873abb01`. +The exact constructor and independent checks below are finite checks; the +publication verifier separately binds native maps, the complete caller, +ordinary allowances and the numerical pricing claim. + +## Initial basis and retirement + +Use the cut immediately after source event14330. Roles708 and154 share frame602, +of rank2. Let A be the scalar prefix, B its suffix, T=BA, e=e708, and define + +``` +a = e708^T A, c = e154^T A / 2, +h = a+c, d = B e708 = -2e126+2e188+e708, +k = h-e708^T. +``` + +Exact replay verifies that T has identity input columns and output rows for +helpers126,188,708. It also gives h708=d708=1, hd=1 and k708=kd=0. Every term of h has its +initial value at the empty frame. Its only main-input terms are +`(x154+x217)/4`. The covector c has zero coefficients on126,188,708. + +Apply the ordinary initial basis change + +``` +Q = (I+(d-e)e^T)(I-e k) = I+(d-e)e^T-d k. +``` + +The first factor is implemented after the second:87 initial ADDs +`708 -= k_r*r`, then `126 -=2*708` and `188 +=2*708`. All operands share the +empty frame, and the main fields are read but unchanged. The identities +`hQ=e^T`, `Qe=d` and `cQ=c` follow directly. + +At the cut, `708 +=154/2` restores exactly x708. Retire original708 at rank2. +A new independent helper starts in frame602 with arbitrary input z and replaces +every subsequent occurrence of original708. No subtraction of154/2 is applied +to this new helper, and no MOVE is inserted or removed. + +## Output normalization at an existing meeting + +Before retirement the transformed continuation value was `aQ=e^T-c`. Replacing +it by z injects `d*(z-e^T+c)` into the suffix. Combining this with TQ gives the +following three dirty full-frame values, with every other endpoint unchanged: + +``` +126 = x126 - 2*t, +188 = x188 + 2*t, +new = t = z-k+c. +``` + +The output nuisance is `g=k-c=a-e708^T`. It differs from the input nuisance k. +An independent backwards calculation expresses g using118 full-frame endpoint +fields. This provides a direct exact endpoint check, but the final program +uses the shorter current-version identity below. + +Original708 has only one destination update after the cut: +`708 +=146/2` at source event17433, at frame127 of rank9. Because the original +endpoint is x708, the exact value of146 at that event satisfies +`g=-value(146)/2`. In the candidate the renamed update is event17523, +`new +=146/2`. Immediately after it, insert these three ordinary operations: + +``` +126 += 2*new +188 -= 2*new +new -= 146/2 +``` + +The first two remove the126/188 defects at this point; later ADDs still build +their final values. The third restores new to z. Their order is +necessary: applying the inverse146 update first leaves errors at126 and188. +The literal suffix has no later source reads from126,188 or new, and no later +write to new. Later writes to126 and188 are only ADDs at frame127. Consequently +the first two normalizations commute with that suffix, and the source146 is +read at precisely its required live version. A separate covector check verifies +that this146 value is unchanged by the initial basis and raw-z replacement: its +126/188/708 input coefficients and its response to the cut perturbation vanish. + +The pure constructor first builds the equivalent terminal normalization and +then performs this checked substitution: three early operations replace the +two terminal restorations plus118 final correction operations. No algebraic +search, historical-value assumption, or new transport is used. + +## Complete signed invoice + +The paid histogram is unchanged. Original708's H9 productive target is replaced +by its retired H2 target and the new independent helper's H7 target: + +``` +Delta paid = 0 +Delta targets = H2+H7-H9 +Delta(targets-paid) = H2+H7-H9 > 0. +``` + +For `H_r=r^t` and09^t`. Rank mass +is unchanged. The eighteen local calls multiply this delta by18. The complete +paid occurrence count stays66348 and the productive count increases to12976; +the complete rank surplus remains760. The extra independent helper's ordinary +routing and allocation costs are still charged. + +The final local word has25546 events and scalar allowance221474. Its paid +histogram is `{1:2184,2:459,3:495,4:92,5:159,6:22,7:15}` and its productive +histogram is `{1:2,2:5,4:91,5:6,7:6,8:15,9:411}`. + +## Finite verification + +The pure constructor accepts only the pinned canonical source and returns +the exact final candidate plus a witness. The independent literal checker +verifies all753 arbitrary input columns, frames, owned initialization/use/clear +rules, both complete local histograms and the ordinary scalar count. A separate +backwards implementation verifies all753 transpose columns. + +Ten actual mutations are rejected under ordinary Python and `python -O`: +missing retirement; either omitted early restoration; omitted or wrong-sign146 +inverse; incorrect cleanup order; reinstated obsolete decoder; omitted owned +identifier shift; overstated old helper target; and wrong new helper boundary. + +Independent agents separately derived the88-term h and118-term output +functional and checked the temporal simplification. These are independent +agent calculations, not independent human review or proof-kernel acceptance. +Prepared for flyingviper with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/p104-two-boundary-helper-split/README.md b/research/p104-two-boundary-helper-split/README.md new file mode 100644 index 0000000000..d86aa5b78c --- /dev/null +++ b/research/p104-two-boundary-helper-split/README.md @@ -0,0 +1,112 @@ +# A P104 helper split using different input and output bases + +This package improves the complete conditional exponent saving from +**0.00310915222 to 0.00311024570**, building on Ali Romman's +[PR5713](https://github.com/CrocSwap/integer-mult-bounds/pull/5713), head +`a5348f7143f95fe0046b92b96172e30763c7d731`. +The increase is 0.00000109348, approximately 0.0352% over that source. +This is a modest improvement; the selected frontier is unchanged. + +The initial helper basis can use main inputs at zero-dimensional frames. +Those inputs have arbitrary values: they are not initialized zeros. An actual +coframed relation later restores the old helper and permits a new independent +helper to take its place. A different, legal output combination restores the +remaining fields. Requiring the same combination at both boundaries would +miss this split. The construction adds no paid recursive transport. + +## Complete cost + +For `H_r = r^(1-kappa)`, one local call changes the signed invoice by + +``` +paid: unchanged +targets: +H2 +H7 -H9 +targets-paid: H2 +H7 -H9 > 0. +``` + +Strict subadditivity proves the positive gain for `0 < kappa < 1`. All added +ordinary work is separately funded. The complete caller uses eighteen LOCALs. + +| Quantity | Verified value | +|---|---:| +| Conditional kappa | 0.00311024570 | +| Strict raw crossing enclosure | (0.00311024572012, 0.00311024572013) | +| Complete paid jobs | 66,348 | +| Complete productive fields | 12,976 | +| Complete rank surplus | 760 | +| Local independent inputs / owned labels | 744 / 9 | +| Local owned lifetimes / peak simultaneous | 11 / 2 | +| Distinct native maps checked | 2,917 | +| Local scalar / routing allowance | 221,474 / 5,166,000 | + +Original helper708 retires at rank two. New helper743 starts there and follows +the original continuation to rank nine. All nine owned identifiers shift by +one, without a new lifetime. The 25,546-instruction word contains 89 initial +basis additions, one retirement addition and three cleanup additions. At the +cleanup contact, the exact current146 value replaces a 118-term terminal +functional; the proof verifies both its version and the required order. + +## Reproduction and checks + +```sh +python3 -B scripts/research_package.py --package research/p104-two-boundary-helper-split +python3 -B scripts/check_research_commit.py --package research/p104-two-boundary-helper-split --check-source-history +``` + +Expected marker: `PASS_P104_TWO_BOUNDARY_SPLIT_KAPPA_00311024570`. +The registered normal and optimized commands check the exact construction, +all 753 arbitrary-input columns, separate dense transpose, actual binary +coframes and owned intervals, every native map and absolute phase, and the +complete physical caller. The price replay uses two exact moment engines, +compiler completion and all 54 strict plus four functional outer predicates. +Complete WORD, WITNESS and RESULT payloads are compared; compression container +bytes are not used as mathematical equality. + +Ten actual instruction/boundary mutations are rejected, covering missing or +wrong retirement/cleanup, reversed cleanup order, the obsolete fresh decoder, +wrong helper boundaries and an omitted owned-identifier shift. Two further +invoice controls reject an unpaid query and an invented target. Inherited +caller, phase, cutoff and BIT controls remain active. See [PROOF.md](PROOF.md). + +Separate agents derived the input basis and output correction, verified the +exact intermediate146 value, and replayed all scalar columns and ownership +without importing the constructor. Compact receipts are retained in `evidence/`. +The final caller-audit and publication checks are reported in +[VALIDATION.md](VALIDATION.md). Independent AI checks are not independent human +or formal mathematical acceptance. + +## Source custody, credit and limits + +Main provenance is `df0137efd35e11b4445734bf612bdd4c7ebc330c`. +The exact 21-file PR5713 export is authenticated before source imports; all +nested source checks remain active. Git-history metadata binds the archive +retained in this branch; `archived_files` separately preserves its exact +origin-head and payload pins. Replay needs no cached pending-PR Git objects. The complete price adapter differs only +by the explicit substitutions in `PRICING-EDITS.json`. Frozen predecessors and +shared framework files are unchanged. + +Credit Ali Romman's PR5713 temporal update and predecessor proofs, Joel +Pulikkan/GamingPuzzled's PR5684, the retained helper-split constructions, and +the caller, native and pricing authors listed in NOTICE. Chris R/Clear1nsight's +PR5550 and the maintainer's PR5599 review supply the separate caller lineage. +The elementary linear basis identities are standard; the contribution is this +source-specific construction, legal schedule and complete invoice. Prepared +for flyingviper with substantial OpenAI Codex assistance, including separate +verification and literature agents. Apache-2.0. + +The native all-width, owned erasure, compiler, precision/tape and +analytic/recovery assumptions remain. COPY is an ADD into an ideally initialized +owned zero with numerical residuals retained. No complete rounded multiplier +or huge uniform word is materialized. This package claims neither a large gain, +a general optimality result, nor admission to the selected frontier. + +## Open next questions + +- Independently inspect the two boundary functionals and early cleanup order; + both matter to the endpoint identity. +- Find another pair of legal boundary functionals at an actual coframed cut, + with the complete native, helper and ordinary bill included. +- Audit one remaining source-specific framework assumption before promoting + a complete supplier into the selected result. + +Concrete first steps and blockers are recorded in `TASK.json`. diff --git a/research/p104-two-boundary-helper-split/RESULT.json b/research/p104-two-boundary-helper-split/RESULT.json new file mode 100644 index 0000000000..a83d70e025 --- /dev/null +++ b/research/p104-two-boundary-helper-split/RESULT.json @@ -0,0 +1,366 @@ +{ + "complete_cost": { + "compiler": { + "H": 80511200000000000, + "N": "2^80511200000000000", + "eta": { + "lower": "0.000000130293974939177582367425", + "upper": "0.000000130293974939177582367426" + }, + "gap": "1/1400000000000", + "integer_test_exponent": 57508, + "logarithm_power": 1024, + "theta": "63/64", + "uniform_saving": "2177171993/700000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "27337/25000000000", + "kappa": "31102457/10000000000", + "kappa_decimal": "0.00311024570", + "margin_at_previous": { + "lower": "0.265423369162460429568591881457", + "upper": "0.265423369162460429568591881458" + }, + "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": 5987, + "local_routes": 5166000, + "local_scalar": 221474, + "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": "6096081577595645656017/1960000000000000000000000", + "fused_gaussian": "6096081577586936968051/1960000000000000000000000", + "global_coordinate_router": "272146499/87500000000", + "group_bit_router": "381005098686683560503/122500000000000000000000", + "group_scans": "699999999999/700000000000", + "main_transform": "6096081576195645656017/1960000000000000000000000", + "microbox_face_corrections": "26950000000001/350000000000", + "polynomial_products": "1399999999999/1400000000000", + "sparse_union_movement": "802346081577595645656017/1960000000000000000000000" + }, + "parameters": { + "a": "272146499/87500000000", + "b": "870868797/280000000000", + "beta": "1399999999997/1400000000000", + "bit_saving": "17/5000", + "cap_xi": "1782346081576195645656017/1960000000000000000000000", + "complex_uniform_saving": "2177171993/700000000000", + "d": "1/1400000000000", + "epsilon": "1399999999999/1400000000000", + "kappa": "31102457/10000000000", + "lambda_": "398755901719/400000000000", + "lambda_prime": "1395645656017/1400000000000", + "layout": "1/1400000000000", + "q": "4354343983/1400000000000", + "r0": "1/14000000000000", + "stop": "1/1400000000000", + "tested_saving": "622049141/200000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "25353501/87500000000", + "actual_logarithmic_gamma_guard": "1/1400000000000", + "actual_logarithmic_group_guard": "177653918425904354343983/980000000000000000000000", + "alpha_logarithm_absorption": "1/14000000000000", + "boundary_algebraic_matrix_above_kappa": "5595645656017/1960000000000000000000000", + "cap_above_band": "802346081576195645656017/1960000000000000000000000", + "cap_below_cell": "177653918422404354343983/1960000000000000000000000", + "cap_below_phase_cell_power": "2137653918423804354343983/1960000000000000000000000", + "complex_above_effective": "1/1400000000000", + "complex_below_one_over_32": "7879131203/280000000000", + "complex_endpoint": "1/700000000000", + "epsilon_below_one": "1/1400000000000", + "epsilon_positive": "1399999999999/1400000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "5586936968051/1960000000000000000000000", + "gaussian_above_main": "695645656017/980000000000000000000000", + "global_coordinate_router_above_kappa": "1/350000000000", + "global_gamma_power_slack": "9/14000000000000", + "group_below_dimension": "1/700000000000", + "group_bit_router_above_kappa": "436683560503/122500000000000000000000", + "group_gauge_power_slack": "177653918425834354343983/980000000000000000000000", + "group_key_fits_record": "1/700000000000", + "group_positive": "1399999999997/1400000000000", + "group_scans_above_kappa": "697822828009/700000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "689637640400418148631/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": "559129131203/392000000000000000000000", + "leaf_saving_above_effective": "279129131203/392000000000000000000000", + "main_transform_above_kappa": "4195645656017/1960000000000000000000000", + "membership_arithmetic_fits_record": "1/1400000000000", + "microbox_face_corrections_above_kappa": "13474455707003/175000000000", + "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": "1395645656019/1400000000000", + "positive_layout_slack": "1/1400000000000", + "q_below_effective": "1/1400000000000", + "q_below_internal": "1/1400000000000", + "q_below_leaf": "559129131203/392000000000000000000000", + "q_positive": "4354343983/1400000000000", + "short_record_fallback": "279129131203/280000000000", + "source_axis_superpolynomial": "1/1400000000000", + "sparse_union_movement_above_kappa": "796250000005595645656017/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": 40872, + "16": 416, + "2": 8262, + "24": 416, + "3": 8910, + "32": 416, + "4": 1656, + "40": 416, + "48": 416, + "5": 2862, + "56": 416, + "6": 396, + "64": 416, + "7": 270, + "72": 208 + }, + "paid_calls": 66348, + "previous_open_pr5713": "155457611/50000000000", + "productive_fields": 12976, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_ceiling": { + "derivative_upper": "-369633362694406560545046337101738171609683586723251074624328749/1569275433846670190958947355801916604025588861116008628224", + "interval": [ + "0", + "17/5000" + ] + }, + "raw_headroom": [ + "503/25000000000000", + "2013/100000000000000" + ], + "raw_root_interval": [ + "77756143003/25000000000000", + "311024572013/100000000000000" + ], + "relative_gain_percent": "5467400/155457611", + "strictification": { + "alpha": { + "lower": "0.999999999984633711012925911331", + "upper": "0.999999999984633711012925911332" + }, + "cutoff": 17, + "delta": { + "lower": "0.968803893336188607862541966226", + "upper": "0.968803893336188607862541966227" + }, + "floor": 18, + "gamma": { + "lower": "0.968263210279894472263420498148", + "upper": "0.968263210279894472263420498149" + }, + "normalized_paid_upper": "1048576000976562501/1048576001073741824", + "power": 1024, + "reserve": "1/1000000000000", + "tail_block": 128, + "tail_decay": "39/40", + "tail_offset": "1/5", + "tested": "622049141/200000000000" + }, + "targets": { + "1": 36, + "145": 208, + "17": 416, + "2": 90, + "25": 416, + "33": 416, + "4": 1638, + "41": 416, + "49": 416, + "5": 108, + "57": 416, + "65": 416, + "7": 108, + "73": 208, + "8": 270, + "9": 7398 + }, + "whole_idle_jobs": 3120 + }, + "independent_literal_audit": { + "columns": 753, + "owned_lifetimes": 11, + "owned_peak": 2, + "paid": { + "1": 2184, + "2": 459, + "3": 495, + "4": 92, + "5": 159, + "6": 22, + "7": 15 + }, + "scalar": 221474, + "status": "PASS_ALL_SCALAR_INPUTS_FRAMES_OWNERSHIP_INVOICES", + "targets": { + "1": 2, + "2": 5, + "4": 91, + "5": 6, + "7": 6, + "8": 15, + "9": 411 + } + }, + "limits": [ + "The five inherited framework assumptions remain.", + "No selected-frontier admission or large improvement is claimed.", + "The huge uniform word and complete rounded multiplier are not materialized.", + "Independent agent checks are not human or formal acceptance." + ], + "local": { + "endpoint_coefficients": 567009, + "helpers": { + "1": 2, + "2": 5, + "4": 91, + "5": 6, + "7": 6, + "8": 15, + "9": 411 + }, + "owned_fields": 9, + "owned_lifetimes": 11, + "paid": { + "1": 2184, + "2": 459, + "3": 495, + "4": 92, + "5": 159, + "6": 22, + "7": 15 + }, + "paid_rank_mass": 5987, + "peak_owned_fields": 2, + "public_inputs": 744, + "real_scalar_allowance": 221474 + }, + "native": { + "distinct_maps": 2917, + "helper_normalizers": 1072, + "helpers": { + "1": 2, + "2": 5, + "4": 91, + "5": 6, + "7": 6, + "8": 15, + "9": 411 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "626b4ce338e77fd1f5c5d90cf107d91bb73af42c107cd8eea14fe657ddb324e4", + "wrong_phase_rejected": true + }, + "negative_controls": { + "invented_extra_H9_target": "Every productive helper has a native target", + "inverse_before_normalizing126188": "Exact arbitrary-input endpoint row 126", + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "omit_current146_inverse": "Exact arbitrary-input endpoint row 743", + "omit_early126_restoration": "Exact arbitrary-input endpoint row 126", + "omit_early188_restoration": "Exact arbitrary-input endpoint row 188", + "omit_original_retirement": "Exact arbitrary-input endpoint row 708", + "omit_owned_identifier_shift": "Scalar destination coframe", + "reintroduce_obsolete_decoder": "Exact arbitrary-input endpoint row 743", + "restore_uncharged_old_H9_target": "All declared final charts and owned exits", + "unpaid_rank7_query": "Complete field and call counts", + "wrong_current146_inverse_sign": "Exact arbitrary-input endpoint row 743", + "wrong_new_helper_boundary": "MOVE source and ownership" + }, + "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": 567009, + "columns": 753 + }, + "source_commit": "a5348f7143f95fe0046b92b96172e30763c7d731", + "status": "PASS_P104_TWO_BOUNDARY_SPLIT_KAPPA_00311024570" +} diff --git a/research/p104-two-boundary-helper-split/SOURCES.json b/research/p104-two-boundary-helper-split/SOURCES.json new file mode 100644 index 0000000000..8ac6a642e0 --- /dev/null +++ b/research/p104-two-boundary-helper-split/SOURCES.json @@ -0,0 +1,186 @@ +{ + "archived_files": [ + { + "git_blob": "36c1b859be8f5c1325811e633ac51149e1cd7bc0", + "path": "research/p104-temporal-updates/NOTICE", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/NOTICE", + "sha256": "a252225cb4d9c61fc94b5b7f638600393a859e47750cfea7688c75b1f6610077", + "usage": "provenance" + }, + { + "git_blob": "a8dce0d2f6a4cccba049473610e3fccae70ae9c3", + "path": "research/p104-temporal-updates/PRICING-EDITS.json", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/PRICING-EDITS.json", + "sha256": "b525d9852aa3056fe813ab14a3f0e10dffa06fba920ef8c962101547c11fd032", + "usage": "provenance" + }, + { + "git_blob": "308d19427b6ca0c6b52af414245f4c6fe5ebce0f", + "path": "research/p104-temporal-updates/PROOF.md", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/PROOF.md", + "sha256": "f33c7a9a23e582b822cb75ab12df923732128045734b9562d7703280bd78c507", + "usage": "provenance" + }, + { + "git_blob": "fae45de92d394c21cda68012d87684b9362e207f", + "path": "research/p104-temporal-updates/README.md", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/README.md", + "sha256": "c61e96e261aee3b1d2b4a8b5009b98b0a41a4c2062b16d35bd9763df4626e3a5", + "usage": "provenance" + }, + { + "git_blob": "8fc639f9b389d89eacac696b129cf378d336c98c", + "path": "research/p104-temporal-updates/RESULT.json", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/RESULT.json", + "sha256": "3ce2dfdd7ccb6b0d6d8d674bc7614a8302a0f2f9e23f16ece95dedb9d7ea561e", + "usage": "provenance" + }, + { + "git_blob": "d7d9ab3b6ceb631ca5a74d2f837c8b50e6fdd959", + "path": "research/p104-temporal-updates/SOURCES.json", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/SOURCES.json", + "sha256": "ea42b63fdff8a30ddc6205ee4844effdd1fa8768e99f3a95d82a3d72575e6782", + "usage": "provenance" + }, + { + "git_blob": "d8c2c1d866a829dfafee49a96a2f9c33a7e71063", + "path": "research/p104-temporal-updates/TASK.json", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/TASK.json", + "sha256": "5bffc23b9542c026eb7086152c50c5ab7ce658c4e3068a9848ae0b9e3090f0db", + "usage": "provenance" + }, + { + "git_blob": "b105d24f8ffb212768173f78ee3dd3042511c1dd", + "path": "research/p104-temporal-updates/VALIDATION.md", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/VALIDATION.md", + "sha256": "fe35ba2483fa262e02ff5af40007df99d080117f17c7c747c482d005e4af4252", + "usage": "provenance" + }, + { + "git_blob": "953ffaee175e1ea5ccc1525d4c1b1d4456b4f6d2", + "path": "research/p104-temporal-updates/VERIFY.json", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/VERIFY.json", + "sha256": "58f08d7eeedbf28b12de7bc8786f059a56cdec47db00adda16095642cb1857c5", + "usage": "provenance" + }, + { + "git_blob": "2b69faf0cdd9916002825106ba728590fa709ca4", + "path": "research/p104-temporal-updates/WITNESS.json", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/WITNESS.json", + "sha256": "74b50f1e59bb68387b1ab449e5268146c1c036bba25d3a09a8a0d60a7233acd8", + "usage": "provenance" + }, + { + "git_blob": "45f6c10bf8a0ad6eb5f6714377a464e274db7dbd", + "path": "research/p104-temporal-updates/WORD.json.gz", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/WORD.json.gz", + "sha256": "9fd67dd89ed24a644257cd9aef06934ed4c6fbe0441804684a968868f2ef66a8", + "usage": "provenance" + }, + { + "git_blob": "3852bff77c1af9fdc3608451e772138891798cc1", + "path": "research/p104-temporal-updates/construct.py", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/construct.py", + "sha256": "dbd3c6a230a2ee94ac3424f34a5caab338bd335f71296ceeb6e0ef2ec349dcb4", + "usage": "provenance" + }, + { + "git_blob": "cd87254d84b594ea7809e8106b26d01775e138e7", + "path": "research/p104-temporal-updates/inputs/pr5678-source.tar", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/inputs/pr5678-source.tar", + "sha256": "edd6ce029b39abf2f72c28bbc377c9793ddf275e19f3f2b5a6cab0a65670161b", + "usage": "provenance" + }, + { + "git_blob": "fa0bd1401f5775f4351cfa23b08f3998dba6129e", + "path": "research/p104-temporal-updates/inputs/pr5684/NOTICE", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/inputs/pr5684/NOTICE", + "sha256": "e8e0cabef6cf40d63f3cea3b6403dfd1af8727e40df03f09b2932718bcddc1b0", + "usage": "provenance" + }, + { + "git_blob": "e80d32af1801c3dcf97f0904f7c3cecc9d3ca418", + "path": "research/p104-temporal-updates/inputs/pr5684/README.md", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/inputs/pr5684/README.md", + "sha256": "1e75a8e010f6e22406f9cdd84c2d07c7c8a92b4b9436b4e2afd6f8defd3ff201", + "usage": "provenance" + }, + { + "git_blob": "f3fb0e2144ec8a5c3407e4eaa6528bb3436ba573", + "path": "research/p104-temporal-updates/inputs/pr5684/WORD.json.gz", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/inputs/pr5684/WORD.json.gz", + "sha256": "d6db1d0d97b13ea483a462c65437664d15d34dec56c3682cf6e1de31266ec6c2", + "usage": "provenance" + }, + { + "git_blob": "3b0109e0fae47f1961238ed418821861a756ab56", + "path": "research/p104-temporal-updates/inputs/pr5684/construct.py", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/inputs/pr5684/construct.py", + "sha256": "b83fe6e745f18dede23328b5a670e582b2da23ed15ee83c8f78d71b9f40f8261", + "usage": "provenance" + }, + { + "git_blob": "e817f4da7deb0120c51e10b98bdbf9f9c53fa57c", + "path": "research/p104-temporal-updates/inputs/pr5684/pricing.py", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/inputs/pr5684/pricing.py", + "sha256": "b4edb4a45f30720956167c07d88b102e596dd6a001c7eced4d282d32225833e2", + "usage": "provenance" + }, + { + "git_blob": "ed290f105903d9a6da66cd89681d5ab6a11f62d6", + "path": "research/p104-temporal-updates/pricing.py", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/pricing.py", + "sha256": "f3d500ada46124241e2b35cd649d58b2f3a43418aeda8834a48c1c06e5306e90", + "usage": "provenance" + }, + { + "git_blob": "720cc95b2b13589e00eee64907805751f8dd68e4", + "path": "research/p104-temporal-updates/sources.py", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/sources.py", + "sha256": "631cfcbfe2459386652220301e4eb83855334a84fb49a088bd44324435817519", + "usage": "provenance" + }, + { + "git_blob": "9ff8a38435b8277b063f1880737fc4e295d20c51", + "path": "research/p104-temporal-updates/verify.py", + "pin": "head:a5348f7143f95fe0046b92b96172e30763c7d731:research/p104-temporal-updates/verify.py", + "sha256": "21259016a0980065e9348718504f4f5c9d06773c072c23b63384b41608a46dfa", + "usage": "provenance" + } + ], + "attribution": "PR5713 supplies the frozen temporal word and complete source stack. All predecessor notices are retained. Two-boundary main-assisted helper split by flyingviper with substantial OpenAI Codex assistance and separate AI checks.", + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "direct_sources": [], + "files": [ + { + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "path": "certificates/selected-result.json", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "usage": "provenance" + }, + { + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "path": "docs/research/agent-task-catalog.json", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72", + "usage": "provenance" + }, + { + "git_blob": "ec8f4bccaca147bc80cec078147fb95bc515036e", + "path": "research/p104-two-boundary-helper-split/inputs/pr5713-source.tar", + "pin": "head:d504eda8236e5cc5acabc10a373af1bab58b1c6f:research/p104-two-boundary-helper-split/inputs/pr5713-source.tar", + "sha256": "c4d8d0bcd6231eb4539a76d66b0dbd465313cbc50d279ca974a55fecb935d544", + "usage": "provenance" + } + ], + "schema_version": 1, + "source_custody": "Runtime sources come from the self-contained archive retained at d504eda8236e5cc5acabc10a373af1bab58b1c6f. archived_files preserve exact origin heads and byte pins, checked before imports; no origin Git object is needed at replay.", + "source_export": { + "commit": "a5348f7143f95fe0046b92b96172e30763c7d731", + "files": 21, + "git_blob": "ec8f4bccaca147bc80cec078147fb95bc515036e", + "local_path": "inputs/pr5713-source.tar", + "package": "research/p104-temporal-updates", + "sha256": "c4d8d0bcd6231eb4539a76d66b0dbd465313cbc50d279ca974a55fecb935d544", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5713" + } +} diff --git a/research/p104-two-boundary-helper-split/TASK.json b/research/p104-two-boundary-helper-split/TASK.json new file mode 100644 index 0000000000..a37c6de3ba --- /dev/null +++ b/research/p104-two-boundary-helper-split/TASK.json @@ -0,0 +1,78 @@ +{ + "actual_scope": "Split helper708 using different input and output boundary functionals, with no extra paid transport, and shorten cleanup at the exact last source version. Complete conditional kappa0.00311024570.", + "ai_assistance": "Substantial OpenAI Codex assistance for construction, exact scripts, primary replay, independent agent checks, literature review and writing. Not independent human or formal acceptance.", + "author": "flyingviper with substantial OpenAI Codex assistance", + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "bottleneck_link": "Changed boundary bases increase productive helper targets without adding native recursive jobs; all ordinary basis preparation and cleanup are funded.", + "budget_minutes": 180, + "evidence": "PROOF.md, WITNESS.json, RESULT.json and VALIDATION.md", + "open_questions": [ + { + "blocked_by": "No known technical blocker for this fixed finite construction.", + "first_step": "Replay the source-bound constructor, omitted-repair control and complete full caller.", + "question": "Can a separate reviewer verify the different input/output bases and early cleanup order?", + "why_it_matters": "Requiring the same correction at both boundaries misses a valid split, while reversing the actual normalization order breaks endpoints." + }, + { + "blocked_by": "No additional complete witness is claimed.", + "first_step": "Identify a coframed cut correction linking a legal rank-zero input functional to a legal full-frame output functional; check the complete caller and all ordinary costs.", + "question": "Do other pairs of legal boundary functionals support profitable helper splits?", + "why_it_matters": "The current gain is small; the mechanism may be reusable." + }, + { + "blocked_by": "The complete rounded multiplier and huge uniform word are not materialized.", + "first_step": "Select one source-specific native, owned-erasure, compiler, precision/tape or analytic premise from the selected review.", + "question": "Can the retained framework assumptions be resolved?", + "why_it_matters": "The resulting exponent saving remains conditional." + } + ], + "original_card": { + "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.", + "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." + ], + "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.", + "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.", + "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." + }, + "id": "complex-new-helper-inventory", + "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." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ], + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "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." + ], + "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" + ] + }, + "outcome": "completed", + "priority_revision": 7, + "schema_version": 1, + "scope_change_reason": "The initial basis may use arbitrary main inputs at rank-zero frames while a different full-frame functional restores outputs. The cut coframe relates these two legal boundary changes; the unchanged paid invoice and new targets give a complete signed gain.", + "scope_status": "changed", + "stop_rule": "Verify one complete source-bound candidate and publish. Further expansion requires a distinct changed dependency with its full repair budget.", + "task_id": "complex-new-helper-inventory" +} diff --git a/research/p104-two-boundary-helper-split/VALIDATION.md b/research/p104-two-boundary-helper-split/VALIDATION.md new file mode 100644 index 0000000000..241904e35d --- /dev/null +++ b/research/p104-two-boundary-helper-split/VALIDATION.md @@ -0,0 +1,49 @@ +# Validation + +The complete source-bound primary replay and the registered normal/optimized +pair pass with marker PASS_P104_TWO_BOUNDARY_SPLIT_KAPPA_00311024570. Both +registered commands reproduce complete WORD, WITNESS and RESULT payloads. +They retain753-column forward/transpose checks,2917 native maps and phases, +complete caller, two exact moment engines, compiler,54 strict plus4functional +outer predicates,10 actual word mutations and2 invoice mutations. + +Separate agents checked the boundary algebra, exact live146 version, scalar +columns, binary coframes, lifetime rules, source custody and pricing edits. +The final independent caller run passed in26.718seconds with sampled peak RSS +72,060,928bytes, below its120-second/512-MiB caps. It checked66348 paid jobs, +12976 targets,306 phase anchors,9648 fresh helpers and all16 fault controls. +Its ordinary allowance124341508 is below184647552. Complete caller output +SHA256: fea5c02bde0fef9a424da9dffb70767c55c102b6324ce4b0ad83f0850cef8c64. +Compact exact-candidate receipts are retained in evidence/. The boundary +receipt explicitly concerns the equivalent long form; scalar/version/caller +receipts concern the final short word. No receipt is silently rebound. + +The independent caller uses the explicit-owned adapter published in PR5717 +at41fda9302e5de79911b0c91c6161beaf386798b3. It checks caller and normalizer +obligations; it does not independently replay all paid native maps or admit +the machine/precision premises. Those limits remain in its receipt. + +Publication gates are the committed-byte/source-history check, official export, +export integrity and Git-free read-only replay. Their results are reported in +the PR after completion so this committed document need not attest to its own +future export. Main was refreshed atdf0137efd35e11b4445734bf612bdd4c7ebc330c. + +## Inherited CI limitation + +The unchanged canonical-main test_current_ci_section_matches_selected_record +fails on its review and source_manifest links: PROOF-REVIEW.md and +frontier5599-source.json are missing from the current-CI documentation section. +The same two failures reproduce in the focused six-test file locally; both +that test and current-status.md are byte-identical to canonical main. The +hosted PR5717 plan job reproduces the failures and skips scientific replay: +https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40314285344/job/121542860148 + +Existing PR5703 supplies the documentation fix. This package changes no shared +documentation, tests, workflows or selected-result values. Local scientific +success is not presented as hosted CI success or full theorem acceptance. + +The source-history gate first rejected direct Git pins to the pending PR5713 +head. Runtime bytes were already self-contained. The metadata now binds the +retained archive in this branch history, while archived_files preserves every +origin head and payload hash and the verifier authenticates them before import. +No source bytes or mathematical assertions changed. diff --git a/research/p104-two-boundary-helper-split/VERIFY.json b/research/p104-two-boundary-helper-split/VERIFY.json new file mode 100644 index 0000000000..5550c891e8 --- /dev/null +++ b/research/p104-two-boundary-helper-split/VERIFY.json @@ -0,0 +1,28 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "checks": "Authenticated source, exact constructor, all arbitrary-input/transpose/native/caller obligations, complete charged pricing and actual rejection controls.", + "timeout_seconds": 600 + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "checks": "Authenticated source, exact constructor, all arbitrary-input/transpose/native/caller obligations, complete charged pricing and actual rejection controls.", + "timeout_seconds": 600 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-two-boundary-helper-split/WITNESS.json b/research/p104-two-boundary-helper-split/WITNESS.json new file mode 100644 index 0000000000..88d2559001 --- /dev/null +++ b/research/p104-two-boundary-helper-split/WITNESS.json @@ -0,0 +1,288 @@ +{ + "after_candidate_event": 17523, + "cleanup_anchor": [ + "ADD", + 743, + 146, + "1/2", + 127 + ], + "early_cleanup": [ + [ + "ADD", + 126, + 743, + "2", + 127 + ], + [ + "ADD", + 188, + 743, + "-2", + 127 + ], + [ + "ADD", + 743, + 146, + "-1/2", + 127 + ] + ], + "early_cleanup_adds": 3, + "events": 25546, + "h": { + "146": "-1/2", + "151": "-1/2", + "154": "1/4", + "217": "1/4", + "224": "-1/4", + "227": "-1/4", + "229": "1/4", + "235": "-1/4", + "237": "1/4", + "238": "1/4", + "239": "-1/4", + "274": "1/8", + "276": "-1/8", + "279": "-1/8", + "283": "1/4", + "285": "-1/4", + "286": "-1/8", + "290": "1/8", + "292": "-1/8", + "295": "-1/8", + "299": "1/4", + "301": "-1/4", + "302": "-1/8", + "306": "-1/8", + "308": "1/8", + "315": "-1/4", + "317": "1/4", + "318": "1/8", + "322": "-1/8", + "324": "1/8", + "331": "-1/4", + "333": "1/4", + "334": "1/8", + "338": "1/8", + "34": "-1/2", + "340": "-1/8", + "343": "-1/8", + "347": "1/4", + "349": "-1/4", + "350": "-1/8", + "354": "1/8", + "356": "-1/8", + "359": "-1/8", + "363": "1/4", + "365": "-1/4", + "366": "-1/8", + "370": "-1/8", + "372": "1/8", + "375": "1/8", + "379": "-1/4", + "381": "1/4", + "382": "1/8", + "386": "-1/8", + "388": "1/8", + "39": "-1/2", + "391": "1/8", + "395": "-1/4", + "397": "1/4", + "398": "1/8", + "401": "-1/4", + "402": "1/4", + "403": "-1/4", + "409": "-1/4", + "411": "-1/4", + "413": "-1/4", + "415": "-1/4", + "417": "-1/4", + "418": "1/4", + "419": "-1/4", + "425": "-1/4", + "427": "-1/4", + "429": "-1/4", + "431": "-1/4", + "478": "-1/4", + "479": "-1/4", + "490": "-1/4", + "491": "-1/4", + "499": "1/8", + "502": "1/4", + "503": "1/4", + "511": "1/8", + "514": "1/4", + "515": "1/4", + "706": "-1", + "708": "1", + "712": "1/2", + "716": "-1", + "725": "1/2" + }, + "initial_ordinary_adds": 89, + "local_paid": { + "1": 2184, + "2": 459, + "3": 495, + "4": 92, + "5": 159, + "6": 22, + "7": 15 + }, + "local_targets": { + "1": 2, + "2": 5, + "4": 91, + "5": 6, + "7": 6, + "8": 15, + "9": 411 + }, + "owned_fields": 9, + "owned_lifetimes": 11, + "owned_peak": 2, + "paid_delta": {}, + "public_inputs": 744, + "removed_terminal_events": 120, + "scalar_allowance": 221474, + "scope": "Exact source-bound split, frame/ownership/invoice checks, then a validated three-operation temporal normalization. Independent full final scalar and native/caller/pricing checks are separate obligations.", + "signed_target_minus_paid_delta": { + "2": 1, + "7": 1, + "9": -1 + }, + "source_canonical_sha256": "32adce6656e49aa020d3e6317f1c45c11fccadeeb67a8d506172d101703d2138", + "source_head": "a5348f7143f95fe0046b92b96172e30763c7d731", + "status": "PASS_EXACT_SCALAR_CHART_OWNERSHIP", + "target_delta": { + "2": 1, + "7": 1, + "9": -1 + }, + "terminal_cleanup_adds": 118, + "terminal_full9_cleanup": { + "0": "1/4", + "10": "1/4", + "100": "1/4", + "101": "1/4", + "106": "-1/4", + "109": "-1/4", + "111": "1/4", + "146": "-1/2", + "15": "1/4", + "16": "-1/4", + "17": "1/4", + "18": "1/4", + "20": "-1/4", + "22": "1/4", + "226": "-1/4", + "227": "1/4", + "229": "1/4", + "233": "1/4", + "237": "1/4", + "238": "1/4", + "239": "-1/4", + "240": "1/4", + "241": "1/4", + "243": "1/4", + "245": "1/4", + "249": "1/4", + "25": "1/4", + "253": "1/4", + "254": "1/4", + "255": "-1/4", + "257": "1/4", + "261": "1/4", + "262": "1/4", + "266": "-1/4", + "267": "1/4", + "269": "1/4", + "270": "1/4", + "272": "1/4", + "280": "-1/4", + "283": "1/4", + "288": "1/4", + "296": "-1/4", + "299": "1/4", + "30": "1/4", + "303": "-1/2", + "304": "1/4", + "308": "1/4", + "31": "1/4", + "312": "-1/4", + "318": "1/4", + "319": "-1/2", + "32": "1/4", + "320": "1/2", + "33": "1/4", + "352": "1/4", + "356": "-1/4", + "366": "-1/4", + "367": "1/4", + "368": "1/4", + "37": "-1/4", + "379": "-1/4", + "383": "1/4", + "384": "1/4", + "395": "-1/4", + "399": "-1/4", + "40": "1/4", + "400": "1/4", + "411": "-1/4", + "414": "1/4", + "415": "-1/2", + "418": "1/4", + "419": "-1/4", + "42": "-1/4", + "421": "1/4", + "422": "1/4", + "425": "-1/4", + "426": "-1/4", + "43": "-1/4", + "430": "1/4", + "431": "-1/4", + "434": "1/4", + "435": "-1/4", + "437": "1/4", + "438": "1/4", + "441": "-1/4", + "442": "-1/4", + "446": "1/4", + "447": "-1/4", + "47": "1/4", + "48": "1/4", + "49": "1/4", + "5": "1/4", + "51": "1/4", + "52": "1/4", + "54": "1/4", + "60": "-1/4", + "63": "1/4", + "65": "-1/4", + "66": "-1/4", + "67": "1/4", + "68": "1/4", + "7": "1/4", + "70": "1/4", + "73": "1/4", + "77": "1/4", + "79": "1/4", + "8": "-1/4", + "84": "-1/4", + "85": "1/4", + "87": "1/4", + "88": "1/4", + "89": "1/4", + "9": "1/4", + "90": "1/4", + "92": "1/4", + "97": "-1/4", + "98": "1/4", + "99": "1/4" + }, + "terminal_intermediate_canonical_sha256": "892cfd5907ee1420b40cd511098c48eb3251501a7e6196367b3bfb4189e5d1a6", + "word_canonical_sha256": "a1c8277189a811546bdc7b147d72e6a594504ff9585c9bf59a5681aa873abb01" +} diff --git a/research/p104-two-boundary-helper-split/WORD.json.gz b/research/p104-two-boundary-helper-split/WORD.json.gz new file mode 100644 index 0000000000..4db015aca3 Binary files /dev/null and b/research/p104-two-boundary-helper-split/WORD.json.gz differ diff --git a/research/p104-two-boundary-helper-split/checks.py b/research/p104-two-boundary-helper-split/checks.py new file mode 100644 index 0000000000..308805a32d --- /dev/null +++ b/research/p104-two-boundary-helper-split/checks.py @@ -0,0 +1,120 @@ +"""Independent literal candidate walk and focused actual invalid-word controls. + +No constructor imports, source search, native engine, or pricing dependencies. +Prepared with substantial OpenAI Codex assistance for flyingviper. Apache-2.0. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction + +def need(ok,message): + if not ok:raise ValueError(message) + +def binary_span(basis): + result={0} + for x in basis: + need(type(x) is int and 0=n and charts[dst] is None,'Owned INIT uses an inactive owned label') + active.add(dst);unwritten.add(dst);charts[dst]=e[2];values[dst]={} + lifetimes+=1;peak=max(peak,len(active));scalar+=2 + elif op=='CLEAR': + need(dst in active and charts[dst]==e[2],'Matching owned CLEAR') + active.remove(dst);unwritten.discard(dst);charts[dst]=None;values[dst]={};scalar+=2 + elif op=='MOVE': + _,_,a,b,private=e + need(charts[dst]==a and private==(dst in active),'MOVE source and ownership') + need(frames[b] cut and r == pivot: + return fresh + return r + 1 if r >= n else r + for index, original in enumerate(w['program']): + e = deepcopy(original) + e[1] = rename(e[1], index) + if e[0] in ('ADD', 'COPY'): + e[2] = rename(e[2], index) + program.append(e) + if index == cut: + program.append(['ADD', pivot, 154, '1/2', 602]) + program.extend([['ADD', 126, fresh, '2', 127], ['ADD', 188, fresh, '-2', 127]]) + replayed = [{r: Q(1)} for r in range(total + 1)] + for e in program: + apply(replayed, e) + wrong = [] + for r, row in enumerate(replayed): + expected = {r: Q(1)} if r < n + 1 else {} + if r - 112 in w['live']: + expected[r - 112] = Q(1) + if row != expected: + wrong.append(r) + need(wrong == [fresh], wrong) + correction = {fresh: Q(1)} + add(correction, replayed[fresh], Q(-1)) + need(fresh not in correction and all((r < n + 1 and candidate['final'][r] == 127 for r in correction)), "Exact constructor obligation: fresh not in correction and all((r < n + 1 and candidate['final'][r] == 127 for r in correction))") + need(not {154, 217, pivot} & set(correction), 'Exact constructor obligation: not {154, 217, pivot} & set(correction)') + cleanup = [['ADD', fresh, r, str(q), 127] for r, q in sorted(correction.items())] + program.extend(cleanup) + candidate['program'] = program + for e in cleanup: + apply(replayed, e) + for r, row in enumerate(replayed): + expected = {r: Q(1)} if r < n + 1 else {} + if r - 112 in w['live']: + expected[r - 112] = Q(1) + need(row == expected, (r, row, expected)) + + def span(b): + s = {0} + for x in b: + s |= {x ^ y for y in tuple(s)} + return s + frames = [span(b) for b in candidate['frames']] + current = candidate['initial'] + [None] * candidate['owned_fields'] + active = set() + paid = Counter() + peak = 0 + lifetimes = 0 + scalar = 0 + for e in program: + op, r = e[:2] + if op == 'INIT': + need(r >= n + 1 and current[r] is None, 'Exact constructor obligation: r >= n + 1 and current[r] is None') + active.add(r) + current[r] = e[2] + peak = max(peak, len(active)) + lifetimes += 1 + scalar += 2 + elif op == 'CLEAR': + need(r in active and current[r] == e[2], 'Exact constructor obligation: r in active and current[r] == e[2]') + active.remove(r) + current[r] = None + scalar += 2 + elif op == 'MOVE': + _, _, a, b, private = e + need(current[r] == a and private == (r in active), 'Exact constructor obligation: current[r] == a and private == (r in active)') + need(frames[b] < frames[a] if private else frames[a] < frames[b], 'Exact constructor obligation: frames[b] < frames[a] if private else frames[a] < frames[b]') + paid[abs(len(candidate['frames'][a]) - len(candidate['frames'][b]))] += 1 + current[r] = b + else: + need(current[r] == e[-1], 'Exact constructor obligation: current[r] == e[-1]') + if op in ('ADD', 'COPY'): + need(current[e[2]] == e[-1] and e[2] != r, 'Exact constructor obligation: current[e[2]] == e[-1] and e[2] != r') + q = Q(e[-2]) + a, b = (abs(q.numerator), q.denominator) + need(q and b & b - 1 == 0 and (abs(q) + 1 < 2 ** 16), 'Exact constructor obligation: q and b & b - 1 == 0 and (abs(q) + 1 < 2 ** 16)') + scalar += 2 * (abs(a.bit_length() - b.bit_length()) + (q < 0)) if op == 'SCALE' else 2 * (2 + a.bit_length() + a.bit_count() + b.bit_length() - 1) + need(not active and current[:n + 1] == candidate['final'], "Exact constructor obligation: not active and current[:n + 1] == candidate['final']") + oldpaid = Counter((abs(len(w['frames'][e[2]]) - len(w['frames'][e[3]])) for e in w['program'] if e[0] == 'MOVE')) + targets = Counter((len(candidate['frames'][candidate['final'][r]]) - len(candidate['frames'][candidate['initial'][r]]) for r in range(n + 1) if r not in main)) + oldtargets = Counter((len(w['frames'][w['final'][r]]) - len(w['frames'][w['initial'][r]]) for r in range(n) if r not in main)) + + def delta(a, b): + return {str(r): a[r] - b[r] for r in sorted(a.keys() | b.keys()) if a[r] != b[r]} + need(delta(paid, oldpaid) == {}, "Exact constructor obligation: delta(paid, oldpaid) == {}") + need(delta(targets, oldtargets) == {'2': 1, '7': 1, '9': -1}, "Exact constructor obligation: delta(targets, oldtargets) == {'2': 1, '7': 1, '9': -1}") + canonical = json.dumps(candidate, sort_keys=True, separators=(',', ':')).encode() + receipt = dict(status='PASS_EXACT_SCALAR_CHART_OWNERSHIP', source_head='a5348f7143f95fe0046b92b96172e30763c7d731', source_canonical_sha256=sha256(source_bytes).hexdigest(), word_canonical_sha256=sha256(canonical).hexdigest(), public_inputs=n + 1, owned_fields=candidate['owned_fields'], owned_lifetimes=lifetimes, owned_peak=peak, events=len(program), initial_ordinary_adds=prefix_count, cleanup_adds=len(cleanup), scalar_allowance=scalar, local_paid=dict(paid), local_targets=dict(targets), paid_delta=delta(paid, oldpaid), target_delta=delta(targets, oldtargets), signed_target_minus_paid_delta={'2': 1, '7': 1, '9': -1}, h={str(r): str(q) for r, q in sorted(h.items())}, full9_cleanup={str(r): str(q) for r, q in sorted(correction.items())}, scope='All753 rational input columns/endpoints plus exact frame containment and owned intervals. Native maps, full caller, ordinary compiler and complete pricing remain unrun.') + return (candidate, receipt) + + +def construct(source): + """Reconstruct one pinned split and commute its normalization to an actual meeting.""" + word,witness=_construct_terminal(source) + intermediate=sha256(json.dumps(word,sort_keys=True,separators=(',',':')).encode()).hexdigest() + need(intermediate=='892cfd5907ee1420b40cd511098c48eb3251501a7e6196367b3bfb4189e5d1a6','Exact terminal split witness') + p=word['program'];fresh=word['public']-1 + restores=[['ADD',126,fresh,'2',127],['ADD',188,fresh,'-2',127]] + need(p[-120:-118]==restores,'Actual terminal normalization order') + need(all(e[0]=='ADD' and e[1]==fresh and e[-1]==127 for e in p[-118:]),'Actual118-term terminal cleanup') + body=p[:-120] + anchor=['ADD',fresh,146,'1/2',127] + need(body.count(anchor)==1,'Unique actual146 correction version') + at=body.index(anchor) + need(at==17523,'Exact candidate correction event') + for event in body[at+1:]: + need(not (event[0] in ('ADD','COPY') and event[2] in (126,188,fresh)),'No later reads from normalized fields') + need(event[1]!=fresh,'No later continuation write') + if event[1] in (126,188): + need(event[0]=='ADD' and event[-1]==127,'Normalization commutes with later destination ADDs') + inserted=restores+[['ADD',fresh,146,'-1/2',127]] + word['program']=body[:at+1]+inserted+body[at+1:] + word['schema']='p104-terminal-main-split-short-cleanup/1' + canonical=json.dumps(word,sort_keys=True,separators=(',',':')).encode() + digest=sha256(canonical).hexdigest() + need(digest=='a1c8277189a811546bdc7b147d72e6a594504ff9585c9bf59a5681aa873abb01','Frozen final candidate') + def scalar_cost(e): + op=e[0] + if op=='MOVE':return 0 + if op in ('INIT','CLEAR'):return 2 + q=Q(e[-2]);a,b=abs(q.numerator),q.denominator + if op=='SCALE':return 2*(abs(a.bit_length()-b.bit_length())+(q<0)) + return 2*(2+a.bit_length()+a.bit_count()+b.bit_length()-1) + scalar=sum(scalar_cost(e) for e in word['program']) + need(scalar==221474 and len(word['program'])==25546,'Literal final scalar/event counts') + witness=dict(witness) + witness['terminal_intermediate_canonical_sha256']=intermediate + witness['terminal_full9_cleanup']=witness.pop('full9_cleanup') + witness['terminal_cleanup_adds']=witness.pop('cleanup_adds') + witness.update(word_canonical_sha256=digest,events=len(word['program']),scalar_allowance=scalar, + after_candidate_event=at,cleanup_anchor=anchor,early_cleanup=inserted, + removed_terminal_events=120,early_cleanup_adds=3, + scope='Exact source-bound split, frame/ownership/invoice checks, then a validated three-operation temporal normalization. Independent full final scalar and native/caller/pricing checks are separate obligations.') + return word,witness diff --git a/research/p104-two-boundary-helper-split/evidence/independent-boundary-receipt.json b/research/p104-two-boundary-helper-split/evidence/independent-boundary-receipt.json new file mode 100644 index 0000000000..2ff3807f9d --- /dev/null +++ b/research/p104-two-boundary-helper-split/evidence/independent-boundary-receipt.json @@ -0,0 +1,12 @@ +{ + "status": "PASS_INDEPENDENT_TERMINAL_VARIANT_MATCH", + "cleanup_terms": 118, + "word_canonical_sha256": "892cfd5907ee1420b40cd511098c48eb3251501a7e6196367b3bfb4189e5d1a6", + "paid_delta": {}, + "target_delta": { + "2": 1, + "7": 1, + "9": -1 + }, + "scope": "118-term adjoint correction and h match independently; no added continuation MOVE and no added paid rank. Root owns full replay." +} diff --git a/research/p104-two-boundary-helper-split/evidence/independent-caller-receipt.json b/research/p104-two-boundary-helper-split/evidence/independent-caller-receipt.json new file mode 100644 index 0000000000..f5dc48b2dc --- /dev/null +++ b/research/p104-two-boundary-helper-split/evidence/independent-caller-receipt.json @@ -0,0 +1,40 @@ +{ + "candidate_canonical_sha256": "a1c8277189a811546bdc7b147d72e6a594504ff9585c9bf59a5681aa873abb01", + "checker_reference": "PR5717 at41fda9302e5de79911b0c91c6161beaf386798b3", + "controls": { + "exterior_sign": "literal complete free-Laurent endpoint and exterior signs", + "global_phase": "nonzero absolute spectral phase", + "helper_alias_collision": "helper output alias collision", + "laurent_exponent_overflow": "Laurent exponent overflow rejected, never wrapped", + "lost_idle": "literal complete free-Laurent endpoint and exterior signs", + "missing_final_main_translation": "missing final main translation", + "missing_inverse_Q_correction": "literal clear/copy/positive-child/correct/add/clear chronology", + "omitted_contact_translation": "missing nonzero physical contact translation", + "overlapping_local_owned_alias": "Overlapping owned lifetime alias", + "owned_lifetime": "owned query/source/destination separation", + "owned_marked_productive": "Distinct independent public roles", + "reused_owned_label_before_clear": "Owned initialization chronology", + "stale_independent_inventory": "Every field is independent or owned", + "stale_source_lifetime_inventory": "Independently recounted input and lifetime inventory", + "thin_query_overlaps_local_owned": "Caller owned intervals cannot overlap on one field", + "wrong_route": "contact absolute/quadratic phase" + }, + "native_checks": { + "distinct_signed_Pauli_and_independent_phase_anchors": 306, + "fresh_helpers": 9648, + "owned_peak": 2 + }, + "ordinary": { + "abstract_address_phase_scalar_pass_upper": 124341508, + "local_contact_pass_bound": 306, + "machine_and_precision_admitted": false, + "main_map_pair_pass_bound": 699, + "meaning": "fixed finite descriptor passes under retained per-pass/tape contract; not a new tape or precision theorem", + "paid_native_maps_replayed": false, + "retained_raw_scalar_upper": 184647552 + }, + "output_sha256": "fea5c02bde0fef9a424da9dffb70767c55c102b6324ce4b0ad83f0850cef8c64", + "paid": 66348, + "status": "PASS_CANDIDATE_SCOPED_CALLER", + "targets": 12976 +} diff --git a/research/p104-two-boundary-helper-split/evidence/independent-scalar-receipt.json b/research/p104-two-boundary-helper-split/evidence/independent-scalar-receipt.json new file mode 100644 index 0000000000..5ab83bf2af --- /dev/null +++ b/research/p104-two-boundary-helper-split/evidence/independent-scalar-receipt.json @@ -0,0 +1,38 @@ +{ + "status": "PASS_INDEPENDENT_ALL_753_SCALAR_COLUMNS_AND_OWNERSHIP", + "candidate_canonical_sha256": "a1c8277189a811546bdc7b147d72e6a594504ff9585c9bf59a5681aa873abb01", + "fields": 753, + "independent_public": 744, + "dirty_owned": 9, + "events": 25546, + "peak_sparse_row_terms": 193, + "owned_lifetimes": 11, + "owned_peak": 2, + "paid": { + "1": 2184, + "2": 459, + "5": 159, + "4": 92, + "3": 495, + "7": 15, + "6": 22 + }, + "helpers": { + "9": 411, + "2": 5, + "8": 15, + "4": 91, + "5": 6, + "7": 6, + "1": 2 + }, + "paid_delta": {}, + "target_delta": { + "2": 1, + "7": 1, + "9": -1 + }, + "scalar_allowance": 221474, + "local_route_allowance": 5166000, + "scope": "Full exact rational scalar endpoints with independent dirty owned inputs, actual binary coframes and ownership, signed inventory and scalar/routing recount. No native/caller/compiler/pricing claim." +} diff --git a/research/p104-two-boundary-helper-split/evidence/independent-version-receipt.json b/research/p104-two-boundary-helper-split/evidence/independent-version-receipt.json new file mode 100644 index 0000000000..8e967beadc --- /dev/null +++ b/research/p104-two-boundary-helper-split/evidence/independent-version-receipt.json @@ -0,0 +1,21 @@ +{ + "status": "PASS_EXACT_SHORT_CLEANUP_CURRENT_VERSIONS", + "source_event": 17433, + "candidate_event": 17523, + "source_146_terms": 118, + "source_g_terms": 118, + "identities": [ + "g=a-e708=-current146/2", + "candidate_current146=source_current146", + "fresh_before=z", + "fresh_after=z+current146/2" + ], + "source_feedback_coordinates": [ + 126, + 188, + 708 + ], + "all_feedback_coefficients_zero": true, + "candidate_canonical_sha256": "a1c8277189a811546bdc7b147d72e6a594504ff9585c9bf59a5681aa873abb01", + "scope": "Exact current-version scalar identities only; no native/caller/pricing replay." +} diff --git a/research/p104-two-boundary-helper-split/inputs/pr5713-source.tar b/research/p104-two-boundary-helper-split/inputs/pr5713-source.tar new file mode 100644 index 0000000000..ec8f4bccac Binary files /dev/null and b/research/p104-two-boundary-helper-split/inputs/pr5713-source.tar differ diff --git a/research/p104-two-boundary-helper-split/pricing.py b/research/p104-two-boundary-helper-split/pricing.py new file mode 100644 index 0000000000..737aa1906e --- /dev/null +++ b/research/p104-two-boundary-helper-split/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('31102457/10000000000'), Q('622049141/200000000000') +PREVIOUS = Q('.00310915222') + + +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()) == 12976 and sum(paid.values()) == 66348, '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':'0.00311024570','previous_open_pr5713':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-two-boundary-helper-split/sources.py b/research/p104-two-boundary-helper-split/sources.py new file mode 100644 index 0000000000..65b9ac26ab --- /dev/null +++ b/research/p104-two-boundary-helper-split/sources.py @@ -0,0 +1,73 @@ +"""Authenticate the retained PR5713 export before any source import. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Rebound to PR5713 by flyingviper with substantial OpenAI Codex assistance. +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(): + pins = json.loads((HERE/'SOURCES.json').read_bytes()) + for row in pins['direct_sources']: + payload = (HERE/row['local_path']).read_bytes() + need(sha256(payload).hexdigest() == row['sha256'], 'Exact direct source SHA256') + need(sha1(b'blob '+str(len(payload)).encode()+b'\0'+payload).hexdigest() == row['git_blob'], + 'Exact direct source Git blob') + pin = pins['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-paid-main-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') + origins = {row['path']: row for row in pins['archived_files']} + for row in manifest['files']: + origin = origins[row['path']] + need(origin['pin'] == 'head:'+pin['commit']+':'+row['path'] + and origin['sha256'] == row['sha256'], + 'Export payload has an exact source pin') + 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-two-boundary-helper-split/verify.py b/research/p104-two-boundary-helper-split/verify.py new file mode 100644 index 0000000000..77f203216a --- /dev/null +++ b/research/p104-two-boundary-helper-split/verify.py @@ -0,0 +1,104 @@ +"""Replay the two-boundary helper split and complete conditional exponent invoice. + +Prepared for flyingviper with substantial OpenAI Codex assistance. Apache-2.0. +The full local, native, caller and price engines retain predecessor attribution. +""" +import argparse +from contextlib import ExitStack +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 +import checks + + +def reject(action): + try: + action() + except ValueError as error: + return str(error) + raise ValueError('Invalid invoice accepted') + + +def run(): + with ExitStack() as contexts: + parent, _ = contexts.enter_context(sources()) + cursor = parent + for depth in range(3): + module = load(cursor/'sources.py', 'two_boundary_split_sources_'+str(depth)) + cursor, root = contexts.enter_context(module.sources()) + L = load(cursor/'local.py', 'local') + L.ROOT = root + source = L.read(parent/'WORD.json.gz') + word, witness = construct.construct(source) + independent = checks.audit(word) + controls = checks.negative_controls(word, witness) + local = L.replay(word) + columns = L.reverse_columns(word) + need(local['public_inputs'] == 744 and local['owned_fields'] == 9 + and local['owned_lifetimes'] == 11 and local['peak_owned_fields'] == 2, + 'Exact public/owned lifetime inventory') + print('PASS all 753 scalar columns, literal charts and actual repair controls', flush=True) + native = L.native(word) + C = load(root/'research/p104-productive-controller/caller.py', 'two_boundary_split_caller') + caller = C.construct() + need(caller == L.read(root/'research/p104-productive-controller/CONTROLLER.json'), + 'Retained complete physical caller') + physical = C.physical(caller, word) + print('PASS all 2917 native maps, phases and complete physical caller', flush=True) + text = (parent/'pricing.py').read_text(encoding='utf-8') + for before, after in L.read(HERE/'PRICING-EDITS.json'): + need(text.count(before) == 1, 'Unique declared pricing edit') + text = text.replace(before, after) + need(text == (HERE/'pricing.py').read_text(encoding='utf-8'), + 'Only declared complete pricing edits') + P = load(HERE/'pricing.py', 'two_boundary_split_price') + price = P.run(local, native, caller, physical) + controls.update(C.controls(caller)) + bad = deepcopy(local) + bad['paid'][7] -= 1 + controls['unpaid_rank7_query'] = reject(lambda: P.assemble(bad, native, caller, physical)) + bad = deepcopy(local) + bad['helpers'][9] += 1 + controls['invented_extra_H9_target'] = reject(lambda: P.assemble(bad, native, caller, physical)) + result = {'status': 'PASS_P104_TWO_BOUNDARY_SPLIT_KAPPA_00311024570', + 'source_commit': 'a5348f7143f95fe0046b92b96172e30763c7d731', + 'local': local, 'separate_columns': columns, 'native': native, + 'physical_caller': physical, 'complete_cost': price, + 'independent_literal_audit': independent, 'negative_controls': controls, + 'limits': ['The five inherited framework assumptions remain.', + 'No selected-frontier admission or large improvement is claimed.', + 'The huge uniform word and complete rounded multiplier are not materialized.', + 'Independent agent checks are not human or formal acceptance.']} + return P.encode(result), P.encode(witness), word + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + with tempfile.TemporaryDirectory(prefix='p104-two-boundary-bytecode-') as cache: + sys.pycache_prefix = cache + result, witness, word = run() + for name, value in (('RESULT.json', result), ('WITNESS.json', witness), ('WORD.json.gz', word)): + path = HERE/name + if args.write: + raw = (json.dumps(value, sort_keys=True, indent=2)+'\n').encode() + path.write_bytes(gzip.compress(raw, mtime=0) if name.endswith('.gz') else raw) + else: + raw = path.read_bytes() + need(json.loads(gzip.decompress(raw) if name.endswith('.gz') else raw) == value, + 'Complete retained output: '+name) + print(result['status']) + + +if __name__ == '__main__': + main()