diff --git a/research/native-error-channel-amplification/README.md b/research/native-error-channel-amplification/README.md new file mode 100644 index 0000000000..9e2b055088 --- /dev/null +++ b/research/native-error-channel-amplification/README.md @@ -0,0 +1,94 @@ +# Sharp source-ordered native-port error channels + +Prepared by JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. + +## Result and exact interface + +This answers [PR4828](https://github.com/CrocSwap/integer-mult-bounds/pull/4828)'s Open next question2 for the literal [PR4743](https://github.com/CrocSwap/integer-mult-bounds/pull/4743) full-input ports. Sharp Euclidean endpoint conditioning and coordinatewise chronological error propagation are different quantities. Keep every individual tensorized phase letter, two arbitrary independent input banks, and every forward/reverse paid call. Write `L=2^(f/2)` for every integer f>=1. + +Assume independent initial input-coordinate perturbations and an additive complex-coordinate defect after each completed paid call, each of modulus at most rho on that call's actual stored input. Monomial updates, integer mixing and their reverses are exact on the common grid. Then the **exact largest output-coordinate error**, over those abstract independent defect balls and both output banks, is bounded by `E rho`, with these sharp constants: + +| Literal schedule | E(f) | Sufficient completed-call/input tolerance for output2^-P | +| --- | --- | --- | +| two-call forward | `3L^2+4L+1` | `rho=2^(-P-f-3)` | +| three-call forward | `2L^3+4L^2+2L+1` | `rho=2^(-P-ceil(3f/2)-3)` | +| two-call reverse | `L+4` | `rho=2^(-P-ceil(f/2)-2)` | +| three-call reverse | `L^2+L+4` | `rho=2^(-P-f-2)` | + +The original sufficient tolerance `2^(-P-2f-6)` remains valid. These are improved **external completed-call accuracy requests**, not measured word/time savings from a new Gaussian implementation. The abstract independent defects need not all be attainable errors of one concrete rounded algorithm. Sharpness is a property of this explicitly stated error contract; it is not a lower bound on every numerical realization. No paid calls are removed and no new κ is claimed. + +## Actual chronology and defect maps + +Use source `A=C0`, `P=S U S`, `Q=S V01 S`, `W=Z0 Z2`, `M=Z1 V01`, `J=M C2`, `D=J W A`; each subscript f tensors the individual base matrix before addition. In this section suppress f. Source order is + +``` +t = A(x+dx)+e1; +s = A((y+dy)+P t+2Q t)+e2; +u = M(C2 W s+e3) # three-call variant only +``` + +The third defect is immediately after C2 and before M. It cannot be replaced by an identity channel when checking the actual vector error, even though M has coordinate norm1. With `F=A P A+2 A Q A`, `B=D P A+2 D Q A`, the lower-bank maps of the independent error variables are + +| schedule | dx | dy | e1 | e2 | e3 | +| --- | --- | --- | --- | --- | --- | +| forward2 | F | A | `A P+2 A Q` | I | absent | +| forward3 | B | D | `D P+2 D Q` | `J W` | M | + +The upper bank has error `A dx+e1`. There are no products between defects: the maps are linear and every paid-call error is defined against its actual perturbed input. Using a defect guarantee only at an ideal input would change the premise. + +For the reverse3 program, apply M^-1 then C2^-1 to the second input, insert its first defect, apply W^-1 then A^-1 and insert its second defect. Subtract P t and2Q t using the retained first input **before** its final A^-1 call. That last call's defect reaches only the first output. Reverse2 omits the first C2 stage. Thus the lower output channels are + +| schedule | first-input quantization | second-input quantization | first paid defect | second paid defect | third paid defect | +| --- | --- | --- | --- | --- | --- | +| reverse2 | `-(P+2Q)` | A^-1 | I | zero | absent | +| reverse3 | `-(P+2Q)` | D^-1 | `A^-1 W^-1` | I | zero | + +The upper bank is `A^-1 dt+e_last`. An inverse paid call can use the source's forward-call-plus-X realization; its exact monomial merely transports the defect ball and preserves its coordinate tolerance. No optional odd division by15 is executed in these schedules. + +## Uniform norms and sharpness + +For a finite row r of a complex matrix, the induced complex-coordinate norm is `sum_j |r_j|`. Tensor products multiply row1-norms. The following exact eight-coordinate facts follow by multiplying the literal Gaussian-rational source letters. The verifier binds the source declarations and independently reconstructs those matrices; it imports no predecessor checker. + +* A,A^-1,JW,A^-1 W^-1 have flat rows of1-norm sqrt2; D,D^-1 have flat rows of1-norm2; P,Q,M are monomial. +* The two separately tensorized branches of F have flat row1-norm2, those of AP+2AQ have flat branch norm sqrt2, those of DP+2DQ have flat branch norm2, and those of P+2Q have flat branch norm1. +* B's first branch `D P A` has flat row norm sqrt2; its second branch `D Q A` has flat row norm sqrt8, as checked directly from the literal matrices. The source residual identity names another monomial M; it differs from this note's post-call `M=Z1 V01` and is not substituted here. Neither branch statement tensors the sum B. +* In base row0, every overlapping nonzero entry of each listed branch pair has the same complex phase: `x_j conjugate(y_j)` is positive real. This includes B's unequal-magnitude branches. + +The triangle inequality therefore gives the uniform upper bounds + +``` +||F_f||inf=3L^2, ||A_f P_f+2A_f Q_f||inf=3L, +||B_f||inf=2L^3+L, ||D_f P_f+2D_f Q_f||inf=3L^2, +||P_f+2Q_f||inf=3. +``` + +The equalities are attained by row `(0,...,0)`: entrywise same-phase overlap is preserved by products under tensorization, including support intersections, so the triangle inequality is exact there for every f. All the other single-unitary channels have their stated flat row norm. The proof is an application of explicit finite base identities and tensor functoriality, not extrapolation from the later width1/2/3 tests. + +For independent coordinate errors, concatenate all channel matrices horizontally. Its induced norm is the maximum, over output rows, of the sum of all channel row1-norms. Every channel above attains its own bound at the same row0, so summing gives the asserted E. For a sharpness witness, independently set each error coordinate to rho times the conjugate phase of its channel's row0 entry (zero entries may receive0). Every summand then points along the positive real axis and attains E rho. The two banks' upper error constant is only L+1, smaller than the lower-bank total. The mathematical witnesses can use eighth roots of unity; the finite execution tests use exact Gaussian-rational perturbations and do not claim that a dyadic quantizer necessarily generates every sharpness witness. + +## Guard consequence and retained costs + +Since f>=1, L>=sqrt2. Dividing forward2/forward3 constants by L^2/L^3 gives respectively at most `7/2+2sqrt2<8` and `3+(9/4)sqrt2<8`. Reverse2/reverse3 divided by L/L^2 are at most `1+2sqrt2<4` and `3+1/sqrt2<4`. Rounding the exponent upward yields the four stated dyadic tolerances with strict output margin. The checker uses rational squared comparisons, not floating logarithms. These guards are sufficient; the exact minimal dyadic guard can instead be selected by the explicit E table, and no optimality of the integer constants3/2 is claimed. + +The original conservative intermediate allowance `2^(H+2f+4)` for inputs of magnitude2^H remains sufficient: at most three Gaussian stages contribute at most L^3, the one mixed update contributes total coefficient3, and all new tolerances are at most1/8 for H,P>=0. Writing M0=2^H, the forward stages are bounded by `(3L^3+L^2)M0+(3L^3+4L^2+L+1)rho` and the reverse stages by `(L^2+3)M0+(L^2+L+4)rho` (the smaller two-call cases fit these envelopes). Each is below `8L^3 M0 <= 2^(H+2f+3)`. The looser original allowance therefore accommodates the perturbed states. Exact free monomial/scalar passes and their existing owned address workspace remain charged as in #4743. The Gaussian implementation's internal-prefix guard, internal error guarantee and execution cost are additional; this package neither installs nor prices one. It also does not price complete recursive substitution, general nonunitary encodings, full supplier/outer transfer or physical tapes. + +Research decision: stop at the actual error interface. Inherited paid/source/ownership/native contracts keep their status; source-ordered amplification and a sharper completed-call tolerance are established here; physical implementation and recursive consequences remain open. This is a focused precision obligation and does not reopen a fixed-word paid-saving search. + +## Evidence and reproduction + +Generated `RESULT.json` records12cases (two/three calls, forward/reverse, f1/2/3),54exact dirty perturbed trajectories and144independent impulse columns at width1. Exact row norms and row0 sharpness are checked at every row of the bounded lifted matrices. A separately executed chronological vector program agrees with the independent error maps. Six controls reject unsupported width, wrong phase family, wrong defect order, a false cap, dropping the third defect's post-call monomial and unsupported entry-angle assumptions. Complete typed receipt comparison rejects altered fields and bool/int substitutions. Normal and optimized commands use only CPython3.12 standard library. + +``` +python3.12 -B scripts/research_package.py --package research/native-error-channel-amplification +python3 -B scripts/check_research_commit.py --package research/native-error-channel-amplification --check-source-history +``` + +The official committed export can execute `verify.py` directly with `-I -W error -B`, and separately `-O`, without Git/network. `--emit NEW_PATH` writes a new deterministic receipt and refuses overwrite. Source pins bind the exact base and retained source bytes. Hosted CI is unverified at publication. + +Base canonical main `bee95ce88f9f19802f0613f92838895cd0e14a1f`, priority7, selected conditional κ0.00302015 unchanged. Entry overlap at06:05–06:06UTC October23 covered310openPRs,4096Discussion records and6690base notes with complete reported pagination/inventory. Related #4828/#4743, shared-port/cascade and later compensated-port work were distinguished. Coverage is advisory, not novelty proof; arbitrary diffs and unpublished work remain outside it. Canonical claim: https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19139368. + +Credit Nick Petalas #4828 for sharp endpoint conditioning and the explicit error-channel question; Dugongue #4743 for literal all-input schedules and conservative precision contract; Yiyang/Lyy-iiis #4710 for repaired phases; lee-phys #4688, Jacob Alan Sussman #4628, eumemic, Swapnil Jain and all notices retained in those packages. No source archive is modified or reissued. No independent human or formal proof-kernel acceptance is claimed. + +## Open next questions + +Can one concrete rounded Cj_f implementation meet these completed-call tolerances on each actual stored input with its internal range, data-grid, movement and time costs retained? Begin with one nonzero-rounding invocation and compare its actual radius/tolerance to the table. The sharp external contract supplies no internal Gaussian guarantee. Complete recursive substitution requires its own error-channel composition and is outside this package. Structured question: TASK.json. diff --git a/research/native-error-channel-amplification/RESULT.json b/research/native-error-channel-amplification/RESULT.json new file mode 100644 index 0000000000..8ba4e84a30 --- /dev/null +++ b/research/native-error-channel-amplification/RESULT.json @@ -0,0 +1,359 @@ +{ + "base_coherence_checks": 5, + "controls": 6, + "gaussian_implementation_internal_error_guarantee": "premise", + "impulse_columns": 144, + "new_kappa": false, + "perturbed_trajectories": 54, + "physical_execution": false, + "records": [ + { + "channel_norms": [ + [ + "6", + "0" + ], + [ + "0", + "1" + ], + [ + "0", + "3" + ], + [ + "1", + "0" + ] + ], + "f": 1, + "kind": 2, + "reverse": false, + "total": [ + "7", + "4" + ] + }, + { + "channel_norms": [ + [ + "3", + "0" + ], + [ + "0", + "1" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "f": 1, + "kind": 2, + "reverse": true, + "total": [ + "4", + "1" + ] + }, + { + "channel_norms": [ + [ + "0", + "5" + ], + [ + "2", + "0" + ], + [ + "6", + "0" + ], + [ + "0", + "1" + ], + [ + "1", + "0" + ] + ], + "f": 1, + "kind": 3, + "reverse": false, + "total": [ + "9", + "6" + ] + }, + { + "channel_norms": [ + [ + "3", + "0" + ], + [ + "2", + "0" + ], + [ + "0", + "1" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "f": 1, + "kind": 3, + "reverse": true, + "total": [ + "6", + "1" + ] + }, + { + "channel_norms": [ + [ + "12", + "0" + ], + [ + "2", + "0" + ], + [ + "6", + "0" + ], + [ + "1", + "0" + ] + ], + "f": 2, + "kind": 2, + "reverse": false, + "total": [ + "21", + "0" + ] + }, + { + "channel_norms": [ + [ + "3", + "0" + ], + [ + "2", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "f": 2, + "kind": 2, + "reverse": true, + "total": [ + "6", + "0" + ] + }, + { + "channel_norms": [ + [ + "18", + "0" + ], + [ + "4", + "0" + ], + [ + "12", + "0" + ], + [ + "2", + "0" + ], + [ + "1", + "0" + ] + ], + "f": 2, + "kind": 3, + "reverse": false, + "total": [ + "37", + "0" + ] + }, + { + "channel_norms": [ + [ + "3", + "0" + ], + [ + "4", + "0" + ], + [ + "2", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "f": 2, + "kind": 3, + "reverse": true, + "total": [ + "10", + "0" + ] + }, + { + "channel_norms": [ + [ + "24", + "0" + ], + [ + "0", + "2" + ], + [ + "0", + "6" + ], + [ + "1", + "0" + ] + ], + "f": 3, + "kind": 2, + "reverse": false, + "total": [ + "25", + "8" + ] + }, + { + "channel_norms": [ + [ + "3", + "0" + ], + [ + "0", + "2" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "f": 3, + "kind": 2, + "reverse": true, + "total": [ + "4", + "2" + ] + }, + { + "channel_norms": [ + [ + "0", + "34" + ], + [ + "8", + "0" + ], + [ + "24", + "0" + ], + [ + "0", + "2" + ], + [ + "1", + "0" + ] + ], + "f": 3, + "kind": 3, + "reverse": false, + "total": [ + "33", + "36" + ] + }, + { + "channel_norms": [ + [ + "3", + "0" + ], + [ + "8", + "0" + ], + [ + "0", + "2" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "f": 3, + "kind": 3, + "reverse": true, + "total": [ + "12", + "2" + ] + } + ] +} diff --git a/research/native-error-channel-amplification/SOURCES.json b/research/native-error-channel-amplification/SOURCES.json new file mode 100644 index 0000000000..e6231683d5 --- /dev/null +++ b/research/native-error-channel-amplification/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/complex-prefix-native-ports/FULL-INPUT-PORT.md", + "usage": "input", + "git_blob": "39a461f2fbf2e009423cd784f56de121d190d842", + "sha256": "52b8462e28f9e87925ccfea27872630e2b2da23f19fd3d2265c2654bc016088c" + }, + { + "path": "research/complex-prefix-native-ports/SECTOR-COMPLETION.md", + "usage": "input", + "git_blob": "d3fcedfa0ef8c569810cbfe3b001e509be1274aa", + "sha256": "2e72e19c4733213d1875f60cf87eddb733dde9266cf2581cb56393c3fabf1933" + }, + { + "path": "research/complex-prefix-native-ports/verify_full_input_port.py", + "usage": "input", + "git_blob": "d036eacfecfdf7aa3260d48a02f7b4c394973b82", + "sha256": "51a690ad73e60ce6f4e71231ab647059cc6da5381b0eb831f8fd3cac1f47174d" + }, + { + "path": "research/complex-prefix-native-ports/pr4710/verify_residual.py", + "usage": "input", + "git_blob": "9130ce2171e4af01338be27e7ffbf1feaf88da9e", + "sha256": "0d277854396e4ceda1e0f26916bd576b6decb474c0692b6671ebf2595283ddb9" + }, + { + "path": "research/complex-prefix-native-ports/NOTICE.md", + "usage": "input", + "git_blob": "6f2cac2711e1f6c4c5578b215ae07d700cd60f35", + "sha256": "04a7423af5af1f5c2e9e2772fb1e3bfeb6158abb1464bfe3ffad7f00b7946782" + }, + { + "path": "research/complex-port-sharp-conditioning/README.md", + "usage": "input", + "git_blob": "8ed9841de4e2e84a3a3e7f707200f4099f0849d5", + "sha256": "f2f1036299fd5d12aed0dd1dca009c97f0484bd1f1567fa02f750460a86edebc" + } + ] +} diff --git a/research/native-error-channel-amplification/TASK.json b/research/native-error-channel-amplification/TASK.json new file mode 100644 index 0000000000..9231103af0 --- /dev/null +++ b/research/native-error-channel-amplification/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Sharp source-ordered complex-coordinate error amplification for the literal forward and reverse full-input two/three-call native ports at every positive tensor width.", + "scope_change_reason": "PR4828 Open next question2 explicitly separates sharp Euclidean endpoint conditioning from the actual paid-call/initial-quantization defect channels in PR4743; the new proof retains each defect insertion and monomial phase.", + "bottleneck_link": "Completed-call accuracy requests determine an external native precision interface; multiplying complete endpoint condition numbers misses the chronological defect maps and can overfund their required tolerances.", + "budget_minutes": 60, + "stop_rule": "Stop at this source-bound linear error contract with phase/order controls; no changed paid word, physical Gaussian implementation or recursive supplier campaign.", + "outcome": "partial", + "evidence": "README.md gives the all-width proof and sharpness construction; RESULT.json binds12normal/reverse width1/2/3 cases,54actual perturbed schedules,144independent impulse columns and6controls.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance for exact source interpretation, mathematical proof, independent rational matrix/vector implementation, testing and separate source/proof review. No independent human or formal-kernel acceptance.", + "open_questions": [ + { + "question": "Can an actual rounded Gaussian implementation meet these completed-call tolerances on every actual stored input while retaining its own internal-prefix and movement costs?", + "why_it_matters": "The sharp external interface does not supply the Gaussian implementation or make its internal errors independently attainable; numerical width/time savings require that concrete binding.", + "first_step": "Choose one completed Cj_f implementation, bind the actual incoming radius and requested complex-coordinate tolerance from this channel table, then replay a nonzero rounding case with its internal range and data-grid guards.", + "blocked_by": "No physical Gaussian implementation, internal-cut error guarantee, fixed-tape routing or full recursive substitution is supplied here." + } + ] +} diff --git a/research/native-error-channel-amplification/VERIFY.json b/research/native-error-channel-amplification/VERIFY.json new file mode 100644 index 0000000000..b181a78a07 --- /dev/null +++ b/research/native-error-channel-amplification/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-prefix-native-ports/FULL-INPUT-PORT.md", + "research/complex-prefix-native-ports/SECTOR-COMPLETION.md", + "research/complex-prefix-native-ports/verify_full_input_port.py", + "research/complex-prefix-native-ports/pr4710/verify_residual.py", + "research/complex-prefix-native-ports/NOTICE.md", + "research/complex-port-sharp-conditioning/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact actual source bindings, base coherence/flat-row facts, source-ordered forward/reverse paid defects at widths1/2/3, independent impulse columns, guard margins and phase/order/receipt controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact actual source bindings, base coherence/flat-row facts, source-ordered forward/reverse paid defects at widths1/2/3, independent impulse columns, guard margins and phase/order/receipt controls." + } + ] +} diff --git a/research/native-error-channel-amplification/channels.py b/research/native-error-channel-amplification/channels.py new file mode 100644 index 0000000000..57817c6715 --- /dev/null +++ b/research/native-error-channel-amplification/channels.py @@ -0,0 +1,167 @@ +"""Exact source-ordered defect maps; independent Gaussian-rational arithmetic. + +JoyboyBrian, substantial OpenAI Codex assistance; Apache-2.0. +""" +from fractions import Fraction as Q + +ZERO=(Q(0),Q(0)); ONE=(Q(1),Q(0)); PHASES=(ONE,(Q(0),Q(1)),(-Q(1),Q(0)),(Q(0),-Q(1))) + + +def need(ok, why): + if not ok: raise ValueError(why) + + +def add(a,b): return a[0]+b[0],a[1]+b[1] +def mul(a,b): return a[0]*b[0]-a[1]*b[1],a[0]*b[1]+a[1]*b[0] +def scale(c,a): return c*a[0],c*a[1] +def conj(a): return a[0],-a[1] + + +def eye(n=8): return [{i:ONE} for i in range(n)] + + +def put(row,j,z): + z=add(row.get(j,ZERO),z) + if z==ZERO: row.pop(j,None) + else: row[j]=z + + +def plus(a,b,c=1): + out=[dict(row) for row in a] + for row,source in zip(out,b): + for j,z in source.items(): put(row,j,scale(c,z)) + return out + + +def product(a,b): + out=[{} for row in a] + for i,row in enumerate(a): + for k,x in row.items(): + for j,y in b[k].items(): put(out[i],j,mul(x,y)) + return out + + +def word(*matrices): + out=eye(len(matrices[0])) + for a in matrices: out=product(out,a) + return out + + +def adjoint(a): + out=[{} for row in a] + for i,row in enumerate(a): + for j,z in row.items(): out[j][i]=conj(z) + return out + + +def monomial(perm,phases=None): + phases=phases or [0]*len(perm) + need(sorted(perm)==list(range(len(perm))),'monomial bijection') + out=[{} for i in perm] + for j,i in enumerate(perm): out[i][j]=PHASES[phases[j]%4] + return out + + +def pauli(x,z): + return monomial([j^x for j in range(8)],[(x&z).bit_count()+2*(j&z).bit_count() for j in range(8)]) + + +def letters(): + C=[plus([{i:(Q(1,2),Q(1,2))} for i in range(8)], + [{i^(1<=0 and y>=0: return True + if x<=0 and y<=0: return x==y==0 + return x*x>=2*y*y if x>=0 else 2*y*y>=x*x + + +def Lpower(k): + return (Q(1<< (k//2)),Q(0)) if k%2==0 else (Q(0),Q(1<<(k//2))) + + +def pair_sum(*parts): return tuple(sum(z[i] for z in parts) for i in (0,1)) +def pair_scale(c,a): return c*a[0],c*a[1] + + +def maps(base,f,kind,reverse=False): + A,P,T,D,J,W,M,I=(base[k] for k in ('A','P','Q','D','J','W','M','I')) + def lifted(*terms): + out=[{} for i in range(8**f)] + for c,a in terms: out=plus(out,power(a,f),c) + return out + if reverse: + cols=[lifted((-1,P),(-2,T)),lifted((1,adjoint(A if kind==2 else D)))] + cols += ([lifted((1,I))] if kind==2 else + [lifted((1,word(adjoint(A),adjoint(W)))),lifted((1,I))]) + cols.append(None) + return cols + B=A if kind==2 else D + cols=[lifted((1,word(B,P,A)),(2,word(B,T,A))),lifted((1,B)), + lifted((1,word(B,P)),(2,word(B,T)))] + cols.append(lifted((1,I if kind==2 else word(J,W)))) + if kind==3: cols.append(lifted((1,M))) + return cols + + +def schedule(base,f,kind,reverse,x,y,defects): + lifted={k:power(v,f) for k,v in base.items()} + A,P,T,W,M,C2=(lifted[k] for k in ('A','P','Q','W','M','C2')) + dx,dy,*e=defects; x=vplus(x,dx); y=vplus(y,dy) + if not reverse: + t=vplus(apply(A,x),e[0]); z=vplus(y,apply(P,t)); z=vplus(z,apply(T,t),2) + out=vplus(apply(A,z),e[1]) + if kind==3: out=apply(M,vplus(apply(C2,apply(W,out)),e[2])) + return t,out + if kind==3: + out=vplus(apply(adjoint(C2),apply(adjoint(M),y)),e[0]) + out=vplus(apply(adjoint(A),apply(adjoint(W),out)),e[1]) + else: out=vplus(apply(adjoint(A),y),e[0]) + out=vplus(vplus(out,apply(P,x),-1),apply(T,x),-2) + return vplus(apply(adjoint(A),x),e[-1]),out diff --git a/research/native-error-channel-amplification/verify.py b/research/native-error-channel-amplification/verify.py new file mode 100644 index 0000000000..7c4b1c4659 --- /dev/null +++ b/research/native-error-channel-amplification/verify.py @@ -0,0 +1,122 @@ +"""Exact small-width execution and all-width channel certificates.""" +import argparse,ast,hashlib,json +from pathlib import Path +import sys +HERE=Path(__file__).resolve().parent; ROOT=HERE.parents[1] +sys.path.insert(0,str(HERE)) +from channels import * + + +def reject(call,text): + try: call() + except ValueError as exc: + need(text in str(exc),'wrong rejection '+str(exc)); return + raise ValueError('missing rejection '+text) + + +def main(): + source={} + for r in json.loads((HERE/'SOURCES.json').read_text())['files']: + if r['usage']=='input': + content=(ROOT/r['path']).read_bytes() + need(hashlib.sha256(content).hexdigest()==r['sha256'],'source bytes '+r['path']) + source[r['path']]=content + tree=ast.parse(source['research/complex-prefix-native-ports/verify_full_input_port.py']) + mainfn=next(n for n in tree.body if isinstance(n,ast.FunctionDef) and n.name=='main') + assignments={ast.unparse(n.targets[0]):ast.unparse(n.value) for n in mainfn.body if isinstance(n,ast.Assign)} + expected={'U':'v.monomial([0, 5, 2, 7, 4, 1, 6, 3])', + 'V':'v.monomial([0, 2, 1, 3, 4, 6, 5, 7])','S':'v.s_letter(7)', + '(P, Q)':'(v.word(S, U, S), v.word(S, V, S))', + 'W':'v.pauli(0, 5)','J':'v.word(v.pauli(0, 2), V, C[2])', + 'A':'C[0]','D':'v.word(J, W, C[0])'} + need(all(assignments.get(k)==v for k,v in expected.items()),'actual phase-letter/source bindings') + b=letters() + for k,a in b.items(): + need(product(a,adjoint(a))==eye(),'unitary actual letter '+k) + # Flat row norms and row-zero coherent overlaps are finite base facts, + # which tensor functoriality then extends to every positive width. + checks=[('F',word(b['A'],b['P'],b['A']),word(b['A'],b['Q'],b['A']),2), + ('AL',word(b['A'],b['P']),word(b['A'],b['Q']),1), + ('B',word(b['D'],b['P'],b['A']),word(b['D'],b['Q'],b['A']),None), + ('DL',word(b['D'],b['P']),word(b['D'],b['Q']),2), + ('L',b['P'],b['Q'],0)] + for name,x,y,k in checks: + for row in (x[0],): + for j,z in row.items(): + if j in y[0]: + ratio=mul(z,conj(y[0][j])) + need(ratio[1]==0 and ratio[0]>0,'coherent row-zero overlap '+name) + if k is not None: + need(all(l1(row)==Lpower(k) for row in x+y),'flat branch row norms '+name) + else: + need(all(l1(row)==Lpower(1) for row in x) + and all(l1(row)==Lpower(3) for row in y),'different-rank B branch norms') + records=[]; trajectories=0; basis_cases=0 + for f in (1,2,3): + n=8**f; zero=[ZERO]*n + for kind in (2,3): + for reverse in (False,True): + channels=maps(b,f,kind,reverse) + if reverse: + norms=[(Q(3),Q(0)),Lpower(f if kind==2 else 2*f)] + norms+=([(Q(1),Q(0))] if kind==2 else [Lpower(f),(Q(1),Q(0))]) + norms.append((Q(0),Q(0))) + else: + norms=[pair_scale(3,Lpower(2*f)) if kind==2 else pair_sum(pair_scale(2,Lpower(3*f)),Lpower(f)), + Lpower(f if kind==2 else 2*f),pair_scale(3,Lpower(f if kind==2 else 2*f)), + (Q(1),Q(0)) if kind==2 else Lpower(f)] + if kind==3: norms.append((Q(1),Q(0))) + for matrix,wanted in zip(channels,norms): + if matrix is None: continue + need(l1(matrix[0])==wanted and all(leq(l1(r),wanted) for r in matrix),'sharp channel norm') + summed=pair_sum(*norms) + expected_sum=(pair_sum(Lpower(f),(Q(4),Q(0))) if kind==2 else + pair_sum(Lpower(2*f),Lpower(f),(Q(4),Q(0)))) if reverse else ( + pair_sum(pair_scale(3,Lpower(2*f)),pair_scale(4,Lpower(f)),(Q(1),Q(0))) if kind==2 else + pair_sum(pair_scale(2,Lpower(3*f)),pair_scale(4,Lpower(2*f)),pair_scale(2,Lpower(f)),(Q(1),Q(0)))) + need(summed==expected_sum,'source-ordered total sharp amplification') + x=[(Q((3*i+1)%7-3,8),Q((5*i+2)%9-4,8)) for i in range(n)] + y=[(Q((-1)**i,4),Q(i%3,8)) for i in range(n)] + unperturbed=schedule(b,f,kind,reverse,x,y,[zero]*(kind+2)) + for site in range(kind+2): + delta=[(Q((i+site)%5-2,16),Q((2*i+site)%7-3,16)) for i in range(n)] + ds=[zero]*(kind+2);ds[site]=delta + actual=schedule(b,f,kind,reverse,x,y,ds) + lower=zero if channels[site] is None else apply(channels[site],delta) + upper=(apply(power(adjoint(b['A']) if reverse else b['A'],f),delta) if site==0 else + delta if site==(kind+1 if reverse else 2) else zero) + need(actual==(vplus(unperturbed[0],upper),vplus(unperturbed[1],lower)),'actual chronological defect propagation') + trajectories+=1 + if f==1: + for site,matrix in enumerate(channels): + for j in range(n): + ds=[zero]*(kind+2); ds[site]=[ONE if i==j else ZERO for i in range(n)] + got=schedule(b,f,kind,reverse,zero,zero,ds)[1] + want=zero if matrix is None else [r.get(j,ZERO) for r in matrix] + need(got==want,'independent impulse columns');basis_cases+=1 + records.append(dict(f=f,kind=kind,reverse=reverse,total=[str(q) for q in summed], + channel_norms=[[str(q) for q in z] for z in norms])) + # Rational all-width gate: sqrt(2)<3/2, f>=1. + need(Q(3,2)**2>2 and Q(51,8)<8 and Q(15,4)<4,'uniform dyadic guard margins') + reject(lambda: power(b['A'],0),'bounded executable width') + reject(lambda: l1({0:(Q(1),Q(2))}),'eighth-root') + wrong=dict(b,Q=b['P']) + need(maps(wrong,1,3)[0]!=maps(b,1,3)[0],'changed phase/monomial control') + actual=maps(b,1,3)[3] + need(actual!=power(word(b['W'],b['J']),1),'reversed second-defect propagation control') + need(maps(b,1,3)[4]!=eye(),'third defect retains its post-call monomial') + need(not leq((Q(7),Q(0)),(Q(6),Q(0))),'false cap control') + result=dict(records=records,perturbed_trajectories=trajectories,impulse_columns=basis_cases, + base_coherence_checks=len(checks),controls=6,new_kappa=False, + gaussian_implementation_internal_error_guarantee='premise',physical_execution=False) + encoded=json.dumps(result,sort_keys=True,separators=(',',':')) + parser=argparse.ArgumentParser();parser.add_argument('--emit',type=Path);args=parser.parse_args() + if args.emit: + with args.emit.open('x') as out:json.dump(result,out,indent=2,sort_keys=True);out.write('\n') + else:need(encoded==json.dumps(json.loads((HERE/'RESULT.json').read_text()),sort_keys=True,separators=(',',':')),'complete typed receipt') + print(json.dumps(dict(cases=len(records),trajectories=trajectories,impulse_columns=basis_cases, + result_sha256=hashlib.sha256(encoded.encode()).hexdigest()),sort_keys=True)) + print('PASS_NATIVE_ERROR_CHANNEL_AMPLIFICATION all_width_source_order no_new_kappa') + + +if __name__=='__main__':main()