From 6919161525e69b687630cb6468aa32b9414d7206 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 17:53:17 -0500 Subject: [PATCH 1/2] Retain the owned native profile for the controller ceiling --- .../global-query-controller-ceiling/source/NOTICE.md | 10 ++++++++++ .../source/transpose-RESULT.json | 1 + 2 files changed, 11 insertions(+) create mode 100644 research/global-query-controller-ceiling/source/NOTICE.md create mode 100644 research/global-query-controller-ceiling/source/transpose-RESULT.json diff --git a/research/global-query-controller-ceiling/source/NOTICE.md b/research/global-query-controller-ceiling/source/NOTICE.md new file mode 100644 index 0000000000..97dacf2cd0 --- /dev/null +++ b/research/global-query-controller-ceiling/source/NOTICE.md @@ -0,0 +1,10 @@ +# Copied source files + +Apache-2.0. Preserve the source headers. No copied source file is modified. + +- `owned/native.py` and its unchanged `WITNESS.json`: Ali Romman's [PR5383 native construction](https://github.com/aliromman/integer-mult-bounds/blob/4bd6efa51a495a7c7b7754915cf0244e7e60969e/research/kappa-joint-relations-20261023/native.py). Only its pure construction, scalar allowance and exact row replay functions are called. The package's independent pins bind its source inputs. Its original notices credit Cao Yifan, Cinna Davis and zxv. +- `cutoff/exact.py`, `cutoff/native.py`, `cutoff/native_identity.py` and `cutoff/check_certificate.py`: Ali Romman's [PR5369 native tensor package](https://github.com/aliromman/integer-mult-bounds/tree/18354f41de4dc7bfda4692e814cf1d91a6d619ef/research/native-tensor-cutoff). The [complete proof and source credit](https://github.com/aliromman/integer-mult-bounds/blob/18354f41de4dc7bfda4692e814cf1d91a6d619ef/research/native-tensor-cutoff/PROOF.md) retain the native recipe lineage of Jose Manuel/jmbarrancoml, Douglas Colkitt and the listed contributors, plus the classical Fourier, binary Gram factorization, finite-group, Cook and Barrington results. This package uses the positive identity decision and the separately implemented certificate checker. It does not claim those results as new. + +The local `price.py` is an adapted version of the [PR5377 complete price engine](https://github.com/aliromman/integer-mult-bounds/blob/c448d13c71908647f968b06cddb795ce7d288139/research/kappa-owned-relation-20261023/price.py). Its notice credits Cao Yifan, Cinna Davis, zxv and Jacob Alan Sussman. The new census debits the eight owned helpers in all 18 full calls and includes every forward transpose wrapper. + +Substantial OpenAI Codex assistance was used in both source packages and in this contribution. Source links are fixed commits; SOURCES.json records each copied blob and byte hash. diff --git a/research/global-query-controller-ceiling/source/transpose-RESULT.json b/research/global-query-controller-ceiling/source/transpose-RESULT.json new file mode 100644 index 0000000000..32d9851bca --- /dev/null +++ b/research/global-query-controller-ceiling/source/transpose-RESULT.json @@ -0,0 +1 @@ +{"arithmetic":{"PR5383_raw_root_upper":"37833434601/12500000000000","compiler":{"H":31385200000000,"N":"2^31385200000000","eta":{"lower":"0.000000198896818191972299783809","upper":"0.000000198896818191972299783810"},"gap":"1/700000000","integer_test_exponent":44836,"logarithm_power":1000,"theta":"63/64","uniform_saving":"2119081/700000000","word_materialized":false},"fixed_profile_ceiling":{"decreasing_through":"1/20","derivative_upper":{"lower":"-195429.853549519051730354837623051264","upper":"-195429.853549519051730354837623051263"},"remaining_interval_moment_upper":{"lower":"-6817.813214098317476830090331963946","upper":"-6817.813214098317476830090331963945"}},"full_backward":16,"full_forward":2,"gain_over_PR4610":"27371/5000000000","gain_over_PR5383":"59/100000000","kappa":"12109/4000000","kappa_decimal":".00302725","margin_at_PR5383_raw_root_upper":{"lower":"0.151387988317648054643094222493","upper":"0.151387988317648054643094222494"},"margin_at_previous_kappa":{"lower":"1.360313469048365037022624303111","upper":"1.360313469048365037022624303112"},"margin_at_previous_root_upper":{"lower":"1.360296002377893907536683455026","upper":"1.360296002377893907536683455027"},"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":10292000,"local_scalar":159320,"owned_slots_per_direction":17,"raw_budget":1000000000,"raw_scalar_upper":361098496},"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":"741677648940461/245000000000000000","fused_gaussian":"741677646821383/245000000000000000","global_coordinate_router":"2119079/700000000","group_bit_router":"1483355993642763/490000000000000000","group_scans":"349999999/350000000","main_transform":"741677298940461/245000000000000000","microbox_face_corrections":"13475000001/175000000","polynomial_products":"699999999/700000000","sparse_union_movement":"100272927648940461/245000000000000000"},"parameters":{"a":"2119079/700000000","b":"52977/17500000","beta":"699999997/700000000","bit_saving":"17/5000","cap_xi":"222772927298940461/245000000000000000","complex_uniform_saving":"2119081/700000000","d":"1/700000000","epsilon":"699999999/700000000","kappa":"12109/4000000","lambda_":"199394549/200000000","lambda_prime":"348940461/350000000","layout":"1/700000000","q":"1059539/350000000","r0":"1/7000000000","stop":"1/700000000","tested_saving":"151363/50000000"},"strict_checks":{"actual_bit_above_effective":"260921/700000000","actual_logarithmic_gamma_guard":"1/700000000","actual_logarithmic_group_guard":"22227073226059539/122500000000000000","alpha_logarithm_absorption":"1/7000000000","boundary_algebraic_matrix_above_kappa":"1398940461/245000000000000000","cap_above_band":"100272927298940461/245000000000000000","cap_below_cell":"22227072351059539/245000000000000000","cap_below_phase_cell_power":"267227072701059539/245000000000000000","complex_above_effective":"1/700000000","complex_below_one_over_32":"246949/8750000","complex_endpoint":"1/350000000","epsilon_below_one":"1/700000000","epsilon_positive":"699999999/700000000","fine_prime_halo_umbrella":"7/2","fused_gaussian_above_kappa":"1396821383/245000000000000000","gaussian_above_main":"173940461/122500000000000000","global_coordinate_router_above_kappa":"1/175000000","global_gamma_power_slack":"9/7000000000","group_below_dimension":"1/350000000","group_bit_router_above_kappa":"3493642763/490000000000000000","group_gauge_power_slack":"22227073208559539/122500000000000000","group_key_fits_record":"1/350000000","group_positive":"699999997/700000000","group_scans_above_kappa":"697880923/700000000","halo_covers_generic_inverse_radius":"5","improvement_over_user_baseline":"648139790400418148631/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":"34947023/12250000000000000","leaf_saving_above_effective":"17447023/12250000000000000","main_transform_above_kappa":"1048940461/245000000000000000","membership_arithmetic_fits_record":"1/700000000","microbox_face_corrections_above_kappa":"53897880929/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":"174470231/175000000","positive_layout_slack":"1/700000000","q_below_effective":"1/700000000","q_below_internal":"1/700000000","q_below_leaf":"34947023/12250000000000000","q_positive":"1059539/350000000","short_record_fallback":"17447023/17500000","source_axis_superpolynomial":"1/700000000","sparse_union_movement_above_kappa":"99531251398940461/245000000000000000","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":41154,"16":448,"2":7416,"24":448,"3":9180,"32":448,"4":2286,"40":448,"48":448,"5":720,"56":448,"64":448,"72":224},"paid_calls":64116,"productive_fields":10784,"query_shears":15,"rank_mass_surplus":752,"raw_headroom":["3824993/100000000000000","1912497/50000000000000"],"raw_root_interval":["302728824993/100000000000000","151364412497/50000000000000"],"strictification":{"alpha":{"lower":"0.999999970464534591128115679621","upper":"0.999999970464534591128115679622"},"cutoff":20,"delta":{"lower":"0.950818834663934748568486126695","upper":"0.950818834663934748568486126696"},"floor":21,"gamma":{"lower":"0.957062946439347991413082521771","upper":"0.957062946439347991413082521772"},"normalized_paid_upper":"2097152001953127/2097154147483648","power":1024,"reserve":"1/1000000000","tail_offset":"1/5","tested":"151363/50000000"},"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":5724}},"interface":{"D_exponent_is_formal":true,"Q_exponents_modulus":4,"copy_and_clear_checked":true,"identity":"F = J B^T J; J = diag(Q^2,-I)","missing_transpose_rejected":true,"scalar_coefficients_checked":5,"scalar_sign_counterexample":{"axes":9,"character":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"discrepancy":["2","0"],"input_points":[0,1,2,4,8,16,32,64,128,256,1,2,4,8,16,32,64,128,256,511,511,0,0,0],"input_role":0,"output_points":[0,1,2,4,8,16,32,64,128,256,1,2,4,8,16,32,64,128,256,511,511,0,0,0],"output_role":0,"peak_expanded_terms":1,"problem_sha256":"21a755f2a34d1a25e602dd888bb935c67dae506c5a2fd326d0178e554e5866bb","residual_terms":2,"roles":1,"schema":"native-tensor-cutoff/v1","status":"COUNTEREXAMPLE","window":[22,25]},"wrong_Q_correction_rejected":true},"native":{"controls":{"missing_owned_clear":"('Endpoint', 112, 3, {(112, ()): Fraction(1, 1), (0, ()): Fraction(-1, 1), (633, ()): Fraction(1, 4)})","wrong_native_transpose":"('Endpoint', 400, 12, {(411, ()): Fraction(-1, 2), (400, ()): Fraction(1, 2), (15, ()): Fraction(-1, 2), (410, ()): Fraction(1, 2), (406, ()): Fraction(-1, 2), (53, ()): Fraction(-","wrong_prepared_relation":"('Endpoint', 384, 151, {(384, ()): Fraction(1, 1), (388, ()): Fraction(-1, 1), (398, ()): Fraction(-1, 1), (253, ()): Fraction(1, 1), (239, ()): Fraction(1, 1), (81, ()): Fraction(","wrong_transposed_add":"('Endpoint', 382, 1, {(383, ()): Fraction(-1, 1)})"},"literal_word_sha256":"737caaf8ed380ec2bdac2452839c3fb8a3ddf68136a8f6fee8c4419cfccdc076","native":{"axes":9,"peak_expanded_terms":24664,"problem_sha256":"a4c901e27b21dc7033ff8ace1217165eabb5e59ecd301dba321f76940db8be05","residual_terms":0,"roles":641,"schema":"native-tensor-cutoff/v1","status":"IDENTITY_ALL_POSITIVE_WIDTHS","window":[22,25]},"native_sign_counterexample":{"axes":9,"character":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"discrepancy":["-1/2","0"],"input_points":[0,1,2,4,8,16,32,64,128,256,1,2,4,8,16,32,64,128,256,511,511,0,0,0],"input_role":411,"output_points":[0,1,2,4,8,16,32,64,128,256,1,2,4,8,16,32,64,128,256,511,511,0,0,0],"output_role":400,"peak_expanded_terms":24746,"problem_sha256":"e2134063e1fb9a6073200d9f298253829c96d767d46aa7a77d17ae0977ed450a","residual_terms":84,"roles":641,"schema":"native-tensor-cutoff/v1","status":"COUNTEREXAMPLE","window":[22,25]},"new_monomial_passes_bound":624,"paid":{"1":2193,"2":412,"3":510,"4":127,"5":40},"real_scalar_allowance":159320,"real_scalar_allowance_before_wrappers":158872,"source_counts":{"adapter":448,"climb":3282,"phase":10,"scalar":17563,"warp":240,"zero_retag":8},"source_replay":{"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},"source_word_sha256":"2aee5e997df99726fc763e510d9cb69fbe4f86114dc8d2cd33ad26c6c462a21d","transpose":{"all_entry_columns":641,"ghost_terms_at_return":0,"max_denominator":32,"max_formal_prefix_l1":"442"}},"physical":{"Q_squared_ports":112,"literal_native_transpose_columns":92160,"native_warp_classes":180,"paid_classes":2847,"source_clifford_sha256":"2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962","symmetric_helper_ranks":[4,7,8,9],"wrong_absolute_phase_rejected":"Transposed paid absolute phase"},"status":"PASS_CONDITIONAL_KAPPA_00302725_OWNED_TRANSPOSE"} From 314b56a6c0056c2358538f072c6fde9d365be44d Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 18:01:16 -0500 Subject: [PATCH 2/2] Prove the unbounded FULL/QUERY controller ceiling --- .../global-query-controller-ceiling/PROOF.md | 208 +++++ .../global-query-controller-ceiling/README.md | 74 ++ .../RESULT.json | 839 ++++++++++++++++++ .../SOURCES.json | 76 ++ .../global-query-controller-ceiling/TASK.json | 110 +++ .../VERIFY.json | 40 + .../global-query-controller-ceiling/verify.py | 230 +++++ 7 files changed, 1577 insertions(+) create mode 100644 research/global-query-controller-ceiling/PROOF.md create mode 100644 research/global-query-controller-ceiling/README.md create mode 100644 research/global-query-controller-ceiling/RESULT.json create mode 100644 research/global-query-controller-ceiling/SOURCES.json create mode 100644 research/global-query-controller-ceiling/TASK.json create mode 100644 research/global-query-controller-ceiling/VERIFY.json create mode 100644 research/global-query-controller-ceiling/verify.py diff --git a/research/global-query-controller-ceiling/PROOF.md b/research/global-query-controller-ceiling/PROOF.md new file mode 100644 index 0000000000..5ad89d4ba1 --- /dev/null +++ b/research/global-query-controller-ceiling/PROOF.md @@ -0,0 +1,208 @@ +# A ceiling for every prefix/suffix FULL/QUERY allocation + +## Result and scope + +Fix the bidirectional local profiles from PR5392: + +``` +paid P = {1:2193, 2:412, 3:510, 4:127, 5:40} +helper targets H = {4:28, 7:7, 8:47, 9:318}. +``` + +A full stage has 112 main ports and a fresh block of rank eight. A query stage +costs 112 H1 jobs and has no helper targets. Use the paired path controller +with any integer p >= 1, any split 0 <= a <= p-1, and b = p-1-a. Keep the +first a initial idle windows, all middle idle windows, and the last b terminal +idle windows. Each of the 2p+1 stages can independently be FULL or QUERY. +Specialize D_s=1 at each QUERY stage in both the main and idle products. + +**Theorem.** Every invoice in this family has paid moment greater than target +moment for every `0.00302728825 <= kappa < 1`. Thus this entire family fails +the necessary strict moment test in that range. The result includes arbitrarily +many pairs, every split, and all stage masks. It is not restricted to a small +number of changes from the current mask. + +This is an upper bound for the invoices defined by (1) and the strict moment +method. A different target list or idle law is outside the theorem. It is +not a lower bound for all native circuits or all multiplication algorithms. +It does not raise kappa. In particular, it does not prove the physical validity +of every masked word, a new compiler bound, or an unconditional multiplication +theorem. We grant the listed diagonal jobs to the entire family. A member that +fails a separate native or endpoint requirement cannot evade this ceiling. + +The local profile is a premise supplied by PR5392. The source receipt is retained +byte for byte. The complete source construction and its five framework assumptions +are not re-proved here. PR5398 uses the same recursive profile and reports complete +conditional kappa .00302728823. Its distance from this universal family ceiling +is less than 2e-11. This comparison does not independently admit PR5398. + +## 1. Complete interval invoice + +Put t=1-kappa, f(r)=r^t for r>0, and f(0)=0. Define + + L(t) = sum_r P[r] f(r) - sum_r H[r] f(r). + +Write x_s in {0,1} for the FULL indicator of stage s, and +`n=sum_{s=0}^{2p} x_s`. The local and query part of paid minus target is + + 112(2p+1) + (L(t)-112)n. + +There are 224 full-path main targets of rank 1+8n. For j=1,...,a, put + + h_j = sum_{s=0}^{2j-1} x_s, e_j = x_(2j). + +For j=a+1,...,p-1, put + + h_j = sum_{s=2j+1}^{2p} x_s, e_j = x_(2j). + +Each j contributes a retained whole idle of rank 8h_j, a main target of rank +`1+8(h_j+e_j)`, and a middle idle of rank eight if e_j=1. Each multiplicity is +224. Zero-rank idles are omitted. The complete difference is therefore + + E(t) = 112(2p+1) + (L(t)-112)n - 224 f(1+8n) + + 224 sum_j [f(8h_j) + e_j f(8) - f(1+8(h_j+e_j))]. (1) + +This includes every lost helper and every changed main and idle factor. +In particular, a FULL even stage restores its middle idle charge. The source +Laurent controller supplies the prefix/suffix products. Substitution of D_s=1 +preserves any established source identity; it does not preserve a removed +stage's helper credit. + +The verifier compares (1), as separate paid and target histograms, with the +retained literal Laurent controller on every mask for p=1,...,5 and every a. +It also compares the current p16/a7 invoice with the retained PR5392 receipt +and the separate main diagonal in `joint-helper-lattice/CONTROLLER.json`. +These checks bind the general formula to the source family. They are not a +native admission of all p or a proof from finite examples. + +## 2. An infinite tail becomes finite + +For 0=0 and e in {0,1}, + + f(8h) + e f(8) - f(1+8(h+e)) >= -1. (2) + +For e=0, use `f(z+1)-f(z) <= f(1)=1`. For e=1, use +`f(z+8+1) <= f(z)+f(8)+f(1)`. There are p-1 summands. Equation (1) gives + + E(t) >= B_t(n) := 336 + (L(t)-112)n - 224(1+8n)^t. (3) + +At `kappa_0 = 0.00302728825`, exact outward rational arithmetic proves + + B_t(96) > 104.185162541469147567554569434096, + B_t'(96) > 5.188985973480417120924401618389. + +Here `B_t'(n)=L(t)-112-1792t(1+8n)^(t-1)`. Since t<1, this derivative +increases with n. Thus every n>=96 has E(t)>0, for every p and split. +The program uses a lower bound for L and an upper bound for the power in +both comparisons. No floating tolerance is used. + +It remains to bound p when n<=95. Read the left side in the order +`x_0,(x_1,x_2),...,(x_(2a-1),x_(2a))`. Read the right side from the opposite +end in the same form. The central stage is `x_(2a+1)`. If a side pair has +both indicators zero, delete that pair and reduce p by one. The full-stage +count n and every later partial count stay fixed. The two removed queries +reduce the first term in (1) by 224. The removed summand is + + -224 [f(8h+1)-f(8h)] >= -224. + +The deletion therefore cannot increase E. It produces another member of the +same invoice family after reindexing. Repeat until each remaining side pair +contains a FULL stage. Then `p-1=a+b <= n`, so p<=96. Consequently, positivity +for all p<=96 and n<=95, together with (3), proves positivity at kappa_0 for +the unbounded family. This reduction does not claim that deletion preserves +a particular caller's input set; it compares the optimistic invoices needed +for this ceiling. + +## 3. Exact dynamic program for the finite part + +For a side with q pairs and k FULL stages, let D_q(k) be the minimum sum of +its summands in (1), including their factor 224. The single end stage gives + + D_0(0)=D_0(1)=0. + +Append the next odd/even indicators o,e in {0,1}. The recurrence is + + D_(q+1)(k+o+e) = min [D_q(k) + +224 (f(8(k+o)) + e f(8) - f(1+8(k+o+e)))]. (4) + +The minimum is over all predecessors. This follows directly from the partial +count before the even stage. Induction on q proves that (4) covers every side +mask. States with k>=96 can be omitted because total FULL count cannot decrease. + +For p=a+b+1, combine left count l, right count r, and central indicator c: + + 112(2p+1) + (L-112)(l+r+c) + D_a(l) + D_b(r) + -224 f(1+8(l+r+c)). (5) + +Discard only totals at least 96. Reflection exchanges a and b, so it suffices +to check a<=b. The program checks p=1,...,96 and 10,290,000 state combinations. +It uses integer bounds on the exact grid 2^192. Positive terms use lower +power bounds; negative terms use upper bounds. Taking a minimum of lower +bounds remains a lower bound, so interval overlap cannot create a false +positive certificate. The minimum certified lower bound is + + E(t) > 0.000000014914967918767741908079. + +It occurs at p=16, a=7, with eight FULL stages on the left, nine on the right, +and a FULL central stage. The receipt retains the exact rational bound and +the minimum for each p. Independent exhaustive mask enumeration through p=5 +agrees exactly with the integer dynamic-program minima. + +The interval engine is the unchanged rational logarithm/exponential engine +from `higher-moment-strictification`. The dynamic program is new. Neither is +a solver result, and no SciPy or floating arithmetic is used for acceptance. + +## 4. Extend the ceiling to all larger savings + +It is not enough to reject one value of kappa. We now show that no larger +value can become favorable in this family. + +First delete zero/zero side pairs as above, at the t under consideration. +If n=0, (1) gives E(t)=112, which is positive. Otherwise n>=1. Normalize (1) +by 8^t. In a reduced side pair, h>=1 if e=0, while h>=0 if e=1. Its normalized +summand is + + h^t + e - (h+e+1/8)^t. + +For h>=1 its derivative in t is negative, because `z^t log z` strictly +increases for z>=1. For h=0, reduction forces e=1, and the derivative of +`1-(9/8)^t` is also negative. The normalized full-path target term has negative +derivative, since n+1/8>1. The query term is nonnegative and nonincreasing. + +Finally the local term is strictly decreasing after the same normalization: + + L(t)/8^t = 2193(1/8)^t + 412(1/4)^t + 510(3/8)^t + + 99(1/2)^t + 40(5/8)^t + - 7(7/8)^t - 47 - 318(9/8)^t. + +Its only positive derivative term is less than `7 log(8/7) < 1`. The negative +term from `2193(1/8)^t` alone has magnitude at least `2193 log(8)/8 > 274` +on 0=1. + +Therefore a reduced invoice that is positive at t_0=1-kappa_0 remains +positive for every 0=1, every split, +and every FULL/QUERY assignment among the 2p+1 stages. + +[PROOF.md](PROOF.md) gives the reduction from this infinite family to a finite +dynamic program. [RESULT.json](RESULT.json) records exact rational bounds, +all per-p minima, source checks and negative controls. A tail inequality removes +all cases with at least 96 FULL stages. Deleting a pair of QUERY stages reduces +the remaining search to p<=96. The verifier then checks 10,290,000 state +combinations with directed integer arithmetic. It uses no floating solver. + +The smallest certified paid-minus-target margin at the ceiling is greater than +`0.000000014914967918767741908079`. The best finite state remains p16/a7 with +18 FULL stages. Literal Laurent invoices on all masks through p=5 provide a +separate check of the formula and dynamic program. + +The existing complete conditional comparison is +[kappa .00302728823 in PR5398](https://github.com/CrocSwap/integer-mult-bounds/pull/5398), +which uses the same recursive profile. Its remaining room within this whole +family is less than 2e-11. That construction and its compiler are credited +external results, not newly admitted here. The selected record remains +.0030217758 at canonical main `1ec1119972c9aefe42525172d07b332fcff81cb4`. + +The fixed profiles come from +[PR5392](https://github.com/CrocSwap/integer-mult-bounds/pull/5392), head +`329b2ff35d2994b11abbb59f770d12da75c494ac`. Its exact result and source notice +are retained under `source/`. Paths and package descriptions in that unchanged +notice refer to PR5392, not to this package. The new theorem extends the at-most-two-stage +screen in [PR5393](https://github.com/CrocSwap/integer-mult-bounds/pull/5393) +and the fixed center-exchange invoice ceiling in +[PR5397](https://github.com/CrocSwap/integer-mult-bounds/pull/5397). It does not +repeat their construction or claim a global native-circuit lower bound. + +## Reproduce + +Python 3.12 and the standard library are sufficient. From the repository root: + +```sh +python3 -B scripts/research_package.py --package research/global-query-controller-ceiling +``` + +Expected scientific result, in both registered modes: + +```text +PASS_GLOBAL_QUERY_CONTROLLER_CEILING_NO_KAPPA_GAIN +``` + +Direct read-only replay is `python3 -I -B research/global-query-controller-ceiling/verify.py`. +The explicit `--write` option regenerates the deterministic receipt. Source +bytes are authenticated before execution. The verifier executes authenticated +source text directly, so a preexisting bytecode cache cannot replace it. +The interval engine and source Laurent engine are reused, with their credit; +the dynamic program and the infinite-family proof are new. + +The full native phase suite, complete compiler/outer replay, selected cold +replay, physical tape execution and formal kernel are not run by this package. +They are not needed for this raw necessary-condition ceiling. The retained +five framework assumptions still apply to the cited positive constructions. + +## Open next questions + +A larger gain needs a changed local profile, query price, idle law, connection +graph or recursive contract. First derive its complete paid and productive +inventory and identify which premise of this theorem changes. Then check the +actual operator and compiler costs before making a kappa claim. No further +search of masks or pair counts in this fixed family is proposed. TASK.json +records the scope and the specific reopening condition. + +Credit Cinna Davis, Cao Yifan, zxv, Chris R, Dugongue, Jacob Alan Sussman and +the retained source authors. Ali Romman with substantial OpenAI Codex assistance; +no subagents. Apache-2.0. See source/NOTICE.md for the retained source notice. diff --git a/research/global-query-controller-ceiling/RESULT.json b/research/global-query-controller-ceiling/RESULT.json new file mode 100644 index 0000000000..06f6291fc2 --- /dev/null +++ b/research/global-query-controller-ceiling/RESULT.json @@ -0,0 +1,839 @@ +{ + "best": { + "a": 7, + "center": 1, + "full_calls": 18, + "left_full": 8, + "p": 16, + "right_full": 9 + }, + "ceiling": "12109153/4000000000", + "ceiling_decimal": ".00302728825", + "finite_combinations": 10290000, + "global_lower": { + "lower": "0.000000014914967918767741908079", + "upper": "0.000000014914967918767741908080" + }, + "global_lower_exact": "46811385503066831490325404171729210464493663497933/3138550867693340381917894711603833208051177722232017256448", + "grid": "6277101735386680763835789423207666416102355444464034512896", + "new_kappa": null, + "per_p": [ + { + "a": 0, + "center": 1, + "left_full": 1, + "lower_scaled": 369432627232185295287392662306567701127449909928040144329791, + "p": 1, + "right_full": 1 + }, + { + "a": 0, + "center": 1, + "left_full": 1, + "lower_scaled": 305619837594236762679648060422162941195507967380538318819017, + "p": 2, + "right_full": 3 + }, + { + "a": 1, + "center": 1, + "left_full": 2, + "lower_scaled": 255578409409758061886322902331686059962547709150284635181417, + "p": 3, + "right_full": 2 + }, + { + "a": 1, + "center": 1, + "left_full": 2, + "lower_scaled": 211019533135182412871155970935092502451732743642584256949022, + "p": 4, + "right_full": 3 + }, + { + "a": 2, + "center": 1, + "left_full": 3, + "lower_scaled": 171963234465690672340111464008431540326127483892015514404435, + "p": 5, + "right_full": 3 + }, + { + "a": 2, + "center": 1, + "left_full": 3, + "lower_scaled": 138816661763415942871935228145722385732041251190450838064616, + "p": 6, + "right_full": 4 + }, + { + "a": 3, + "center": 1, + "left_full": 4, + "lower_scaled": 109806554451425473087146273748204959354652618441886948378269, + "p": 7, + "right_full": 4 + }, + { + "a": 3, + "center": 1, + "left_full": 4, + "lower_scaled": 85400193492735107570928356732203523377925728056802061986994, + "p": 8, + "right_full": 5 + }, + { + "a": 4, + "center": 1, + "left_full": 5, + "lower_scaled": 64307989919955095715804780054114479534284233922127234184967, + "p": 9, + "right_full": 5 + }, + { + "a": 4, + "center": 1, + "left_full": 5, + "lower_scaled": 46986610531635600796091818186538402543244736847499898372476, + "p": 10, + "right_full": 6 + }, + { + "a": 5, + "center": 1, + "left_full": 6, + "lower_scaled": 32429839359890552419332917320180658261251955286740674501265, + "p": 11, + "right_full": 6 + }, + { + "a": 5, + "center": 1, + "left_full": 6, + "lower_scaled": 21066215936647308037307491083323493472551489507690118265638, + "p": 12, + "right_full": 7 + }, + { + "a": 6, + "center": 1, + "left_full": 7, + "lower_scaled": 12073941772987126694186953822586331235538636319757592290811, + "p": 13, + "right_full": 7 + }, + { + "a": 6, + "center": 1, + "left_full": 7, + "lower_scaled": 5850586336126958024230400140306867767806349631643984690064, + "p": 14, + "right_full": 8 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 1703220228059276569728514845149271386803624555152988159685, + "p": 15, + "right_full": 8 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 93622771006133662980650808343458420928987326995866, + "p": 16, + "right_full": 9 + }, + { + "a": 8, + "center": 1, + "left_full": 9, + "lower_scaled": 142792586205665388707582439041281344148658384898480129839, + "p": 17, + "right_full": 9 + }, + { + "a": 8, + "center": 1, + "left_full": 9, + "lower_scaled": 2473103002233613026432766664721965774444010891929072145380, + "p": 18, + "right_full": 10 + }, + { + "a": 9, + "center": 1, + "left_full": 10, + "lower_scaled": 6465284384237881130116226464055848264687057743385472191961, + "p": 19, + "right_full": 10 + }, + { + "a": 9, + "center": 1, + "left_full": 10, + "lower_scaled": 12437087591328821361304221333609711567650622931543387005806, + "p": 20, + "right_full": 11 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 21, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 22, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 23, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 24, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 25, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 26, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 27, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 28, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 29, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 30, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 31, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 32, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 33, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 34, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 35, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 36, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 37, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 38, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 39, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 40, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 41, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 42, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 43, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 44, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 45, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 46, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 47, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 48, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 49, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 50, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 51, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 52, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 53, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 54, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 55, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 56, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 57, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 58, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 59, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 60, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 61, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 62, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 63, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 64, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 65, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 66, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 67, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 68, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 69, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 70, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 71, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 72, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 73, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 74, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 75, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 76, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 77, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 78, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 79, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 80, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 81, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 82, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 83, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 84, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 85, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 86, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 87, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 88, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 89, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 90, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 91, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 92, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 93, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 94, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 95, + "right_full": 9 + }, + { + "a": 7, + "center": 1, + "left_full": 8, + "lower_scaled": 13306574555605041873836809770122123090163596987862890877882, + "p": 96, + "right_full": 9 + } + ], + "profile": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 318 + }, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40 + } + }, + "saving_domain": "ceiling <= kappa < 1", + "source_checks": { + "controls": [ + "omitted_idle_false_positive", + "unearned_helper_credit", + "full_even_stage_middle_idle" + ], + "exhaustive_masks": 12744, + "full_Laurent_factorizations": 15, + "p16_lower_scaled": 93622771006133662980650808343458420928987326995866, + "p16_paid_calls": 64116, + "p16_targets": 10784 + }, + "source_sha256": { + "research/global-query-controller-ceiling/source/NOTICE.md": "d4199d37458047d62f374c991de694a7db8579cecdee4dd1d809fab1435c3cb3", + "research/global-query-controller-ceiling/source/transpose-RESULT.json": "093f9fc5927affec080bb38a08bff9833a796117b88033c22cb44428d82e8070", + "research/higher-moment-strictification/verify.py": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", + "research/joint-helper-lattice/CONTROLLER.json": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85", + "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", + "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e", + "research/query-thinned-controllers/PROOF.md": "5ade59641f2ed70d045d6f60e89db7d979b1d1e9967f3acbe5c56eac81312841", + "research/query-thinned-controllers/controller.py": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2" + }, + "status": "PASS_GLOBAL_QUERY_CONTROLLER_CEILING_NO_KAPPA_GAIN", + "tail_derivative_lower": { + "lower": "5.188985973480417120924401618389", + "upper": "5.188985973480417120924401618390" + }, + "tail_lower": { + "lower": "104.185162541469147567554569434096", + "upper": "104.185162541469147567554569434097" + }, + "tail_start": 96 +} diff --git a/research/global-query-controller-ceiling/SOURCES.json b/research/global-query-controller-ceiling/SOURCES.json new file mode 100644 index 0000000000..2aca305bc4 --- /dev/null +++ b/research/global-query-controller-ceiling/SOURCES.json @@ -0,0 +1,76 @@ +{ + "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/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-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "usage": "input", + "git_blob": "8b40135a84e7f0f0cd44bed69655801310b916a7", + "sha256": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85" + }, + { + "path": "research/kappa-rebuild/bit/complex_controller_factor.py", + "usage": "input", + "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947", + "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497" + }, + { + "path": "research/kappa-rebuild/bit/mixed_productive_bit.py", + "usage": "input", + "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96", + "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e" + }, + { + "path": "research/query-thinned-controllers/PROOF.md", + "usage": "input", + "git_blob": "9068f429896112082664455ab00bab083c99d1d8", + "sha256": "5ade59641f2ed70d045d6f60e89db7d979b1d1e9967f3acbe5c56eac81312841" + }, + { + "path": "research/query-thinned-controllers/controller.py", + "usage": "input", + "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583", + "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2" + }, + { + "path": "research/global-query-controller-ceiling/source/transpose-RESULT.json", + "usage": "input", + "git_blob": "32d9851bca632352cfd92bcdc5c87d23f02c257e", + "sha256": "093f9fc5927affec080bb38a08bff9833a796117b88033c22cb44428d82e8070", + "pin": "head:6919161525e69b687630cb6468aa32b9414d7206:research/global-query-controller-ceiling/source/transpose-RESULT.json", + "source_pin": "https://github.com/aliromman/integer-mult-bounds/blob/329b2ff35d2994b11abbb59f770d12da75c494ac/research/native-transpose-owned/RESULT.json" + }, + { + "path": "research/global-query-controller-ceiling/source/NOTICE.md", + "usage": "input", + "git_blob": "97dacf2cd0296cd26cf5d6cce8095d01e85dff9e", + "sha256": "d4199d37458047d62f374c991de694a7db8579cecdee4dd1d809fab1435c3cb3", + "pin": "head:6919161525e69b687630cb6468aa32b9414d7206:research/global-query-controller-ceiling/source/NOTICE.md", + "source_pin": "https://github.com/aliromman/integer-mult-bounds/blob/329b2ff35d2994b11abbb59f770d12da75c494ac/research/native-transpose-owned/source/NOTICE.md" + } + ] +} diff --git a/research/global-query-controller-ceiling/TASK.json b/research/global-query-controller-ceiling/TASK.json new file mode 100644 index 0000000000..4f042d4e7e --- /dev/null +++ b/research/global-query-controller-ceiling/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove an upper ceiling for every pair count, split and FULL/QUERY mask in the prefix/suffix controller family with the current owned local profile.", + "scope_change_reason": "The user requested a stronger complete bound. Multiple changed circuit models found no gain. A new tail reduction and dynamic program now cover the unbounded controller family, beyond the existing finite neighborhoods and fixed-invoice ceilings.", + "bottleneck_link": "Further masks or pair counts in this family cannot fund kappa at or above .00302728825. A meaningful further gain must change a listed premise.", + "budget_minutes": 60, + "stop_rule": "Complete the unbounded-family proof, exact directed arithmetic, independent literal invoice checks, semantic controls, source binding and publication checks; do not claim a higher kappa.", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json; registered normal and optimized verifier.", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, coding, searches, review and writing. No subagents.", + "open_questions": [ + { + "question": "Can a different local profile or controller contract beat this family ceiling?", + "why_it_matters": "The present complete conditional bound is within 2e-11 of the ceiling for this fixed family.", + "first_step": "State a changed premise and a complete paid and productive invoice. A positive moment must precede native and compiler admission.", + "blocked_by": "No stronger verified native circuit or complete changed caller was found in this continuation." + } + ], + "overlap_coverage": { + "base": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "priorities": 7, + "compared": [ + "PR5393 at 5744cc24d89df28d8c889615f7e667003d5fdf25: at most two stage changes at fixed p16.", + "PR5397 at 46314299ea9579f228129ec23a6a8e207de887c5: fixed 144-exchange invoice." + ], + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19155111", + "limits": "Unpublished work and arbitrary historical diffs are outside coverage." + } +} diff --git a/research/global-query-controller-ceiling/VERIFY.json b/research/global-query-controller-ceiling/VERIFY.json new file mode 100644 index 0000000000..1b12ad46ee --- /dev/null +++ b/research/global-query-controller-ceiling/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/global-query-controller-ceiling/source/NOTICE.md", + "research/global-query-controller-ceiling/source/transpose-RESULT.json", + "research/higher-moment-strictification/verify.py", + "research/joint-helper-lattice/CONTROLLER.json", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "research/kappa-rebuild/bit/complex_controller_factor.py", + "research/kappa-rebuild/bit/mixed_productive_bit.py", + "research/query-thinned-controllers/PROOF.md", + "research/query-thinned-controllers/controller.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Authenticate exact source bytes, prove the infinite tail bounds, check the complete integer dynamic program, and compare literal invoices and exhaustive masks with rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Repeat the same exact checks with Python optimization enabled." + } + ] +} diff --git a/research/global-query-controller-ceiling/verify.py b/research/global-query-controller-ceiling/verify.py new file mode 100644 index 0000000000..4d32e21e83 --- /dev/null +++ b/research/global-query-controller-ceiling/verify.py @@ -0,0 +1,230 @@ +"""Exact ceiling for all prefix/suffix FULL/QUERY allocations. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The controller is due to Cinna Davis and the retained source authors. +The directed interval engine is due to zxv. See PROOF.md for the scope. +""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256, sha1 +from pathlib import Path +import argparse +import json +import sys +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +CEILING = Q('.00302728825') +TAIL = 96 +PAID = {1: 2193, 2: 412, 3: 510, 4: 127, 5: 40} +HELPERS = {4: 28, 7: 7, 8: 47, 9: 318} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(path, name): + module = types.ModuleType(name) + module.__file__ = str(ROOT / path) + sys.modules[name] = module + exec(compile((ROOT / path).read_bytes(), module.__file__, 'exec'), module.__dict__) + return module + + +def authenticate(): + result = {} + for row in json.loads((HERE / 'SOURCES.json').read_text())['files']: + if row['usage'] != 'input': + continue + raw = (ROOT / row['path']).read_bytes() + digest = sha256(raw).hexdigest() + need(digest == row['sha256'], 'Source SHA256: ' + row['path']) + need(sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + == row['git_blob'], 'Source Git blob: ' + row['path']) + result[row['path']] = digest + return result + + +def check_profile(row): + native = row['native'] + paid = {int(k): v for k, v in native['paid'].items()} + helper = {int(k): v for k, v in native['source_replay']['helpers'].items()} + need(paid == PAID and helper == HELPERS, 'Exact owned supplier profile') + need(native['source_replay']['paid'] == native['paid'], 'Both source orientations') + need(native['source_replay']['independent_persistent_columns'] == 624, + 'All retained source fields') + + +def formula(p, a, chosen): + """Return the complete literal interval invoice for this family.""" + n = len(chosen) + paid = Counter({r: n * c for r, c in PAID.items()}) + target = Counter({r: n * c for r, c in HELPERS.items()}) + paid[1] += 112 * (2 * p + 1 - n) + target[1 + 8 * n] += 224 + for j in range(1, p): + idle = range(2 * j) if j <= a else range(2 * j + 1, 2 * p + 1) + count = sum(s in chosen for s in idle) + even = int(2 * j in chosen) + if count: + paid[8 * count] += 224 + if even: + paid[8] += 224 + target[1 + 8 * (count + even)] += 224 + return +paid, +target + + +def engine_checks(w, source): + load('research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py', 'joint_pair_dag') + load('research/kappa-rebuild/bit/mixed_productive_bit.py', 'mixed_productive_bit') + engine = load('research/kappa-rebuild/bit/complex_controller_factor.py', 'ceiling_controller_engine') + query = load('research/query-thinned-controllers/controller.py', 'ceiling_query_engine') + trials, factorizations, minima = 0, 0, {} + def lower(paid, target): + return sum(c * w[r][0] for r, c in paid.items()) - sum(c * w[r][1] for r, c in target.items()) + for p in range(1, 6): + best = None + for a in range(p): + co, _, idles = engine.controller(p, query.keep_mask(p, a)) + factor = engine.factor(co) + need(factor is not None, 'Exact full Laurent factorization') + factorizations += 1 + terms = [sum((v != 0) << s for s, v in enumerate(k[1:])) for k in factor['diagonal']] + idle_terms = [sum(1 << s for s in row['stages']) for row in idles if row['retained']] + for mask in range(1 << (2 * p + 1)): + n = mask.bit_count() + paid = Counter({r: n * c for r, c in PAID.items()}) + target = Counter({r: n * c for r, c in HELPERS.items()}) + paid[1] += 112 * (2 * p + 1 - n) + for term in terms: + target[1 + 8 * (mask & term).bit_count()] += 112 + for term in idle_terms: + rank = 8 * (mask & term).bit_count() + if rank: + paid[rank] += 224 + chosen = {s for s in range(2 * p + 1) if mask >> s & 1} + need((+paid, +target) == formula(p, a, chosen), 'Literal interval invoice') + bill = lower(paid, target) + best = bill if best is None else min(best, bill) + trials += 1 + minima[p] = best + chosen = {0, 32, *range(1, 32, 2)} + paid, target = formula(16, 7, chosen) + need(paid == Counter({int(k): v for k, v in source['arithmetic']['paid'].items()}), 'Published complete paid profile') + need(target == Counter({int(k): v for k, v in source['arithmetic']['targets'].items()}), 'Published complete target profile') + # The retained p16 receipt supplies another diagonal and idle census. + receipt = json.loads((ROOT / 'research/joint-helper-lattice/CONTROLLER.json').read_text()) + main = Counter() + for term in receipt['diagonal']: + main[1 + 8 * sum(term[1:])] += 112 + actual_main = Counter(target) + actual_main.subtract({r: 18 * c for r, c in HELPERS.items()}) + need(+actual_main == main, 'Retained p16 main targets') + need(sum(paid.values()) == 64116 and sum(target.values()) == 10784, + 'Complete p16 field and call counts') + # An omitted whole idle falsely passes the moment test. + wrong_paid = paid.copy() + wrong_paid[64] -= 1 + need(wrong_paid != paid and lower(wrong_paid, target) < 0 < lower(paid, target), + 'Reject omitted idle with a false positive bill') + # An unearned helper restores the discarded productive credit. + wrong = json.loads(json.dumps(source)) + wrong['native']['source_replay']['helpers']['9'] += 8 + try: + check_profile(wrong) + except ValueError: + pass + else: + raise ValueError('Unearned helper credit accepted') + # A FULL even stage has a separate middle idle charge. + changed = chosen | {2} + changed_paid, _ = formula(16, 7, changed) + need(changed_paid[8] == paid[8] + 224, 'Middle idle charge after a FULL even stage') + return dict(exhaustive_masks=trials, full_Laurent_factorizations=factorizations, + p16_paid_calls=sum(paid.values()), p16_targets=sum(target.values()), + p16_lower_scaled=lower(paid, target), + controls=['omitted_idle_false_positive', 'unearned_helper_credit', 'full_even_stage_middle_idle']), minima + + +def run(): + sources = authenticate() + source = json.loads((HERE / 'source/transpose-RESULT.json').read_text()) + check_profile(source) + engine = load('research/higher-moment-strictification/verify.py', 'ceiling_intervals') + grid, t = engine.GRID, 1 - CEILING + ranks = {0, 1, 2, 3, 4, 5, 7, 8, 9} | {8 * k + e for k in range(TAIL + 1) for e in (0, 1)} + w = {0: (0, 0)} + for rank in sorted(ranks - {0}): + lo, hi = engine.power(rank, t) + need((lo * grid).denominator == (hi * grid).denominator == 1, 'Exact outward grid') + w[rank] = int(lo * grid), int(hi * grid) + local = sum(c * w[r][0] for r, c in PAID.items()) - sum(c * w[r][1] for r, c in HELPERS.items()) + tail = 336 * grid + (local - 112 * grid) * TAIL - 224 * w[1 + 8 * TAIL][1] + slope = Q(local, grid) - 112 - 1792 * t * Q(w[1 + 8 * TAIL][1], grid * (1 + 8 * TAIL)) + need(tail > 0 and slope > 0, 'Positive increasing tail for every n >= 96') + dp = [[0, 0]] + for q in range(1, TAIL): + row = [None] * min(2 * q + 2, TAIL) + for k, value in enumerate(dp[-1]): + for odd in (0, 1): + for even in (0, 1): + count = k + odd + even + if count >= TAIL: + continue + fee = 224 * (w[8 * (k + odd)][0] + even * w[8][0] - w[1 + 8 * count][1]) + candidate = value + fee + if row[count] is None or candidate < row[count]: + row[count] = candidate + need(all(v is not None for v in row), 'Every side state is reachable') + dp.append(row) + per_p, candidates, global_best = [], 0, None + for p in range(1, TAIL + 1): + best = None + for a in range((p - 1) // 2 + 1): + b = p - 1 - a + for left, lvalue in enumerate(dp[a]): + for right, rvalue in enumerate(dp[b]): + for center in (0, 1): + n = left + right + center + if n >= TAIL: + continue + bill = 112 * (2 * p + 1) * grid + (local - 112 * grid) * n + lvalue + rvalue - 224 * w[1 + 8 * n][1] + candidates += 1 + if best is None or bill < best[0]: + best = bill, a, left, right, center + need(best[0] > 0, 'Every finite controller fails the necessary moment') + if global_best is None or best[0] < global_best[0]: + global_best = best[0], p, *best[1:] + per_p.append(dict(p=p, a=best[1], left_full=best[2], right_full=best[3], center=best[4], lower_scaled=best[0])) + checks, brute_minima = engine_checks(w, source) + need(all(per_p[p - 1]['lower_scaled'] == bill for p, bill in brute_minima.items()), 'Independent exhaustive minima equal the dynamic program') + lo = Q(global_best[0], grid) + need(global_best[1:] == (16, 7, 8, 9, 1), 'Best finite configuration') + need(global_best[0] == checks['p16_lower_scaled'], 'Current p16 invoice attains the minimum lower bound') + return dict(status='PASS_GLOBAL_QUERY_CONTROLLER_CEILING_NO_KAPPA_GAIN', new_kappa=None, + ceiling=str(CEILING), ceiling_decimal='.00302728825', saving_domain='ceiling <= kappa < 1', + profile=dict(paid=PAID, helpers=HELPERS), grid=str(grid), tail_start=TAIL, + tail_lower=engine.display((Q(tail, grid),) * 2), tail_derivative_lower=engine.display((slope,) * 2), + global_lower=engine.display((lo,) * 2), global_lower_exact=str(lo), + best=dict(p=16, a=7, full_calls=18, left_full=8, right_full=9, center=1), + finite_combinations=candidates, per_p=per_p, source_checks=checks, source_sha256=sources) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = run() + if args.write: + (HERE / 'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + saved = json.loads((HERE / 'RESULT.json').read_text()) + need(json.loads(json.dumps(result)) == saved, 'Deterministic exact receipt') + print(result['status']) + + +if __name__ == '__main__': + main()