diff --git a/.github/workflows/p16-cao-dual-34add.yml b/.github/workflows/p16-cao-dual-34add.yml new file mode 100644 index 0000000000..794b768993 --- /dev/null +++ b/.github/workflows/p16-cao-dual-34add.yml @@ -0,0 +1,55 @@ +name: Cao P16 dual 34-ADD source-bound certification +on: + push: + branches: + - research/p16-cao-scalar-dag-20261023 + pull_request: + paths: + - 'research/p16-cao-scalar-dag/**' + workflow_dispatch: +permissions: + contents: read +jobs: + exact-dual: + runs-on: ubuntu-latest + timeout-minutes: 25 + strategy: + fail-fast: false + matrix: + python-version: ['3.11','3.13'] + steps: + - uses: actions/checkout@v4 + with: + path: contribution + sparse-checkout: | + research/p16-cao-scalar-dag + sparse-checkout-cone-mode: false + - uses: actions/checkout@v4 + with: + repository: CrocSwap/integer-mult-bounds + ref: 20bb93cd990d2ff683e4d0fc56b87a42cd5d3296 + path: frozen-source + sparse-checkout: | + research/kappa-round3-warp-20261022 + research/warp-interface-20261022 + research/joint-helper-lattice + research/fresh-helper-boundary + research/kappa-causal-continuation/buffer-borrowing + research/kappa-rebuild/complex + research/kappa-function-composition/complex + research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford + sparse-checkout-cone-mode: false + - uses: actions/setup-python@v5 + with: + python-version: ${{ matrix.python-version }} + - name: Screen exact commuting inverse ADD pairs + run: python -I -B contribution/research/p16-cao-scalar-dag/inverse_add_dag_search.py frozen-source + - name: Reconstruct and check 632 columns with two interpreters in both directions + run: python -I -B contribution/research/p16-cao-scalar-dag/combined_inverse_add_certificate.py frozen-source + - uses: actions/upload-artifact@v4 + if: always() + with: + name: cao-p16-34add-${{ matrix.python-version }} + path: | + contribution/research/p16-cao-scalar-dag/*RECEIPT.json + contribution/research/p16-cao-scalar-dag/SCALAR_CANCEL_PATCH.json diff --git a/research/p16-cao-scalar-dag/README.md b/research/p16-cao-scalar-dag/README.md new file mode 100644 index 0000000000..1d1635976f --- /dev/null +++ b/research/p16-cao-scalar-dag/README.md @@ -0,0 +1,38 @@ +# Cao P16: 17 commuting inverse ADD pairs removed, exact dual native word + +**Result: 34 scalar ADD instructions eliminated; 312 lower real-scalar allowance in each orientation. No new κ claimed.** + +Source-bound starting point: Cao Yifan's merged #4610 frozen native word `CrocSwap/integer-mult-bounds@20bb93cd990d2ff683e4d0fc56b87a42cd5d3296`, canonical decompressed SHA256 `cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd`. + +## Why this is a circuit change, not just a simulation + +A rational elementary ADD `L_d += c L_s` commutes with a second ADD `L_x += b L_y` when `d != y` and `x != s`; it also commutes with unrelated scalar and warp operations. A later ADD `L_d += -c L_s` can be eliminated together with the first only if every intermediate event commutes with it. Both the forward and the inverse-transpose emitters must satisfy these **independent conditions**, including all 632 arbitrary source columns and dirty spectators. + +`inverse_add_dag_search.py` screens all opposite pairs within 160 source events, finding 542 matching syntactic pairs, 19 valid in both orientations. `combined_inverse_add_certificate.py` chooses 17 **nonoverlapping** pairs (34 ADDs), removes them simultaneously, and reconstructs the complete native word with the original `warp_merge.synthesize`. + +Verified on the Dell using the exact frozen original source: + +| Quantity | Original | Changed | +|---|---:|---:| +| Scalar ADD instructions removed | 0 | **34** | +| Scalar allowance, forward | 158120 | **157808** | +| Scalar allowance, backward | 158168 | **157856** | +| Paid recursive jobs per local call | 3298 | **3298** | +| Original and changed native chart climbs | Exact same chronological trajectory | **Yes** | +| Native warp, owned centre, adapter and phase events | Original | **Identical** | +| Arbitrary output columns, forward and dual | 632 each | **Both exact interpreters pass** | + +Both retained interpreters reproduce every final column in both directions, including clearing the owned `C0` register, and maintain identical whole paid rank histograms `{1:2201,2:412,3:510,4:127,5:40,8:8}`. A negative control removing only the first half of one inverse pair is rejected. The source-defined patch `SCALAR_CANCEL_PATCH.json` is regenerated by the certificate; no hand-edited native gzip is authoritative. + +The scalar allowance improvement is **per native call**. Since p16 has 18 full calls, it could reduce the source-level scalar allowance by `18 * 312 = 5616` before the controller's other scalar overhead, subject to all-size implementation contracts. The recursive rank moment and κ remain **unchanged**: selected κ stays the repository's selected value, and the merged #4610 conditional claim remains 0.0030217758. + +## Run + +```bash +python -I -B research/p16-cao-scalar-dag/inverse_add_dag_search.py /path/to/frozen-pr4610-repo +python -I -B research/p16-cao-scalar-dag/combined_inverse_add_certificate.py /path/to/frozen-pr4610-repo +``` + +Fresh proof assumptions remain: native/Clifford absolute phase (unchanged paid-edge list and maps; full inherited phase adapter still required), ownership/precision, fixed tape, stock, analytic decomposition and exact integer recovery. This script certifies exact scalar semantics under its retained interpreters; it is **not** a complete mathematical proof of the multiplication exponent. Future scalar-DAG exploration should allow non-cancelling Steinberg/braid relations, changed order and jointly optimized chart allocation, with full charged invoices. + +Credit Cao Yifan and #4610, Cinna Davis #4470, Dugongue's warp implementation, zxv, Jacob Alan Sussman and upstream contributors. New independent search and script prepared for Chrisbryan17 with GPT-6 assistance, Apache-2.0. diff --git a/research/p16-cao-scalar-dag/combined_inverse_add_certificate.py b/research/p16-cao-scalar-dag/combined_inverse_add_certificate.py new file mode 100644 index 0000000000..dc92706b69 --- /dev/null +++ b/research/p16-cao-scalar-dag/combined_inverse_add_certificate.py @@ -0,0 +1,138 @@ +#!/usr/bin/env python3 +"""Remove a maximal nonoverlapping subset of exact commuting inverse ADD pairs. + +Run against Cao #4610 source snapshot; recompiles both orientations with +the original synthesize(), and requires exact all-632-column literal +replay and owner restoration. This improves *scalar instruction count*, +not kappa unless complete recursive rank profile improves too. +""" +from collections import Counter +from copy import deepcopy +from pathlib import Path +import gzip,json,sys +HERE=Path(__file__).resolve().parent +ROOT=Path(sys.argv[1]).resolve() if len(sys.argv)>1 else HERE.parents[2] +sys.path.insert(0,str(ROOT/'research/warp-interface-20261022')) +import warp_merge as W +sys.path.insert(0,str(HERE)) +from inverse_add_dag_search import operand,commute_with_pair,paid +F=W.F + +def run(): + source=ROOT/'research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz' + original=json.loads(gzip.decompress(source.read_bytes())) + c=original['canonical'] + program={d:[deepcopy(e) for e in v if e[0]!='climb'] + for d,v in original['programs'].items()} + f,b=program['forward'],program['backward'] + assert len(f)==len(b) + proposals=[] + for right,e in enumerate(f): + second=operand(e) + if second is None:continue + dst,src,coef=second + for left in range(max(0,right-160),right): + first=operand(f[left]) + if first is None or first[:2]!=(dst,src) or first[2]!=-coef:continue + if any(not commute_with_pair(f[k],src[1],dst[1]) + for k in range(left+1,right)):continue + inv1,inv2=operand(b[left]),operand(b[right]) + if inv1 is None or inv2 is None or inv1[:2]!=inv2[:2] or inv1[2]!=-inv2[2]: + continue + if any(not commute_with_pair(b[k],inv1[1][1],inv1[0][1]) + for k in range(left+1,right)):continue + proposals.append((left,right)) + # Select disjoint closed intervals. The algebraic identity for each + # deletion then survives simultaneous elimination without relying on + # possibly overlapping commutation arguments. + proposals.sort(key=lambda p:(p[1]-p[0],p[0])) + active=set();chosen=[] + for left,right in proposals: + if any(k in active for k in range(left,right+1)):continue + chosen.append((left,right));active.update(range(left,right+1)) + assert chosen and len(set(k for a,b in chosen for k in (a,b)))==2*len(chosen) + rejected={i for a,b in chosen for i in (a,b)} + modified={} + for d,events in program.items(): + kept=[deepcopy(event) for i,event in enumerate(events) if i not in rejected] + modified[d]=W.synthesize(c,kept) + a,b=paid(modified['forward']),paid(modified['backward']) + old=paid(original['programs']['forward']) + assert a==b==old,('paid_tariff_changed',dict(a),dict(b),dict(old)) + # Preserve every native Clifford chart trajectory and all owned operations. + def role_edge_trace(word): + return [(e[2],e[3],e[4],e[5]) for e in word if e[0]=='climb'] + def non_scalar_trace(word): + return [e for e in word if e[0] in ('warp','center','adapter','residual_adapter','phase')] + assert all(role_edge_trace(modified[d])==role_edge_trace(original['programs'][d]) + for d in modified), 'Chronological paid chart trajectories changed' + assert all(non_scalar_trace(modified[d])==non_scalar_trace(original['programs'][d]) + for d in modified), 'Native warp, owner, adapter or phase changed' + V=F.load(ROOT/'research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py','dag_all_columns') + X=F.load(ROOT/'research/kappa-rebuild/complex/native_extensions.py','dag_all_native') + literal={} + for d in ('forward','backward'): + rows,r=X.literal_replay(V,c,modified[d],d=='backward') + assert all(rows['L',i]==V.expected(('L',i),[],d=='backward',False) + for i in range(632)) + assert r['arbitrary_owned_C0_cleared'] and r['scalar_frames_checked'] + rebound=deepcopy(c) + rebound['R']=len(c['start'])-2*c['v'] + rebound['local_profile']={int(k):v for k,v in r['paid_profile'].items()} + second=V.replay(modified[d],rebound,[],d=='backward',False) + assert second['all_scalar_frames_checked'] + assert second['paid_profile']==r['paid_profile'] + assert not second['mismatch_examples'] + literal[d]={'event_count':len(modified[d]), + 'real_scalar_allowance':r['real_scalar_allowance'], + 'paid_profile':r['paid_profile'], + 'paid_rank_mass':r['paid_rank_mass']} + assert literal['forward']['real_scalar_allowance']<158120 + assert literal['backward']['real_scalar_allowance']<158168 + # Deliberately remove just one of the inverse ADD pair, and ensure the + # exact all-column interpreter does not silently accept the wrong operator. + lone=chosen[0][0] + false_word=W.synthesize(c,[deepcopy(e) for i,e in enumerate(program['forward']) + if i!=lone]) + rejected=False + try: + false_rows,check=X.literal_replay(V,c,false_word,False) + rejected=any(false_rows['L',i]!=V.expected(('L',i),[],False,False) + for i in range(632)) + except (AssertionError,ValueError): + rejected=True + assert rejected,'Unpaired deliberate wrong ADD did not fail' + # Patch has no mutable binary or trust in discovery / solver output. + (HERE/'SCALAR_CANCEL_PATCH.json').write_text(json.dumps({ + 'source':'20bb93cd990d2ff683e4d0fc56b87a42cd5d3296', + 'removed_raw_scalar_event_pairs':chosen, + 'precondition':'Frozen Cao round3 word; unchanged native frames and warps', + 'original_native_payload':json.loads((ROOT/'research/kappa-round3-warp-20261022/ACTUAL-WORD-FREEZE.json').read_text())['canonical_payload_sha256'] + },sort_keys=True,indent=2)+'\\n') + def native_pairs(p): + return {(e[3],e[4],e[-1]) for e in p if e[0]=='climb'} + same_pairs={d:native_pairs(modified[d])==native_pairs(original['programs'][d]) + for d in modified} + report={'status':'PASS_DUAL_632_NATIVE_SCALAR_CANCEL', + 'source_pin':'20bb93cd990d2ff683e4d0fc56b87a42cd5d3296', + 'proposed_valid_pair_count':len(proposals), + 'simultaneously_removed_inverse_pairs':len(chosen), + 'removed_ADD_instructions':2*len(chosen), + 'selected_raw_event_intervals':chosen, + 'source_forward_scalar_allowance':158120, + 'source_backward_scalar_allowance':158168, + 'native_paid_histogram_unchanged':True, + 'same_native_climb_pair_sets':same_pairs, + 'dual_literal_checks':literal, + 'negative_control_one_unpaired_add_rejected':rejected, + 'two_independent_632_column_interpreters_each_orientation':True, + 'new_kappa':False, + 'required_next_checks':'Full absolute-phase native audit, whole controller and uniform compiler at changed scalar word.'} + (HERE/'COMBINED_SCALAR_CANCEL_RECEIPT.json').write_text( + json.dumps(report,indent=2,sort_keys=True)+'\n') + print('PASS_CAO_DUAL_632_SCALAR_CANCELLATION', + 'removed_pairs',len(chosen), + 'forward_scalar_allowance',literal['forward']['real_scalar_allowance'], + 'backward_scalar_allowance',literal['backward']['real_scalar_allowance'], + 'native_pairs_preserved',same_pairs) +if __name__=='__main__':run() diff --git a/research/p16-cao-scalar-dag/inverse_add_dag_search.py b/research/p16-cao-scalar-dag/inverse_add_dag_search.py new file mode 100644 index 0000000000..75e3e570b0 --- /dev/null +++ b/research/p16-cao-scalar-dag/inverse_add_dag_search.py @@ -0,0 +1,119 @@ +#!/usr/bin/env python3 +"""Exact additive inverse-pair elimination on Cao Yifan's frozen native word. + +A candidate removes two ADD instructions A_i<-c*A_j and A_i<--c*A_j +separated solely by gates commuting with that ADD, so their product is +the identity. The removal is applied to BOTH directions; native words are +regenerated; full paid profiles, and 632-column identities when applicable, +are checked. Zero candidates is an exact restriction on this bounded family. +""" +from collections import Counter +from copy import deepcopy +from pathlib import Path +from fractions import Fraction +from decimal import Decimal,localcontext +import gzip,json,sys +HERE=Path(__file__).resolve().parent +ROOT=Path(sys.argv[1]).resolve() if len(sys.argv)>1 else HERE.parents[2] +sys.path.insert(0,str(ROOT/'research/warp-interface-20261022')) +import warp_merge as W +F=W.F +def read(f):return json.loads(gzip.decompress(f.read_bytes())) +def operand(e): + if e[0]!='scalar':return None + g=e[1] + if g[0]!='add' or g[1][0]!='L' or g[2][0]!='L':return None + return (tuple(g[1]),tuple(g[2]),Fraction(g[3],g[4])) +def touches(e,regions): + if e[0]=='scalar': + return bool(set(W.roles(e)) & regions) + if e[0]=='warp': + return e[1][0]=='L' and e[1][1] in regions + return False +def commute_with_pair(e,source,target): + if e[0]=='warp': + return not touches(e,{source,target}) + if e[0]!='scalar':return True + g=e[1] + if g[0]!='add': + return not touches(e,{source,target}) + if g[1][0]!='L' or g[2][0]!='L': + return not touches(e,{source,target}) + d,s=g[1][1],g[2][1] + # [E_target,source, E_d,s]=0 iff target!=s and d!=source + return target!=s and d!=source +def paid(w): + return Counter(e[-1] for e in w if e[0] in ('climb','center')) +def scan(): + c,allwords=None,None + data=read(ROOT/'research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz') + c=data['canonical'];allwords=data['programs'] + raw={d:[deepcopy(e) for e in word if e[0]!='climb'] + for d,word in allwords.items()} + f=raw['forward'];b=raw['backward'] + assert len(f)==len(b) + base=paid(allwords['forward']) + assert base==Counter({1:2201,2:412,3:510,4:127,5:40,8:8}) + opportunities=[];considered=0 + for right in range(len(f)): + x=operand(f[right]) + if x is None:continue + tgt,src,coeff=x + for left in range(max(0,right-160),right): + y=operand(f[left]) + if y is None:continue + if y[:2]!=(tgt,src) or y[2]!=-coeff:continue + considered+=1 + if any(not commute_with_pair(f[k],src[1],tgt[1]) + for k in range(left+1,right)):continue + # Independently require ordinary inverse-transpose commuting + # and cancellation at the SAME chronological event indices. + bb1=operand(b[left]);bb2=operand(b[right]) + if bb1 is None or bb2 is None or bb1[:2]!=bb2[:2] or bb1[2]!=-bb2[2]: + continue + if any(not commute_with_pair(b[k],bb1[1][1],bb1[0][1]) + for k in range(left+1,right)):continue + opportunities.append((left,right)) + receipts={'status':'NO_GLOBAL_CLAIM', + 'pinned_source':'20bb93cd990d2ff683e4d0fc56b87a42cd5d3296', + 'candidate_window':160, + 'inverse_add_pairs_considered':considered, + 'commuting_dual_legal_pairs':len(opportunities), + 'examples':opportunities[:35], + 'source_paid_before':dict(sorted(base.items())), + 'new_kappa':False,'candidate_receipts':[]} + V=None;X=None + for left,right in opportunities[:15]: + compiled={} + try: + for direction in ('forward','backward'): + word=[e for i,e in enumerate(raw[direction]) if i not in (left,right)] + compiled[direction]=W.synthesize(c,word) + a=paid(compiled['forward']);bpaid=paid(compiled['backward']) + assert a==bpaid + with localcontext() as ctx: + ctx.prec=55;t=Decimal(1)-Decimal('0.0030217758') + delta=sum(Decimal(k)**t*(base[k]-a[k]) for k in set(base)|set(a)) + rec={'left':left,'right':right,'paid_gain':str(delta), + 'modified_paid':dict(sorted(a.items()))} + if delta>0: + if V is None: + V=F.load(ROOT/'research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py','cao_dag_rows') + X=F.load(ROOT/'research/kappa-rebuild/complex/native_extensions.py','cao_dag_literal') + for direction in compiled: + rows,r=X.literal_replay(V,c,compiled[direction],direction=='backward') + assert all(rows['L',i]==V.expected(('L',i),[],direction=='backward',False) for i in range(632)) + rec['both_literal_directions']='PASS' + receipts['status']='POSITIVE_NATIVE_MOMENT_DUAL_LITERAL_PHASE_OPEN' + receipts['candidate_receipts'].append(rec) + except (ValueError,AssertionError) as err: + receipts['candidate_receipts'].append({'left':left,'right':right, + 'rejection':str(err)}) + if receipts['status']=='NO_GLOBAL_CLAIM': + receipts['status']='PASS_BOUNDED_INVERSE_ADD_SEARCH_NO_ADMITTED_NEW_KAPPA' + (HERE/'SCALAR_DAG_INVERSE_PAIRS_RECEIPT.json').write_text( + json.dumps(receipts,indent=2,sort_keys=True)+'\n') + print(receipts['status'],'inverse_pair_considered',considered, + 'commuting_in_both_orientations',len(opportunities)) + print('SCREEN',receipts['candidate_receipts'][:3]) +if __name__=='__main__':scan()