diff --git a/.github/workflows/p16-tight-transfer-chris.yml b/.github/workflows/p16-tight-transfer-chris.yml new file mode 100644 index 0000000000..0e6c68f2b4 --- /dev/null +++ b/.github/workflows/p16-tight-transfer-chris.yml @@ -0,0 +1,29 @@ +name: P16 independent exact tighter κ transfer +on: + push: + branches: + - research/p16-tight-transfer-upstream-clean-20261022 + pull_request: + paths: + - 'research/p16-tight-transfer-20261022/**' + - '.github/workflows/p16-tight-transfer-chris.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + exact-conditional: + runs-on: ubuntu-latest + timeout-minutes: 15 + strategy: + fail-fast: false + matrix: + python-version: ['3.11','3.13'] + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: ${{ matrix.python-version }} + - name: Check exact source-selected raw rank moments + run: python -I -B research/p16-tight-transfer-20261022/frontier_rational_gate.py + - name: Certify κ=0.0030201659769 with all 54+4 gates and fixed rank + run: python -I -B research/p16-tight-transfer-20261022/critical_root_tight_transfer.py diff --git a/research/p16-tight-transfer-20261022/PROOF.md b/research/p16-tight-transfer-20261022/PROOF.md new file mode 100644 index 0000000000..1842361704 --- /dev/null +++ b/research/p16-tight-transfer-20261022/PROOF.md @@ -0,0 +1,45 @@ +# P16 tighter critical-root transfer: conditional κ = 0.0030201659769 + +**Research status (22 October 2026):** a new **exact-rational conditional parameter point** above pending PR #4535 κ=0.003020165, using its *unchanged* PR #4470 physical supplier and PR #4532 critical-root lemma. **No new native algorithm, unconditional theorem, formal proof, independent human acceptance, or maintainer-selected κ** is claimed. Preserve prior contributors and licenses (zxv, Cinna Davis, Jacob Alan Sussman, Dillon, hexapode, Ryanson Jonathan and the complete PR4470 source manifest). New source for @Chrisbryan17 with GPT-6 assistance, Apache-2.0. + +## Source pins and exact novel parameter point + +- Selected source: `CrocSwap/integer-mult-bounds@b9a13c1673e0e9697de410de16e8bbf3207a7363` (#4470), selected conditional κ=0.00302015. +- Critical-root theorem: `CrocSwap/integer-mult-bounds@644607ba59ebe401ac7ecd627ae7f331f924d1b0` (#4532). +- Pending transfer: `CrocSwap/integer-mult-bounds@a6d7237f697185e857090e174c23c1cb22c6563c` (#4535), κ=0.003020165. +- Original outer equations: `research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py`. + +Fix **κ=0.0030201659769**, **d=10^-15**, `s_C=κ+6d=0.003020165976906`. Put `b=κ+5d`, `a=κ+4d`, `q=κ+3d`, `ε=1-d`, `β=1-3d`, `r0=d/10`, `stop=layout=d`; ordinary BIT saving remains 0.0034 and BIT atom=0.004. This uses no new native rank profile. + +The pinned PR4470 paid/target histograms, independently checked by `frontier_rational_gate.py`, give a raw critical saving bracket + +`0.0030201659770 < κ_raw < 0.0030201659771`, + +equivalently critical exponent `θ*∈(0.9969798340229,0.9969798340230)`. Thus `z=1-s_C=0.996979834023094` satisfies + +`z-θ_hi=94/10^15>0`. + +Under PR4532's fixed critical-root logarithmic majorant `L(n)≤A n^θ*(133+ln n)^(2/5)` with `n0=145×1024^650`, choose the **fixed local compiler rank** `N=2^(10^15)`. Elementary rational comparisons give `ln A<20`, `ln(133+ln N)<50` and `ln N>(2/3)10^15`. Therefore the logarithmic absorption surplus is strictly greater than + +`(94/10^15)×(2/3)10^15−20−(2/5)50=68/3>0`. + +The derivative `(z-θ_hi)−(2/5)/(133+ln N)>0` guarantees the positive bound persists for all larger ranks. This explicitly funds the logarithmic overhead rather than identifying the raw critical root with a usable saving. PR4535's finite-template closure and arbitrary-height integer compiler are invoked as conditional premises; **their extended code/physical execution has not been independently replayed**. + +The exact `Fraction` certificate checks **all 54 original named PR4359 strict inequalities**, **all four functional guards**, **all nine row savings greater than κ**, the unchanged selected raw profile and both moment signs. The smallest positive strict predicate is `d/10=10^-16`; the binding main-transform margin is `εq−κ=2.996979834...×10^-15>0`. The uniform compiler height upper bound becomes `G_depth≤2×10^14`; the conservative class-count bound becomes `C_N<2^(3400000000000031)`. This is astronomically finite and not materialized or practical. + +## Acceptance scope + +This is an improved **conditional mathematical parameter certificate**, an absolute `0.0000000009769` above the still-open #4535 point and `0.0000000159769` above the official selected point. It does **not** improve the native supplier or certify unconditional `T(n)=O(n(log n)^(1-κ))`: all all-column native, owned scratch, whole-job, physical movement, semantic precision, fixed-tape, analytic decomposition, prime-avoidance, and exact-recovery contracts remain inherited. Peer review and the complete registered PR4532/4535 package replay are still needed. Do not promote this as the maintainer-selected value. + +## Reproduction + +From this branch: + +```bash +python -I -B research/p16-joint-lab/frontier_rational_gate.py +python -I -B research/p16-joint-lab/critical_root_tight_transfer.py +``` + +The second script emits `TIGHT_TRANSFER_RECEIPT.json` with exact fractions and fail-closed scope flags. A Python 3.11/3.13 GitHub Actions workflow is committed; hosted success is unconfirmed. The 54 check identities are independently transcribed from the credited `endpoint.py`; the smaller conditional proof is an inference from its already documented general transfer theorem, not a second verification of that theorem. + +**Next acceptance gate:** separate independent audit of the all-size compiler's quantified arbitrary-rank conclusion and matching source/native premise, then upstream review. Even a tiny exponent record requires both arithmetic and that proof bridge. diff --git a/research/p16-tight-transfer-20261022/critical_root_tight_transfer.py b/research/p16-tight-transfer-20261022/critical_root_tight_transfer.py new file mode 100644 index 0000000000..0c10bfae74 --- /dev/null +++ b/research/p16-tight-transfer-20261022/critical_root_tight_transfer.py @@ -0,0 +1,155 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact standalone conditional critical-root tightening over PR4470/4532/4535. + +Improved *conditional parameter point* only. Native/physical, critical-root +theorem and analytic transfer remain retained prerequisites, not re-proven. +This imports the previous independent rational PR4470 raw-moment oracle. +""" +from fractions import Fraction as Q +from math import factorial +from pathlib import Path +import json,sys +sys.path.insert(0,str(Path(__file__).resolve().parent)) +from frontier_rational_gate import profiles,moment_interval + +K=Q('0.0030201659769') +D=Q(1,10**15) +S=K+6*D +THETA_LO,THETA_HI=Q('.9969798340229'),Q('.9969798340230') +H=10**15 + +def outer(k,d): + b,a,q=k+5*d,k+4*d,k+3*d + epsilon,beta,r0,stop,layout=1-d,1-3*d,d/10,d,d + sigma,tau=1-b,1-a + internal=tau+(1-stop)*max(sigma-tau,Q(0)) + leaf=sigma+stop*(1-sigma) + lam,c=1-(q+a)/2,Q(3,32) + xi,key=epsilon*(1+q)-c+layout,beta+1-epsilon + margins={ + 'main_transform':epsilon*q, + 'global_coordinate_router':a, + 'fused_gaussian':1-epsilon+q*beta, + 'group_bit_router':1-epsilon+a*beta, + 'group_scans':1-epsilon+beta, + 'boundary_algebraic_matrix':c+xi-epsilon, + 'sparse_union_movement':xi+Q(1,2)-epsilon, + 'polynomial_products':epsilon, + 'microbox_face_corrections':1-(epsilon+beta+48-128+2)} + checks={ + 'actual_bit_above_effective':Q('.0034')-a, + 'complex_above_effective':b-a, + 'q_positive':q,'complex_endpoint':b-q, + 'q_below_effective':a-q, + 'stop_positive':stop,'stop_below_one':1-stop, + 'leaf_saving_above_effective':(1-stop)*b-a, + 'q_below_internal':1-internal-q, + 'q_below_leaf':1-leaf-q, + 'lambda_above_tau':lam-tau, + 'lambda_above_sigma':lam-sigma, + 'lambda_above_internal':lam-internal, + 'lambda_prime_above_lambda':1-q-lam, + 'lambda_prime_above_leaf':1-q-leaf, + 'epsilon_positive':epsilon, + 'epsilon_below_one':1-epsilon, + 'cap_above_band':xi-Q(1,2), + 'cap_below_cell':epsilon-xi, + 'group_positive':beta, + 'group_below_dimension':epsilon-beta, + 'support_router_span':1-beta, + 'group_gauge_power_slack':1-(2*xi-2)-r0-beta, + 'actual_logarithmic_group_guard':1-(2*xi-2)-beta, + 'global_gamma_power_slack':1-epsilon-r0, + 'actual_logarithmic_gamma_guard':1-epsilon, + 'alpha_logarithm_absorption':r0, + 'group_key_fits_record':1-key, + 'membership_arithmetic_fits_record':1-beta-2*(1-epsilon), + 'microbox_halo_volume':128-48-beta, + 'positive_layout_slack':layout, + 'short_record_fallback':epsilon-a, + 'complex_below_one_over_32':Q(1,32)-b, + 'strassen_integer_power_gap':Q(2**45-7**16), + 'theta_positive_polynomial_power':Q(2), + 'cap_below_phase_cell_power':2-xi, + 'halo_covers_generic_inverse_radius':Q(5), + 'union_tag_work_per_visit_fits_record':1-beta, + 'union_header_fits_record':1-beta, + 'source_axis_superpolynomial':1-epsilon, + 'gaussian_above_main':margins['fused_gaussian']-margins['main_transform'], + 'new_complex_uniform_saving_above_b':k+6*d-b, + 'improvement_over_user_baseline':k-Q('0.001730970419199163702738'), + 'new_semantic_guard_with_C1_one':1-epsilon, + 'fine_prime_halo_umbrella':10-(2*2+2+Q(1,2))} + checks.update({name+'_above_kappa':value-k for name,value in margins.items()}) + functional={ + 'new_semantic_group_guard':1-beta, + 'new_BIT_row_stock_sublinear_in_active_group':beta*(1-Q(3,1000)), + 'fixed_halo_explicit_metadata_branch':128-48-epsilon-beta-1, + 'actual_new_BIT_stock_sublinear':beta*(1-Q('.004'))} + assert (len(margins),len(checks),len(functional))==(9,54,4) + return margins,checks,functional + +def run(): + target,paid=profiles() + lo,hi=1-THETA_HI,1-THETA_LO + assert moment_interval(target,paid,lo)['positive'] + assert moment_interval(target,paid,hi)['negative'] + assert moment_interval(target,paid,S)['positive'] + assert THETA_HI<1-S and lo>S + m,c,f=outer(K,D) + assert all(v>K for v in m.values()) + assert all(v>0 for v in c.values()) + assert all(v>0 for v in f.values()) + assert any(v<=0 for v in outer(K,Q(0))[1].values()) + # Logarithmic majorant from PR4532 is A*N^theta*(133+ln N)^(2/5). + # ln A < (1-theta_lo)*(ln145+650*ln1024)<20, explicitly bounded. + assert sum(Q(8**i,factorial(i)) for i in range(6))>145 + assert sum(Q(7**i,factorial(i)) for i in range(19))>1024 + assert (1-THETA_LO)*(8+650*7)<20 + assert 133+H<2**50 and H>8+650*10 + gap=(1-S)-THETA_HI + assert gap==Q(94,10**15) + # ln2 > 2/3 from 2 atanh(1/3); ln2 < 1 from e>2. + # At N=2^H: gap*ln N - ln A-(2/5)ln(133+ln N) + # > gap*(2/3)*H-20-20 = 68/3 >0. + absorption_lower=gap*Q(2*H,3)-40 + assert absorption_lower==Q(68,3)>0 + assert gap>Q(2,5)/(133+Q(2*H,3)) + height=2*(H//10) + assert H%10==0 and (14+17*(height+1))==3400000000000031 + assert K>Q('.003020165') + result={ + 'status':'PASS_EXACT_CONDITIONAL_PARAMETER_SCREEN', + 'source_pins':{ + 'native_PR4470':'b9a13c1673e0e9697de410de16e8bbf3207a7363', + 'critical_theorem_PR4532':'644607ba59ebe401ac7ecd627ae7f331f924d1b0', + 'transfer_PR4535':'a6d7237f697185e857090e174c23c1cb22c6563c', + 'outer_source':'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py'}, + 'kappa_candidate':str(K),'existing_selected':'0.00302015', + 'open_PR4535':'0.003020165', + 'gain_over_pending':str(K-Q('.003020165')), + 'uniform_complex_saving':str(S),'slack_d':str(D), + 'raw_root_bracket':[str(lo),str(hi)], + 'verified_exact_outer_checks':len(c), + 'verified_exact_functional_guards':len(f), + 'all_outer_predicates_positive':True, + 'minimum_strict_predicate':str(min(c.values())), + 'minimum_margin_above_kappa':str(min(m.values())-K), + 'N':'2^(10^15)', + 'rigorous_log_absorption_margin_lower':str(absorption_lower), + 'compiler_height_bound':height, + 'log2_class_envelope_bound':14+17*(height+1), + 'physical_native_and_unconditional_analytic_interfaces':'INHERITED_NOT_PROVEN', + 'whole_new_compiler_implementation':'NOT_MATERIALIZED', + 'independent_oracle':'Exact previous PR4470 moment gate, no input rounding', + 'hosted_CI':'NOT_CONFIRMED', + 'reviewed_or_selected':False, + 'new_unconditional_multiplication_theorem':False} + return result + +if __name__=='__main__': + out=run() + Path(__file__).with_name('TIGHT_TRANSFER_RECEIPT.json').write_text(json.dumps(out,indent=2,sort_keys=True)+'\n') + print('PASS_EXACT_TIGHT_TRANSFER kappa',out['kappa_candidate'], + 'strict=54 functional=4 log_margin',out['rigorous_log_absorption_margin_lower']) diff --git a/research/p16-tight-transfer-20261022/frontier_rational_gate.py b/research/p16-tight-transfer-20261022/frontier_rational_gate.py new file mode 100644 index 0000000000..99891f0020 --- /dev/null +++ b/research/p16-tight-transfer-20261022/frontier_rational_gate.py @@ -0,0 +1,107 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Standalone selected PR4470 exact P16 interval verifier. No dependencies. +This is an arithmetic gate, NOT a new physical supplier or kappa theorem. +""" +from fractions import Fraction as F +from functools import lru_cache +from collections import Counter +import json + +HELP={4:28,7:7,8:47,9:326} +PAID={1:2237,2:388,3:494,4:147,5:36,8:8} +MAIN={145:224,73:224,**{k:448 for k in (17,25,33,41,49,57,65)}} +IDLE={72:224,**{k:448 for k in (16,24,32,40,48,56,64)}} + +def add(*hists): + out=Counter() + for hist in hists:out.update(hist) + return +out + +def scaled(hist,k):return {r:n*k for r,n in hist.items()} + +def counts(hist):return (sum(hist.values()),sum(r*n for r,n in hist.items())) + +def profiles(): + T=add(MAIN,scaled(HELP,18));P=add(IDLE,scaled(PAID,18),{1:1680}) + assert counts(HELP)==(408,3471) and counts(PAID)==(3310,5327) + assert counts(T)==(10928,239886) and counts(P)==(64620,239134) + return T,P + +@lru_cache(None) +def log_bounds(rank,n=28): + if rank==1:return F(0),F(0) + e=rank.bit_length()-1;q=F(rank,1<0,'negative':hi<0} + +def balanced(count,mass): + k,rem=divmod(mass,count) + return {k:count-rem,k+1:rem} if rem else {k:count} + +def extreme(count,mass,maxrank=9): + q,rem=divmod(mass-count,maxrank-1) + d={1:count-q-int(rem>0),maxrank:q} + if rem:d[rem+1]=1 + return {k:v for k,v in d.items() if v} + +def run(): + T,P=profiles() + left=moment_interval(T,P,'0.0030201659770') + right=moment_interval(T,P,'0.0030201659771') + deficit=moment_interval(T,P,'0.006') + assert left['positive'] and right['negative'] and deficit['negative'] + H=balanced(408,3471);Q=extreme(3310,5327) + CT=add(MAIN,scaled(H,18));CP=add(IDLE,scaled(Q,18),{1:1680}) + assert counts(CT)==counts(T) and counts(CP)==counts(P) + ceiling=moment_interval(CT,CP,'0.006') + assert ceiling['negative'] + def needed(change): + for n in range(1,200): + t,p=T.copy(),P.copy();change(n,t,p) + if moment_interval(t,p,'0.006')['positive']:return n + idle=needed(lambda n,t,p:p.__setitem__(64,p[64]-n)) + helper=needed(lambda n,t,p:(t.__setitem__(9,t[9]+18*n),p.__setitem__(1,p[1]+18*n))) + assert (idle,helper)==(12,6) + return {'status':'PASS_EXACT_RATIONAL_MOMENTS_ONLY', + 'repo':'CrocSwap/integer-mult-bounds','selected_PR':4470, + 'selected_sha':'b9a13c1673e0e9697de410de16e8bbf3207a7363', + 'selected_kappa':'0.00302015', + 'root_bracket':[left,right], 'failed_target_0_006':deficit, + 'frozen_rank_shape_at_0_006':ceiling, + 'hypothetical_min_idle_P64_jobs_deleted':idle, + 'hypothetical_min_rank9_new_helpers_per_call_with_P1_each':helper, + 'new_supplier':'NONE','new_kappa':False} + +if __name__=='__main__':print(json.dumps(run(),indent=2,sort_keys=True))