diff --git a/research/kappa-owned-relation-20261023/README.md b/research/kappa-owned-relation-20261023/README.md new file mode 100644 index 0000000000..777f4e1d51 --- /dev/null +++ b/research/kappa-owned-relation-20261023/README.md @@ -0,0 +1,249 @@ +# Conditional kappa 0.00302235 from one owned helper relation + +This construction gives **conditional kappa = 60447/20000000 = 0.00302235**. +The gain over Cao Yifan's final +[PR #4610](https://github.com/CrocSwap/integer-mult-bounds/pull/4610) +value, 0.0030217758, is **2871/5000000000 = 0.0000005742**. +The construction changes the complete paid profile. It does not obtain the +gain by taking more digits of the old root. + +One helper becomes owned storage in each backward call. A prepared relation +then makes one paid rank-eight center equal to an earlier saved value. The same +relation makes one later rank-one job act on zero. Both jobs can be removed, +with the rank-nine helper credit also removed. All other independent outputs +and all main interfaces keep their source operators. + +[WORD.json.gz](WORD.json.gz) is the complete emitted word. +[RESULT.json](RESULT.json) records the exact native checks, the two source +identities, both full profiles, completion, compiler and outer calculations. +[SOURCES.json](SOURCES.json) pins every external input by Git blob and SHA256. +The proof below explains why the changed word has the stated contract. + +## Source and scope + +The base is canonical main +[7c472563474e60185e6ca101a17622133d047e56](https://github.com/CrocSwap/integer-mult-bounds/commit/7c472563474e60185e6ca101a17622133d047e56). +The native source is the final PR #4610 word at +[20bb93cd990d2ff683e4d0fc56b87a42cd5d3296](https://github.com/intqwq/integer-mult-bounds/blob/20bb93cd990d2ff683e4d0fc56b87a42cd5d3296/research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz). +Its decompressed SHA256 is +`cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd`. +The comparison value and old crossing come from its +[final compiler arithmetic](https://github.com/intqwq/integer-mult-bounds/blob/20bb93cd990d2ff683e4d0fc56b87a42cd5d3296/research/kappa-round6-compiler-tightening-20261022/ARITHMETIC.json). +All consumed bytes are already in the recorded main base. + +This is one instance of the current `complex-new-helper-inventory` priority. +The [scoped claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19153737) +reserves only the relation and two replacements below. +[Discussion #5355](https://github.com/CrocSwap/integer-mult-bounds/discussions/5355) +retains all 632 independent inputs and all eight centers. +[Discussion #4930](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930) +retains every original helper endpoint. This construction removes the +independent L230 job in backward calls. It does not claim those broader scopes. +The selected certificate is unchanged. A fresh check at 20:20 UTC found that +Discussion #5355 had released its original-input scope without a saving. +Canonical main still had the recorded base commit. + +## Exact replacement proof + +All indices below are zero-based indices in the frozen backward program. +Let `h_r` be the source logical input of helper `Lr`. The five helpers in + +```math +\Delta=h_{230}-h_{324}+h_{326}+h_{328}-h_{333} +``` + +all start in frame 0 and finish in frame 1, of rank nine. The new backward +contract has 224 independent main fields and 407 independent helper fields. +L230 is private. Clear it, then use four same-frame ADDs to prepare + +```math +h_{230}=h_{324}-h_{326}-h_{328}+h_{333}. +``` + +The other helper inputs remain arbitrary and independent. This preparation +sets Delta to zero for every input. It uses no recursive job. It removes one +rank-nine productive target; the dependent field receives no output credit. + +Run the original source program on unrestricted inputs. Let `q` be the +logical row of L92 just after event 11205, a paid climb into frame 254. +The separate predecessor row engine gives these exact identities: + +| Source position | Exact logical row | +| --- | --- | +| C0 at the rank-eight center, event 11332 | `q + Delta/4` | +| L92 at the rank-one climb, event 15584 | `-Delta/4` | + +These identities are over rational coefficients and free native operator +words. They hold for every value of every source input and for every invertible +interpretation of the native symbols. They do not use numerical samples or an +assumed relation between distinct native maps. + +For every positive tensor width f, substitute each native generator by its +source operator tensor power and each inverse by the inverse tensor power. +This defines a representation of the free group. Keep the rational scalar +coefficients outside the substitution. The two row identities therefore hold +at every such width. In particular, Delta/4 remains a scalar linear form; it +is not a tensor power of that sum. This uses the termwise argument recorded in +the [free-word tensor audit](https://github.com/CrocSwap/integer-mult-bounds/blob/7c472563474e60185e6ca101a17622133d047e56/research/free-word-tensor-lift-audit/PROOF.md), +which credits Cinna Davis's proposal and ToikY's scoped audit. Physical frame +realization and the complete all-size compiler retain their source contracts. + +Immediately after event 11205, clear a new private field C1 in frame 254 and +COPY L92 into it. C1 is not written until the replacement of event 11332. At +that event, clear owned C0, set its frame to 254, COPY C1 into C0, then clear C1. +The copy coefficient is exactly one. Under Delta = 0, the copied field is the +same physical value as the old center output: the logical rows and the exact +frame gauge are equal. The old C0 input can be erased because C0 is owned. +This removes one rank-eight recursive job. + +At event 15584, L92 is exactly zero in every input column. The physical +identity therefore has the same result as the old rank-one frame change. +`zero_retag` records this fact. It performs no physical write and is accepted +only when the full exact row is empty and the current frame is 254. It then +records frame 1. This removes one rank-one recursive job. It does not erase a +main input or replace a nonzero transform with a free frame change. + +Every other event stays in source order. Clear private L230 at return. The +source clears C0, and the new program has already cleared C1. The original +linear endpoint identity, restricted by the prepared relation, gives all 224 +main outputs and all 407 retained helper outputs. The literal new-word replay +checks these outputs separately, with all 631 retained inputs and all three +owned entry fields initially arbitrary. It also checks every scalar frame, +paid rank, native frame transition and final frame. + +The 4,429 source frames, 72 native maps, all remaining paid operators, and main +adapters are unchanged. The source +[absolute-phase certificate](https://github.com/intqwq/integer-mult-bounds/blob/20bb93cd990d2ff683e4d0fc56b87a42cd5d3296/research/kappa-round3-warp-20261022/PHASE-VALIDATION.json.gz) +is authenticated and reused. Same-frame COPY and identity on zero introduce no +phase recipe. The source's amplitude and Clifford-lowering checks are not +rerun by this package. The new free-word identities prove equivalence for the +source operators with their full phases, not just their projective classes. + +## Complete cost and conditional compiler + +The forward word is unchanged. Each backward call has these counts: + +```text +paid: {1:2200, 2:412, 3:510, 4:127, 5:40, 8:7} +helpers: {4:28, 7:7, 8:47, 9:325} +``` + +The full p16/a7 controller contains 16 backward calls, two forward calls and +15 query shears. Thus the complete difference is **minus 16 H1 and 16 H8 paid +jobs, and minus 16 H9 productive targets**. It includes every idle and main +target. There are 64,372 paid jobs and 10,912 productive fields. Their rank +masses are 238,990 and 239,742; the surplus remains 752. + +For every real `0 < t < 1`, the complete target-minus-paid moment increases by + +```math +16(1+8^t-9^t)>0. +``` + +For a direct proof, both `(1/9)^t > 1/9` and `(8/9)^t > 8/9`; multiply their +sum by `9^t`. The improvement is strict throughout the required range. + +The backward word has 158,214 real scalar operations under the source macro +allowance, exactly 46 more than its source. Its maximum formal prefix L1 norm +is 169, with maximum denominator 64; both equal the source bounds. The forward +bounds remain 457 and 32. One extra physical private slot holds C1. L230 uses +an existing slot. The route bound also charges two routes for each of the two +new owned lifetimes. The local scalar-plus-route bound stays below 10^7, and +the complete raw nonrecursive bound stays **181,098,496 < 10^9**. Preparation, +COPY, CLEAR and storage therefore do not introduce an unpaid recursive cost. + +Two rational interval engines check the complete moment. Its unique crossing +in `0 < kappa < 1` lies in +**(0.00302238736347, 0.00302238736348)**. The verifier proves the moment decreases +on `[0,0.05]` and remains negative on `[0.05,1]`. This is a ceiling for this +fixed complete profile, not an optimum over circuits or helper relations. +The claimed kappa leaves more than **0.00000003736347** raw headroom. + +The separately tested saving is 0.00302236. The paid/target ratio is below +`0.999999971483293515393313955730`, with reserve `1e-9`. Both charged tails are +below `0.97`. The source power 1024, cutoff 20, floor 21, tail offset 1/5, +complement factor 63/64 and logarithm power 1000 still pass. The compiler gap +is `1/700000000`, with `j=44836`, `H=31385200000000` and `N=2^31385200000000`. +The exact integer test `(H+1)^1000 < 2^44836` passes; the preceding grid integer +fails. The uniform complex saving is `2115651/700000000`. All 54 strict outer +predicates and four functional predicates pass, using the retained ordinary +BIT saving 0.0034. + +## Verification and reproduction + +Use Python 3.12 or 3.14, with the standard library only. From the repository root: + +```sh +python3 -B scripts/research_package.py --package research/kappa-owned-relation-20261023 --check-only +python3 -B scripts/research_package.py --package research/kappa-owned-relation-20261023 +``` + +The registered commands run normal and optimized Python. The direct command, +also used for a Git-free export, is: + +```sh +python3 -B research/kappa-owned-relation-20261023/verify.py +python3 -O -B research/kappa-owned-relation-20261023/verify.py +``` + +Each prints status +`PASS_CONDITIONAL_KAPPA_00302235_ONE_OWNED_RELATION`. +The verifier reconstructs the word and compares its bytes and exact result with +the published artifacts. `--write` is a separate authoring command. It changes +only this package's word and result after all checks pass. + +Fresh checks cover both source words, both candidate words, every independent +entry column and owned return, the two unrestricted source identities, retained +phase bindings, the p16 rational Laurent factorization, both scalar boundary +programs, two complete invoice counts, two rational interval engines, the fixed +profile ceiling, completion, compiler, BIT conversion and all outer predicates. +The emitted word replaces the old single `canonical.local_profile` metadata +field with explicit `paid_profiles` for the two directions. + +Seven native controls reject a wrong relation sign, omitted input clear, wrong +snapshot, wrong zero frame, wrong paid rank, wrong copy gauge, and omitted +output clear. Five cost/outer controls reject the lost helper's output credit, +old BIT stock, closed uniform gap, unfunded endpoint and closed epsilon. + +Normal and optimized registered replays passed on CPython 3.12.14. The direct +author check also passed on CPython 3.14. Source metadata and pins passed. +The optional full-history preflight is not claimed in the shallow checkout. +The publication handoff records export and committed-byte checks. + +The full source phase lowering, BIT native replay, Lean, Docker, physical tape +execution, numerical precision execution, analytic decomposition and integer +recovery are not rerun here. The complete bound retains those predecessor +contracts, including permitted owned erasure, whole-job normalizers, mixed +productive-target recursion and all-size closure. The expanded compiled word +is specified by a finite algorithm, not materialized. This is a conditional +construction with exact finite evidence, not an unconditional multiplication +theorem, a practical timing result or independent human acceptance. + +## Credit + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Cao Yifan's [PR #4610](https://github.com/CrocSwap/integer-mult-bounds/pull/4610) +supplies the exact source word, phase evidence and previous compiler value. +Cinna Davis's [PR #4470](https://github.com/CrocSwap/integer-mult-bounds/pull/4470) +supplies the p16 controller and helper-interface lineage. The source code keeps +credit for Dugongue's transported frames, zxv's native and finite-compiler +work, Jacob Alan Sussman's mixed-target recursion and their predecessors. +The [pricing source](https://github.com/CrocSwap/integer-mult-bounds/blob/7c472563474e60185e6ca101a17622133d047e56/research/kappa-interface-round2-20261022/price_profile.py) +and [literal native source](https://github.com/CrocSwap/integer-mult-bounds/blob/7c472563474e60185e6ca101a17622133d047e56/research/kappa-rebuild/complex/native_extensions.py) +are pinned as provenance for the adapted checks. + +zxv's [PR #5283](https://github.com/CrocSwap/integer-mult-bounds/pull/5283) +supplies the related cache contract and the explicit handoff to find actual +matching rows and their lifetimes. Its standalone cache example is not part of +this word. The new contribution is the five-helper relation, its actual cache +and zero identities, the full owned-field replacement and the complete positive +bill. No priority is claimed for the general cache or paid-history ideas. + +## Open next questions + +Independent review should first check the three source rows and the physical +COPY/zero argument above, then the retained all-size and phase premises. +A later construction could test a different helper relation, but it must claim +a disjoint scope and pay every lost target and owned field. This package does +not classify such relations. [TASK.json](TASK.json) records the first steps, +relevance and blockers for both questions. diff --git a/research/kappa-owned-relation-20261023/RESULT.json b/research/kappa-owned-relation-20261023/RESULT.json new file mode 100644 index 0000000000..27b4e54708 --- /dev/null +++ b/research/kappa-owned-relation-20261023/RESULT.json @@ -0,0 +1,373 @@ +{ + "arithmetic": { + "compiler": { + "H": 31385200000000, + "N": "2^31385200000000", + "eta": { + "lower": "0.000000203927056311365991628189", + "upper": "0.000000203927056311365991628190" + }, + "gap": "1/700000000", + "integer_test_exponent": 44836, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "2115651/700000000", + "word_materialized": false + }, + "fixed_profile_ceiling": { + "decreasing_through": "1/20", + "derivative_upper": { + "lower": "-195778.630038840116414999953237565269", + "upper": "-195778.630038840116414999953237565268" + }, + "remaining_interval_moment_upper": { + "lower": "-6836.549542075249598033582799619360", + "upper": "-6836.549542075249598033582799619359" + } + }, + "full_backward": 16, + "full_forward": 2, + "gain_over_PR4610": "2871/5000000000", + "kappa": "60447/20000000", + "kappa_decimal": ".00302235", + "margin_at_previous_kappa": { + "lower": "0.151161494385402651700356241377", + "upper": "0.151161494385402651700356241378" + }, + "margin_at_previous_root_upper": { + "lower": "0.151143999513185007311808491175", + "upper": "0.151143999513185007311808491176" + }, + "negative_controls": { + "closed_epsilon": [ + "epsilon_below_one", + "global_gamma_power_slack", + "actual_logarithmic_gamma_guard", + "source_axis_superpolynomial", + "gaussian_above_main", + "new_semantic_guard_with_C1_one" + ], + "closed_uniform": [ + "new_complex_uniform_saving_above_b" + ], + "old_BIT": [ + "actual_bit_above_effective" + ], + "unearned_helper_credit": "Rejected by the independent complete census", + "unfunded_endpoint": [ + "main_transform_above_kappa", + "global_coordinate_router_above_kappa", + "fused_gaussian_above_kappa", + "group_bit_router_above_kappa", + "boundary_algebraic_matrix_above_kappa" + ] + }, + "nonrecursive": { + "additional_private_slots": 1, + "local_routes": 4806000, + "local_scalar": 158214, + "owned_slots_backward": 3, + "raw_budget": 1000000000, + "raw_scalar_upper": 181098496 + }, + "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": "174299999253/175000000000", + "fixed_halo_explicit_metadata_branch": "13475000001/175000000", + "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000", + "new_semantic_group_guard": "3/700000000" + }, + "margins": { + "boundary_algebraic_matrix": "23139910904443/7656250000000000", + "fused_gaussian": "23139910838329/7656250000000000", + "global_coordinate_router": "2115649/700000000", + "group_bit_router": "1480954993653053/490000000000000000", + "group_scans": "349999999/350000000", + "main_transform": "23139899966943/7656250000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "3133491473404443/7656250000000000" + }, + "parameters": { + "a": "2115649/700000000", + "b": "42313/14000000", + "beta": "699999997/700000000", + "bit_saving": "17/5000", + "cap_xi": "6961616462466943/7656250000000000", + "complex_uniform_saving": "2115651/700000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "60447/20000000", + "lambda_": "199395529/200000000", + "lambda_prime": "10904443/10937500", + "layout": "1/700000000", + "q": "33057/10937500", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "75559/25000000" + }, + "strict_checks": { + "actual_bit_above_effective": "264351/700000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "694633553939307/3828125000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "43716943/7656250000000000", + "cap_above_band": "3133491462466943/7656250000000000", + "cap_below_cell": "694633526595557/7656250000000000", + "cap_below_phase_cell_power": "8350883537533057/7656250000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "395187/14000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "43650829/7656250000000000", + "gaussian_above_main": "5435693/3828125000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "3493653053/490000000000000000", + "group_gauge_power_slack": "43414597087027/239257812500000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "697884353/700000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "645689790400418148631/500000000000000000000000", + "lambda_above_internal": "1/1400000000", + "lambda_above_sigma": "3/1400000000", + "lambda_above_tau": "1/1400000000", + "lambda_prime_above_lambda": "1/1400000000", + "lambda_prime_above_leaf": "27957687/9800000000000000", + "leaf_saving_above_effective": "13957687/9800000000000000", + "main_transform_above_kappa": "32779443/7656250000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "53897884359/700000000", + "microbox_halo_volume": "55300000003/700000000", + "new_complex_uniform_saving_above_b": "1/700000000", + "new_semantic_guard_with_C1_one": "1/700000000", + "polynomial_products_above_kappa": "348942177/350000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "27957687/9800000000000000", + "q_positive": "33057/10937500", + "short_record_fallback": "13957687/14000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "3110351606216943/7656250000000000", + "stop_below_one": "699999999/700000000", + "stop_positive": "1/700000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/700000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/700000000", + "union_tag_work_per_visit_fits_record": "3/700000000" + } + }, + "paid": { + "1": 41282, + "16": 448, + "2": 7416, + "24": 448, + "3": 9180, + "32": 448, + "4": 2286, + "40": 448, + "48": 448, + "5": 720, + "56": 448, + "64": 448, + "72": 224, + "8": 128 + }, + "paid_calls": 64372, + "productive_fields": 10912, + "query_shears": 15, + "rank_mass_surplus": 752, + "raw_headroom": [ + "3736347/100000000000000", + "934087/25000000000000" + ], + "raw_root_interval": [ + "302238736347/100000000000000", + "75559684087/25000000000000" + ], + "strictification": { + "alpha": { + "lower": "0.999999971483293515393313955729", + "upper": "0.999999971483293515393313955730" + }, + "cutoff": 20, + "delta": { + "lower": "0.957459689758527661921334851512", + "upper": "0.957459689758527661921334851513" + }, + "floor": 21, + "gamma": { + "lower": "0.956310980726438847618396606911", + "upper": "0.956310980726438847618396606912" + }, + "normalized_paid_upper": "2097152001953127/2097154147483648", + "power": 1024, + "reserve": "1/1000000000", + "tail_offset": "1/5", + "tested": "75559/25000000" + }, + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 846, + "9": 5852 + } + }, + "candidate_native": { + "backward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 325 + }, + "independent_owned_entry_columns": 3, + "independent_persistent_columns": 631, + "max_denominator": 64, + "max_formal_prefix_l1": "169", + "owned_outputs_zero": true, + "paid": { + "1": 2200, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 7 + }, + "real_scalar_allowance": 158214, + "zero_identities": 1 + }, + "forward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "independent_owned_entry_columns": 1, + "independent_persistent_columns": 632, + "max_denominator": 32, + "max_formal_prefix_l1": "457", + "owned_outputs_zero": true, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "real_scalar_allowance": 158120, + "zero_identities": 0 + } + }, + "independent_source_identities": { + "center_minus_snapshot": "Delta/4", + "center_replaced": 11332, + "copy_coefficient": "1", + "relation": { + "230": 1, + "324": -1, + "326": 1, + "328": 1, + "333": -1 + }, + "snapshot_after": 11205, + "snapshot_terms_before_substitution": 61, + "source_event_indices_are_zero_based": true, + "zero_identity_at": 15584, + "zero_site_row": "-Delta/4" + }, + "native_negative_controls": { + "missing_owned_input_clear": "Every independent main/helper endpoint: 0", + "uncleared_owned_output": "Every owned entry column is erased at return", + "under_or_overstated_paid_rank": "Exact paid rank and frame", + "wrong_copy_gauge": "Exact scalar destination frame", + "wrong_relation_sign": "Every independent main/helper endpoint: 0", + "wrong_snapshot_source": "Zero identity requires an identically zero full row", + "wrong_zero_input_frame": "Zero identity requires an identically zero full row" + }, + "phase_inheritance": { + "absolute_phase_receipt_reused": "research/kappa-round3-warp-20261022/PHASE-VALIDATION.json.gz", + "all_retained_paid_events_and_warps_from_source": true, + "new_gaussian_operators": 0, + "new_native_maps": 0, + "new_operations": "Same-frame COPY, owned CLEAR/ADD, and physical identity on a proved zero row.", + "source_amplitudes_and_phase_lowering_freshly_replayed": false + }, + "scope": "Exact finite word, full all-column endpoints, ownership, p16 bill and compiler arithmetic. Retains source native phase, allowed owned erasure, mixed-target all-size, analytic, precision, tape, prime and exact-recovery contracts. No selected-frontier update.", + "source_native": { + "backward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "independent_owned_entry_columns": 1, + "independent_persistent_columns": 632, + "max_denominator": 64, + "max_formal_prefix_l1": "169", + "owned_outputs_zero": true, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "real_scalar_allowance": 158168, + "zero_identities": 0 + }, + "forward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "independent_owned_entry_columns": 1, + "independent_persistent_columns": 632, + "max_denominator": 32, + "max_formal_prefix_l1": "457", + "owned_outputs_zero": true, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "real_scalar_allowance": 158120, + "zero_identities": 0 + } + }, + "source_payload_sha256": "cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd", + "status": "PASS_CONDITIONAL_KAPPA_00302235_ONE_OWNED_RELATION", + "word_payload_sha256": "645b32ff67dfd49bbe8c2287d21f12a66a775d3c5e187db6f813e17e9f8fae35" +} diff --git a/research/kappa-owned-relation-20261023/SOURCES.json b/research/kappa-owned-relation-20261023/SOURCES.json new file mode 100644 index 0000000000..9854abbb4f --- /dev/null +++ b/research/kappa-owned-relation-20261023/SOURCES.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/free-word-tensor-lift-audit/PROOF.md", + "usage": "provenance", + "git_blob": "69c337a7704ce589798269ab4b8606189c070c4e", + "sha256": "cc8ad3698a673fb225419a3636a39aa99a66c7a0676f12e329b1e76564fa1459" + }, + { + "path": "research/higher-moment-strictification/verify.py", + "usage": "input", + "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699", + "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326" + }, + { + "path": "research/joint-helper-lattice/CONTROLLER.json", + "usage": "input", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + }, + { + "path": "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "usage": "input", + "git_blob": "5a55034ec9e6185d981e16c28e1e2e455069e2cb", + "sha256": "106b4d5e052427230df452f0c901d5390a0583782960b80a8af94d9a984022c7" + }, + { + "path": "research/kappa-interface-round2-20261022/price_profile.py", + "usage": "provenance", + "git_blob": "1d93e43d1cb888d128c2faa2be83a96d85b84295", + "sha256": "adde619968d3ac37147d239e25145b28150650e9ce0f76035f680f22589adcbb" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "usage": "input", + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + }, + { + "path": "research/kappa-rebuild/complex/native_extensions.py", + "usage": "provenance", + "git_blob": "7f84894efc309546a903d314c7ac1473e7f594a8", + "sha256": "50ad007d9c386393657e86c99a96ae0a63a8fbc52872579b185002cc626e88e3" + }, + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/kappa-round3-warp-20261022/PHASE-VALIDATION.json.gz", + "usage": "input", + "git_blob": "ac77b78547d6dbf2e6bd102e1047c5b16c1bca88", + "sha256": "6eae66ed3cfa8a1533e89b9660a57276908e6646640a12f8b1e3489f4ea1354b" + }, + { + "path": "research/kappa-round6-compiler-tightening-20261022/ARITHMETIC.json", + "usage": "input", + "git_blob": "0fdb65f946d557c13d8e2781b9151e2a8ddee5c3", + "sha256": "b4f720a7ccbb5b46e472eaf85dc8739a40598986f19b37d26c4f9ecfbd31f0de" + }, + { + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "usage": "input", + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + } + ] +} diff --git a/research/kappa-owned-relation-20261023/TASK.json b/research/kappa-owned-relation-20261023/TASK.json new file mode 100644 index 0000000000..f5df24ffe3 --- /dev/null +++ b/research/kappa-owned-relation-20261023/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "refined", + "actual_scope": "Make helper L230 owned in each backward call, prepare one five-helper relation, retain one exact frame-254 snapshot, remove one rank-eight center and one rank-one zero job, and debit one rank-nine target.", + "scope_change_reason": "This uses the current helper-inventory priority. It changes the independent input inventory and scalar word; all physical native maps and the p16 controller remain fixed.", + "bottleneck_link": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19153737", + "budget_minutes": 240, + "stop_rule": "Publish one exact complete-profile kappa improvement after native, ownership, phase-inheritance, compiler and cold-export checks.", + "outcome": "completed", + "evidence": "README.md, WORD.json.gz, RESULT.json and verify.py. The complete conditional kappa is 60447/20000000.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance in discovery, code, proof, verification and publication.", + "open_questions": [ + { + "question": "Can a separate reviewer validate this one-relation restriction and the inherited physical transfer premises?", + "why_it_matters": "The new finite construction is exact, but the complete bound still uses the source phase and all-size contracts.", + "first_step": "Replay the three unrestricted source rows in native.py and check the COPY and zero-identity argument in README.md.", + "blocked_by": "Independent review has not yet occurred." + }, + { + "question": "Can a different helper relation give another complete positive bill?", + "why_it_matters": "This construction gives one positive instance, not an optimum for changed helper inventories.", + "first_step": "Claim a disjoint relation in Discussions, derive its exact rows, and include every lost target and owned-storage cost.", + "blocked_by": "Current active cache and paid-history scopes must be checked first." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19153737", + "distinct_scopes": [ + "https://github.com/CrocSwap/integer-mult-bounds/discussions/5355", + "https://github.com/CrocSwap/integer-mult-bounds/discussions/4930" + ], + "boundary": "The first scope retains 632 arbitrary inputs and eight centers. The second retains every original helper endpoint. This package removes the independent L230 job only in backward calls and claims only the stated relation and two event replacements." + } +} diff --git a/research/kappa-owned-relation-20261023/VERIFY.json b/research/kappa-owned-relation-20261023/VERIFY.json new file mode 100644 index 0000000000..8098df4c80 --- /dev/null +++ b/research/kappa-owned-relation-20261023/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/higher-moment-strictification/verify.py", + "research/joint-helper-lattice/CONTROLLER.json", + "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "research/kappa-rebuild/architecture/mixed_target_probe.py", + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "research/kappa-round3-warp-20261022/PHASE-VALIDATION.json.gz", + "research/kappa-round6-compiler-tightening-20261022/ARITHMETIC.json", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "research/query-thinned-controllers/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Exact native rows, owned entry columns, event ranks, independent source identities, p16 Laurent controller, complete asymmetric invoice, two interval engines, compiler and outer predicates, negative controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "The same checks remain active with Python assertions disabled." + } + ] +} diff --git a/research/kappa-owned-relation-20261023/WORD.json.gz b/research/kappa-owned-relation-20261023/WORD.json.gz new file mode 100644 index 0000000000..5e79bd826c Binary files /dev/null and b/research/kappa-owned-relation-20261023/WORD.json.gz differ diff --git a/research/kappa-owned-relation-20261023/native.py b/research/kappa-owned-relation-20261023/native.py new file mode 100644 index 0000000000..b8249ed7ba --- /dev/null +++ b/research/kappa-owned-relation-20261023/native.py @@ -0,0 +1,299 @@ +"""One prepared helper removes two paid jobs in the PR4610 backward word. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +The source word is by Cao Yifan. The row convention and scalar allowance +follow the credited native work of Cinna Davis and zxv. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha1, sha256 +from pathlib import Path +import gzip +import importlib.util +import json +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = 'research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz' +PHASE = 'research/kappa-round3-warp-20261022/PHASE-VALIDATION.json.gz' +PAYLOAD = 'cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd' +RELATION = {230: 1, 324: -1, 326: 1, 328: 1, 333: -1} +OLD_PAID = {1: 2201, 2: 412, 3: 510, 4: 127, 5: 40, 8: 8} +NEW_PAID = dict(OLD_PAID) +NEW_PAID[1] -= 1 +NEW_PAID[8] -= 1 +OLD_HELPERS = {4: 28, 7: 7, 8: 47, 9: 326} + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def read(path): + data = path.read_bytes() + return json.loads(gzip.decompress(data) if path.suffix == '.gz' else data) + + +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 load(relative, name): + spec = importlib.util.spec_from_file_location(name, ROOT / relative) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def authenticate(): + pins = read(HERE / 'SOURCES.json') + for row in pins['files']: + if row['usage'] != 'input': + continue + p = ROOT + for part in Path(row['path']).parts: + p /= part + need(not p.is_symlink(), 'No source aliases') + raw = p.read_bytes() + need(sha256(raw).hexdigest() == row['sha256'], 'Changed source: ' + row['path']) + need(sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == row['git_blob'], 'Source Git blob') + need(sha256(gzip.decompress((ROOT / SOURCE).read_bytes())).hexdigest() == PAYLOAD, 'Exact source payload') + return pins + + +def span(basis): + out = {0} + for vector in basis: + need(isinstance(vector, int) and 0 <= vector < 512, 'Binary frame coordinate') + out |= {v ^ vector for v in tuple(out)} + need(len(out) == 2 ** len(basis), 'Independent frame basis') + return out + + +def add(dst, src, q): + for k, v in tuple(src.items()): + value = dst.get(k, Q(0)) + q * v + if value: + dst[k] = value + else: + dst.pop(k, None) + + +def allowance(g): + if g[0] in ('clear', 'copy'): + return 2 + q = Q(*g[3:]) if g[0] == 'add' else Q(*g[2:]) + n, d = abs(q.numerator), q.denominator + need(n > 0 and d & (d - 1) == 0, 'Nonzero dyadic scalar') + if g[0] == 'scale': + need(n & (n - 1) == 0, 'Dyadic unit SCALE') + return 2 * (abs(n.bit_length() - d.bit_length()) + int(q < 0)) + need(g[0] == 'add', 'Known scalar operation') + return 2 * (3 + n.bit_length() - 1 + n.bit_count() + d.bit_length() - 1) + + +def construct(source): + c = source['canonical'] + old = source['programs']['backward'] + need(old[11205] == ['climb', 'warp_retimed', 92, 310, 254, 4], 'Snapshot source event') + need(old[11332] == ['center', 0, 0, 254, 8], 'Center source event') + need(old[15584] == ['climb', 'warp_retimed', 92, 254, 1, 1], 'Zero source event') + need(all(c['start'][h] == 0 and c['final'][h] == 1 for h in RELATION), 'Five cold full-ended helpers') + word = [['scalar', ['clear', ['L', 230]], 0]] + word += [['scalar', ['add', ['L', 230], ['L', h], -q, 1], 0] + for h, q in RELATION.items() if h != 230] + for i, event in enumerate(old): + if i == 11332: + word += [['scalar', ['clear', ['C', 0]], 254], + ['scalar', ['copy', ['C', 0], ['C', 1]], 254], + ['scalar', ['clear', ['C', 1]], 254]] + elif i == 15584: + word.append(['zero_retag', ['L', 92], 254, 1]) + else: + word.append(deepcopy(event)) + if i == 11205: + word += [['scalar', ['clear', ['C', 1]], 254], + ['scalar', ['copy', ['C', 1], ['L', 92]], 254]] + word.append(['scalar', ['clear', ['L', 230]], 1]) + physical = deepcopy(c) + physical.pop('local_profile') + return {'schema': 'owned-helper-relation-word/1', 'canonical': physical, + 'paid_profiles': {'forward': OLD_PAID, 'backward': NEW_PAID}, + 'owned': {'forward': [['C', 0]], 'backward': [['C', 0], ['C', 1], ['L', 230]]}, + 'programs': {'forward': deepcopy(source['programs']['forward']), 'backward': word}} + + +def replay(c, program, backward, specialized): + """Run every event on all independent entry columns and exact frames.""" + owned = {('C', 0)} | ({('C', 1), ('L', 230)} if specialized else set()) + roles = {('L', i) for i in range(632)} | owned + rows = {r: {(r, ()): Q(1)} for r in roles} + frames = {('L', i): f for i, f in enumerate(c['start'])} + frames.update({r: None for r in owned if r[0] == 'C'}) + spaces = [span(b) for b in c['frames']] + paid = Counter() + cost, max_l1, denominator, zero_count = 0, Q(1), 1, 0 + for e in program: + kind, touched = e[0], None + if kind == 'scalar': + g, frame = e[1:] + dst = tuple(g[1]); touched = dst + need(dst in rows and 0 <= frame < len(spaces), 'Declared scalar destination and frame') + cost += allowance(g) + if g[0] == 'clear': + need(dst in owned, 'Only owned fields can be erased') + rows[dst] = {}; frames[dst] = frame + else: + need(frames[dst] == frame, 'Exact scalar destination frame') + if g[0] in ('add', 'copy'): + src = tuple(g[2]) + need(src in rows and frames[src] == frame and dst != src, 'Exact scalar source frame') + if g[0] == 'copy': + need(dst in owned and not rows[dst], 'COPY into cleared owned storage') + rows[dst] = dict(rows[src]) + else: + add(rows[dst], rows[src], Q(g[3], g[4])) + else: + need(g[0] == 'scale', 'Known scalar operation') + rows[dst] = {k: Q(g[2], g[3]) * v for k, v in rows[dst].items()} + elif kind == 'warp': + _, role, op, old, new = e + dst = tuple(role); touched = dst + need(frames[dst] == old and 1 <= abs(op) <= len(c['warps']), 'Exact warp input') + symbol = (1 if op > 0 else -1) * (abs(op) + (10**6 if backward else 0)) + rows[dst] = {(r, w[1:] if w and w[0] == -symbol else (symbol,) + w): q + for (r, w), q in rows[dst].items()} + frames[dst] = new + elif kind in ('climb', 'center'): + if kind == 'climb': + _, _, i, old, new, rank = e + dst = ('L', i) + need(spaces[old] < spaces[new], 'Ascending paid climb') + else: + _, i, old, new, rank = e + dst = ('C', i) + need(spaces[old] < spaces[new] or spaces[new] < spaces[old], 'Nested paid center') + need(frames[dst] == old and rank == abs(len(c['frames'][new]) - len(c['frames'][old])), 'Exact paid rank and frame') + frames[dst] = new; paid[rank] += 1 + elif kind == 'zero_retag': + _, role, old, new = e + dst = tuple(role) + need(specialized and backward and dst == ('L', 92), 'Declared zero identity') + need(frames[dst] == old and not rows[dst], 'Zero identity requires an identically zero full row') + need((old, new) == (254, 1), 'Declared zero frame change') + frames[dst] = new; zero_count += 1 + else: + need(kind in ('phase', 'adapter'), 'Known inert source marker') + if touched is not None: + max_l1 = max(max_l1, sum(map(abs, rows[touched].values()), Q(0))) + denominator = max(denominator, max((q.denominator for q in rows[touched].values()), default=1)) + need([frames['L', i] for i in range(632)] == c['final'], 'Every final native frame') + for i in range(632): + r = ('L', i) + if r in owned: + continue + expected = {(r, ()): Q(1)} + if i < 112 if backward else 112 <= i < 224: + expected[(('L', i + 112 if backward else i - 112), ())] = Q(-1 if backward else 1) + need(rows[r] == expected, 'Every independent main/helper endpoint: ' + str(i)) + need(all(not rows[r] for r in owned), 'Every owned entry column is erased at return') + need(zero_count == int(specialized), 'Exactly one checked zero identity') + helpers = Counter() + for i in range(224, 632): + if ('L', i) in owned: + continue + a, b = c['start'][i], c['final'][i] + need(spaces[a] < spaces[b], 'Strict independent productive helper') + helpers[len(c['frames'][b]) - len(c['frames'][a])] += 1 + return {'paid': dict(sorted(paid.items())), 'helpers': dict(sorted(helpers.items())), + 'independent_persistent_columns': 631 if specialized else 632, + 'independent_owned_entry_columns': len(owned), 'owned_outputs_zero': True, + 'real_scalar_allowance': cost, 'max_formal_prefix_l1': str(max_l1), + 'max_denominator': denominator, 'zero_identities': zero_count} + + +def independent_source_identities(source): + """Use the predecessor row engine on the unrestricted original word.""" + v = load('research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py', 'owned_relation_source_rows') + rows = {('L', i): v.identity(('L', i)) for i in range(632)} + rows['C', 0] = v.identity(('C', 0)) + delta = {(('L', i), ()): Q(q) for i, q in RELATION.items()} + saved = None + for index, e in enumerate(source['programs']['backward']): + if e[0] == 'scalar': + g = e[1]; dst = tuple(g[1]) + if g[0] == 'clear': rows[dst] = {} + elif g[0] == 'copy': rows[dst] = dict(rows[tuple(g[2])]) + elif g[0] == 'scale': rows[dst] = {k: Q(g[2], g[3]) * a for k, a in rows[dst].items()} + else: v.add(rows[dst], rows[tuple(g[2])], Q(g[3], g[4])) + elif e[0] == 'warp': + dst = tuple(e[1]); rows[dst] = v.warp(rows[dst], e[2], True) + if index == 11205: saved = dict(rows['L', 92]) + if index == 11332: + diff = dict(rows['C', 0]); v.add(diff, saved, -1) + need(diff == {k: q / 4 for k, q in delta.items()}, 'Independent exact center minus snapshot = Delta/4') + if index == 15584: + need(rows['L', 92] == {k: -q / 4 for k, q in delta.items()}, 'Independent exact zero-site row = -Delta/4') + need(all(rows['L', i] == v.expected(('L', i), [], True, False) for i in range(632)), 'Independent unrestricted source endpoints') + return {'source_event_indices_are_zero_based': True, 'snapshot_after': 11205, + 'center_replaced': 11332, 'zero_identity_at': 15584, + 'snapshot_terms_before_substitution': len(saved), 'copy_coefficient': '1', + 'center_minus_snapshot': 'Delta/4', 'zero_site_row': '-Delta/4', 'relation': RELATION} + + +def phase_inheritance(source, candidate): + receipt = read(ROOT / PHASE) + need(receipt['status'] == 'PASS_JOINT_HELPER_MAPS_ALL_ACTUAL_ABSOLUTE_PHASES' and + receipt['actual_word_canonical_sha256'] == PAYLOAD, 'Authenticated source absolute-phase receipt') + physical = deepcopy(source['canonical']); physical.pop('local_profile') + need(candidate['canonical'] == physical, 'Every frame, native map and main adapter unchanged') + for direction, program in candidate['programs'].items(): + old = source['programs'][direction] + for kind in ('warp', 'adapter', 'phase'): + need([e for e in program if e[0] == kind] == [e for e in old if e[0] == kind], 'Exact inherited ' + kind + ' sequence') + old_paid = Counter(tuple(e) for e in old if e[0] in ('climb', 'center')) + new_paid = Counter(tuple(e) for e in program if e[0] in ('climb', 'center')) + expected = Counter() if direction == 'forward' else Counter(tuple(old[i]) for i in (11332, 15584)) + need(old_paid - new_paid == expected and not new_paid - old_paid, 'Only the two proved jobs are removed') + return {'new_gaussian_operators': 0, 'new_native_maps': 0, + 'all_retained_paid_events_and_warps_from_source': True, + 'absolute_phase_receipt_reused': PHASE, + 'source_amplitudes_and_phase_lowering_freshly_replayed': False, + 'new_operations': 'Same-frame COPY, owned CLEAR/ADD, and physical identity on a proved zero row.'} + + +def controls(c, candidate): + controls = {} + base = candidate['programs']['backward'] + variants = {} + bad = deepcopy(base); bad[1][1][3] *= -1; variants['wrong_relation_sign'] = bad + variants['missing_owned_input_clear'] = deepcopy(base[1:]) + bad = deepcopy(base) + next(e for e in bad if e[0] == 'scalar' and e[1][:2] == ['copy', ['C', 1]])[1][2] = ['L', 63] + variants['wrong_snapshot_source'] = bad + bad = deepcopy(base); next(e for e in bad if e[0] == 'zero_retag')[2] = 0 + variants['wrong_zero_input_frame'] = bad + bad = deepcopy(base); next(e for e in bad if e[0] == 'climb')[5] += 1 + variants['under_or_overstated_paid_rank'] = bad + bad = deepcopy(base) + next(e for e in bad if e[0] == 'scalar' and e[1][:2] == ['copy', ['C', 0]])[2] = 0 + variants['wrong_copy_gauge'] = bad + variants['uncleared_owned_output'] = deepcopy(base[:-1]) + for name, program in variants.items(): + try: + replay(c, program, True, True) + except ValueError as err: + controls[name] = str(err) + else: + raise ValueError('Control accepted: ' + name) + return controls diff --git a/research/kappa-owned-relation-20261023/price.py b/research/kappa-owned-relation-20261023/price.py new file mode 100644 index 0000000000..6077adf74c --- /dev/null +++ b/research/kappa-owned-relation-20261023/price.py @@ -0,0 +1,196 @@ +"""Complete p16 bill and finite compiler for one owned helper relation. + +The interval and compiler proof follows Cao Yifan's PR4610 pricing, Cinna +Davis's PR4470 controller, zxv's completion and logarithmic majorant, and +Jacob Alan Sussman's mixed-target recursion. Apache-2.0. +Ali Romman, with substantial OpenAI Codex assistance. +""" +from collections import Counter +from fractions import Fraction as Q +from native import ROOT, read, load, need, encode, OLD_PAID, OLD_HELPERS + +KAPPA = Q('.00302235') +TESTED = Q('.00302236') +PREVIOUS = Q('.0030217758') +OLD_ROOT_UPPER = Q('.00302177587078') + + +def controller(): + """Check the literal p16 word and both rational boundary programs.""" + word = read(ROOT / 'research/joint-helper-lattice/CONTROLLER.json') + need((word['kind'], word['pairs'], word['prefix_pairs'], word['ambient_rank']) == ('complex', 16, 7, 145), 'Source p16/a7 controller') + zero = (0,) * 34 + def plus(dst, src, q): + for k, v in src.items(): + value = dst.get(k, Q(0)) + q * v + if value: dst[k] = value + else: dst.pop(k, None) + def shifted(row, term, sign=1): + return [{tuple(a + b for a, b in zip(k, term)): sign * v for k, v in cell.items()} for cell in row] + for side in ('left', 'right'): + matrix = [[Q(i == j) for j in range(32)] for i in range(32)] + for e in word['boundaries'][side + '_program']: + if e[0] == 'SWAP': matrix[e[1]], matrix[e[2]] = matrix[e[2]], matrix[e[1]] + elif e[0] == 'SCALE': matrix[e[1]] = [Q(e[2]) * x for x in matrix[e[1]]] + else: + need(e[0] == 'ADD', 'Boundary scalar opcode') + matrix[e[1]] = [x + Q(e[3]) * y for x, y in zip(matrix[e[1]], matrix[e[2]])] + need(matrix == [[Q(x) for x in row] for row in word['boundaries'][side]], 'Exact scalar boundary program') + rows = [[{zero: Q(x)} if Q(x) else {} for x in row] for row in word['boundaries']['right']] + for e in word['physical_events']: + if e[0] in ('LOCAL', 'QUERY_SHEAR'): + _, stage, pair, back = e + x, y = 2 * pair, 2 * pair + 1 + if back: x, y = y, x + term = (1 if back else -1,) + (0,) * 33 + for dst, src in zip(rows[y], shifted(rows[x], term)): + plus(dst, src, Q(-1 if back else 1)) + if e[0] == 'LOCAL': + term = (0,) + tuple(int(s == stage) for s in range(33)) + for r in (x, y): rows[r] = shifted(rows[r], term) + elif e[0] == 'IDLE': + term = (0,) + tuple(int(s in e[2]) for s in range(33)) + for r in (2 * e[1], 2 * e[1] + 1): rows[r] = shifted(rows[r], term) + elif e[0] == 'ADD': + for dst, src in zip(rows[e[1]], rows[e[2]]): plus(dst, src, Q(e[3])) + else: + need(e[0] in ('SWAP', 'SIGNED_SWAP'), 'Controller physical opcode') + rows[e[1]], rows[e[2]] = rows[e[2]], shifted(rows[e[1]], zero, -1 if e[0] == 'SIGNED_SWAP' else 1) + out = [[{} for _ in range(32)] for _ in range(32)] + for i, row in enumerate(word['boundaries']['left']): + for k, q in enumerate(row): + if Q(q): + for j in range(32): plus(out[i][j], rows[k][j], Q(q)) + expected = [[{tuple(word['diagonal'][i]): Q(1)} if i == j else {} for j in range(32)] for i in range(32)] + need(out == expected, 'All p16 Laurent coefficients, central signs and boundary factors') + return word + + +def assemble(native, word): + T, P = Counter(), Counter() + orientations = Counter(); thin = 0 + for e in word['physical_events']: + if e[0] == 'LOCAL': + direction = 'backward' if e[3] else 'forward' + orientations[direction] += 1 + T.update(native[direction]['helpers']); P.update(native[direction]['paid']) + elif e[0] == 'QUERY_SHEAR': thin += 1; P[1] += 112 + elif e[0] == 'IDLE': P[8 * len(e[2])] += 224 + main = Counter() + for term in word['diagonal']: + need(term[0] in (-1, 1) and all(x in (0, 1) for x in term[1:]), 'Whole Gaussian main target') + main[1 + 8 * sum(term[1:])] += 112 + T.update(main) + need(orientations == {'backward': 16, 'forward': 2} and thin == 15, 'Every actual call orientation') + # This second census uses the source invoice and the two local deltas. + check_T = Counter({int(r): n for r, n in word['invoice']['main'].items()}) + check_T.update({r: 18 * n for r, n in OLD_HELPERS.items()}); check_T[9] -= 16 + check_P = Counter({int(r): n for r, n in word['invoice']['whole_idle'].items()}) + check_P.update({r: 18 * n for r, n in OLD_PAID.items()}); check_P[1] += 1680 - 16; check_P[8] -= 16 + need(T == check_T and P == check_P, 'Independent full invoice substitution') + need(sum(T.values()) == 10912 and sum(P.values()) == 64372, 'Complete productive and paid counts') + need(sum(r * n for r, n in T.items()) - sum(r * n for r, n in P.items()) == 752, 'Unchanged complete rank surplus') + return T, P + + +def run(native): + word = controller(); T, P = assemble(native, word) + prior = read(ROOT / 'research/kappa-round6-compiler-tightening-20261022/ARITHMETIC.json') + need(Q(prior['kappa']) == PREVIOUS and Q(prior['raw_root_interval'][1]) == OLD_ROOT_UPPER, 'Pinned prior conditional bound and raw crossing') + prior_T = Counter({int(r): n for r, n in prior['targets'].items()}) + prior_P = Counter({int(r): n for r, n in prior['paid'].items()}) + prior_T[9] -= 16; prior_P[1] -= 16; prior_P[8] -= 16 + need(T == prior_T and P == prior_P, 'Complete delta from the final PR4610 bill') + E = load('research/higher-moment-strictification/verify.py', 'owned_relation_intervals') + other = load('research/kappa-rebuild/architecture/mixed_target_probe.py', 'owned_relation_second_intervals') + def margin(c): + t, p = E.moment(T, 1 - c), E.moment(P, 1 - c) + return t[0] - p[1], t[1] - p[0] + need(margin(OLD_ROOT_UPPER)[0] > 0, 'Changed invoice beats the prior raw root upper endpoint') + lo, hi, grid = 0, 10**12, 10**14 + while hi - lo > 1: + mid = (lo + hi) // 2 + if margin(Q(mid, grid))[0] > 0: lo = mid + else: hi = mid + root_low, root_high = Q(lo, grid), Q(hi, grid) + need(margin(root_low)[0] > 0 and margin(root_high)[1] < 0, 'Strict rational root enclosure') + need(PREVIOUS < KAPPA < TESTED < root_low, 'New bound and explicit compiler headroom') + # The complete signed profile decreases on [0, .05], and stays negative + # on [.05, 1]. This proves a fixed-profile ceiling, not a circuit ceiling. + signed = {r: T[r] - P[r] for r in T.keys() | P.keys()} + derivative, upper = None, None + for i in range(16): + l, r = Q(i, 320), Q(i + 1, 320); low = Q(0) + for rank, n in signed.items(): + term = E.mul(E.power(rank, 1 - r if n > 0 else 1 - l), E.log_bounds(rank)) + low += n * term[0 if n > 0 else 1] + derivative = low if derivative is None else min(derivative, low) + for i in range(128): + l, r = Q(1, 20) + Q(19 * i, 2560), Q(1, 20) + Q(19 * (i + 1), 2560) + value = sum(n * E.power(rank, 1 - l if n > 0 else 1 - r)[1 if n > 0 else 0] for rank, n in signed.items()) + upper = value if upper is None else max(upper, value) + need(derivative > 0 and upper < 0, 'Fixed-profile ceiling on all 0 < kappa < 1') + t, u, v, c, b = 1 - TESTED, Q(1, 5), 1024, 20, 21 + target, paid = E.moment(T, t), E.moment(P, t) + tl, th = other.moment(T, TESTED); pl, ph = other.moment(P, TESTED) + need(tl > ph and max(tl, target[0]) <= min(th, target[1]) and max(pl, paid[0]) <= min(ph, paid[1]), 'Two exact interval engines agree') + 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 = Q(1, 10**9); g = d = Q(97, 100) + need(alpha[1] < 1 - reserve and gamma[1] < g and delta[1] < d, 'Original and completion tails charged') + need(g**128 < Q(1, 16) and d**128 < Q(1, 16), 'Two strict tail decay blocks') + normalized = 1 / (1 + v * reserve) + Q(4, 2**32) + need(normalized < 1 and c**64 < b**63, 'Paid completion, splitting and rounding') + theta, power = Q(63, 64), 1000 + eta = E.scale(E.power(145, -v * TESTED), t) + need(2 * (20**v)**64 <= (145**v)**63 and eta[0] > theta**power, 'Shifted exits and complement capacity') + need(E.power(145, v * TESTED)[1] < 2**power, 'Compiler initial range') + gap = (TESTED - KAPPA) / 7; need(gap.numerator == 1, 'Finite 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: + mid = (left + right) // 2 + if wins(mid): right = mid + else: left = mid + height = step * right + need(height > 8 * v and wins(right) and not wins(right - 1), 'Finite uniform-rank threshold') + local_scalar = max(x['real_scalar_allowance'] for x in native.values()) + # The old route allowance is retained. Charge two additional owned field + # lifetimes at two routes each, even though L230 uses an existing slot. + routes = (max(sum(x['paid'].values()) for x in native.values()) + 2 * 408 + 688 + 4) * 1000 + need(local_scalar + routes < 10**7, 'All new preparation, COPY, CLEAR and fixed routes fit') + scalar_upper = 18 * 10**7 + 15 * 1792 + 32 * 112 * (len(word['physical_events']) + sum(len(word['boundaries'][k + '_program']) for k in ('left', 'right'))) + need(scalar_upper < 10**9, 'Complete raw nonrecursive bound') + bit = read(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']) + need(atom == Q('.004') and atom > ordinary > admitted > TESTED and atom < 1 - ordinary, 'Retained stronger BIT admission and stock') + L = load('research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py', 'owned_relation_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 = L.ledger(params); outer['functional_checks']['actual_new_BIT_stock_sublinear'] = params['beta'] * (1 - atom) + need(len(outer['strict_checks']) == 54 and len(outer['functional_checks']) == 4, 'Complete outer predicate inventory') + need(all(x > 0 for key in ('strict_checks', 'functional_checks') for x in outer[key].values()), 'Every outer inequality is strict') + controls = {} + for name, patch in [('old_BIT', {'bit_saving': Q('.0027')}), ('closed_uniform', {'complex_uniform_saving': params['b']}), ('unfunded_endpoint', {'kappa': TESTED}), ('closed_epsilon', {'epsilon': Q(1)})]: + bad = L.ledger(dict(params, **patch)); failed = [k for k, x in bad['strict_checks'].items() if x <= 0] + need(failed, 'Reject outer patch ' + name); controls[name] = failed + bad_native = {d: dict(x) for d, x in native.items()} + bad_native['backward']['helpers'] = OLD_HELPERS + try: assemble(bad_native, word) + except ValueError: controls['unearned_helper_credit'] = 'Rejected by the independent complete census' + else: raise ValueError('Unowned helper credit was accepted') + return encode({'kappa': KAPPA, 'kappa_decimal': '.00302235', 'gain_over_PR4610': KAPPA - PREVIOUS, + 'raw_root_interval': [root_low, root_high], 'raw_headroom': [root_low - KAPPA, root_high - KAPPA], + 'margin_at_previous_kappa': E.display(margin(PREVIOUS)), + 'margin_at_previous_root_upper': E.display(margin(OLD_ROOT_UPPER)), + 'fixed_profile_ceiling': {'decreasing_through': Q(1, 20), 'derivative_upper': E.display((-derivative,) * 2), 'remaining_interval_moment_upper': E.display((upper,) * 2)}, + 'targets': T, 'paid': P, 'productive_fields': sum(T.values()), 'paid_calls': sum(P.values()), 'rank_mass_surplus': 752, + 'full_backward': 16, 'full_forward': 2, 'query_shears': 15, + 'strictification': {'tested': TESTED, 'power': v, 'cutoff': c, 'floor': b, 'tail_offset': u, 'reserve': reserve, '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, 'uniform_saving': params['complex_uniform_saving'], 'H': height, 'N': '2^' + str(height), 'integer_test_exponent': right, 'word_materialized': False}, + 'nonrecursive': {'local_scalar': local_scalar, 'local_routes': routes, 'raw_scalar_upper': scalar_upper, 'raw_budget': 10**9, 'additional_private_slots': 1, 'owned_slots_backward': 3}, + 'ordinary_BIT': bit, 'outer': outer, 'negative_controls': controls}) diff --git a/research/kappa-owned-relation-20261023/verify.py b/research/kappa-owned-relation-20261023/verify.py new file mode 100644 index 0000000000..b19f7d0ca4 --- /dev/null +++ b/research/kappa-owned-relation-20261023/verify.py @@ -0,0 +1,64 @@ +#!/usr/bin/env python3 +"""Replay the one-relation native word and its complete conditional kappa. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +Read README.md for the source credit and inherited proof obligations. +""" +from hashlib import sha256 +import argparse +import gzip +import json +from pathlib import Path +import sys +sys.dont_write_bytecode = True +import native as N +import price + + +def run(): + N.authenticate() + source = N.read(N.ROOT / N.SOURCE) + candidate = N.construct(source) + c = candidate['canonical'] + before, after = {}, {} + for direction in ('forward', 'backward'): + back = direction == 'backward' + before[direction] = N.replay(c, source['programs'][direction], back, False) + after[direction] = N.replay(c, candidate['programs'][direction], back, back) + N.need(before[direction]['paid'] == N.OLD_PAID and before[direction]['helpers'] == N.OLD_HELPERS, 'Pinned source census') + N.need(after[direction]['paid'] == candidate['paid_profiles'][direction], 'Emitted direction-specific paid profile') + helpers = dict(N.OLD_HELPERS) + if back: helpers[9] -= 1 + N.need(after[direction]['paid'] == (N.NEW_PAID if back else N.OLD_PAID) and after[direction]['helpers'] == helpers, 'Actual complete changed native census') + identities = N.independent_source_identities(source) + phase = N.phase_inheritance(source, candidate) + controls = N.controls(c, candidate) + arithmetic = price.run(after) + data = (json.dumps(candidate, sort_keys=True, separators=(',', ':')) + '\n').encode() + result = N.encode({'status': 'PASS_CONDITIONAL_KAPPA_00302235_ONE_OWNED_RELATION', + 'source_payload_sha256': N.PAYLOAD, 'word_payload_sha256': sha256(data).hexdigest(), + 'source_native': before, 'candidate_native': after, 'independent_source_identities': identities, + 'phase_inheritance': phase, 'native_negative_controls': controls, 'arithmetic': arithmetic, + 'scope': 'Exact finite word, full all-column endpoints, ownership, p16 bill and compiler arithmetic. Retains source native phase, allowed owned erasure, mixed-target all-size, analytic, precision, tape, prime and exact-recovery contracts. No selected-frontier update.'}) + return data, result + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--write', action='store_true', help='Write only this package word and result after all checks pass.') + ap.add_argument('--out', type=Path, help='Write a replay result to a separate path.') + args = ap.parse_args() + data, result = run() + if args.write: + (N.HERE / 'WORD.json.gz').write_bytes(gzip.compress(data, mtime=0)) + (N.HERE / 'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True) + '\n', encoding='utf-8') + else: + N.need(gzip.decompress((N.HERE / 'WORD.json.gz').read_bytes()) == data, 'Exact literal published word') + N.need(N.read(N.HERE / 'RESULT.json') == result, 'Exact published replay result') + if args.out: + args.out.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n', encoding='utf-8') + print(json.dumps({'status': result['status'], **{k: result['arithmetic'][k] for k in ('kappa', 'gain_over_PR4610', 'raw_root_interval', 'paid_calls', 'productive_fields')}}, sort_keys=True)) + + +if __name__ == '__main__': + main()