diff --git a/research/p104-temporal-updates/NOTICE b/research/p104-temporal-updates/NOTICE new file mode 100644 index 0000000000..36c1b859be --- /dev/null +++ b/research/p104-temporal-updates/NOTICE @@ -0,0 +1,44 @@ +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. diff --git a/research/p104-temporal-updates/PRICING-EDITS.json b/research/p104-temporal-updates/PRICING-EDITS.json new file mode 100644 index 0000000000..a8dce0d2f6 --- /dev/null +++ b/research/p104-temporal-updates/PRICING-EDITS.json @@ -0,0 +1,18 @@ +[ + [ + "KAPPA, TESTED = Q('.00310871312'), Q('.003108713125')", + "KAPPA, TESTED = Q('155457611/50000000000'), Q('124366089/40000000000')" + ], + [ + "PREVIOUS = Q('.00310815849')", + "PREVIOUS = Q('.00310871312')" + ], + [ + "sum(paid.values()) == 66366", + "sum(paid.values()) == 66348" + ], + [ + "'kappa_decimal':'.00310871312'", + "'kappa_decimal':'0.00310915222'" + ] +] diff --git a/research/p104-temporal-updates/PROOF.md b/research/p104-temporal-updates/PROOF.md new file mode 100644 index 0000000000..308d19427b --- /dev/null +++ b/research/p104-temporal-updates/PROOF.md @@ -0,0 +1,154 @@ +# Proof and complete price + +Prepared for Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +## 1. Sources and claim + +The input is PR5684 at `d0f6fa2555410a1e23fe4191424c2097ab3d5d97`. +Its word, constructor, price and attribution are retained without edits. +The official 16-file export of PR5678 at +`af814f6f3c477fdd13b8f04380a33cf32004966b` retains the full checker stack, +including its exact predecessor archives. Authentication precedes source imports. +Every exported file has a separate Git source pin. The generated archive has +its own fixed integrity hashes; those hashes do not claim a pre-existing +upstream archive object. Base main is `df0137efd35e11b4445734bf612bdd4c7ebc330c`. + +The claim is a complete **conditional** construction at kappa .00310915222. +It preserves the source five framework assumptions. It does not change the +selected frontier, prove a global optimum or give a practical runtime claim. + +## 2. A temporal update lemma + +Use decoded scalar coordinates for a fixed native word. A cut `c` is immediately +before source event `c`. Suppose field `r` is not read in `[a,b)`. Its operations +in that interval are ADDs into `r` and changes of its native chart. In particular, +there is no SCALE, COPY, initialization or erasure of `r` in the interval. + +Remove some ADDs into `r`. Let their total scalar source functional be `g`. +Suppose actual fields `s_j`, at cuts `c_j` in `[a,b]`, satisfy + +`g = sum_j q_j value(s_j, c_j)`. + +Require `s_j != r` and an actual common frame for each replacement ADD into `r`. +Insert those ADDs at their declared cuts. Every other field follows its original +trajectory: no original operation reads the changed field in the interval. +The replacement sources therefore have their original values. The difference +in `r` is the accumulated replacement sum minus the removed sum. It is zero +at cut `b`, before its next read. The full endpoint is unchanged. + +This is an exact linear-circuit identity. No old value is stored or read later +without an operation. Each source is read at its declared physical cut. +Native transports still use their actual charts and phases. Their decoded action +is the identity under the retained native contract. The native replay checks the +changed transport separately; scalar reasoning does not waive that obligation. + +## 3. The fixed witness + +All event positions below are zero-based in the pinned PR5684 word. +Take `r=715`, `a=823` and `b=14983`. Remove event 13578, +`ADD 715, 747, 1`, at frame 598. The exact prefix calculation proves + +``` +value(747,13578) + = value(525,823)/4 - value(712,823) + - value(525,14983)/4 + value(340,14983)/4. +``` + +The identity also has a short direct derivation. Let `A=value(525,823)`, +`B=value(712,823)`, `V=value(747,13578)` and `C=value(340,14983)`. +Field 712 has only one write in the interval: event 13572 adds `V`. +The owned value is unchanged between that read and event 13578. +Field 525 has only two writes: event 13737 subtracts four times field 712, +and event 14654 adds field 340. Field 340 has no write from event 11202 +through cut 14983, so that last added value is `C`. +Consequently `value(525,14983)=A-4(B+V)+C`. Rearrangement gives the identity. +The complete prefix check independently confirms all 105 source coefficients. + +The first two replacement ADDs use frame 3. The last two use frame 396. +Each source and field 715 have that frame at the stated cut. There is no read +of715 in `[823,14983)`. Event14983 is the next read, `ADD 340,715,-4`. +The verifier calculates every coefficient of the displayed identity over Q, +and separately checks the no-read condition and all common frames. + +Remove event 13577, `MOVE 715,3,598`, and change event 14982 from +`MOVE 715,598,396` to `MOVE 715,3,396`. The old frame dimensions are0,1,3, +and their binary spaces form a strict chain. Thus the two old queries H1,H2 +become one H3. All other source records remain in order and unchanged. +Four ADDs replace one ADD, so the emitted word has 25453 records. +The complete rational replay and a separate dense transpose replay check all +565504 endpoint coefficients. All743 public inputs remain independent; +9 owned fields have11 lifetimes and peak occupancy2. + +The alternative rewrite found on field 525 has the same price. It is not added +to this gain. A further scan of771 single visits and214 joint visit sets on +the changed word found no additional gain in that tested domain. These discovery +screens are not an optimality certificate and are not proof inputs. + +## 4. Native and ordinary costs + +The retained exact native engine lowers every paid request, main adapter and +helper normalizer, including absolute phase. It checks 2917 distinct native maps. +All original helper endpoints and the actual18-call physical caller stay fixed. +All eight owned H7 queries remain; the removed ADD only changes one recipient. +The original centre erasures, other reads, COPY instructions and ownership +contracts remain in the word. + +The local paid profile is + +``` +2184 H1 +459 H2 +495 H3 +92 H4 +159 H5 +22 H6 +15 H7. +``` + +The unchanged local productive profile is + +``` +2 H1 +4 H2 +91 H4 +6 H5 +5 H7 +15 H8 +412 H9. +``` + +The exact local scalar allowance is220326. Native routes and adapters have a +separate allowance 5164000. Their sum stays below the retained local budget 10^7. +The complete raw ordinary upper bound is184647552, below 10^9. The fixed scalar +growth and native tensor growth bounds are unchanged. Thus no new history bank, +free query, uncharged route, COPY, CLEAR or storage lifetime is introduced. + +## 5. Complete moment, compiler and outer ledger + +The literal caller has 18 forward local calls,15 paid rank-one query shears and +3120 whole idle jobs. It has 66348 paid calls and12958 productive fields. +The target-minus-paid rank mass is760. The complete change from PR5684 is + +`Delta P = -18 H1 -18 H2 +18 H3`, `Delta T = 0`. + +For every `00`, by strict subadditivity. Hence the changed +bill strictly improves every such signed moment. The proof does not add PR +root decimals or use unchanged target credit after a helper removal. +Two exact rational interval engines verify the full invoice. The unique raw +root in the retained interval below .0034 lies in + +`(.00310915224562, .00310915224563)`. + +The declared kappa is .00310915222. The tested saving is .003109152225. +The remaining raw headroom is between .00000000002562 and .00000000002563. +This is a ceiling for this fixed invoice in the certified interval, not a +ceiling for other constructions. + +The retained completion proof is re-evaluated with cutoff 17, floor 18, +tail offset 1/5, tensor power 1024 and reserve 10^-12. All three tail ratios, +splitting, rounding, complement capacity and shifted exits pass. The finite +compiler threshold is calculated on its exact integer grid and its immediate +predecessor fails. All54 strict outer inequalities and all 4 functional checks +pass. The unchanged ordinary BIT input is admitted at .0034. Its full cover, +atom and stock obligations remain charged through the retained ledger. + +The claim exceeds PR5684 by .00000043910, about .01412482 percent. +This modest gain is the result supplied here. A large breakthrough is open. + +## 6. Limits and next checks + +The all-column native extension, owned-erasure contract, uniform compiler, +precision/tape prescriptions and analytic/recovery framework remain assumptions. +The enormous uniform word and complete rounded multiplier are not executed. +The source receipts and new finite checks do not imply independent human or +proof-kernel acceptance. Independent verification of the temporal identity and +its complete bill is the next review task. A larger construction must keep the +same distinction between an exact scalar identity and a fully paid caller. diff --git a/research/p104-temporal-updates/README.md b/research/p104-temporal-updates/README.md new file mode 100644 index 0000000000..fae45de92d --- /dev/null +++ b/research/p104-temporal-updates/README.md @@ -0,0 +1,56 @@ +# Distributed scalar updates: conditional kappa .00310915222 + +The new construction replaces one read from owned centre 747 by four ordinary +updates at two other contacts. The target field 715 is not read between those +contacts. Their exact sum gives the old update before the next read. +This removes an intermediate frame visit and replaces one H1 plus one H2 +query by one H3 query. Every public input and productive target is retained. + +The complete conditional saving is **kappa = .00310915222**, compared with +**.00310871312** in [PR5684](https://github.com/CrocSwap/integer-mult-bounds/pull/5684). +The gain is **.00000043910**, about **.01412482 percent**. This is a small gain, +not the requested large breakthrough. It changes the scalar program and the +complete paid bill; it does not combine the published decimals of other PRs. + +[PROOF.md](PROOF.md) gives the temporal identity and full cost argument. +[WITNESS.json](WITNESS.json) fixes the cuts, sources and source event positions. +[construct.py](construct.py) checks the identity and emits the complete word. +[RESULT.json](RESULT.json) records exact endpoint, native, caller, compiler and +outer evidence. [SOURCES.json](SOURCES.json) pins the complete source closure. + +```sh +python3.12 -B scripts/research_package.py --package research/p104-temporal-updates +``` + +Expected: `PASS_P104_TEMPORAL_UPDATES_KAPPA_00310915222` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. Python 3.12 and its standard library suffice. +No optimizer, network access or Git process is used by the scientific verifier. +The package exporter gives a separate Git-free replay. + +The complete invoice has 66348 paid calls and12958 productive targets. +The whole change is `-18 H1 -18 H2 +18 H3`, with no target change. +All eight H7 centre queries remain paid. This is not a centre-query deletion. +The raw root lies strictly in `(.00310915224562, .00310915224563)`. +[VALIDATION.md](VALIDATION.md) separates checks that ran from pending review. + +The five inherited native, owned-erasure, compiler, precision/tape and +analytic/recovery assumptions remain. The huge uniform word and complete +rounded multiplier are not materialized. Author checks do not establish +independent human or proof-kernel acceptance. The selected frontier is unchanged. + +Credit Joel Pulikkan/GamingPuzzled with Claude assistance for PR5684, +Ali Romman's PR5678/5660 and complete caller lineage, zxv, Cao Yifan, +Cinna Davis, Jacob Alan Sussman and every retained source notice. +New construction, proof and verification: Ali Romman with substantial OpenAI +Codex assistance. No subagents. Apache-2.0. + +## Open next questions + +- Independently check the fixed temporal identity, exact native maps and complete + price. Start with the source event positions in WITNESS.json. There is no known + technical blocker; independent acceptance remains open. +- Find a distributed update that removes a complete centre query or gives a + larger gain. Include every intervening target read, source dependency and + replacement native path. No such positive construction is supplied here. +- Resolve one inherited framework assumption through the selected record and + its proof review. This finite package does not close those obligations. diff --git a/research/p104-temporal-updates/RESULT.json b/research/p104-temporal-updates/RESULT.json new file mode 100644 index 0000000000..8fc639f9b3 --- /dev/null +++ b/research/p104-temporal-updates/RESULT.json @@ -0,0 +1,404 @@ +{ + "complete_cost": { + "compiler": { + "H": 80511200000000000, + "N": "2^80511200000000000", + "eta": { + "lower": "0.000000131022217212430301374984", + "upper": "0.000000131022217212430301374985" + }, + "gap": "1/1400000000000", + "integer_test_exponent": 57508, + "logarithm_power": 1024, + "theta": "63/64", + "uniform_saving": "2176406557/700000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "4391/10000000000", + "kappa": "155457611/50000000000", + "kappa_decimal": "0.00310915222", + "margin_at_previous": { + "lower": "0.106625834236318763156961686328", + "upper": "0.106625834236318763156961686329" + }, + "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": 5164000, + "local_scalar": 220326, + "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": "6093938356795647186889/1960000000000000000000000", + "fused_gaussian": "6093938356786941560667/1960000000000000000000000", + "global_coordinate_router": "544101639/175000000000", + "group_bit_router": "761742294773367695083/245000000000000000000000", + "group_scans": "699999999999/700000000000", + "main_transform": "6093938355395647186889/1960000000000000000000000", + "microbox_face_corrections": "26950000000001/350000000000", + "polynomial_products": "1399999999999/1400000000000", + "sparse_union_movement": "802343938356795647186889/1960000000000000000000000" + }, + "parameters": { + "a": "544101639/175000000000", + "b": "4352813113/1400000000000", + "beta": "1399999999997/1400000000000", + "bit_saving": "17/5000", + "cap_xi": "1782343938355395647186889/1960000000000000000000000", + "complex_uniform_saving": "2176406557/700000000000", + "d": "1/1400000000000", + "epsilon": "1399999999999/1400000000000", + "kappa": "155457611/50000000000", + "lambda_": "398756339111/400000000000", + "lambda_prime": "1395647186889/1400000000000", + "layout": "1/1400000000000", + "q": "4352813111/1400000000000", + "r0": "1/14000000000000", + "stop": "1/1400000000000", + "tested_saving": "124366089/40000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "50898361/175000000000", + "actual_logarithmic_gamma_guard": "1/1400000000000", + "actual_logarithmic_group_guard": "177656061646704352813111/980000000000000000000000", + "alpha_logarithm_absorption": "1/14000000000000", + "boundary_algebraic_matrix_above_kappa": "5595647186889/1960000000000000000000000", + "cap_above_band": "802343938355395647186889/1960000000000000000000000", + "cap_below_cell": "177656061643204352813111/1960000000000000000000000", + "cap_below_phase_cell_power": "2137656061644604352813111/1960000000000000000000000", + "complex_above_effective": "1/1400000000000", + "complex_below_one_over_32": "39397186887/1400000000000", + "complex_endpoint": "1/700000000000", + "epsilon_below_one": "1/1400000000000", + "epsilon_positive": "1399999999999/1400000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "5586941560667/1960000000000000000000000", + "gaussian_above_main": "695647186889/980000000000000000000000", + "global_coordinate_router_above_kappa": "1/350000000000", + "global_gamma_power_slack": "9/14000000000000", + "group_below_dimension": "1/700000000000", + "group_bit_router_above_kappa": "873367695083/245000000000000000000000", + "group_gauge_power_slack": "177656061646634352813111/980000000000000000000000", + "group_key_fits_record": "1/700000000000", + "group_positive": "1399999999997/1400000000000", + "group_scans_above_kappa": "139564718689/140000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "689090900400418148631/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": "2795647186887/1960000000000000000000000", + "leaf_saving_above_effective": "1395647186887/1960000000000000000000000", + "main_transform_above_kappa": "4195647186889/1960000000000000000000000", + "membership_arithmetic_fits_record": "1/1400000000000", + "microbox_face_corrections_above_kappa": "6737227949181/87500000000", + "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": "1395647186891/1400000000000", + "positive_layout_slack": "1/1400000000000", + "q_below_effective": "1/1400000000000", + "q_below_internal": "1/1400000000000", + "q_below_leaf": "2795647186887/1960000000000000000000000", + "q_positive": "4352813111/1400000000000", + "short_record_fallback": "1395647186887/1400000000000", + "source_axis_superpolynomial": "1/1400000000000", + "sparse_union_movement_above_kappa": "796250000005595647186889/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_pr5660": "19429457/6250000000", + "productive_fields": 12958, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_ceiling": { + "derivative_upper": "-739527737203957000275288525290373783419970457168925055914772323/3138550867693340381917894711603833208051177722232017256448", + "interval": [ + "0", + "17/5000" + ] + }, + "raw_headroom": [ + "1281/50000000000000", + "2563/100000000000000" + ], + "raw_root_interval": [ + "155457612281/50000000000000", + "310915224563/100000000000000" + ], + "relative_gain_percent": "548875/38858914", + "strictification": { + "alpha": { + "lower": "0.999999999979045390727904314922", + "upper": "0.999999999979045390727904314923" + }, + "cutoff": 17, + "delta": { + "lower": "0.967460429302773034801102736481", + "upper": "0.967460429302773034801102736482" + }, + "floor": 18, + "gamma": { + "lower": "0.968263729732811178316707419523", + "upper": "0.968263729732811178316707419524" + }, + "normalized_paid_upper": "1048576000976562501/1048576001073741824", + "power": 1024, + "reserve": "1/1000000000000", + "tail_block": 128, + "tail_decay": "39/40", + "tail_offset": "1/5", + "tested": "124366089/40000000000" + }, + "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": 270, + "9": 7416 + }, + "whole_idle_jobs": 3120 + }, + "limits": [ + "The five inherited framework assumptions remain.", + "The complete rounded multiplier and huge uniform word are not materialized.", + "Author checks do not establish independent scientific acceptance.", + "The gain is small. No large gain or global optimum is claimed." + ], + "local": { + "endpoint_coefficients": 565504, + "helpers": { + "1": 2, + "2": 4, + "4": 91, + "5": 6, + "7": 5, + "8": 15, + "9": 412 + }, + "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": 743, + "real_scalar_allowance": 220326 + }, + "local_helper_delta": {}, + "local_paid_delta": { + "1": -1, + "2": -1, + "3": 1 + }, + "native": { + "distinct_maps": 2917, + "helper_normalizers": 1070, + "helpers": { + "1": 2, + "2": 4, + "4": 91, + "5": 6, + "7": 5, + "8": 15, + "9": 412 + }, + "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": { + "extra_target": "Every productive helper has a native target", + "interval_crosses_target_read": "No original instruction reads the changed target", + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "missing_late_update": "Exact distributed source functional", + "missing_native_transport": "Scalar destination and coefficient", + "missing_owned_erasure": "All public and owned exits", + "unpaid_query": "Complete field and call counts", + "wrong_common_frame": "Each replacement has an actual common frame", + "wrong_history_sign": "Exact distributed source functional" + }, + "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": "d0f6fa2555410a1e23fe4191424c2097ab3d5d97", + "source_local": { + "endpoint_coefficients": 565504, + "helpers": { + "1": 2, + "2": 4, + "4": 91, + "5": 6, + "7": 5, + "8": 15, + "9": 412 + }, + "owned_fields": 9, + "owned_lifetimes": 11, + "paid": { + "1": 2185, + "2": 460, + "3": 494, + "4": 92, + "5": 159, + "6": 22, + "7": 15 + }, + "paid_rank_mass": 5987, + "peak_owned_fields": 2, + "public_inputs": 743, + "real_scalar_allowance": 220290 + }, + "status": "PASS_P104_TEMPORAL_UPDATES_KAPPA_00310915222", + "temporal_identity": { + "observations": [ + [ + 823, + 525, + 3, + 1 + ], + [ + 823, + 712, + 3, + 1 + ], + [ + 14983, + 525, + 396, + 106 + ], + [ + 14983, + 340, + 396, + 7 + ] + ], + "removed_event": 13578, + "role": 715, + "source_coefficients": 105, + "source_sha256": "cddffb3e9a025e4a68c44ef66cc5c88b2d8eb88c6180415d7552f04ff6a48689", + "start": 823, + "stop": 14983 + } +} diff --git a/research/p104-temporal-updates/SOURCES.json b/research/p104-temporal-updates/SOURCES.json new file mode 100644 index 0000000000..d7d9ab3b6c --- /dev/null +++ b/research/p104-temporal-updates/SOURCES.json @@ -0,0 +1,212 @@ +{ + "attribution": "PR5684 supplies the exact source word. PR5678 supplies the closed checker and framework stack. All source notices are retained. Distributed scalar updates and their full price are by Ali Romman with substantial OpenAI Codex assistance. No subagents.", + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "direct_sources": [ + { + "commit": "d0f6fa2555410a1e23fe4191424c2097ab3d5d97", + "git_blob": "fa0bd1401f5775f4351cfa23b08f3998dba6129e", + "local_path": "inputs/pr5684/NOTICE", + "sha256": "e8e0cabef6cf40d63f3cea3b6403dfd1af8727e40df03f09b2932718bcddc1b0", + "source_path": "research/p104-reframe-r22/NOTICE" + }, + { + "commit": "d0f6fa2555410a1e23fe4191424c2097ab3d5d97", + "git_blob": "e80d32af1801c3dcf97f0904f7c3cecc9d3ca418", + "local_path": "inputs/pr5684/README.md", + "sha256": "1e75a8e010f6e22406f9cdd84c2d07c7c8a92b4b9436b4e2afd6f8defd3ff201", + "source_path": "research/p104-reframe-r22/README.md" + }, + { + "commit": "d0f6fa2555410a1e23fe4191424c2097ab3d5d97", + "git_blob": "f3fb0e2144ec8a5c3407e4eaa6528bb3436ba573", + "local_path": "inputs/pr5684/WORD.json.gz", + "sha256": "d6db1d0d97b13ea483a462c65437664d15d34dec56c3682cf6e1de31266ec6c2", + "source_path": "research/p104-reframe-r22/WORD.json.gz" + }, + { + "commit": "d0f6fa2555410a1e23fe4191424c2097ab3d5d97", + "git_blob": "3b0109e0fae47f1961238ed418821861a756ab56", + "local_path": "inputs/pr5684/construct.py", + "sha256": "b83fe6e745f18dede23328b5a670e582b2da23ed15ee83c8f78d71b9f40f8261", + "source_path": "research/p104-reframe-r22/construct.py" + }, + { + "commit": "d0f6fa2555410a1e23fe4191424c2097ab3d5d97", + "git_blob": "e817f4da7deb0120c51e10b98bdbf9f9c53fa57c", + "local_path": "inputs/pr5684/pricing.py", + "sha256": "b4edb4a45f30720956167c07d88b102e596dd6a001c7eced4d282d32225833e2", + "source_path": "research/p104-reframe-r22/pricing.py" + } + ], + "files": [ + { + "git_blob": "fa0bd1401f5775f4351cfa23b08f3998dba6129e", + "path": "research/p104-reframe-r22/NOTICE", + "pin": "head:d0f6fa2555410a1e23fe4191424c2097ab3d5d97:research/p104-reframe-r22/NOTICE", + "sha256": "e8e0cabef6cf40d63f3cea3b6403dfd1af8727e40df03f09b2932718bcddc1b0", + "usage": "provenance" + }, + { + "git_blob": "e80d32af1801c3dcf97f0904f7c3cecc9d3ca418", + "path": "research/p104-reframe-r22/README.md", + "pin": "head:d0f6fa2555410a1e23fe4191424c2097ab3d5d97:research/p104-reframe-r22/README.md", + "sha256": "1e75a8e010f6e22406f9cdd84c2d07c7c8a92b4b9436b4e2afd6f8defd3ff201", + "usage": "provenance" + }, + { + "git_blob": "f3fb0e2144ec8a5c3407e4eaa6528bb3436ba573", + "path": "research/p104-reframe-r22/WORD.json.gz", + "pin": "head:d0f6fa2555410a1e23fe4191424c2097ab3d5d97:research/p104-reframe-r22/WORD.json.gz", + "sha256": "d6db1d0d97b13ea483a462c65437664d15d34dec56c3682cf6e1de31266ec6c2", + "usage": "provenance" + }, + { + "git_blob": "3b0109e0fae47f1961238ed418821861a756ab56", + "path": "research/p104-reframe-r22/construct.py", + "pin": "head:d0f6fa2555410a1e23fe4191424c2097ab3d5d97:research/p104-reframe-r22/construct.py", + "sha256": "b83fe6e745f18dede23328b5a670e582b2da23ed15ee83c8f78d71b9f40f8261", + "usage": "provenance" + }, + { + "git_blob": "e817f4da7deb0120c51e10b98bdbf9f9c53fa57c", + "path": "research/p104-reframe-r22/pricing.py", + "pin": "head:d0f6fa2555410a1e23fe4191424c2097ab3d5d97:research/p104-reframe-r22/pricing.py", + "sha256": "b4edb4a45f30720956167c07d88b102e596dd6a001c7eced4d282d32225833e2", + "usage": "provenance" + }, + { + "git_blob": "fa0bd1401f5775f4351cfa23b08f3998dba6129e", + "path": "research/p104-paid-interior-bases/NOTICE", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/NOTICE", + "sha256": "e8e0cabef6cf40d63f3cea3b6403dfd1af8727e40df03f09b2932718bcddc1b0", + "usage": "provenance" + }, + { + "git_blob": "21f898d14e19b0bbef33eab7cf42d1bcdf3267cf", + "path": "research/p104-paid-interior-bases/PRICING-EDITS.json", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/PRICING-EDITS.json", + "sha256": "a4b4ca656610e07573bc5c058f91d3afe2a8b12d4d7cb1497f435c185063bff0", + "usage": "provenance" + }, + { + "git_blob": "77ef428c1ad8bc20690edecee92d8dd16c28ba52", + "path": "research/p104-paid-interior-bases/PROOF.md", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/PROOF.md", + "sha256": "a599f482ec35ddf84b1ddf72da92a6edbb77b9c4eccab6ffe31fdece2419f099", + "usage": "provenance" + }, + { + "git_blob": "4b3e17e186175c994c3b47ab42a1edeec59f747c", + "path": "research/p104-paid-interior-bases/README.md", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/README.md", + "sha256": "35b252cc37339041c4cf8851134781fe8e79739170b3bd6e536dc87d962cbd24", + "usage": "provenance" + }, + { + "git_blob": "d5a73ee8eceab0b4ac6850c06bca7152d3d6800e", + "path": "research/p104-paid-interior-bases/RESULT.json", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/RESULT.json", + "sha256": "ab036dc5fd6c1b19255d03007a858325a18bb7de12843687db74d85f146f5020", + "usage": "provenance" + }, + { + "git_blob": "5c13f25a07882c22c7e5ede4f1aaa5cfc94928da", + "path": "research/p104-paid-interior-bases/SOURCES.json", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/SOURCES.json", + "sha256": "d87d48095d56bdc26a2f86e05760915b2b341000e53c1f877d6348331f66dded", + "usage": "provenance" + }, + { + "git_blob": "65842d6cff0e5cc85b098c2e29a807fc5328e775", + "path": "research/p104-paid-interior-bases/TASK.json", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/TASK.json", + "sha256": "e9d942a3f062d1a183cbd947a968146c6a38102e1463f065e7fc1d0f24fc95cd", + "usage": "provenance" + }, + { + "git_blob": "11b30c4ba197db66ecb9ec8468ea892568aa9a0b", + "path": "research/p104-paid-interior-bases/VALIDATION.md", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/VALIDATION.md", + "sha256": "e5de967a8c8a0bde2436fa0b39778690bed1fe7751228a8ec6985053aa017e3f", + "usage": "provenance" + }, + { + "git_blob": "d1d1093b24979afa5d1d8b598529d09d92275222", + "path": "research/p104-paid-interior-bases/VERIFY.json", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/VERIFY.json", + "sha256": "2a70cf3a09fd82a92d12d9417223ef65a2dcb8e80b5b900d21ecf4d1f43257b0", + "usage": "provenance" + }, + { + "git_blob": "d3554cd80f0d7534c07b76dd64eadfb228c0c8d6", + "path": "research/p104-paid-interior-bases/WITNESS.json", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/WITNESS.json", + "sha256": "0753bc9933fbb954ec79b3d054b4f60bb3ee5c97801f426d4104da5fc5bc38b3", + "usage": "provenance" + }, + { + "git_blob": "8be2b3e1c2d02034d4579bef5d36df7761d826ff", + "path": "research/p104-paid-interior-bases/WORD.json.gz", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/WORD.json.gz", + "sha256": "b56281a67f84832198be2f2ad36d87b75244d424f1e0a6f4dda2df74f20cc08d", + "usage": "provenance" + }, + { + "git_blob": "ff4d7701fc1eaa7e31a9b937ac7f6c732c6634a9", + "path": "research/p104-paid-interior-bases/construct.py", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/construct.py", + "sha256": "ab9b0e00e67caac137477c0b8e646ba5604d02a7a0a297c4e3fce9e20105812e", + "usage": "provenance" + }, + { + "git_blob": "5b84cf23231082376660b7295744b64655039d8c", + "path": "research/p104-paid-interior-bases/inputs/pr5660-source.tar", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/inputs/pr5660-source.tar", + "sha256": "397b1f99061f670ed904198d0458808769c0a8693394bee0d9648f1f280d88d3", + "usage": "provenance" + }, + { + "git_blob": "83e015643b455135b1263bfb9c8d1690016e3276", + "path": "research/p104-paid-interior-bases/pricing.py", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/pricing.py", + "sha256": "0f333369792e7cbec5bbcfb5a6ec6577c2e766598bd6b7f3a9b5c7c3a616a52d", + "usage": "provenance" + }, + { + "git_blob": "108e075404ff04066172df27e71f55cd844cfc61", + "path": "research/p104-paid-interior-bases/sources.py", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/sources.py", + "sha256": "9c02f057d1153f202c142c543ef83c3e1555b771621d1da434069f8317b9f787", + "usage": "provenance" + }, + { + "git_blob": "47d103c523b334bd9c6261029089f37baa72abc7", + "path": "research/p104-paid-interior-bases/verify.py", + "pin": "head:af814f6f3c477fdd13b8f04380a33cf32004966b:research/p104-paid-interior-bases/verify.py", + "sha256": "28c11370ae7a11e073c58c75055085191358702256061bd963f0fd8ee16457da", + "usage": "provenance" + }, + { + "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" + } + ], + "schema_version": 1, + "source_export": { + "commit": "af814f6f3c477fdd13b8f04380a33cf32004966b", + "files": 16, + "git_blob": "cd87254d84b594ea7809e8106b26d01775e138e7", + "local_path": "inputs/pr5678-source.tar", + "package": "research/p104-paid-interior-bases", + "sha256": "edd6ce029b39abf2f72c28bbc377c9793ddf275e19f3f2b5a6cab0a65670161b", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5678" + } +} diff --git a/research/p104-temporal-updates/TASK.json b/research/p104-temporal-updates/TASK.json new file mode 100644 index 0000000000..d8c2c1d866 --- /dev/null +++ b/research/p104-temporal-updates/TASK.json @@ -0,0 +1,78 @@ +{ + "actual_scope": "Replace one P104 centre read by four scalar updates at two unobserved cuts. The complete conditional kappa is .00310915222.", + "ai_assistance": "Substantial OpenAI Codex assistance for algebra, exact scripts, source checks and writing. No subagents.", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "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, + "evidence": "PROOF.md, WITNESS.json, RESULT.json and VALIDATION.md", + "open_questions": [ + { + "blocked_by": "No known technical blocker.", + "first_step": "Replay the fixed witness and its source pins, then inspect the unobserved interval proof.", + "question": "Can an independent reviewer check the temporal identity and full price?", + "why_it_matters": "Author checks do not establish independent acceptance." + }, + { + "blocked_by": "No such positive construction is known.", + "first_step": "Find one complete distributed update with every later read and native cost included.", + "question": "Can this method remove a complete centre query or produce a large gain?", + "why_it_matters": "The current gain is small and leaves all eight H7 centre queries." + }, + { + "blocked_by": "The complete rounded multiplier and huge uniform word are not materialized.", + "first_step": "Use the selected record to choose one precise proof obligation.", + "question": "Can the five inherited framework assumptions be resolved?", + "why_it_matters": "The kappa result is 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": "A source value need not be delivered at one contact. Its exact linear functional can be distributed over an interval in which the target is not read.", + "scope_status": "changed", + "stop_rule": "Verify and publish the changed complete construction. A larger gain needs a new source-bound construction and full price.", + "task_id": "complex-new-helper-inventory" +} diff --git a/research/p104-temporal-updates/VALIDATION.md b/research/p104-temporal-updates/VALIDATION.md new file mode 100644 index 0000000000..b105d24f8f --- /dev/null +++ b/research/p104-temporal-updates/VALIDATION.md @@ -0,0 +1,41 @@ +# Validation record + +Base: df0137efd35e11b4445734bf612bdd4c7ebc330c. Environment: macOS arm64, +CPython 3.12.13, standard library. All native replays ran serially. + +The publication constructor generated the word and RESULT.json. Registered +normal and optimized replays passed with +`PASS_P104_TEMPORAL_UPDATES_KAPPA_00310915222` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. They checked the exact temporal identity, +all 565504 endpoint coefficients, the separate dense transpose, 2917 native +maps with absolute phase, the physical caller, both interval engines, +completion/compiler tests and all 54 strict plus 4 functional outer checks. +All nine semantic rejection controls passed. A separate copy with one changed +byte in the frozen PR5684 WORD was rejected by source authentication before +any scientific source import. + +Scientific replay commit: `c1ec999229213f052e899d89e2e3dd696ceb33ef`. +All 21 committed package files passed the byte check. The official export +passed integrity checks. Its optimized scientific replay passed with empty +PATH in a read-only tree. All 22 export files, including the manifest, retained +their exact bytes and modes. No Git process, network, solver or installed +third-party package was available to that replay. + +The final documentation adds the short three-update derivation and this record. +The executable files, witness, source inputs, price, word and scientific receipt +are unchanged from the sealed replay. Final committed/export byte checks bind +the publication; those custody checks do not repeat the mathematical replay. +The draft GitHub Markdown render was inspected for the exact claim and limits. +Hosted CI and independent human review remain separate publication statuses. + +The overlap refresh through 2026-10-26 08:27 UTC covered all 392 open PR bodies +and 5043 Discussion records. Sparse local coverage was 9 of 7676 note paths. +The scoped matches concerned older mutable-source results and separate G20 or +helper-retirement work. No matching active claim was found in that coverage; +this is not a global novelty certificate. Canonical main and the selected +conditional .00310045 record remain unchanged. + +Full-history ancestry preflight is unavailable in this shallow checkout. +The immediate main-base ancestry check and exact source-object checks passed. +No independent human or proof-kernel acceptance is claimed. The five inherited +framework assumptions remain, and discovery failures are not global barriers. diff --git a/research/p104-temporal-updates/VERIFY.json b/research/p104-temporal-updates/VERIFY.json new file mode 100644 index 0000000000..953ffaee17 --- /dev/null +++ b/research/p104-temporal-updates/VERIFY.json @@ -0,0 +1,37 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Source authentication, exact temporal identity, all columns, native phases, full caller, two price engines and rejection controls.", + "timeout_seconds": 600 + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "checks": "The same complete replay with assertions disabled.", + "timeout_seconds": 600 + } + ], + "inputs": [ + "research/p104-temporal-updates/inputs/pr5684/NOTICE", + "research/p104-temporal-updates/inputs/pr5684/README.md", + "research/p104-temporal-updates/inputs/pr5684/WORD.json.gz", + "research/p104-temporal-updates/inputs/pr5684/construct.py", + "research/p104-temporal-updates/inputs/pr5684/pricing.py", + "research/p104-temporal-updates/inputs/pr5678-source.tar" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-temporal-updates/WITNESS.json b/research/p104-temporal-updates/WITNESS.json new file mode 100644 index 0000000000..2b69faf0cd --- /dev/null +++ b/research/p104-temporal-updates/WITNESS.json @@ -0,0 +1,39 @@ +{ + "inserts": [ + { + "coefficient": "1/4", + "cut": 823, + "frame": 3, + "source": 525 + }, + { + "coefficient": "-1", + "cut": 823, + "frame": 3, + "source": 712 + }, + { + "coefficient": "-1/4", + "cut": 14983, + "frame": 396, + "source": 525 + }, + { + "coefficient": "1/4", + "cut": 14983, + "frame": 396, + "source": 340 + } + ], + "merged_move": 14982, + "old_frames": [ + 3, + 598, + 396 + ], + "removed_event": 13578, + "removed_move": 13577, + "role": 715, + "start": 823, + "stop": 14983 +} diff --git a/research/p104-temporal-updates/WORD.json.gz b/research/p104-temporal-updates/WORD.json.gz new file mode 100644 index 0000000000..45f6c10bf8 Binary files /dev/null and b/research/p104-temporal-updates/WORD.json.gz differ diff --git a/research/p104-temporal-updates/construct.py b/research/p104-temporal-updates/construct.py new file mode 100644 index 0000000000..3852bff77c --- /dev/null +++ b/research/p104-temporal-updates/construct.py @@ -0,0 +1,97 @@ +"""Distribute one scalar update over an interval without a target read. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from copy import deepcopy +from fractions import Fraction as Q +from collections import defaultdict +from hashlib import sha256 +import json +from sources import need + + +def add(dst, src, coefficient): + for column, value in src.items(): + value = dst.get(column, Q(0)) + coefficient * value + if value: + dst[column] = value + else: + dst.pop(column, None) + + +def identity(word, witness): + role = witness['role'] + start, stop = witness['start'], witness['stop'] + removed = witness['removed_event'] + need(0 <= role < word['public'] and 0 <= start <= removed < stop <= len(word['program']), + 'One public target and a bounded interval') + old = word['program'][removed] + need(old[0] == 'ADD' and old[1] == role, 'One removed target update') + terms = defaultdict(list) + for term in witness['inserts']: + need(start <= term['cut'] <= stop and term['source'] != role, + 'Replacement source and cut are in scope') + terms[term['cut']].append(term) + rows = [{r: Q(1)} for r in range(word['public'] + word['owned_fields'])] + frames = word['initial'][:] + [None] * word['owned_fields'] + total, expected, observations = {}, {}, [] + for index in range(stop + 1): + for term in terms.get(index, []): + source, frame, coefficient = term['source'], term['frame'], Q(term['coefficient']) + need(coefficient and frames[role] == frames[source] == frame, + 'Each replacement has an actual common frame') + add(total, rows[source], coefficient) + observations.append([index, source, frame, len(rows[source])]) + if index == stop: + break + event = word['program'][index] + op, target = event[:2] + if start <= index < stop: + need(not (op in ('ADD', 'COPY') and event[2] == role), + 'No original instruction reads the changed target') + need(not (target == role and op in ('SCALE', 'COPY', 'INIT', 'CLEAR')), + 'The changed target has only additive writes and native moves') + if index == removed: + add(expected, rows[event[2]], Q(event[-2])) + if op == 'MOVE': + frames[target] = event[3] + elif op in ('INIT', 'CLEAR'): + rows[target] = {} + frames[target] = event[2] if op == 'INIT' else None + elif op == 'SCALE': + rows[target] = {j: Q(event[-2]) * value for j, value in rows[target].items()} + elif op == 'COPY': + rows[target] = {j: Q(event[-2]) * value for j, value in rows[event[2]].items()} + else: + need(op == 'ADD', 'Known scalar instruction') + add(rows[target], rows[event[2]], Q(event[-2])) + need(total == expected and expected, 'Exact distributed source functional') + encoded = [[j, str(value)] for j, value in sorted(expected.items())] + return {'start': start, 'stop': stop, 'removed_event': removed, 'role': role, + 'source_coefficients': len(expected), 'observations': observations, + 'source_sha256': sha256(json.dumps(encoded, separators=(',', ':')).encode()).hexdigest()} + + +def construct(source, witness): + receipt = identity(source, witness) + role = witness['role'] + a, b, c = witness['old_frames'] + first, last = witness['removed_move'], witness['merged_move'] + need(source['program'][first] == ['MOVE', role, a, b, False] + and source['program'][last] == ['MOVE', role, b, c, False], + 'Exact two source transports') + need(first < witness['removed_event'] < last, 'Removed contact lies between the transports') + inserts = defaultdict(list) + for term in witness['inserts']: + inserts[term['cut']].append(['ADD', role, term['source'], term['coefficient'], term['frame']]) + word = deepcopy(source) + program = [] + for index, event in enumerate(source['program']): + program.extend(deepcopy(inserts.get(index, []))) + if index in (first, witness['removed_event']): + continue + program.append(['MOVE', role, a, c, False] if index == last else deepcopy(event)) + program.extend(deepcopy(inserts.get(len(source['program']), []))) + word['program'] = program + word['schema'] = 'p104-temporal-updates/1' + return word, receipt diff --git a/research/p104-temporal-updates/inputs/pr5678-source.tar b/research/p104-temporal-updates/inputs/pr5678-source.tar new file mode 100644 index 0000000000..cd87254d84 Binary files /dev/null and b/research/p104-temporal-updates/inputs/pr5678-source.tar differ diff --git a/research/p104-temporal-updates/inputs/pr5684/NOTICE b/research/p104-temporal-updates/inputs/pr5684/NOTICE new file mode 100644 index 0000000000..fa0bd1401f --- /dev/null +++ b/research/p104-temporal-updates/inputs/pr5684/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-temporal-updates/inputs/pr5684/README.md b/research/p104-temporal-updates/inputs/pr5684/README.md new file mode 100644 index 0000000000..e80d32af18 --- /dev/null +++ b/research/p104-temporal-updates/inputs/pr5684/README.md @@ -0,0 +1,63 @@ +# Exact reorder+re-frame optimum on PR5678's P104 word: conditional kappa .00310871312 + +Complete conditional kappa **.00310871312** (claim line, tested at .003108713125). The exact raw crossing is in +(0.00310871314031, 0.00310871314032). That is **+5.546e-7** over the raw crossing 0.0031081585098 of +[PR5678](https://github.com/CrocSwap/integer-mult-bounds/pull/5678) (Ali Romman, claim .00310815849), the newest +P104 head when this was written. + +**Conditional on** exactly the assumptions of PR5678 and its inherited P104 line, including free helper endpoints +(PR5561, audited in PR5567). This word changes one helper start frame. The selected record is not changed. +No independent human or proof-kernel acceptance is claimed. + +## What changes + +The word is the optimum of R22's exact reorder+re-frame MIP (commutation poset × subspace charts) on PR5678's word. +The restricted domain and the wide domain (dim gap <= 3) give the same optimum: four re-framed ADDs and one helper start. + +1. **Helper 473** (also in #5666 on PR5660): + - It starts on the empty chart 3 (dim 0) instead of 594 (dim 1). Its credit rises from H8 to H9. + - `213 += 1/2*473` runs on chart 3. It is ordered before the T/T-commuting `213 += 2*706` and that ADD's `MOVE 213 3 -> 594`. + - `473 += 100` runs on 716 (dim 3) instead of 718 (dim 4), so `MOVE 100 716 -> 718` disappears. +2. **Helper 733** (new on PR5678's word): + - 733 moves 597 -> 772 (dim 1 -> 4) before it is read into 585. Before, it moved 597 -> 794 (dim 6) later. + - `585 += -4*733` now runs on 772 instead of 597, so 585 moves 3 -> 772 directly. + - `438 += -4*733` now runs on 772 instead of 794. + - 733 later moves 772 -> 127 instead of 794 -> 127. + +Per local call: +- paid MOVE jobs H1 -3, H4 +1 (66402 -> 66366 paid calls in all); +- helper credits H8 -1, H9 +1; +- rank-mass surplus unchanged at 760, productive fields still 12958. + +## Check + +``` +python3 -W error -B research/p104-reframe-r22/verify.py # ~4 minutes; compares with RESULT.json +python3 -W error -B research/p104-reframe-r22/verify.py --write # regenerates RESULT.json +``` + +`verify.py` runs these checks: +1. Pins PR5678's `WORD.json.gz` (SHA256) and regenerates `WORD.json.gz` from it with `construct.py`. Each edit + replaces one unique event run. +2. Checks that only helper 473's start changes. +3. Checks that the new scalar order is a linear extension of the dependence order: T/T and S/S pairs commute, + every other pair on a shared register keeps its order, and owned registers are exclusive. +4. Runs PR5678's own unmodified stack from its exported sources (`sources.py`, then the retained `sources.py`): + exact replay, every dense transpose column, every native map and phase, the complete physical caller, and + PR5678's `pricing.py`. Only the four literals in `LITERALS` change: claim/tested kappa, previous claim, and the + paid-call total. +5. Runs six controls, all of which must be rejected: + - old helper start; + - read left on the old chart; + - missing helper MOVE; + - unpaid query; + - extra target credit; + - helper read swapped after its write. + +## Attribution + +All retained checkers, words and pricing are by the PR5678 authors and their sources; see `NOTICE`. +R22's search tools (`loop104.py`, `mip104.py`, `poset104.py`, `realize104.py`) are on branch +`r22-p104-reframe-optimum`. + +Joel Pulikkan (GamingPuzzled) with Claude Opus 5.5 (Anthropic) via Claude Code. Apache-2.0. diff --git a/research/p104-temporal-updates/inputs/pr5684/WORD.json.gz b/research/p104-temporal-updates/inputs/pr5684/WORD.json.gz new file mode 100644 index 0000000000..f3fb0e2144 Binary files /dev/null and b/research/p104-temporal-updates/inputs/pr5684/WORD.json.gz differ diff --git a/research/p104-temporal-updates/inputs/pr5684/construct.py b/research/p104-temporal-updates/inputs/pr5684/construct.py new file mode 100644 index 0000000000..3b0109e0fa --- /dev/null +++ b/research/p104-temporal-updates/inputs/pr5684/construct.py @@ -0,0 +1,49 @@ +"""Construct the R22 reorder+reframe word from PR5678's P104 word. + +Joel Pulikkan (GamingPuzzled) with Claude Opus 5.5 (Anthropic) via Claude Code. Apache-2.0. + +Helper 473 starts on the empty chart 3 instead of the one-dimensional chart 594. +Its read into 213 commutes ahead of the T/T-commuting ADD 213 += 2*706, so it runs on +chart 3; 473 then waits on chart 3 and takes the update from 100 on the +three-dimensional chart 716 instead of 718, so 100 never moves 716 -> 718. +Helper 733 moves 597 -> 772 (dim 1 -> 4) before its read into 585 instead of 597 -> 794 (dim 6), +so 585 += -4*733 runs on chart 772 instead of 597 and 438 += -4*733 on 772 instead of 794. +Each edit replaces one exact, unique run of events. +""" +from copy import deepcopy + +HELPER, OLD_START, NEW_START = 473, 594, 3 + +EDITS = [ + ([['MOVE', 213, 3, 594, False], ['ADD', 213, 706, '2', 594]], []), + ([['ADD', 213, 473, '1/2', 594]], + [['ADD', 213, 473, '1/2', 3], ['MOVE', 213, 3, 594, False], ['ADD', 213, 706, '2', 594]]), + ([['MOVE', 100, 716, 718, False]], []), + ([['MOVE', 473, 594, 718, False]], [['MOVE', 473, 3, 716, False]]), + ([['ADD', 473, 100, '1', 718]], [['ADD', 473, 100, '1', 716]]), + ([['MOVE', 473, 718, 719, False]], [['MOVE', 473, 716, 719, False]]), + ([['MOVE', 100, 718, 783, False]], [['MOVE', 100, 716, 783, False]]), + ([['MOVE', 585, 3, 597, False], ['ADD', 585, 733, '-4', 597], ['MOVE', 585, 597, 772, False]], + [['MOVE', 585, 3, 772, False], ['MOVE', 733, 597, 772, False], ['ADD', 585, 733, '-4', 772]]), + ([['MOVE', 438, 772, 794, False], ['MOVE', 733, 597, 794, False], ['ADD', 438, 733, '-4', 794]], + [['ADD', 438, 733, '-4', 772], ['MOVE', 438, 772, 794, False]]), + ([['MOVE', 733, 794, 127, False]], [['MOVE', 733, 772, 127, False]]), +] + + +def locate(program, run): + hits = [i for i in range(len(program) - len(run) + 1) if program[i:i+len(run)] == run] + assert len(hits) == 1, ('unique source run', run, hits) + return hits[0] + + +def construct(base, schema='p104-r22-reframe/1'): + word = deepcopy(base) + assert word['initial'][HELPER] == OLD_START, 'Source helper start' + word['initial'][HELPER] = NEW_START + program = word['program'] + spots = sorted(((locate(program, old), old, new) for old, new in EDITS), reverse=True) + for i, old, new in spots: + program[i:i+len(old)] = deepcopy(new) + word['schema'] = schema + return word diff --git a/research/p104-temporal-updates/inputs/pr5684/pricing.py b/research/p104-temporal-updates/inputs/pr5684/pricing.py new file mode 100644 index 0000000000..e817f4da7d --- /dev/null +++ b/research/p104-temporal-updates/inputs/pr5684/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('.00310871312'), Q('.003108713125') +PREVIOUS = Q('.00310815849') + + +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()) == 66366, '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':'.00310871312','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-temporal-updates/pricing.py b/research/p104-temporal-updates/pricing.py new file mode 100644 index 0000000000..ed290f1059 --- /dev/null +++ b/research/p104-temporal-updates/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('155457611/50000000000'), Q('124366089/40000000000') +PREVIOUS = Q('.00310871312') + + +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()) == 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.00310915222','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-temporal-updates/sources.py b/research/p104-temporal-updates/sources.py new file mode 100644 index 0000000000..720cc95b2b --- /dev/null +++ b/research/p104-temporal-updates/sources.py @@ -0,0 +1,72 @@ +"""Authenticate the retained PR5678 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(): + 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-temporal-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['files'] if row['usage'] == 'provenance'} + 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-temporal-updates/verify.py b/research/p104-temporal-updates/verify.py new file mode 100644 index 0000000000..9ff8a38435 --- /dev/null +++ b/research/p104-temporal-updates/verify.py @@ -0,0 +1,132 @@ +"""Verify the distributed update and its complete conditional kappa. + +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 construction was accepted') + + +def difference(after, before): + delta = Counter(after) + delta.subtract(before) + return {rank: count for rank, count in delta.items() if count} + + +def run(): + witness = json.loads((HERE/'WITNESS.json').read_bytes()) + with sources() as (parent, _): + with load(parent/'sources.py', 'temporal_parent_sources').sources() as (prior, _): + with load(prior/'sources.py', 'temporal_prior_sources').sources() as (stack, root): + L = load(stack/'local.py', 'local') + L.ROOT = root + source = L.read(HERE/'inputs/pr5684/WORD.json.gz') + source_constructor = load(HERE/'inputs/pr5684/construct.py', 'temporal_source_constructor') + need(source_constructor.construct(L.read(parent/'WORD.json.gz')) == source, + 'Exact PR5684 construction from pinned PR5678') + old = L.replay(source) + word, identity = construct.construct(source, witness) + local = L.replay(word) + need(difference(local['paid'], old['paid']) == {1: -1, 2: -1, 3: 1}, + 'One H1 and one H2 are replaced by one H3') + need(local['helpers'] == old['helpers'], 'Every productive target is retained') + need((local['public_inputs'], local['owned_fields'], local['owned_lifetimes'], + local['peak_owned_fields']) == (743, 9, 11, 2), 'Public and owned inventory') + need(len(word['program']) == 25453, 'Complete emitted instruction count') + for key in source: + if key not in ('program', 'schema'): + need(word[key] == source[key], 'Unchanged boundary and geometry: '+key) + columns = L.reverse_columns(word) + print('PASS temporal source identity and all 565504 endpoint entries', flush=True) + native = L.native(word) + C = load(root/'research/p104-productive-controller/caller.py', 'temporal_caller') + caller = C.construct() + need(caller == L.read(root/'research/p104-productive-controller/CONTROLLER.json'), + 'Exact retained caller') + physical = C.physical(caller, word) + print('PASS all native maps, phases and the complete physical caller', flush=True) + price_source = (HERE/'inputs/pr5684/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', 'temporal_price') + price = P.run(local, native, caller, physical) + controls = C.controls(caller) + bad = deepcopy(witness) + bad['inserts'][0]['coefficient'] = '-1/4' + controls['wrong_history_sign'] = rejected(lambda: construct.identity(source, bad)) + bad = deepcopy(witness) + bad['inserts'].pop() + controls['missing_late_update'] = rejected(lambda: construct.identity(source, bad)) + bad = deepcopy(witness) + bad['stop'] += 1 + controls['interval_crosses_target_read'] = rejected(lambda: construct.identity(source, bad)) + bad = deepcopy(witness) + bad['inserts'][0]['frame'] = 598 + controls['wrong_common_frame'] = rejected(lambda: construct.identity(source, bad)) + bad = deepcopy(word) + bad['program'].remove(['MOVE', 715, 3, 396, False]) + controls['missing_native_transport'] = rejected(lambda: L.replay(bad)) + bad = deepcopy(word) + bad['program'].remove(['CLEAR', 747, 598]) + 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'][9] += 1 + controls['extra_target'] = rejected(lambda: P.assemble(bad, native, caller, physical)) + result = {'status': 'PASS_P104_TEMPORAL_UPDATES_KAPPA_00310915222', + 'source_commit': 'd0f6fa2555410a1e23fe4191424c2097ab3d5d97', + 'source_local': old, 'temporal_identity': identity, 'local': local, + 'separate_columns': columns, 'local_paid_delta': {1: -1, 2: -1, 3: 1}, + 'local_helper_delta': {}, 'native': native, 'physical_caller': physical, + 'complete_cost': price, 'negative_controls': controls, + 'limits': ['The five inherited framework assumptions remain.', + 'The complete rounded multiplier and huge uniform word are not materialized.', + 'Author checks do not establish independent scientific acceptance.', + 'The gain is small. No large gain or global optimum is claimed.']} + 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-temporal-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()