From 06a61ba2314094be22e88833b9fdfda598a2a9be Mon Sep 17 00:00:00 2001 From: zxv Date: Tue, 27 Oct 2026 23:19:14 -0400 Subject: [PATCH 1/4] Align current CI navigation with selected PR6030 --- docs/ci-verification.md | 19 ++++++++++++++++++- docs/research/current-status.md | 2 +- 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 006bf5a3d5..63ba3e9aa8 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,6 +1,23 @@ # CI verification -## Current selected-family replay: #5599 +## Current selected-family replay: #6030 + +The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), +and [explicit source closure](../certificates/frontier6030-source.json). +`make frontier6030-verify` follows that source-bound selected replay. The review +separates retained normal primary macOS/Linux evidence from fresh independent +word/invoice/native, original caller, adapted caller and optimized primary checks. +Consult its receipts for exact commands, source heads and limits; the #5599 +checkpoint below retains its own historical replay details. + +The five inherited framework assumptions remain. Neither the full uniform word +nor a complete rounded multiplier is materialized. A source/metadata check is +not an operator replay or a formal theorem proof. Routine research submissions +do not need to rerun this selected-family replay. + +## Historical selected-family replay: #5599 The [selected record](../certificates/selected-result.json) binds conditional κ = 0.00310045 to the [proof review](research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md) diff --git a/docs/research/current-status.md b/docs/research/current-status.md index a84ac12213..c49a245adc 100644 --- a/docs/research/current-status.md +++ b/docs/research/current-status.md @@ -1,6 +1,6 @@ # Current reviewed status -Selected conditional κ: **0.003125804 = 781451/250000000**, DreamingOfClouds' +Selected conditional κ: **0.003125804** = 781451/250000000, DreamingOfClouds' PR6030 on the cumulative P104 construction. The complete caller counts 13,444 productive fields and 66,834 paid calls. The saving is about 0.81775% above the preceding selected PR5599 claim 0.00310045. From cd77e98bcbcdfbe2f4a4529084abfe100e97be0d Mon Sep 17 00:00:00 2001 From: zxv Date: Tue, 27 Oct 2026 23:29:41 -0400 Subject: [PATCH 2/4] Prove full tensor cut modules and fixed-catalogue channel decay --- research/dyadic-tensor-capacity/README.md | 198 +++++++++++++++++++ research/dyadic-tensor-capacity/SOURCES.json | 42 ++++ research/dyadic-tensor-capacity/TASK.json | 79 ++++++++ research/dyadic-tensor-capacity/VERIFY.json | 35 ++++ research/dyadic-tensor-capacity/verify.py | 167 ++++++++++++++++ 5 files changed, 521 insertions(+) create mode 100644 research/dyadic-tensor-capacity/README.md create mode 100644 research/dyadic-tensor-capacity/SOURCES.json create mode 100644 research/dyadic-tensor-capacity/TASK.json create mode 100644 research/dyadic-tensor-capacity/VERIFY.json create mode 100644 research/dyadic-tensor-capacity/verify.py diff --git a/research/dyadic-tensor-capacity/README.md b/research/dyadic-tensor-capacity/README.md new file mode 100644 index 0000000000..084c1d017b --- /dev/null +++ b/research/dyadic-tensor-capacity/README.md @@ -0,0 +1,198 @@ +# Product cuts retain their full dyadic channel module under tensoring + +A pure product of saturated dyadic helper cuts has exactly the tensor product +of their eligible prefix and suffix modules. This includes arbitrary linear +combinations across tensor coordinates: it is not a simple-tensor restriction. +Consequently, tensoring cannot recover hidden channels beyond the primewise +capacity already proved in [Nick Petalas](https://github.com/petalas)'s +[PR #5882](https://github.com/CrocSwap/integer-mult-bounds/pull/5882). + +A second consequence concerns a fixed finite catalogue: if each of its cuts +loses a positive fraction of rational channels at some odd prime, **every +arbitrarily mixed long product retains at most an exponentially vanishing +fraction of its rational channel count**. Complementary primes can still improve finite tensor +capacity, exactly as #5882 shows. Changing the cut/support or catalogue is a +real reopening condition; repeating the same defective catalogue is not. + +This is a scoped module theorem with source-relative causal examples. It does +not construct selected P104 physical tensor carriers or a new supplier or κ. +The numerical tensor-capacity formula and its sharp bounds are predecessor +results, not new claims here. + +## 1. Full eligible-module theorem + +Let D=Z[1/2], with fraction field Q. For each factor i take a finite free +ambient module V_i, an invertible dyadic prefix A_i, coordinate summands F_i +(the cut) and G_i (allowed helper input support). In row convention let + +``` +L_i = F_i intersect (G_i A_i^(-1)). +``` + +For the pure tensor prefix A= tensor_i A_i, cut F=tensor_i F_i and allowed +support G=tensor_i G_i, the **entire** eligible row module is + +``` +L = {v in F : v A in G} = tensor_i L_i. (1) +``` + +The column version gives the same identity for suffix-eligible modules R_i. +With full module bases L0_i,R0_i, their full tensor bases therefore pair by +`K = tensor_i (L0_i R0_i)`. No additional eligible vector is omitted by using +those bases. Basis changes are algebraic coordinates, with no free physical +implementation or channel credit inferred. + +**Proof.** A submodule is saturated when dv in it, for nonzero d in D, implies +v is in it. Coordinate summands are saturated, as are their images under an +invertible dyadic map. Intersections of saturated submodules are saturated. +Since D is a PID, a saturated submodule of a finite free module is a direct +summand: its finitely generated torsion-free quotient is free, and a basis of +the quotient lifts to a splitting. Thus every L_i is a direct summand. + +Over Q, for any subspaces U_i,W_i of V_i, + +``` +(tensor_i U_i) intersect (tensor_i W_i) + = tensor_i (U_i intersect W_i). +``` + +To see this, in each factor choose a basis of U_i intersect W_i, extend it +separately to U_i and W_i, and then to the ambient space. The tensor basis +vectors common to both tensor subspaces use an intersection vector in every +factor. This proves the identity for arbitrary, including nondecomposable, +vectors. Rationalization commutes with these intersections (clearing finitely +many denominators proves the reverse inclusion). + +The two sides of (1) have this same rational span. The left side is saturated +as an intersection of direct summands. The right side is a direct summand by +tensoring splittings of the L_i, so is saturated too. A saturated submodule H +of a free D-module is exactly `(Q H) intersect V`: clear a denominator and +apply saturation. Hence the two sides are equal over D. The column argument +is identical. Multiplication of tensor row/column bases gives the pairing +identity. ∎ + +Invertibility here is **over D**, not merely over Q. F and G are the exact +product supports. A larger cut, cross-factor support not of this form, live +owned fields, or a prefix not factoring as A changes the hypotheses. Equation +(1) alone does not prove timing, common physical charts or native realization. + +## 2. Fixed finite catalogues cannot tensor away their losses + +Use [Ali Romman](https://github.com/aliromman)'s +[PR #5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615) single-cut +criterion and #5882's tensor theorem as cited premises. Let a catalogue contain +q>=1 matrices K_j of positive rational ranks r_j and capacities c_j=3 take one untouched free coordinate f, p coordinates x, and p-1 +coordinates z, all arbitrary dirty. Let V have columns e_j-e_(j+1), and apply + +``` +x <- x + V z; +z <- z + V^T x; (A) +``` + +The suffix B reverses those two operations. Each half consists of 4(p-1) +signed scalar ADDs; the complete identity word costs **8(p-1)** ADDs, uses +2p arbitrary coordinates and restores all of them. There is no clean storage, +erasure or free basis conversion. Every intermediate event is replayed exactly. +At the cut choose F=G=span(f,x), with the original z-support excluded. The +row eligibility equation is v_x V=0; the column equation from B is V^T u_x=0. +Both full D-modules have the basis `(f, sum_j x_j)`, because all adjacent +coordinate differences must vanish. Their pairing is diag(1,p). + +Thus p=3 and p=5 yield explicit causal algebraic cuts with complementary prime +losses. They are calibration circuits, not source-bound P104 helpers: the +required strict chart nesting, native targets, tensor carriers, delivery and +complete caller bill are still absent. In particular their coefficient-basis +channels are not automatically independent productive Gaussian targets. + +The verifier also tensors the actual 3-coordinate K=[5] causal fixture from +#5615 through depth four. Full independently recomputed row/column kernels +have the complete tensor module, pairing [5^d], and zero unit capacity. +Scalar restoration at the base is checked; no exponentially large physical +word is claimed or materialized. + +## Evidence and reproduction + +``` +python3.12 -B scripts/research_package.py --package research/dyadic-tensor-capacity +python3.12 -B scripts/check_research_commit.py --package research/dyadic-tensor-capacity +``` + +The replay authenticates all live inputs. It reuses the pinned #5615 saturated +kernel routine, with a separate Fraction elimination to check ranks and +bidirectional module-basis coordinate changes. Every coordinate change must +be dyadic. It reconstructs the p=3,5 scalar words, their inverse and full cut +modules, checks mixed product cuts and the K=[5] fixture, and tests all binary +catalogue schedules through length 12. Corrupted supports, nonsaturated bases, +wrong capacities and a false nondefective-catalogue inference are rejected. +Normal and optimized modes use no dependencies and write no package files. +The uniform theorem is the written proof; the bounded checks do not replace it. + +Base main was refreshed on 2026-10-28 UTC at +721c03822c421b7f7fcbb2598993b947c4d88419, priority 8. The navigation-only +repair from [PR #6050](https://github.com/CrocSwap/integer-mult-bounds/pull/6050) +is included. No selected cold replay was run. The optional full-history check +is unavailable in this shallow repository; declared source pins use its +reachable main-base descendant. No full-history pass is claimed. + +## Significance for researchers + +This fills the full-module premise of tensor capacity for exactly factored +causal cuts. Searching more general vectors inside the same product support +cannot evade the prime obstruction. A fixed finite collection of defective +cuts also cannot maintain a positive fraction of rational channels at arbitrary +tensor depth. New support, charts or caller boundaries remain legitimate +escape directions, with their implementation costs payable. + +## Open next questions + +Does an actual selected or pending native word admit a legal product cut with +these exact saturated supports and common physical timing? First extract one +prefix/suffix and its cut-field list, then verify the full module and price +its tensor carrier. The scalar calibration circuits do not discharge native +or productive-target obligations. + +Can a controlled nonproduct cut enlarge the eligible module enough to fund its +extra fields and delivery? Begin with one added coordinate outside F tensor F; +state the changed support and full signed bill before expanding a search. + +## Credit + +Prepared by [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance. +[Ali Romman](https://github.com/aliromman) supplies #5615's single-cut criterion, +causal K=[5] fixture and saturated-kernel code, retained unchanged. +[Nick Petalas](https://github.com/petalas) supplies #5882's tensor formula, +sharp bounds and complementary-prime examples. Those are credited premises. +Saturation over a PID, tensor basis arguments and pigeonhole counting are +classical; the contribution is the full eligible-module implication, fixed +catalogue bound and explicit causal-cut calibration here. No independent human +or proof-assistant review is claimed. Apache-2.0. diff --git a/research/dyadic-tensor-capacity/SOURCES.json b/research/dyadic-tensor-capacity/SOURCES.json new file mode 100644 index 0000000000..bcbad55112 --- /dev/null +++ b/research/dyadic-tensor-capacity/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "06a61ba2314094be22e88833b9fdfda598a2a9be", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/dyadic-helper-channel-capacity/PROOF.md", + "usage": "input", + "git_blob": "c97a6edce3070414c81f0ef6e6c099ebb17f3a90", + "sha256": "b258a217f2cd0fc48461285fe8ae24de26b0c5963668d9d8f0955fc6e759e929" + }, + { + "path": "research/dyadic-helper-channel-capacity/README.md", + "usage": "input", + "git_blob": "771c11f6ac4f1c368b4c1dae110956b365dde09e", + "sha256": "e79f7b65102179fc7548f2c40db72fd1581ccf23ad4f30fefa371604a1479d1e" + }, + { + "path": "research/tensor-helper-capacity/PROOF.md", + "usage": "input", + "git_blob": "09f921ccdc6fbd289d46e1d7d9620b20fd72c0d7", + "sha256": "4621e2a382ce0b077aa70a392b5e0b2cdec14e550a369558d795431e14e17262" + }, + { + "path": "research/dyadic-helper-channel-capacity/capacity.py", + "usage": "input", + "git_blob": "d882eb6d049125c67d4c0d47dced60bf0e181268", + "sha256": "1cd82b0beab7983d955cfc1d1e562af490f90bcaad6e3ec7d07e0c5a33608834" + } + ] +} diff --git a/research/dyadic-tensor-capacity/TASK.json b/research/dyadic-tensor-capacity/TASK.json new file mode 100644 index 0000000000..992a08f00d --- /dev/null +++ b/research/dyadic-tensor-capacity/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "06a61ba2314094be22e88833b9fdfda598a2a9be", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Full saturated eligible-module tensor theorem, fixed finite defective-catalogue decay, and restored scalar causal-cut calibration.", + "scope_change_reason": "Live overlap found PR5882 already proves numerical tensor capacity. This answers its separate full eligible-module premise under pure product support and supplies a new catalogue consequence, not another capacity-formula proof.", + "bottleneck_link": "Distinguishes real support/interface changes from tensoring a fixed defective cut; no physical target credit inferred.", + "budget_minutes": 20, + "stop_rule": "Prove exact product-module identity and bounded causal examples; stop before native/P104 implementation expansion.", + "outcome": "completed", + "evidence": "README.md uniform module and catalogue proofs; verify.py full-kernel and module-coordinate checks.", + "author": "zxv (https://github.com/zxv), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance.", + "open_questions": [ + { + "question": "Does a native P104 word provide a legal product cut?", + "why_it_matters": "Needed to apply the algebraic theorem to actual productive targets.", + "first_step": "Extract prefix/suffix, exact cut supports, timing and native carrier costs.", + "blocked_by": "The calibration circuits do not provide those native contracts." + }, + { + "question": "Can one added nonproduct cut coordinate fund its full cost?", + "why_it_matters": "Would change the exact product-support obstruction.", + "first_step": "Specify one larger cut and its complete signed invoice.", + "blocked_by": "No changed physical support or delivery is supplied." + } + ] +} diff --git a/research/dyadic-tensor-capacity/VERIFY.json b/research/dyadic-tensor-capacity/VERIFY.json new file mode 100644 index 0000000000..6396ff4c25 --- /dev/null +++ b/research/dyadic-tensor-capacity/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/dyadic-helper-channel-capacity/PROOF.md", + "research/dyadic-helper-channel-capacity/README.md", + "research/tensor-helper-capacity/PROOF.md", + "research/dyadic-helper-channel-capacity/capacity.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full saturated kernels and bidirectional dyadic module equality of explicit scalar product cuts; all two-type schedules through length 12; restoration and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same exact checks with assertions disabled." + } + ] +} diff --git a/research/dyadic-tensor-capacity/verify.py b/research/dyadic-tensor-capacity/verify.py new file mode 100644 index 0000000000..17afcd5776 --- /dev/null +++ b/research/dyadic-tensor-capacity/verify.py @@ -0,0 +1,167 @@ +"""Full dyadic cut modules and fixed-catalogue decay. Apache-2.0.""" +from fractions import Fraction as Q +from itertools import product as words +from pathlib import Path +import hashlib +import importlib.util +import json + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + + +def need(ok,msg): + if not ok:raise ValueError(msg) + + +def eye(n):return [[int(i==j) for j in range(n)] for i in range(n)] +def tr(a):return [list(x) for x in zip(*a)] +def mm(a,b):return [[sum(x*y for x,y in zip(row,col)) for col in zip(*b)] for row in a] + + +def tensor(a,b): + return [[x*y for x in rowa for y in rowb] for rowa in a for rowb in b] + + +def kron_indices(left,right,nright):return [i*nright+j for i in left for j in right] + + +def rref(a): + a=[[Q(x) for x in row] for row in a] + if not a:return a,[] + piv=[];i=0 + for j in range(len(a[0])): + k=next((k for k in range(i,len(a)) if a[k][j]),None) + if k is None:continue + a[i],a[k]=a[k],a[i] + t=a[i][j];a[i]=[x/t for x in a[i]] + for k in range(len(a)): + if k!=i: + t=a[k][j];a[k]=[x-t*y for x,y in zip(a[k],a[i])] + piv.append(j);i+=1 + if i==len(a):break + return a,piv + + +def rank(a):return len(rref(a)[1]) + + +def module_contains(basis,rows): + # RREF pivot columns give a nonsingular coordinate restriction. + if not basis:return all(not any(row) for row in rows) + _,piv=rref(basis) + need(len(piv)==len(basis),'basis independent') + small=tr([[row[j] for j in piv] for row in basis]) + for row in rows: + augmented=[list(a)+[row[j]] for a,j in zip(small,piv)] + reduced,cols=rref(augmented) + need(cols==list(range(len(basis))),'coordinate system') + coeff=[reduced[i][-1] for i in range(len(basis))] + if any(x.denominator & (x.denominator-1) for x in coeff):return False + if [sum(coeff[i]*basis[i][j] for i in range(len(basis))) + for j in range(len(row))]!=row:return False + return True + + +def same_module(a,b): + need(rank(a)==rank(b),'module rank') + need(module_contains(a,b) and module_contains(b,a),'full dyadic module equality') + + +def eligible(a,b,f,g,kernel): + n=len(a);outside=[j for j in range(n) if j not in g] + # Full kernel bases as columns, transposed to row bases for comparison. + left=tr(kernel([[a[i][j] for i in f] for j in outside],len(f))) + right=tr(kernel([[b[j][i] for i in f] for j in outside],len(f))) + return left,right + + +def causal(p): + n=2*p;a=eye(n);events=[] + # (free, p data, p-1 dirty auxiliary) coordinates. + for j in range(p-1): + z=p+1+j + events.extend([(1+j,z,1),(2+j,z,-1)]) + for j in range(p-1): + z=p+1+j + events.extend([(z,1+j,1),(z,2+j,-1)]) + for dst,src,c in events:a[dst]=[x+c*y for x,y in zip(a[dst],a[src])] + b=eye(n) + for dst,src,c in reversed(events):b[dst]=[x-c*y for x,y in zip(b[dst],b[src])] + need(mm(a,b)==mm(b,a)==eye(n),'arbitrary-input identity word') + need(len(events)*2==8*(p-1),'complete scalar tariff') + expected=[[1]+[0]*p,[0]+[1]*p] + return a,b,list(range(p+1)),expected + + +def rejected(fn): + try:fn() + except ValueError:return + raise ValueError('negative control accepted') + + +def main(): + pins=json.loads((HERE/'SOURCES.json').read_text()) + for row in pins['files']: + if row['usage']=='input': + need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'source hash') + path=ROOT/'research/dyadic-helper-channel-capacity/capacity.py' + spec=importlib.util.spec_from_file_location('retained_capacity',path) + module=importlib.util.module_from_spec(spec);spec.loader.exec_module(module) + kernel=module.kernel + circuits={} + for p in (3,5): + a,b,f,expected=causal(p) + l,r=eligible(a,b,f,f,kernel) + same_module(l,expected);same_module(r,expected) + need(mm(expected,tr(expected))==[[1,0],[0,p]],'causal pairing') + circuits[p]=(a,b,f,expected) + # Independently solve every full eligible module of three small product cuts. + cuts=0 + for pp,qq in ((3,3),(3,5),(5,3)): + a,b,f,e=circuits[pp];aa,bb,ff,ee=circuits[qq] + biga,bigb=tensor(a,aa),tensor(b,bb) + bigf=kron_indices(f,ff,len(aa)) + l,r=eligible(biga,bigb,bigf,bigf,kernel) + expected=tensor(e,ee) + same_module(l,expected);same_module(r,expected) + need(rank(l)==4,'full product eligibility') + cuts+=1 + # Retained literal K=[5] fixture: full tensor kernels, not guessed channels. + a=[[1,0,1],[0,1,2],[1,2,6]] + b=[[2,2,-1],[2,5,-2],[-1,-2,1]] + biga=bigb=[[1]];f=[0];expected=[[1]] + for depth in range(1,5): + biga,bigb=tensor(biga,a),tensor(bigb,b) + f=kron_indices(f,[0,1],3) + expected=tensor(expected,[[-2,1]]) + l,r=eligible(biga,bigb,f,f,kernel) + same_module(l,expected);same_module(r,expected) + need(mm(expected,tr(expected))==[[5**depth]],'zero-capacity tensor fixture') + cuts+=1 + schedules=0 + for n in range(1,13): + for w in words((3,5),repeat=n): + count3=w.count(3);count5=n-count3 + cap=min(2**count3,2**count5) + need(cap==2**min(count3,count5),'exact two-prime profile') + need(cap*2**((n+1)//2)<=2**n,'fixed-catalogue decay') + schedules+=1 + k=[[1,0,0,0],[0,5,0,0],[0,0,3,0],[0,0,0,15]] + x=[[1,0,0,0],[0,-1,2,0]] + y=[[1,0],[0,1],[0,1],[0,0]] + need(mm(mm(x,k),y)==eye(2),'credited complementary-prime witness') + rejected(lambda:same_module([[3,3]],[[1,1]])) + rejected(lambda:same_module([[1,0]],[[0,1]])) + a,b,f,e=circuits[3] + l,r=eligible(a,b,f[:-1],f,kernel) + rejected(lambda:same_module(l,[row[:-1] for row in e])) + bad=[row[:] for row in a];bad[1][1]+=1 + rejected(lambda:need(mm(bad,b)==eye(len(a)),'changed prefix')) + rejected(lambda:need(3<=2,'false three-channel capacity')) + rejected(lambda:need(Q(1,1)<1,'full-capacity type is defective')) + print(json.dumps(dict(status='PASS_DYADIC_FULL_TENSOR_CUT',full_product_cuts=cuts, + schedules=schedules,scope='full-module theorem and catalogue decay; no new kappa'),sort_keys=True)) + + +if __name__=='__main__':main() From a22d09e8323c24944631b922a23941a3c8b5d93f Mon Sep 17 00:00:00 2001 From: zxv Date: Tue, 27 Oct 2026 23:35:41 -0400 Subject: [PATCH 3/4] Render tensor-cut proofs and channel bounds as mathematical equations --- research/dyadic-tensor-capacity/README.md | 213 ++++++++++++---------- 1 file changed, 112 insertions(+), 101 deletions(-) diff --git a/research/dyadic-tensor-capacity/README.md b/research/dyadic-tensor-capacity/README.md index 084c1d017b..8cf2339ccd 100644 --- a/research/dyadic-tensor-capacity/README.md +++ b/research/dyadic-tensor-capacity/README.md @@ -21,124 +21,135 @@ results, not new claims here. ## 1. Full eligible-module theorem -Let D=Z[1/2], with fraction field Q. For each factor i take a finite free -ambient module V_i, an invertible dyadic prefix A_i, coordinate summands F_i -(the cut) and G_i (allowed helper input support). In row convention let +Let $D=\mathbb{Z}[1/2]$, with fraction field $\mathbb{Q}$. For each factor $i$, take a finite free ambient module $V_i$, an invertible dyadic prefix $A_i$, and coordinate summands $F_i$ (the cut) and $G_i$ (allowed helper input support). In row convention, define -``` -L_i = F_i intersect (G_i A_i^(-1)). -``` +$$ +L_i = F_i \cap \bigl(G_i A_i^{-1}\bigr). +$$ -For the pure tensor prefix A= tensor_i A_i, cut F=tensor_i F_i and allowed -support G=tensor_i G_i, the **entire** eligible row module is +For the pure tensor prefix, cut and allowed support, write -``` -L = {v in F : v A in G} = tensor_i L_i. (1) -``` +$$ +A=\bigotimes_i A_i, +\qquad F=\bigotimes_i F_i, +\qquad G=\bigotimes_i G_i. +$$ -The column version gives the same identity for suffix-eligible modules R_i. -With full module bases L0_i,R0_i, their full tensor bases therefore pair by -`K = tensor_i (L0_i R0_i)`. No additional eligible vector is omitted by using -those bases. Basis changes are algebraic coordinates, with no free physical -implementation or channel credit inferred. +Then the **entire** eligible row module is -**Proof.** A submodule is saturated when dv in it, for nonzero d in D, implies -v is in it. Coordinate summands are saturated, as are their images under an -invertible dyadic map. Intersections of saturated submodules are saturated. -Since D is a PID, a saturated submodule of a finite free module is a direct -summand: its finitely generated torsion-free quotient is free, and a basis of -the quotient lifts to a splitting. Thus every L_i is a direct summand. +$$ +\boxed{\displaystyle +L=\{v\in F: vA\in G\}=\bigotimes_i L_i. +} +\tag{1} +$$ -Over Q, for any subspaces U_i,W_i of V_i, +The column version gives the same identity for suffix-eligible modules $R_i$. With full module bases $L_{0,i}$ and $R_{0,i}$, their full tensor bases therefore pair by -``` -(tensor_i U_i) intersect (tensor_i W_i) - = tensor_i (U_i intersect W_i). -``` +$$ +K=\bigotimes_i\bigl(L_{0,i}R_{0,i}\bigr). +$$ + +No additional eligible vector is omitted by using those bases. Basis changes are algebraic coordinates, with no free physical implementation or channel credit inferred. + +**Proof.** A submodule is saturated when $dv$ belonging to it, for nonzero $d\in D$, implies that $v$ belongs to it. Coordinate summands are saturated, as are their images under an invertible dyadic map. Intersections of saturated submodules are saturated. Since $D$ is a PID, a saturated submodule of a finite free module is a direct summand: its finitely generated torsion-free quotient is free, and a basis of the quotient lifts to a splitting. Thus every $L_i$ is a direct summand. -To see this, in each factor choose a basis of U_i intersect W_i, extend it -separately to U_i and W_i, and then to the ambient space. The tensor basis -vectors common to both tensor subspaces use an intersection vector in every -factor. This proves the identity for arbitrary, including nondecomposable, -vectors. Rationalization commutes with these intersections (clearing finitely -many denominators proves the reverse inclusion). - -The two sides of (1) have this same rational span. The left side is saturated -as an intersection of direct summands. The right side is a direct summand by -tensoring splittings of the L_i, so is saturated too. A saturated submodule H -of a free D-module is exactly `(Q H) intersect V`: clear a denominator and -apply saturation. Hence the two sides are equal over D. The column argument -is identical. Multiplication of tensor row/column bases gives the pairing -identity. ∎ - -Invertibility here is **over D**, not merely over Q. F and G are the exact -product supports. A larger cut, cross-factor support not of this form, live -owned fields, or a prefix not factoring as A changes the hypotheses. Equation -(1) alone does not prove timing, common physical charts or native realization. +Over $\mathbb{Q}$, for any subspaces $U_i,W_i\subseteq V_i$, + +$$ +\left(\bigotimes_i U_i\right)\cap +\left(\bigotimes_i W_i\right) +=\bigotimes_i(U_i\cap W_i). +$$ + +To see this, in each factor choose a basis of $U_i\cap W_i$, extend it separately to $U_i$ and $W_i$, and then to the ambient space. The tensor basis vectors common to both tensor subspaces use an intersection vector in every factor. This proves the identity for arbitrary, including nondecomposable, vectors. Rationalization commutes with these intersections: clearing finitely many denominators proves the reverse inclusion. + +The two sides of (1) have this same rational span. The left side is saturated as an intersection of direct summands. The right side is a direct summand by tensoring splittings of the $L_i$, so is saturated too. A saturated submodule $H\subseteq V$ of a free $D$-module satisfies + +$$ +H=\bigl(\operatorname{span}_{\mathbb{Q}}H\bigr)\cap V. +$$ + +Clear a denominator and apply saturation. Hence the two sides are equal over $D$. The column argument is identical. Multiplication of tensor row/column bases gives the pairing identity. ∎ + +Invertibility here is **over $D$**, not merely over $\mathbb{Q}$. The supports $F$ and $G$ are the exact product supports. A larger cut, cross-factor support not of this form, live owned fields, or a prefix not factoring as $A$ changes the hypotheses. Equation (1) alone does not prove timing, common physical charts or native realization. ## 2. Fixed finite catalogues cannot tensor away their losses -Use [Ali Romman](https://github.com/aliromman)'s -[PR #5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615) single-cut -criterion and #5882's tensor theorem as cited premises. Let a catalogue contain -q>=1 matrices K_j of positive rational ranks r_j and capacities c_j=3 take one untouched free coordinate f, p coordinates x, and p-1 -coordinates z, all arbitrary dirty. Let V have columns e_j-e_(j+1), and apply +Here is an explicit reversible scalar realization of those pairing types. For odd $p\geq3$, take one untouched free coordinate $f$, $p$ coordinates $x$, and $p-1$ coordinates $z$, all arbitrary dirty. Let $V$ have columns $e_j-e_{j+1}$, and apply -``` -x <- x + V z; -z <- z + V^T x; (A) -``` +$$ +A:\quad +\begin{aligned} +x&\leftarrow x+Vz,\\ +z&\leftarrow z+V^{\mathsf{T}}x. +\end{aligned} +$$ + +The suffix $B$ reverses those two operations. Each half consists of $4(p-1)$ signed scalar ADDs; the complete identity word costs **$8(p-1)$ ADDs**, uses $2p$ arbitrary coordinates and restores all of them. There is no clean storage, erasure or free basis conversion. Every intermediate event is replayed exactly. + +At the cut choose $F=G=\operatorname{span}(f,x)$, with the original $z$-support excluded. The row and column eligibility equations are + +$$ +v_xV=0, +\qquad V^{\mathsf{T}}u_x=0. +$$ + +Both full $D$-modules have basis $\bigl(f,\sum_jx_j\bigr)$, because all adjacent coordinate differences must vanish. Their pairing is + +$$ +K=\operatorname{diag}(1,p). +$$ + +Thus $p=3$ and $p=5$ yield explicit causal algebraic cuts with complementary prime losses. They are calibration circuits, not source-bound P104 helpers: the required strict chart nesting, native targets, tensor carriers, delivery and complete caller bill are still absent. In particular their coefficient-basis channels are not automatically independent productive Gaussian targets. -The suffix B reverses those two operations. Each half consists of 4(p-1) -signed scalar ADDs; the complete identity word costs **8(p-1)** ADDs, uses -2p arbitrary coordinates and restores all of them. There is no clean storage, -erasure or free basis conversion. Every intermediate event is replayed exactly. -At the cut choose F=G=span(f,x), with the original z-support excluded. The -row eligibility equation is v_x V=0; the column equation from B is V^T u_x=0. -Both full D-modules have the basis `(f, sum_j x_j)`, because all adjacent -coordinate differences must vanish. Their pairing is diag(1,p). - -Thus p=3 and p=5 yield explicit causal algebraic cuts with complementary prime -losses. They are calibration circuits, not source-bound P104 helpers: the -required strict chart nesting, native targets, tensor carriers, delivery and -complete caller bill are still absent. In particular their coefficient-basis -channels are not automatically independent productive Gaussian targets. - -The verifier also tensors the actual 3-coordinate K=[5] causal fixture from -#5615 through depth four. Full independently recomputed row/column kernels -have the complete tensor module, pairing [5^d], and zero unit capacity. -Scalar restoration at the base is checked; no exponentially large physical -word is claimed or materialized. +The verifier also tensors the actual three-coordinate $K=[5]$ causal fixture from [PR #5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615) through depth four. Full independently recomputed row/column kernels have the complete tensor module, pairing $[5^d]$, and zero unit capacity. Scalar restoration at the base is checked; no exponentially large physical word is claimed or materialized. ## Evidence and reproduction @@ -182,7 +193,7 @@ its tensor carrier. The scalar calibration circuits do not discharge native or productive-target obligations. Can a controlled nonproduct cut enlarge the eligible module enough to fund its -extra fields and delivery? Begin with one added coordinate outside F tensor F; +extra fields and delivery? Begin with one added coordinate outside $F\otimes F$; state the changed support and full signed bill before expanding a search. ## Credit From a3595fe3e1c4db6777347d2387b246b4a97d0eea Mon Sep 17 00:00:00 2001 From: zxv Date: Tue, 27 Oct 2026 23:38:20 -0400 Subject: [PATCH 4/4] Use renderer-compatible math in the dyadic tensor proof --- research/dyadic-tensor-capacity/README.md | 32 ++++++++++------------- 1 file changed, 14 insertions(+), 18 deletions(-) diff --git a/research/dyadic-tensor-capacity/README.md b/research/dyadic-tensor-capacity/README.md index 8cf2339ccd..35e1b4ebd9 100644 --- a/research/dyadic-tensor-capacity/README.md +++ b/research/dyadic-tensor-capacity/README.md @@ -35,11 +35,11 @@ A=\bigotimes_i A_i, \qquad G=\bigotimes_i G_i. $$ -Then the **entire** eligible row module is +Let $L$ consist of all vectors $v$ in $F$ satisfying $vA\in G$. Then the **entire** eligible row module is $$ \boxed{\displaystyle -L=\{v\in F: vA\in G\}=\bigotimes_i L_i. +L=\bigotimes_i L_i. } \tag{1} $$ @@ -67,7 +67,7 @@ To see this, in each factor choose a basis of $U_i\cap W_i$, extend it separatel The two sides of (1) have this same rational span. The left side is saturated as an intersection of direct summands. The right side is a direct summand by tensoring splittings of the $L_i$, so is saturated too. A saturated submodule $H\subseteq V$ of a free $D$-module satisfies $$ -H=\bigl(\operatorname{span}_{\mathbb{Q}}H\bigr)\cap V. +H=(\mathbb{Q}H)\cap V. $$ Clear a denominator and apply saturation. Hence the two sides are equal over $D$. The column argument is identical. Multiplication of tensor row/column bases gives the pairing identity. ∎ @@ -83,11 +83,11 @@ $$ \qquad 0\leq\theta<1. $$ -For every length-$n$ sequence $j_1,\ldots,j_n$ of catalogue members, with repetitions and arbitrary ordering, +For every sequence of length $n$ $j_1,\ldots,j_n$ of catalogue members, with repetitions and arbitrary ordering, $$ \boxed{\displaystyle -\frac{c\!\left(\bigotimes_{\ell=1}^{n}K_{j_\ell}\right)} +\frac{c\left(\bigotimes_{\ell=1}^{n}K_{j_\ell}\right)} {\prod_{\ell=1}^{n}r_{j_\ell}} \leq\theta^{\lceil n/q\rceil}. } @@ -105,15 +105,15 @@ If $\theta=0$, any nonempty tensor has zero capacity by the predecessor's zero-c This is uniform over switching schedules, not only repeated equal factors. It assumes a **fixed finite** defective catalogue. Adding new cuts as $n$ grows, a full-capacity type, nonproduct supports or changed endpoints is outside it. It concerns unit-channel capacity, not the entire productive signed invoice: one must not turn it into a universal $\kappa$ ceiling. -For the predecessor's two types $\operatorname{diag}(1,3)$ and $\operatorname{diag}(1,5)$, take $a$ copies of the first and $b$ of the second. Then +Let $K_3$ and $K_5$ be the predecessor's diagonal matrices with entries $(1,3)$ and $(1,5)$. Take $a$ copies of the first and $b$ of the second. Then $$ \begin{aligned} -c\!\left(\operatorname{diag}(1,3)^{\otimes a} -\otimes\operatorname{diag}(1,5)^{\otimes b}\right) +c\left(K_3^{\otimes a} +\otimesK_5^{\otimes b}\right) &=2^{\min(a,b)},\\ -r\!\left(\operatorname{diag}(1,3)^{\otimes a} -\otimes\operatorname{diag}(1,5)^{\otimes b}\right) +r\left(K_3^{\otimes a} +\otimesK_5^{\otimes b}\right) &=2^{a+b}. \end{aligned} $$ @@ -128,24 +128,20 @@ $$ A:\quad \begin{aligned} x&\leftarrow x+Vz,\\ -z&\leftarrow z+V^{\mathsf{T}}x. +z&\leftarrow z+V^Tx. \end{aligned} $$ The suffix $B$ reverses those two operations. Each half consists of $4(p-1)$ signed scalar ADDs; the complete identity word costs **$8(p-1)$ ADDs**, uses $2p$ arbitrary coordinates and restores all of them. There is no clean storage, erasure or free basis conversion. Every intermediate event is replayed exactly. -At the cut choose $F=G=\operatorname{span}(f,x)$, with the original $z$-support excluded. The row and column eligibility equations are +At the cut choose $F=G$ to be the coordinate module generated by $f$ and $x$, with the original $z$-support excluded. The row and column eligibility equations are $$ v_xV=0, -\qquad V^{\mathsf{T}}u_x=0. +\qquad V^Tu_x=0. $$ -Both full $D$-modules have basis $\bigl(f,\sum_jx_j\bigr)$, because all adjacent coordinate differences must vanish. Their pairing is - -$$ -K=\operatorname{diag}(1,p). -$$ +Both full $D$-modules have basis $\bigl(f,\sum_jx_j\bigr)$, because all adjacent coordinate differences must vanish. Their pairing is the diagonal matrix with entries $(1,p)$. Thus $p=3$ and $p=5$ yield explicit causal algebraic cuts with complementary prime losses. They are calibration circuits, not source-bound P104 helpers: the required strict chart nesting, native targets, tensor carriers, delivery and complete caller bill are still absent. In particular their coefficient-basis channels are not automatically independent productive Gaussian targets.