diff --git a/research/kappa-joint-relations-20261023/README.md b/research/kappa-joint-relations-20261023/README.md new file mode 100644 index 0000000000..d0593a46e8 --- /dev/null +++ b/research/kappa-joint-relations-20261023/README.md @@ -0,0 +1,280 @@ +# Conditional kappa 0.00302666 from eight joint helper relations + +This construction gives **conditional kappa = 151333/50000000 = 0.00302666**. +It improves the one-relation [PR #5377](https://github.com/CrocSwap/integer-mult-bounds/pull/5377) +value by **431/100000000 = 0.00000431**. The gain over the selected final +[PR #4610](https://github.com/CrocSwap/integer-mult-bounds/pull/4610) +value is **24421/5000000000 = 0.0000048842**. + +Eight independent helper relations replace all eight backward rank-eight +centers with exact saved values. They also remove eight later rank-one jobs +on zero fields. Each backward call gives up eight rank-nine productive helper +targets. All 224 main inputs and the other 400 helper inputs stay independent. +The forward word and p16 controller stay unchanged. This changes the complete +paid profile and proves a strict moment gain. + +[WITNESS.json](WITNESS.json) lists the eight relations and source events. +[WORD.json.gz](WORD.json.gz) contains the complete literal program. +[RESULT.json](RESULT.json) gives the exact row identities and complete bill. +[SOURCES.json](SOURCES.json) pins every consumed input by Git blob and SHA256. +The package has no runtime dependency on the pending PR #5377 package. + +## Source and research boundary + +The branch starts at canonical main +[1ec1119972c9aefe42525172d07b332fcff81cb4](https://github.com/CrocSwap/integer-mult-bounds/commit/1ec1119972c9aefe42525172d07b332fcff81cb4). +This base selects the final PR4610 result with the independent +[PR #5241](https://github.com/CrocSwap/integer-mult-bounds/pull/5241) audit. +The [selected review](https://github.com/CrocSwap/integer-mult-bounds/blob/1ec1119972c9aefe42525172d07b332fcff81cb4/docs/research/pr-intake-evidence/pr4610/PROOF-REVIEW.md) +records its exact scope and five retained framework assumptions. + +The frozen native source is Cao Yifan's +[round-three word](https://github.com/intqwq/integer-mult-bounds/blob/20bb93cd990d2ff683e4d0fc56b87a42cd5d3296/research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz) +at final PR4610 commit `20bb93cd990d2ff683e4d0fc56b87a42cd5d3296`. +Its decompressed SHA256 is +`cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd`. +The prior complete bill and crossing come from its +[round-six arithmetic](https://github.com/intqwq/integer-mult-bounds/blob/20bb93cd990d2ff683e4d0fc56b87a42cd5d3296/research/kappa-round6-compiler-tightening-20261022/ARITHMETIC.json). +All consumed source bytes occur in the recorded main base. + +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19154290) +covers only the eight named centers and their joint relation system. +The separate [no-snapshot relation search](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19154267) +has released its scope and explicitly excludes joint relations and center reuse. +The original-input cache search in +[Discussion #5355](https://github.com/CrocSwap/integer-mult-bounds/discussions/5355) +is also released. The coded caller in +[Discussion #4930](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930) +retains all original helper outputs. This package changes eight helper inputs +in backward calls. It does not take those other research scopes. + +## General relation construction + +Consider an exact linear register program with independent helper inputs in +one common input frame. Let r independent scalar relations have a reduced +basis with dyadic coefficients and r helper pivots. Make these r fields owned. +Clear them and prepare each pivot from the nonpivot inputs with scalar ADDs. +Each relation is then zero for every remaining independent input. The r owned +fields receive no productive output credit. + +Suppose that an earlier field and a later owned center output have the same +exact frame, and their logical row difference is zero under these relations. +Clear a new owned field, COPY the earlier value into it and retain it. At the +center, clear the old owned center and COPY the saved value into that same +output frame. Clear the snapshot after use. This implements the old output +exactly without the center job. If another paid job has an identically zero +input row, the physical identity also implements that job on the restricted +domain. A frame annotation may change only after this exact zero check. + +Each replacement preserves the source state on that domain. Induction through +the chronological word therefore preserves every retained output. Clear all +owned pivots at return. The complete cost must remove their productive +credits and count every new scalar operation and storage route. Independence +of the relations is necessary: counting eight apparent formulas is not a +proof of eight independent pivots or of eight distinct saved jobs. + +## Eight exact source identities + +Let h_r denote the unrestricted logical input of source helper Lr. Define: + +```text +D1 = h230 - h324 + h326 + h328 - h333 +D2 = h225 - h384 - h388 + h390 + h391 + h392 - h397 +D3 = h225 - h227 + h229 - 2h231 + h232 - h234 - h235 + - h236 - h237 + 2h238 + h239 - h384 - h388 + h390 + + h391 + h392 - h397 +D4 = h227 + h229 - h232 + h234 + h235 - h236 + h237 + - h239 - h324 + h326 + h328 - h333 +D5 = h241 - h243 + h245 - h247 - h252 - h253 + h254 + h255 +D6 = h225 - h241 + h243 + h245 - h247 - h252 + h253 + + h254 - h255 - h324 + h326 + h328 - h333 - h384 + - h388 + h390 + h391 + h392 - h397 +D7 = h257 - h259 + h261 - h263 - h268 - h269 + h270 + h271 +D8 = h288 - h294 - h296 - h297 + h300 + h303 +``` + +Every helper in these relations starts in frame 0 and ends in frame 1, of +rank nine. Exact row reduction gives the eight pivots +**225, 227, 229, 230, 241, 245, 257, 288**. The reduced basis has no other pivot +in any pivot row. Its nonzero coefficients are integers or half-integers. +The emitted preparation thus uses only independent inputs and dyadic ADDs; +it has no cyclic dependence and needs no recursive job. The full reduced +basis is recorded in the word and result. + +The following indices are zero-based indices in the frozen backward source. +A snapshot is taken immediately after its named event. The two last columns +are identities in the unrestricted source, before any relation is imposed. + +| Relation | Snapshot event and role | Frame | Center event | Later zero event and role | Center minus snapshot | Later row | +|---|---|---|---|---|---|---| +| D1 | 11205, L92 | 254 | 11332 | 15584, L92 | D1/4 | -D1/4 | +| D2 | 11218, L57 | 274 | 11358 | 17264, L57 | D2/4 | -D2/4 | +| D3 | 11231, L81 | 619 | 11384 | 17256, L81 | D3/4 | -D3/4 | +| D4 | 11244, L224 | 279 | 11410 | 17722, L224 | -D4/4 | D4/4 | +| D5 | 11257, L11 | 621 | 11436 | 15876, L11 | D5/4 | -D5/4 | +| D6 | 11270, L240 | 280 | 11462 | 17245, L240 | -D6/4 | D6/4 | +| D7 | 11283, L9 | 624 | 11488 | 15870, L9 | D7/4 | -D7/4 | +| D8 | 11306, L288 | 281 | 11514 | 17580, L288 | D8/4 | -D8/4 | + +The COPY coefficient is one in every case. All eight snapshots are live +before the first center replacement. They use distinct owned fields C1 through +C8. Each is read once and cleared after use. The source owned center C0 is +cleared before each replacement. Each later zero job changes from the listed +frame to frame 1 and has rank one. `zero_retag` is a physical no-op; the verifier +requires its complete row to be zero and checks both exact frame identifiers. + +A separate source interpreter checks all sixteen identities on the unrestricted +632 source inputs. The new interpreter then executes the emitted program on +all **624 independent persistent columns and 17 arbitrary owned entry columns**. +It checks every scalar frame, paid rank, native transition, retained endpoint, +final frame and owned return. No independent input is silently set to zero. + +The identities are over rational coefficients and reduced free operator words. +They hold for any invertible interpretation of the native generators. At +positive tensor width f, replace each generator with its source tensor power +and each inverse with the inverse tensor power. Keep each rational coefficient +outside this substitution. Evaluation is a representation of the free group, +so the identities still hold. In particular, no tensor power is distributed +over a sum. The retained +[free-word tensor audit](https://github.com/CrocSwap/integer-mult-bounds/blob/1ec1119972c9aefe42525172d07b332fcff81cb4/research/free-word-tensor-lift-audit/PROOF.md) +records this termwise argument and credits Cinna Davis and ToikY. + +All 4,429 source frames, 72 native maps, adapters and retained paid operators +are unchanged. The package authenticates and reuses the source +[absolute-phase evidence](https://github.com/intqwq/integer-mult-bounds/blob/20bb93cd990d2ff683e4d0fc56b87a42cd5d3296/research/kappa-round3-warp-20261022/PHASE-VALIDATION.json.gz). +Same-frame COPY and identity on zero add no phase recipe. This package does +not rerun the source Clifford lowering or amplitude checks. The new identities +hold for the full source operators, including their absolute phases. + +## Complete bill and compiler + +Each backward call has the following complete local profiles: + +```text +paid: {1:2193, 2:412, 3:510, 4:127, 5:40} +helpers: {4:28, 7:7, 8:47, 9:318} +``` + +The controller has 16 backward calls, two unchanged forward calls and 15 thin +queries. Every idle and main target remains paid or credited as in the source. +Compared with PR4610, the complete difference is **minus 128 H1 and 128 H8 paid +jobs, with minus 128 H9 productive targets**. Compared with PR5377 it removes +224 further paid jobs and 112 further productive fields. The complete bill has +**64,148 paid jobs and 10,800 productive fields**. The respective rank masses +are 237,982 and 238,734, with unchanged surplus 752. + +For every real `0 < t < 1`, the complete target-minus-paid moment increases by + +```math +128(1+8^t-9^t)>0. +``` + +Both `(1/9)^t > 1/9` and `(8/9)^t > 8/9`; summing and multiplying by `9^t` +proves the strict inequality. This comparison charges the lost helper jobs. + +The backward scalar allowance is **158,744**, which is 576 above the source. +Its maximum formal prefix L1 norm is **163**, below the source value 169, and +its maximum denominator stays 64. The forward values remain 158,120, 457 and +32. Eight new physical slots hold C1 through C8; the eight private helpers use +existing slots. The local route allowance charges both routes for each of +these sixteen new owned lifetimes. It is **4,834,000**. The local scalar-plus-route +bill stays below 10^7. The complete raw nonrecursive bound remains +**181,098,496 < 10^9**. These bounds include preparation, storage, COPY and CLEAR. +The retained precision and tape prescriptions must use this expanded fixed +template, not a former numerical template-size cap. + +Two rational interval engines verify the complete moment. Its unique crossing +in `0 < kappa < 1` lies in **(0.00302667476807, 0.00302667476808)**. Exact interval +bounds prove decrease on `[0,0.05]` and negativity on `[0.05,1]`. This is a ceiling +for this fixed complete profile. It does not optimize all relation systems. +The claimed kappa leaves more than **0.00000001476807** raw headroom. + +The tested saving is **0.00302667**. The paid/target ratio is below +`0.999999995016963387587258118167`, with reserve `1e-9`. The two charged tail +ratios are below 0.957 and 0.952, respectively, hence below 0.97. Tensor power +1024, cutoff 20, floor 21, tail offset 1/5, complement factor 63/64 and logarithm +power 1000 all pass. The finite compiler uses gap `1/700000000`, `j=44836`, +`H=31385200000000` and `N=2^31385200000000`. The exact test +`(H+1)^1000 < 2^44836` passes; the preceding grid integer fails. The uniform +complex saving is `529667/175000000`. All **54 strict outer predicates and +four functional predicates** pass with the retained ordinary BIT saving 0.0034. + +## Verification and limitations + +Use CPython 3.12 or 3.14 and the standard library. From the repository root: + +```sh +python3 -B scripts/research_package.py --package research/kappa-joint-relations-20261023 --check-only +python3 -B scripts/research_package.py --package research/kappa-joint-relations-20261023 +``` + +The registered verifier runs normal and optimized modes. The direct commands +also work in the official Git-free export: + +```sh +python3 -B research/kappa-joint-relations-20261023/verify.py +python3 -O -B research/kappa-joint-relations-20261023/verify.py +``` + +Both print `PASS_CONDITIONAL_KAPPA_00302666_EIGHT_JOINT_RELATIONS`. +The verifier reconstructs and compares the literal published word and result. +`--write` is an authoring mode that writes only this package after all checks +pass. Regeneration compares decompressed payloads, not gzip container bytes. + +Fresh checks cover both original and changed words, all retained and owned +entry columns, sixteen unrestricted source identities, exact relation rank, +phase source bindings, the p16 Laurent controller and both boundary programs, +two complete invoice counts, two interval engines, the fixed profile ceiling, +completion, compiler and every outer predicate. Seven native controls reject +a wrong preparation sign, omitted input clear, wrong snapshot, wrong zero +frame, wrong paid rank, wrong COPY gauge and omitted output clear. Five +cost controls reject unearned helper credit and four invalid outer parameters. + +Normal and optimized registered checks passed on CPython 3.12.14. The direct +author replay also passed on CPython 3.14. Metadata and source pins passed. +The publication handoff records committed-byte and Git-free export checks. +The optional full-history preflight is not claimed in this shallow checkout. + +These are author checks. The source phase lowering, BIT native construction, +physical tape execution, numerical precision execution, analytic decomposition, +fine-prime avoidance and exact integer recovery are inherited. They are not +rerun here. No expanded compiled word, Lean proof, Docker run or independent +human acceptance is claimed. The complete result retains the selected five +framework assumptions: all-column native realization, owned erasure, uniform +compiler closure, precision/tape and analytic recovery. No selected record is +changed. This is a conditional mathematical improvement, not a timing result. + +## Credit + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +The new code and proof generalize our +[frozen one-relation package](https://github.com/aliromman/integer-mult-bounds/blob/c448d13c71908647f968b06cddb795ce7d288139/research/kappa-owned-relation-20261023/README.md) +from PR5377. That package supplies D1, its COPY/zero argument and the original +complete-cost verifier. The new work is the joint rank-eight system, seven +further centers, eight simultaneous snapshots and the new complete bound. + +Cao Yifan's [PR #4610](https://github.com/CrocSwap/integer-mult-bounds/pull/4610) +supplies the exact word, phase evidence and compiler lineage. Chris R's +[PR #5241](https://github.com/CrocSwap/integer-mult-bounds/pull/5241) supplies the +independent admission evidence now used by main; that audit does not cover +this changed helper inventory. Cinna Davis's +[PR #4470](https://github.com/CrocSwap/integer-mult-bounds/pull/4470) supplies the +controller and productive-helper lineage. zxv's +[PR #5283](https://github.com/CrocSwap/integer-mult-bounds/pull/5283) supplies the +related cache contract and handoff to actual row/lifetime matches. + +The retained [pricing source](https://github.com/CrocSwap/integer-mult-bounds/blob/1ec1119972c9aefe42525172d07b332fcff81cb4/research/kappa-interface-round2-20261022/price_profile.py) +and [native source](https://github.com/CrocSwap/integer-mult-bounds/blob/1ec1119972c9aefe42525172d07b332fcff81cb4/research/kappa-rebuild/complex/native_extensions.py) +credit Dugongue's transported frames, zxv's native/compiler work, Jacob Alan +Sussman's mixed-target recursion and the earlier contributors. Their notices +and the original source bytes remain unchanged. + +## Open next questions + +An independent reviewer should check the eight pivot preparations and sixteen +unrestricted identities, then the COPY/zero realization and complete bill. +Independent physical and all-size acceptance remains necessary. A further +construction must change another paid job or relation system: all eight +backward centers are already removed here. Check live claims and price every +lost target before that search. [TASK.json](TASK.json) records both questions, +first checks and blockers. No optimum over helper relations is claimed. diff --git a/research/kappa-joint-relations-20261023/RESULT.json b/research/kappa-joint-relations-20261023/RESULT.json new file mode 100644 index 0000000000..b6c9cd0da1 --- /dev/null +++ b/research/kappa-joint-relations-20261023/RESULT.json @@ -0,0 +1,961 @@ +{ + "arithmetic": { + "PR5377_raw_root_upper": "75559684087/25000000000000", + "compiler": { + "H": 31385200000000, + "N": "2^31385200000000", + "eta": { + "lower": "0.000000199495867924466542600392", + "upper": "0.000000199495867924466542600393" + }, + "gap": "1/700000000", + "integer_test_exponent": 44836, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "529667/175000000", + "word_materialized": false + }, + "fixed_profile_ceiling": { + "decreasing_through": "1/20", + "derivative_upper": { + "lower": "-195473.450610684184815935477074865515", + "upper": "-195473.450610684184815935477074865514" + }, + "remaining_interval_moment_upper": { + "lower": "-6820.155255095433991980526890420873", + "upper": "-6820.155255095433991980526890420872" + } + }, + "full_backward": 16, + "full_forward": 2, + "gain_over_PR4610": "24421/5000000000", + "gain_over_PR5377": "431/100000000", + "kappa": "151333/50000000", + "kappa_decimal": ".00302666", + "margin_at_previous_kappa": { + "lower": "1.209169472215494738857340795394", + "upper": "1.209169472215494738857340795395" + }, + "margin_at_previous_root_upper": { + "lower": "1.209152002019805295008574084544", + "upper": "1.209152002019805295008574084545" + }, + "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": 8, + "local_routes": 4834000, + "local_scalar": 158744, + "owned_slots_backward": 17, + "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": "296613239576267/98000000000000000", + "fused_gaussian": "296613238728801/98000000000000000", + "global_coordinate_router": "1059333/350000000", + "group_bit_router": "741533446822001/245000000000000000", + "group_scans": "349999999/350000000", + "main_transform": "296613099576267/98000000000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "40109113239576267/98000000000000000" + }, + "parameters": { + "a": "1059333/350000000", + "b": "2118667/700000000", + "beta": "699999997/700000000", + "bit_saving": "17/5000", + "cap_xi": "89109113099576267/98000000000000000", + "complex_uniform_saving": "529667/175000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "151333/50000000", + "lambda_": "199394667/200000000", + "lambda_prime": "139576267/140000000", + "layout": "1/700000000", + "q": "423733/140000000", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "302667/100000000" + }, + "strict_checks": { + "actual_bit_above_effective": "130667/350000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "8890887110423733/49000000000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "559576267/98000000000000000", + "cap_above_band": "40109113099576267/98000000000000000", + "cap_below_cell": "8890886760423733/98000000000000000", + "cap_below_phase_cell_power": "106890886900423733/98000000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "19756333/700000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "558728801/98000000000000000", + "gaussian_above_main": "69576267/49000000000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "1746822001/245000000000000000", + "group_gauge_power_slack": "8890887103423733/49000000000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "87235167/87500000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "647844790400418148631/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": "1397881333/490000000000000000", + "leaf_saving_above_effective": "697881333/490000000000000000", + "main_transform_above_kappa": "419576267/98000000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "26948940671/350000000", + "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": "697881337/700000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "1397881333/490000000000000000", + "q_positive": "423733/140000000", + "short_record_fallback": "697881333/700000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "39812500559576267/98000000000000000", + "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": 41170, + "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": 16 + }, + "paid_calls": 64148, + "productive_fields": 10800, + "query_shears": 15, + "rank_mass_surplus": 752, + "raw_headroom": [ + "1476807/100000000000000", + "184601/12500000000000" + ], + "raw_root_interval": [ + "302667476807/100000000000000", + "37833434601/12500000000000" + ], + "strictification": { + "alpha": { + "lower": "0.999999995016963387587258118166", + "upper": "0.999999995016963387587258118167" + }, + "cutoff": 20, + "delta": { + "lower": "0.951652473261883819699264316643", + "upper": "0.951652473261883819699264316644" + }, + "floor": 21, + "gamma": { + "lower": "0.956968564096059991841792406781", + "upper": "0.956968564096059991841792406782" + }, + "normalized_paid_upper": "2097152001953127/2097154147483648", + "power": 1024, + "reserve": "1/1000000000", + "tail_offset": "1/5", + "tested": "302667/100000000" + }, + "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": 5740 + } + }, + "candidate_native": { + "backward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 318 + }, + "independent_owned_entry_columns": 17, + "independent_persistent_columns": 624, + "max_denominator": 64, + "max_formal_prefix_l1": "163", + "owned_outputs_zero": true, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40 + }, + "real_scalar_allowance": 158744, + "zero_identities": 8 + }, + "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": { + "checked": [ + [ + "center", + 11332 + ], + [ + "center", + 11358 + ], + [ + "center", + 11384 + ], + [ + "center", + 11410 + ], + [ + "center", + 11436 + ], + [ + "center", + 11462 + ], + [ + "center", + 11488 + ], + [ + "center", + 11514 + ], + [ + "zero", + 15584 + ], + [ + "zero", + 15870 + ], + [ + "zero", + 15876 + ], + [ + "zero", + 17245 + ], + [ + "zero", + 17256 + ], + [ + "zero", + 17264 + ], + [ + "zero", + 17580 + ], + [ + "zero", + 17722 + ] + ], + "owned_pivots": [ + 225, + 227, + 229, + 230, + 241, + 245, + 257, + 288 + ], + "reduced_basis": { + "225": { + "225": "1", + "384": "-1", + "388": "-1", + "390": "1", + "391": "1", + "392": "1", + "397": "-1" + }, + "227": { + "227": "1", + "231": "1", + "232": "-1", + "234": "1", + "235": "1", + "237": "1", + "238": "-1", + "239": "-1", + "324": "-1/2", + "326": "1/2", + "328": "1/2", + "333": "-1/2" + }, + "229": { + "229": "1", + "231": "-1", + "236": "-1", + "238": "1", + "324": "-1/2", + "326": "1/2", + "328": "1/2", + "333": "-1/2" + }, + "230": { + "230": "1", + "324": "-1", + "326": "1", + "328": "1", + "333": "-1" + }, + "241": { + "241": "1", + "243": "-1", + "253": "-1", + "255": "1", + "324": "1/2", + "326": "-1/2", + "328": "-1/2", + "333": "1/2" + }, + "245": { + "245": "1", + "247": "-1", + "252": "-1", + "254": "1", + "324": "-1/2", + "326": "1/2", + "328": "1/2", + "333": "-1/2" + }, + "257": { + "257": "1", + "259": "-1", + "261": "1", + "263": "-1", + "268": "-1", + "269": "-1", + "270": "1", + "271": "1" + }, + "288": { + "288": "1", + "294": "-1", + "296": "-1", + "297": "-1", + "300": "1", + "303": "1" + } + }, + "relation_rank": 8, + "snapshot_terms_before_substitution": { + "11205": 61, + "11218": 63, + "11231": 73, + "11244": 68, + "11257": 64, + "11270": 75, + "11283": 64, + "11306": 62 + }, + "source_event_indices_are_zero_based": true, + "witnesses": [ + { + "cached_event": 11205, + "cached_role": 92, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11332, + "frame": 254, + "relation": [ + [ + 230, + "1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ] + ], + "zero_event": 15584, + "zero_factor": "-1/4", + "zero_role": 92 + }, + { + "cached_event": 11218, + "cached_role": 57, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11358, + "frame": 274, + "relation": [ + [ + 225, + "1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "zero_event": 17264, + "zero_factor": "-1/4", + "zero_role": 57 + }, + { + "cached_event": 11231, + "cached_role": 81, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11384, + "frame": 619, + "relation": [ + [ + 225, + "1" + ], + [ + 227, + "-1" + ], + [ + 229, + "1" + ], + [ + 231, + "-2" + ], + [ + 232, + "1" + ], + [ + 234, + "-1" + ], + [ + 235, + "-1" + ], + [ + 236, + "-1" + ], + [ + 237, + "-1" + ], + [ + 238, + "2" + ], + [ + 239, + "1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "zero_event": 17256, + "zero_factor": "-1/4", + "zero_role": 81 + }, + { + "cached_event": 11244, + "cached_role": 224, + "copy_factor": "1", + "difference_factor": "-1/4", + "event": 11410, + "frame": 279, + "relation": [ + [ + 227, + "1" + ], + [ + 229, + "1" + ], + [ + 232, + "-1" + ], + [ + 234, + "1" + ], + [ + 235, + "1" + ], + [ + 236, + "-1" + ], + [ + 237, + "1" + ], + [ + 239, + "-1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ] + ], + "zero_event": 17722, + "zero_factor": "1/4", + "zero_role": 224 + }, + { + "cached_event": 11257, + "cached_role": 11, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11436, + "frame": 621, + "relation": [ + [ + 241, + "1" + ], + [ + 243, + "-1" + ], + [ + 245, + "1" + ], + [ + 247, + "-1" + ], + [ + 252, + "-1" + ], + [ + 253, + "-1" + ], + [ + 254, + "1" + ], + [ + 255, + "1" + ] + ], + "zero_event": 15876, + "zero_factor": "-1/4", + "zero_role": 11 + }, + { + "cached_event": 11270, + "cached_role": 240, + "copy_factor": "1", + "difference_factor": "-1/4", + "event": 11462, + "frame": 280, + "relation": [ + [ + 225, + "1" + ], + [ + 241, + "-1" + ], + [ + 243, + "1" + ], + [ + 245, + "1" + ], + [ + 247, + "-1" + ], + [ + 252, + "-1" + ], + [ + 253, + "1" + ], + [ + 254, + "1" + ], + [ + 255, + "-1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "zero_event": 17245, + "zero_factor": "1/4", + "zero_role": 240 + }, + { + "cached_event": 11283, + "cached_role": 9, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11488, + "frame": 624, + "relation": [ + [ + 257, + "1" + ], + [ + 259, + "-1" + ], + [ + 261, + "1" + ], + [ + 263, + "-1" + ], + [ + 268, + "-1" + ], + [ + 269, + "-1" + ], + [ + 270, + "1" + ], + [ + 271, + "1" + ] + ], + "zero_event": 15870, + "zero_factor": "-1/4", + "zero_role": 9 + }, + { + "cached_event": 11306, + "cached_role": 288, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11514, + "frame": 281, + "relation": [ + [ + 288, + "1" + ], + [ + 294, + "-1" + ], + [ + 296, + "-1" + ], + [ + 297, + "-1" + ], + [ + 300, + "1" + ], + [ + 303, + "1" + ] + ], + "zero_event": 17580, + "zero_factor": "-1/4", + "zero_role": 288 + } + ] + }, + "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": "Declared zero identity" + }, + "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_00302666_EIGHT_JOINT_RELATIONS", + "word_payload_sha256": "2aee5e997df99726fc763e510d9cb69fbe4f86114dc8d2cd33ad26c6c462a21d" +} diff --git a/research/kappa-joint-relations-20261023/SOURCES.json b/research/kappa-joint-relations-20261023/SOURCES.json new file mode 100644 index 0000000000..71c57c8a90 --- /dev/null +++ b/research/kappa-joint-relations-20261023/SOURCES.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b288ae44032fd84dd5564243422836cbcd29835e", + "sha256": "f9ed52bb642cd1e1486cf2743557ac5fa23cf1514a3277d786a644e39a565038" + }, + { + "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-joint-relations-20261023/TASK.json b/research/kappa-joint-relations-20261023/TASK.json new file mode 100644 index 0000000000..5b57a9e823 --- /dev/null +++ b/research/kappa-joint-relations-20261023/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "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": "Prepare eight independent cold-helper relations, replace all eight backward centers with exact snapshots, remove eight later zero jobs, and debit eight rank-nine helper targets per backward call.", + "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-19154290", + "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": "WITNESS.json, WORD.json.gz, RESULT.json and the full exact verifier. Conditional kappa 0.00302666.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance in discovery, code, proof, verification and publication.", + "open_questions": [ + { + "question": "Can an independent reviewer validate the joint relation system and all inherited physical transfer premises?", + "why_it_matters": "The finite exact construction still uses the five selected framework assumptions.", + "first_step": "Check the sixteen unrestricted row identities, eight pivots and complete cost in README.md and RESULT.json.", + "blocked_by": "Independent review has not yet occurred." + }, + { + "question": "Can a different relation system improve the complete bill beyond this fixed profile?", + "why_it_matters": "The new profile ceiling is not an optimum over helper relations.", + "first_step": "Check live claims, then charge each lost target and prove an additional removed job.", + "blocked_by": "All eight backward center jobs are already removed in this construction." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19154290", + "distinct_scopes": [ + "https://github.com/CrocSwap/integer-mult-bounds/discussions/5355", + "https://github.com/CrocSwap/integer-mult-bounds/discussions/4930" + ], + "boundary": "This extends our frozen PR5377 relation to a joint rank-eight system. The original-input cache scope is released. The coded caller retains all original helpers; this package changes eight helper inputs per backward call. No shared controller or selected file changes." + } +} diff --git a/research/kappa-joint-relations-20261023/VERIFY.json b/research/kappa-joint-relations-20261023/VERIFY.json new file mode 100644 index 0000000000..8098df4c80 --- /dev/null +++ b/research/kappa-joint-relations-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-joint-relations-20261023/WITNESS.json b/research/kappa-joint-relations-20261023/WITNESS.json new file mode 100644 index 0000000000..19665f9eac --- /dev/null +++ b/research/kappa-joint-relations-20261023/WITNESS.json @@ -0,0 +1,434 @@ +[ + { + "relation": [ + [ + 230, + "1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ] + ], + "event": 11332, + "frame": 254, + "cached_event": 11205, + "cached_role": 92, + "zero_event": 15584, + "zero_role": 92, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + }, + { + "relation": [ + [ + 225, + "1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "event": 11358, + "frame": 274, + "cached_event": 11218, + "cached_role": 57, + "zero_event": 17264, + "zero_role": 57, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + }, + { + "relation": [ + [ + 225, + "1" + ], + [ + 227, + "-1" + ], + [ + 229, + "1" + ], + [ + 231, + "-2" + ], + [ + 232, + "1" + ], + [ + 234, + "-1" + ], + [ + 235, + "-1" + ], + [ + 236, + "-1" + ], + [ + 237, + "-1" + ], + [ + 238, + "2" + ], + [ + 239, + "1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "event": 11384, + "frame": 619, + "cached_event": 11231, + "cached_role": 81, + "zero_event": 17256, + "zero_role": 81, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + }, + { + "relation": [ + [ + 227, + "1" + ], + [ + 229, + "1" + ], + [ + 232, + "-1" + ], + [ + 234, + "1" + ], + [ + 235, + "1" + ], + [ + 236, + "-1" + ], + [ + 237, + "1" + ], + [ + 239, + "-1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ] + ], + "event": 11410, + "frame": 279, + "cached_event": 11244, + "cached_role": 224, + "zero_event": 17722, + "zero_role": 224, + "copy_factor": "1", + "difference_factor": "-1/4", + "zero_factor": "1/4" + }, + { + "relation": [ + [ + 241, + "1" + ], + [ + 243, + "-1" + ], + [ + 245, + "1" + ], + [ + 247, + "-1" + ], + [ + 252, + "-1" + ], + [ + 253, + "-1" + ], + [ + 254, + "1" + ], + [ + 255, + "1" + ] + ], + "event": 11436, + "frame": 621, + "cached_event": 11257, + "cached_role": 11, + "zero_event": 15876, + "zero_role": 11, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + }, + { + "relation": [ + [ + 225, + "1" + ], + [ + 241, + "-1" + ], + [ + 243, + "1" + ], + [ + 245, + "1" + ], + [ + 247, + "-1" + ], + [ + 252, + "-1" + ], + [ + 253, + "1" + ], + [ + 254, + "1" + ], + [ + 255, + "-1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "event": 11462, + "frame": 280, + "cached_event": 11270, + "cached_role": 240, + "zero_event": 17245, + "zero_role": 240, + "copy_factor": "1", + "difference_factor": "-1/4", + "zero_factor": "1/4" + }, + { + "relation": [ + [ + 257, + "1" + ], + [ + 259, + "-1" + ], + [ + 261, + "1" + ], + [ + 263, + "-1" + ], + [ + 268, + "-1" + ], + [ + 269, + "-1" + ], + [ + 270, + "1" + ], + [ + 271, + "1" + ] + ], + "event": 11488, + "frame": 624, + "cached_event": 11283, + "cached_role": 9, + "zero_event": 15870, + "zero_role": 9, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + }, + { + "relation": [ + [ + 288, + "1" + ], + [ + 294, + "-1" + ], + [ + 296, + "-1" + ], + [ + 297, + "-1" + ], + [ + 300, + "1" + ], + [ + 303, + "1" + ] + ], + "event": 11514, + "frame": 281, + "cached_event": 11306, + "cached_role": 288, + "zero_event": 17580, + "zero_role": 288, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + } +] diff --git a/research/kappa-joint-relations-20261023/WORD.json.gz b/research/kappa-joint-relations-20261023/WORD.json.gz new file mode 100644 index 0000000000..a4a58afce1 Binary files /dev/null and b/research/kappa-joint-relations-20261023/WORD.json.gz differ diff --git a/research/kappa-joint-relations-20261023/native.py b/research/kappa-joint-relations-20261023/native.py new file mode 100644 index 0000000000..cbff46fe6e --- /dev/null +++ b/research/kappa-joint-relations-20261023/native.py @@ -0,0 +1,344 @@ +"""Eight prepared helpers remove sixteen paid jobs in the PR4610 backward word. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +This extends Ali Romman's one-relation PR5377 at c448d13c71908647f968b06cddb795ce7d288139. +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' +WITNESSES = json.loads((HERE / 'WITNESS.json').read_text(encoding='utf-8')) +COUNT = 8 +OLD_PAID = {1: 2201, 2: 412, 3: 510, 4: 127, 5: 40, 8: 8} +NEW_PAID = dict(OLD_PAID) +NEW_PAID[1] -= COUNT +NEW_PAID.pop(8) +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 relation_system(): + """Find exact independent pivots and eliminate all other pivot columns.""" + basis = {} + need(len(WITNESSES) == COUNT, 'Eight declared witnesses') + for witness in WITNESSES: + pairs = witness['relation'] + row = {h: Q(q) for h, q in pairs} + need(len(row) == len(pairs) and all(224 <= h < 632 and q for h, q in row.items()), 'Distinct helper coefficients') + for pivot, prior in sorted(basis.items()): + add(row, prior, -row.get(pivot, Q(0))) + need(row, 'Independent helper relations') + pivot = min(row); scale = row[pivot] + row = {h: q / scale for h, q in row.items()} + for prior in basis.values(): + add(prior, row, -prior.get(pivot, Q(0))) + basis[pivot] = row + need(len(basis) == COUNT, 'Eight paid helper outputs removed') + for pivot, row in basis.items(): + need(all(row.get(h, 0) == int(h == pivot) for h in basis), 'Reduced pivot columns') + return dict(sorted(basis.items())) + + +BASIS = relation_system() + + +def construct(source): + c = source['canonical']; old = source['programs']['backward'] + all_helpers = {h for x in WITNESSES for h, _ in x['relation']} + need(all(c['start'][h] == 0 and c['final'][h] == 1 for h in all_helpers), 'Every relation uses cold full-ended helpers') + snapshots, centers, zeros = {}, {}, {} + for slot, x in enumerate(WITNESSES, 1): + frame, role = x['frame'], x['cached_role'] + need(old[x['event']] == ['center', 0, 0, frame, 8], 'Exact source center') + event = old[x['cached_event']] + need(event[0] == 'climb' and event[2] == role and event[4] == frame, 'Exact snapshot source') + need(old[x['zero_event']] == ['climb', 'warp_retimed', x['zero_role'], frame, 1, 1], 'Exact zero source job') + need(x['cached_event'] < x['event'] < x['zero_event'] and Q(x['copy_factor']) == 1, 'Snapshot chronology and COPY coefficient') + snapshots[x['cached_event']] = (slot, x) + centers[x['event']] = (slot, x) + zeros[x['zero_event']] = x + need(len(snapshots) == len(centers) == len(zeros) == COUNT, 'Distinct replacement sites') + word = [] + for pivot, row in BASIS.items(): + word.append(['scalar', ['clear', ['L', pivot]], 0]) + for h, q in sorted(row.items()): + if h != pivot: + word.append(['scalar', ['add', ['L', pivot], ['L', h], -q.numerator, q.denominator], 0]) + for index, event in enumerate(old): + if index in centers: + slot, x = centers[index]; f = x['frame'] + word += [['scalar', ['clear', ['C', 0]], f], + ['scalar', ['copy', ['C', 0], ['C', slot]], f], + ['scalar', ['clear', ['C', slot]], f]] + elif index in zeros: + x = zeros[index] + word.append(['zero_retag', ['L', x['zero_role']], x['frame'], 1]) + else: + word.append(deepcopy(event)) + if index in snapshots: + slot, x = snapshots[index]; f = x['frame'] + word += [['scalar', ['clear', ['C', slot]], f], + ['scalar', ['copy', ['C', slot], ['L', x['cached_role']]], f]] + word += [['scalar', ['clear', ['L', h]], 1] for h in BASIS] + physical = deepcopy(c); physical.pop('local_profile') + return {'schema': 'joint-helper-relations-word/1', 'canonical': physical, + 'relation_basis': encode(BASIS), + 'paid_profiles': {'forward': OLD_PAID, 'backward': NEW_PAID}, + 'owned': {'forward': [['C', 0]], 'backward': [['C', i] for i in range(COUNT + 1)] + [['L', h] for h in BASIS]}, + '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', i) for i in range(1, COUNT + 1)} | {('L', h) for h in BASIS} 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 any(dst == ('L', x['zero_role']) and (old, new) == (x['frame'], 1) for x in WITNESSES), 'Declared zero identity') + need(frames[dst] == old and not rows[dst], 'Zero identity requires an identically zero full row') + 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 == COUNT * int(specialized), 'All eight zero identities checked') + 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': 632 - COUNT 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): + """Check unrestricted source identities with the predecessor row engine.""" + v = load('research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py', 'joint_relation_source_rows') + rows = {('L', i): v.identity(('L', i)) for i in range(632)} + rows['C', 0] = v.identity(('C', 0)); saved = {}; checked = [] + 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) + for x in WITNESSES: + delta = {(('L', h), ()): Q(q) for h, q in x['relation']} + if index == x['cached_event']: + saved[index] = dict(rows['L', x['cached_role']]) + if index == x['event']: + diff = dict(rows['C', 0]); v.add(diff, saved[x['cached_event']], -Q(x['copy_factor'])) + need(diff == {k: Q(x['difference_factor']) * q for k, q in delta.items()}, 'Independent exact center minus snapshot identity') + checked.append(('center', index)) + if index == x['zero_event']: + need(rows['L', x['zero_role']] == {k: Q(x['zero_factor']) * q for k, q in delta.items()}, 'Independent exact zero-site row identity') + checked.append(('zero', index)) + need(len(checked) == 2 * COUNT, 'Sixteen unrestricted source identities') + 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, 'witnesses': WITNESSES, + 'relation_rank': COUNT, 'owned_pivots': list(BASIS), 'reduced_basis': BASIS, + 'snapshot_terms_before_substitution': {i: len(row) for i, row in saved.items()}, + 'checked': checked} + + +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 x in WITNESSES for i in (x['event'], x['zero_event'])) + need(old_paid - new_paid == expected and not new_paid - old_paid, 'Only the sixteen 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-joint-relations-20261023/price.py b/research/kappa-joint-relations-20261023/price.py new file mode 100644 index 0000000000..2868905a16 --- /dev/null +++ b/research/kappa-joint-relations-20261023/price.py @@ -0,0 +1,198 @@ +"""Complete p16 bill and finite compiler for eight joint helper relations. + +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, COUNT + +KAPPA = Q('.00302666') +TESTED = Q('.00302667') +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 complete 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 * COUNT + 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 * COUNT; check_P[8] -= 16 * COUNT + need(T == check_T and P == check_P, 'Independent full invoice substitution') + need(sum(T.values()) == 10800 and sum(P.values()) == 64148, '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 * COUNT; prior_P[1] -= 16 * COUNT; prior_P[8] -= 16 * COUNT + 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(Q('.00302238736348'))[0] > 0, 'Changed invoice beats the PR5377 raw crossing') + 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()) + # Charge both routes for each of eight snapshots and eight owned helpers. + # The eight owned helpers use existing physical slots. + routes = (max(sum(x['paid'].values()) for x in native.values()) + 2 * 408 + 688 + 4 * COUNT) * 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': '.00302666', 'gain_over_PR4610': KAPPA - PREVIOUS, + 'gain_over_PR5377': KAPPA - Q('.00302235'), 'PR5377_raw_root_upper': Q('.00302238736348'), + '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': COUNT, 'owned_slots_backward': 2 * COUNT + 1}, + 'ordinary_BIT': bit, 'outer': outer, 'negative_controls': controls}) diff --git a/research/kappa-joint-relations-20261023/verify.py b/research/kappa-joint-relations-20261023/verify.py new file mode 100644 index 0000000000..3f7eb9359a --- /dev/null +++ b/research/kappa-joint-relations-20261023/verify.py @@ -0,0 +1,64 @@ +#!/usr/bin/env python3 +"""Replay the joint-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] -= N.COUNT + 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_00302666_EIGHT_JOINT_RELATIONS', + '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', 'gain_over_PR5377', 'raw_root_interval', 'paid_calls', 'productive_fields')}}, sort_keys=True)) + + +if __name__ == '__main__': + main()