From 8721aa7738db8094a14cb417c5d4ed614b1a2f48 Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 22:08:20 +1100 Subject: [PATCH] Bound sparse feedback volume by conditioning and the native entropy jump --- .../selected-sparse-feedback-volume/PROOF.md | 229 ++++++++++++++++++ .../selected-sparse-feedback-volume/README.md | 97 ++++++++ .../RESULT.json | 33 +++ .../SOURCES.json | 18 ++ .../selected-sparse-feedback-volume/TASK.json | 78 ++++++ .../VERIFY.json | 28 +++ .../selected-sparse-feedback-volume/verify.py | 120 +++++++++ 7 files changed, 603 insertions(+) create mode 100644 research/selected-sparse-feedback-volume/PROOF.md create mode 100644 research/selected-sparse-feedback-volume/README.md create mode 100644 research/selected-sparse-feedback-volume/RESULT.json create mode 100644 research/selected-sparse-feedback-volume/SOURCES.json create mode 100644 research/selected-sparse-feedback-volume/TASK.json create mode 100644 research/selected-sparse-feedback-volume/VERIFY.json create mode 100644 research/selected-sparse-feedback-volume/verify.py diff --git a/research/selected-sparse-feedback-volume/PROOF.md b/research/selected-sparse-feedback-volume/PROOF.md new file mode 100644 index 0000000000..0afdb973ca --- /dev/null +++ b/research/selected-sparse-feedback-volume/PROOF.md @@ -0,0 +1,229 @@ +# Sparse feedback volume, conditioning, and the native-call cut + +All logarithms are base2. Matrices act on complex column vectors. `M^{-*}` +means `(M^{-1})*`, with `*` the conjugate transpose. This is a linear-circuit +result, not an unrestricted arithmetic or native-runtime lower bound. + +## 1. Boundary, operation model, and claim + +Let A,B be V-by-V unitary matrices, C=BA, and suppose every row of B has +exactly 2^f nonzero entries, all of squared magnitude2^-f, for integer f>=1. +The required primary boundary is + + F = [[C, lambda B], [0,I]], lambda=1/2. (1) + +Thus `(x,y)` maps to `(Cx+By/2,y)`. The same proof works for any real +lambda>0. PR4009's exact selected195/521 tensor boundary supplies these +hypotheses: B_f is a tensor product of involutory-Pauli half kernels and C_f +is unitary. Its prior source/native identification is credited, not newly +claimed here. The present theorem changes full-array passes to actual scalar +coordinate-update volume. + +The machine may have any finite number of coordinates, including arbitrary +dirty auxiliaries that must return unchanged and clean zero auxiliaries that +must return zero on every legal input. It is a fixed sequence of invertible +linear operations. Initially every machine coordinate is a formal independent +variable for defining its square matrix M, although legal clean inputs are +specialized to zero. No reset, erasure, nonlinear encoding or free input-dependent +preparation is allowed. + +An arithmetic primitive is a coordinate shear `z_t += c z_s`, t!=s, +with any nonzero complex coefficient c. Its cost is one updated coordinate. +A masked shear on m disjoint source/target pairs is expanded into m such +primitives and charged m; variable block sizes are allowed. We separately +permit arbitrary invertible monomial maps. They are granted zero cost in the +lower bound; their actual routing/scaling cost remains payable in any upper +invoice. Preparation and recovery arithmetic are part of the program. +There is exactly one distinguished invertible native call, on its declared +operand, with no other native calls. Application to4009 uses its normalized +rank2f child on one V-sized payload, never a concatenated2V operand. + +Let K>=1 bound the spectral condition number of EVERY full machine prefix, +including the intermediate primitive cuts of a masked operation. The bound is +on the full formal square machine, not just its restriction to legal inputs. +No separate coefficient bound is assumed; large coefficients or ill-conditioned +preparation must be reflected in K. A coefficient bound alone is not a K bound. + +There is an explicit potential Phi and a native jump + + Delta_Q = Phi(M_after_native) - Phi(M_before_native) + +such that, for total coordinate-ADD volume S, + + 8 K S + Re(Delta_Q) >= lambda f V = fV/2. (2) + +More precisely, if K_t is the maximum of the condition numbers immediately +before and after arithmetic primitive t, then + + 8 sum_t K_t + Re(Delta_Q) >= fV/2. (3) + +For a native call performed on the target payload before ANY arithmetic, +with only payload-preserving monomial maps before it, Delta_Q=0. Consequently + + S >= fV/(16K). (4) + +After that call, arbitrary sparse feedback, mixtures, cross-coordinate +monomial maps and any number of restored auxiliaries remain allowed. Neither +(2) nor(4) claims an fV bound for unrestricted conditioning or unrestricted +native interleaving. The native jump is not silently assigned zero in(2). + +## 2. A preconditioner that detects the triangular correction + +Embed J in the full machine with sole nonzero block + + J_xy = C^{-1} B = A^{-1}. (5) + +All auxiliary blocks are zero. Therefore ||J||_2=1. This matrix is a fixed +ANALYTICAL preconditioner; the algorithm is not given an implementation of J +or allowed to apply it for free. Define + + N = M^{-*} J, + p_ij = M_ij conjugate(N_ij), + h(z) = -z log2|z| (z!=0), h(0)=0, + Phi(M) = sum_ij h(p_ij). (6) + +Phi can be complex. We bound absolute changes and take real parts only in the +final inequality. This avoids assuming quasi-probabilities are nonnegative. +At M=I, each diagonal entry of J is zero, so every p_ij is zero and Phi(I)=0. + +Ignoring auxiliaries first, direct multiplication gives + + F^{-*} J = [[0,B],[0,-lambda I]]. (7) + +The only nonzero p entries are lambda|B_ij|^2 in the xy block and -lambda +on the V diagonal yy entries. Each B row contains2^f entries of weight2^-f. +Thus the xy contribution is lambda V(f-log2 lambda), the yy contribution +is lambda V log2 lambda, and + + Phi(F)=lambda fV. (8) + +Restored dirty auxiliaries add an identity block and zero p entries. +Clean auxiliaries need not have a prescribed nonzero-input behavior. Group +independent primary/dirty variables as w and clean variables as z. Correctness +and clean restoration on z=0 force the final full matrix to be + + M_final = [[T,R],[0,D]], T=F direct-sum I_dirty, + +where D is invertible and R is unrestricted. Embed J as diag(J_w,0). Then + + M_final^{-*}J = [[T^{-*}J_w,0],[-D^{-*}R* T^{-*}J_w,0]]. + +In the original-w columns, bottom rows of M_final vanish; in clean-input +columns, N vanishes. Every auxiliary-associated p therefore vanishes, and +(8) still holds. This argument uses restoration on every independent legal w; +it does not assume correctness when clean inputs are nonzero. + +Ordinary, unpreconditioned quasi-entropy misses the new correction: +for F, its off-diagonal block pairs with zeros of F^{-*}, leaving exactly +the same potential as diag(C,I). Its determinant is also unchanged. This is +why4009's pass lower bound or an ordinary Fourier entropy bound cannot simply +be read as the present volume theorem. + +## 3. Dimension-free cost of a single coordinate update + +For any complex p,q, let L=|p|+|q|. If L=0 the following is immediate. +Otherwise normalize by L. Homogeneity cancels the log L term in the defect. +Writing a=|p|/L and b=|q|/L, a+b=1, gives + + |h(p)+h(q)-h(p+q)| + <= L [ -a log2 a - b log2 b + + r log2(1/r) ] < 2L, (9) + +where r=|p+q|/L in[0,1], and continuous zero conventions apply. We used +binary entropy<=1 and r log2(1/r)<=1/(e ln2)<1. The non-strict bound<=2L +will suffice. This calculation also covers exact cancellation p+q=0. + +A shear G=I+c e_t e_s^T changes row t of M and row s of N, since +`N' = G^{-*}N`. For each column j, the pair satisfies + + p'_tj + p'_sj = p_tj + p_sj. (10) + +Indeed the added c M_sj conjugate(N_tj) cancels the corresponding inverse-dual +term. Other p entries are unchanged. Applying(9) to the old and new pairs +around their common sum yields + + |Delta Phi| <= 2 sum_j (|p_tj|+|p_sj|+|p'_tj|+|p'_sj|). + +For ANY row i at a prefix M, Cauchy-Schwarz and spectral norm bounds give + + sum_j |M_ij| |N_ij| + <= ||row_i M||_2 ||row_i N||_2 + <= ||M||_2 ||M^{-1}||_2 ||J||_2 + = cond_2(M). (11) + +There are two rows at each of two endpoints, so + + |Delta Phi| <= 8 K_t. (12) + +The constant8 is a convenient rigorous upper bound, not claimed sharp. +There is no dimension factor, coefficient bound, entrywise positivity or +bounded fanout premise hidden in(12). + +For an invertible monomial row map, the corresponding rows of M and N +are permuted together and their nonzero scale factors cancel in p. +Hence Phi is exactly unchanged, even for nonunit scales. Treating such maps +as free only makes the necessary condition more generous. A physically +implemented permutation is not declared costless by this theorem. + +## 4. The native cut and what it does not settle + +Telescope from I to M_final. Monomial jumps vanish, the sole native jump is +Delta_Q, and every arithmetic jump is at most8K_t in real part. Equations +(8),(12) prove(2),(3). + +If before the native call there are only payload-preserving monomial maps, +M is block diagonal on target, donor and auxiliary payloads. The product +M^{-*}J remains supported in the target-row/donor-column block. This block +of M is zero. Applying the native call on the TARGET payload preserves that +support disjointness, so both potentials are zero. This proves Delta_Q=0 +and(4). Arbitrary monomial permutations across the target/donor split before +the call are NOT included in this zero-jump argument. + +For a general interleaved call, Delta_Q must be evaluated or bounded from +its actual input matrix. If S=o(fV) and K=O(1), (2) requires + + Re(Delta_Q) >= fV/2-o(fV). + +Thus a sparse interleaved proposal must arrange for its one native call to +supply almost all of this specifically selected coupling potential. This is +a necessary condition, not a construction or a bound on achievable Delta_Q. +The theorem leaves that route open. Likewise, (4) permits smaller volume +if K grows. It quantifies the price in conditioning; it does not itself +translate K into a bit-precision or numerical-stability invoice. + +## 5. Relation to the selected budget + +For the pinned selected exponent00 fixed and +`delta=2-2^(1-alpha)>0`. For the child-first class with K bounded independently +of f, (4) is Omega(fV); crediting the original V-coordinate ADD does not +change that asymptotic conclusion. Hence such a uniformly well-conditioned +sparse adapter cannot fit that rank-only saving for all f. + +More generally, a necessary child-first improvement condition is + + f/(16K) - 1 < A0 delta f^(1-alpha). (13) + +In particular, asymptotic sub-fV designs must give up a uniform K bound or +move to the nonzero-native-jump case, or change another stated model premise. +No finite threshold or new kappa follows without actual constants and the +complete routing/precision/hosting invoice. The general sparse-coordinate +family is not closed by this theorem. + +## 6. Provenance and verification scope + +The potential method is an adaptation of Nir Ailon's well-conditioned +Fourier lower bounds and Ailon--Gal Yehuda's preconditioned quasi-entropy, +not a newly invented lower-bound technique. Primary sources: + +- Ailon, arXiv:1403.1307, https://arxiv.org/abs/1403.1307. +- Ailon and Yehuda, arXiv:1604.02557v4, Section1.1 and Lemma1.1, + https://arxiv.org/abs/1604.02557. + +Here the new scoped contribution is the nilpotent block preconditioner(5), +its exact coupling value lambda fV, the explicit native-cut debit, and the +complex coordinate-shear/returned-clean-auxiliary argument. The proof above +is self-contained; finite checks do not prove the quantified entropy theorem. +PR4009 at89a358aac11d11e0539eb95c27600e7677be7ce4 supplies the selected +boundary. PR3989 and Gonzalo Mier's3975 supply its prior physical-binding +lineage. All remain distinct from supplier admission. diff --git a/research/selected-sparse-feedback-volume/README.md b/research/selected-sparse-feedback-volume/README.md new file mode 100644 index 0000000000..725a61b3fc --- /dev/null +++ b/research/selected-sparse-feedback-volume/README.md @@ -0,0 +1,97 @@ +# Sparse feedback needs arithmetic volume, conditioning, or native-cut entropy + +For the selected coupled boundary `(C_f x+B_f y/2,y)` with restored auxiliaries, +this package proves a genuine sparse-coordinate necessary condition: + + 8 K S + Re(Delta_Q) >= f V / 2. + +Here S counts actual updated coordinates in all scalar ADDs, K bounds every +full-machine prefix condition number, and Delta_Q is an explicitly defined +preconditioned-entropy jump across the sole native call. Variable-sized masks, +arbitrary feedback and mixtures, arbitrary dirty restored auxiliaries and +clean returned auxiliaries are included. Routing/scaling maps are granted free +in this lower bound; their physical invoice remains additional. + +If the rank2f target child runs before arithmetic, with only payload-preserving +monomials before it, its jump is zero and **S >= fV/(16K)**. A constant-K +child-first adapter therefore costs Omega(fV), including sparse implementations. +The general interleaved or ill-conditioned sparse family remains open. No +coefficient-only premise, unconditional arithmetic lower bound, new selected +profile, supplier admission or kappa improvement is claimed. + +The distinction matters: PR4009 proved a count of full-array passes. Multiplying +that count by V is invalid after changing to sparse masks. The present proof +uses a different potential and charges each scalar coordinate update directly. +Ordinary determinant and ordinary quasi-entropy cannot detect the triangular +correction; the block preconditioner here gives exactly fV/2. The proof also +keeps the child's contribution instead of treating a large native operator +as an ordinary scalar gate. + +[PROOF.md](PROOF.md) contains the self-contained all-dimension argument. This +adapts Ailon's conditioning/quasi-entropy method and Ailon--Yehuda's +preconditioned potential; it does not claim a new general lower-bound method. +The novel scoped part is the chosen coupling preconditioner, its exact boundary +value, the explicit native jump, and the complex coordinate-shear/restored-clean +auxiliary extension. Two same-team AI proof reviews found no issue; this is +not human peer review or formal-kernel acceptance. + +## Evidence and reproduction + +Python3.12 standard library only: + +```sh +python3 -B scripts/research_package.py --package research/selected-sparse-feedback-volume +``` + +The registered normal and optimized runs check exact Gaussian-rational +endpoint fixtures at f=1,2, all32 complex two-row column invariants in a +four-shear fixture, nonunit monomial invariance, and a clean-auxiliary fixture +with unspecified off-domain input behavior. An explicit interleaved native +call has jump1+i, so the zero-jump corollary cannot be silently generalized. +Five controls reject a wrong preconditioner orientation, omitted native jump, +clean-output leakage omitted inverse-dual conjugation and noncommuting BA/AB substitution. Exact logarithms +in these fixtures use only power-of-two squared norms. The quantified entropy +inequality is a written proof, not inferred from these examples. + +The verifier is standalone and requires no network or pending-PR checkout. +Its matrix fixtures check the theorem's algebra, not a new native lowering. +PR4009 at `89a358aac11d11e0539eb95c27600e7677be7ce4` supplies the prior literal +195/521 binding and all-f Pauli identification. The application here explicitly +inherits that identification. The abstract theorem holds for any unitary A,B +with the stated B-row flatness. No frozen predecessor is copied or changed. + +## Open next questions + +1. Can a genuinely interleaved candidate make Re(Delta_Q) large enough while + keeping its paid preparation volume and conditioning small? Compute the + proposed native-cut matrices and this potential first; a bound on that + jump is the missing step for a broader obstruction. +2. Can an ill-conditioned sparse proposal improve the complete cost after + precision and restoration are charged? Supply a bound on the full prefix + condition numbers and an actual error/bit invoice. The theorem does not + equate a growing K with a specific number of extra precision bits. +3. What cost model admits variable-size native calls or nonlinear preparation? + Such a change needs its own operator and paid boundary before extending + this one-child linear model. + +## Sources, overlap and credit + +Scientific base `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority6. Parent +entry intake at10:46UTC covered733 open PR bodies including drafts and the +latest active1166/1901 coordination; broader discussion coverage was partial. +Live PR4023 (fixed-support unary query bounds) and4027 (H6 U9 compensation) +have different operators and alphabets. Adjacent PR3954's paired-owner P104 +normalization discussion uses the earlier full-array bound, not this sparse +volume theorem. This review is scoped overlap evidence, not proof of novelty. +The sibling sparse coordinate-pair construction is a complementary upper bound; +its proof and complete primitive costs remain separately attributable. + +Method credit: Nir Ailon, [arXiv:1403.1307](https://arxiv.org/abs/1403.1307), +and Nir Ailon and Gal Yehuda, [arXiv:1604.02557v4](https://arxiv.org/abs/1604.02557), +Section1.1 and Lemma1.1. Boundary credit: [PR4009](https://github.com/CrocSwap/integer-mult-bounds/pull/4009), +[PR3989](https://github.com/CrocSwap/integer-mult-bounds/pull/3989), Gonzalo Mier's +[PR3975](https://github.com/CrocSwap/integer-mult-bounds/pull/3975), and their +retained selected/native lineage, including Cinna Davis and the selected1094 +sources. New work Apache-2.0. Prepared by Clear1nsight with substantial OpenAI +Codex assistance in research, proof, exact implementation, independent agent +review and packaging. diff --git a/research/selected-sparse-feedback-volume/RESULT.json b/research/selected-sparse-feedback-volume/RESULT.json new file mode 100644 index 0000000000..b7f3a511ce --- /dev/null +++ b/research/selected-sparse-feedback-volume/RESULT.json @@ -0,0 +1,33 @@ +{ + "endpoint_fixtures": [ + { + "f": 1, + "V": 4, + "phi": "2" + }, + { + "f": 2, + "V": 16, + "phi": "16" + } + ], + "complex_pair_column_checks": 32, + "noncommuting_endpoint": true, + "interleaved_native_jump": [ + "1", + "1" + ], + "clean_auxiliary_coordinates": 2, + "monomial_controls": 2, + "negative_controls": { + "wrong_preconditioner_orientation": true, + "interleaved_jump_omitted": true, + "clean_output_leak": true, + "missing_inverse_dual_conjugation": true, + "wrong_noncommuting_order": true + }, + "theorem_evidence": "Written all-dimension proof; finite controls are not an exhaustive proof.", + "uniform_K_bound": "S>=fV/(16K) only for zero native jump", + "general_bound": "8K*S+Re(Delta_Q)>=fV/2", + "new_kappa": false +} diff --git a/research/selected-sparse-feedback-volume/SOURCES.json b/research/selected-sparse-feedback-volume/SOURCES.json new file mode 100644 index 0000000000..0839f4876a --- /dev/null +++ b/research/selected-sparse-feedback-volume/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/selected-sparse-feedback-volume/TASK.json b/research/selected-sparse-feedback-volume/TASK.json new file mode 100644 index 0000000000..6e9bc8a18f --- /dev/null +++ b/research/selected-sparse-feedback-volume/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Sparse-coordinate arithmetic-volume, conditioning and explicit native-jump tradeoff for the selected coupled Pauli boundary.", + "scope_change_reason": "Change full-array passes to masks/variable block sizes and charge total updated coordinates; retain native entropy contribution explicitly.", + "bottleneck_link": "Determines when sparse child-first fusion can or cannot fit the ideal recursive saving; general native interleaving remains open.", + "budget_minutes": 60, + "stop_rule": "Complete the scoped proof and meaningful finite controls; no broad sparse impossibility or supplier replay without an explicit bound on conditioning and native jump.", + "outcome": "completed", + "evidence": "PROOF.md, exact Gaussian-rational verifier and RESULT.json; independent same-team proof review.", + "author": "Clear1nsight with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance with research design, algebra/proof drafting, independent agent audit, exact verifier implementation, source/overlap investigation and packaging. Clear1nsight directs the work.", + "open_questions": [ + { + "question": "Can an interleaved native call supply the required coupling potential at low preparation cost?", + "why_it_matters": "The explicit native jump is the remaining term in the total-volume inequality.", + "first_step": "Compute the actual full input matrix and preconditioned jump of one proposed call.", + "blocked_by": "No upper bound on that jump is proved for arbitrary interleaving." + }, + { + "question": "Can growing conditioning fit a complete bit/precision invoice?", + "why_it_matters": "The child-first volume lower bound is divided by the actual full prefix condition number.", + "first_step": "Bind one proposal to full-prefix conditioning and completed-output precision requirements.", + "blocked_by": "Condition number is not automatically a paid bit cost." + } + ] +} diff --git a/research/selected-sparse-feedback-volume/VERIFY.json b/research/selected-sparse-feedback-volume/VERIFY.json new file mode 100644 index 0000000000..5ad370d0d8 --- /dev/null +++ b/research/selected-sparse-feedback-volume/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact endpoint/native-cut/complex inverse-dual/clean-auxiliary fixtures and five substantive controls; written theorem is not replaced by finite tests." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same controls remain active with assertions optimized out." + } + ] +} diff --git a/research/selected-sparse-feedback-volume/verify.py b/research/selected-sparse-feedback-volume/verify.py new file mode 100644 index 0000000000..6e1a534d57 --- /dev/null +++ b/research/selected-sparse-feedback-volume/verify.py @@ -0,0 +1,120 @@ +#!/usr/bin/env python3 +"""Exact finite controls for the written sparse-volume theorem; Apache-2.0.""" +from fractions import Fraction as F +from pathlib import Path +import json +Z=(F(0),F(0));O=(F(1),F(0));I=(F(0),F(1));a=(F(1,2),F(1,2));b=(F(1,2),F(-1,2)) +def require(p,m): + if not p: raise RuntimeError(m) +def add(x,y):return (x[0]+y[0],x[1]+y[1]) +def neg(x):return (-x[0],-x[1]) +def sub(x,y):return add(x,neg(y)) +def cj(x):return (x[0],-x[1]) +def mul(x,y):return (x[0]*y[0]-x[1]*y[1],x[0]*y[1]+x[1]*y[0]) +def scale(x,t):return (x[0]*t,x[1]*t) +def eye(n):return [[O if i==j else Z for j in range(n)] for i in range(n)] +def zero(m,n=None):return [[Z for _ in range(n or m)] for _ in range(m)] +def adj(X):return [[cj(v) for v in r] for r in zip(*X)] +def mm(X,Y): + out=zero(len(X),len(Y[0])) + for i,row in enumerate(X): + for k,u in enumerate(row): + if u==Z:continue + for j,v in enumerate(Y[k]): + if v!=Z:out[i][j]=add(out[i][j],mul(u,v)) + return out +def kron(X,Y):return [[mul(x,y) for x in xr for y in yr] for xr in X for yr in Y] +def plus(X,Y):return [[add(x,y) for x,y in zip(rx,ry)] for rx,ry in zip(X,Y)] +def sc(X,q):return [[scale(v,q) for v in r] for r in X] +def block(A,B,C,D):return [x+y for x,y in zip(A,B)]+[x+y for x,y in zip(C,D)] +def prod(M,N):return [[mul(x,cj(y)) for x,y in zip(rx,ry)] for rx,ry in zip(M,N)] +def pow2log(q): + require(q>0,'positive norm squared') + n,d=q.numerator,q.denominator + require(n&(n-1)==0 and d&(d-1)==0,'fixture norm must be exact power of two') + return n.bit_length()-d.bit_length() +def phi(M,N): + out=Z + for row in prod(M,N): + for z in row: + if z!=Z:out=add(out,scale(z,-F(pow2log(z[0]*z[0]+z[1]*z[1]),2))) + return out +def matrices(f): + K=[[a,b],[b,a]]; A=B=[[O]] + for _ in range(f):A=kron(A,kron(K,eye(2)));B=kron(B,kron(eye(2),K)) + return A,B,mm(B,A) +def fixture(f,wrong=False): + A,B,C=matrices(f);v=len(A);z=zero(v);J=block(z,A if wrong else adj(A),z,z) + M=block(C,sc(B,F(1,2)),z,eye(v)) + Minv=block(adj(C),sc(mm(adj(C),B),F(-1,2)),z,eye(v)) + N=mm(adj(Minv),J) + return v,A,B,C,J,M,N + +def evaluate(): + ends=[] + for f in (1,2): + v,A,B,C,J,M,N=fixture(f) + require(mm(adj(M),N)==J,'exact inverse-dual endpoint') + require(phi(eye(2*v),J)==Z,'initial zero potential') + require(phi(M,N)==(F(f*v,2),F(0)),'coupling entropy endpoint') + require(all(sum(x!=Z for x in row)==2**f for row in B),'row support') + require(all(x==Z or x[0]*x[0]+x[1]*x[1]==F(1,2**f) for row in B for x in row),'row flatness') + # Ordinary potential ignores the off-diagonal coupling. + ordinary=block(C,zero(v),sc(mm(adj(B),C),F(-1,2)),eye(v)) + diag=block(C,zero(v),zero(v),eye(v)) + require(phi(M,ordinary)==phi(diag,diag),'ordinary potential blindness') + ends.append({'f':f,'V':v,'phi':str(F(f*v,2))}) + v,A,B,C,J,Final,Nfinal=fixture(1);n=2*v + # Genuine complex shears: independently update M and its inverse dual N. + M=eye(n);N=[r[:] for r in J];pair_checks=0 + for t,s,c in [(0,4,(F(1,2),F(0))),(1,0,(F(0),F(1,2))),(5,1,(F(2),F(0))),(7,2,(F(-3,2),F(1,2)))]: + old=prod(M,N);M[t]=[add(x,mul(c,y)) for x,y in zip(M[t],M[s])] + N[s]=[sub(x,mul(cj(c),y)) for x,y in zip(N[s],N[t])];new=prod(M,N) + require(all(add(old[t][j],old[s][j])==add(new[t][j],new[s][j]) for j in range(n)),'column-pair invariant') + require(mm(adj(M),N)==J,'full inverse-dual invariant');pair_checks+=n + # Nonunit complex row scale and row permutation preserve every product. + before=prod(M,N);c=(F(2),F(2));ci=(F(1,4),F(1,4)) # 1/conj(c) + M[0]=[mul(c,x) for x in M[0]];N[0]=[mul(ci,x) for x in N[0]] + require(prod(M,N)==before,'nonunit monomial invariant') + M[0],M[6]=M[6],M[0];N[0],N[6]=N[6],N[0];after=prod(M,N);before[0],before[6]=before[6],before[0] + require(after==before,'row permutation invariant') + # The general native jump really can be nonzero after cheap coupling. + pre=block(eye(v),sc(eye(v),F(1,2)),zero(v),eye(v)) + preinv=block(eye(v),sc(eye(v),F(-1,2)),zero(v),eye(v));preN=mm(adj(preinv),J) + Q=block(C,zero(v),zero(v),eye(v));post=mm(Q,pre);postN=mm(Q,preN) + delta=sub(phi(post,postN),phi(pre,preN));require(delta==(F(1),F(1)),'interleaved native jump retained') + require(phi(Q,mm(Q,J))==Z,'target-first native jump zero') + # Unspecified off-domain clean behavior: M=[[Final,R],[0,D]], D nonunit. + d=2;R=[[(F(i%3-1,2),F((i+j)%2,2)) for j in range(d)] for i in range(n)] + D=[[ (F(2),F(0)),O],[Z,(F(1,2),F(0))]];Di=[[(F(1,2),F(0)),neg(O)],[Z,(F(2),F(0))]] + full=block(Final,R,zero(d,n),D);JJ=block(J,zero(n,d),zero(d,n),zero(d)) + NN=block(Nfinal,zero(n,d),sc(mm(mm(adj(Di),adj(R)),Nfinal),F(-1)),zero(d)) + require(mm(adj(full),NN)==JJ,'clean off-domain inverse-dual identity') + require(phi(full,NN)==(F(v,2),F(0)),'clean-returned endpoint potential') + # Controls reject the exact failure modes at issue, not the theorem by sampling. + controls={} + _,_,_,_,_,badM,badN=fixture(1,wrong=True) + controls['wrong_preconditioner_orientation']=phi(badM,badN)!=(F(v,2),F(0)) + controls['interleaved_jump_omitted']=delta!=Z + badfull=[r[:] for r in full];badfull[-1][4]=O + clean_restored=lambda X:all(x==Z for row in X[n:] for x in row[:n]) + require(clean_restored(full),'clean restoration on every legal input') + controls['clean_output_leak']=not clean_restored(badfull) + # Omitting conjugation in inverse-dual update is invalid for imaginary shear. + MM=eye(n);NN0=[r[:] for r in J];cc=(F(0),F(1,2));t,s=0,4 + MM[t]=[add(x,mul(cc,y)) for x,y in zip(MM[t],MM[s])] + NN0[s]=[sub(x,mul(cc,y)) for x,y in zip(NN0[s],NN0[t])] + controls['missing_inverse_dual_conjugation']=mm(adj(MM),NN0)!=J + # A noncommuting fixture catches BA/AB order substitutions hidden by tensors. + An=[[O,Z],[Z,I]];Bn=[[a,b],[b,a]];Cn=mm(Bn,An);zn=zero(2) + Jn=block(zn,adj(An),zn,zn);Fn=block(Cn,sc(Bn,F(1,2)),zn,eye(2)) + expectedN=block(zn,Bn,zn,sc(eye(2),F(-1,2))) + require(mm(adj(Fn),expectedN)==Jn,'noncommuting BA endpoint') + require(phi(Fn,expectedN)==(F(1),F(0)),'noncommuting entropy endpoint') + badF=block(mm(An,Bn),sc(Bn,F(1,2)),zn,eye(2)) + controls['wrong_noncommuting_order']=mm(adj(badF),expectedN)!=Jn + require(all(controls.values()),'all defect controls reject '+str(controls)) + return {'endpoint_fixtures':ends,'complex_pair_column_checks':pair_checks,'noncommuting_endpoint':True,'interleaved_native_jump':['1','1'],'clean_auxiliary_coordinates':d,'monomial_controls':2,'negative_controls':controls,'theorem_evidence':'Written all-dimension proof; finite controls are not an exhaustive proof.','uniform_K_bound':'S>=fV/(16K) only for zero native jump','general_bound':'8K*S+Re(Delta_Q)>=fV/2','new_kappa':False} +if __name__=='__main__': + r=evaluate();require(r==json.loads((Path(__file__).parent/'RESULT.json').read_text()),'frozen result equality') + print('PASS_SPARSE_FEEDBACK_VOLUME endpoint_f=1,2 complex_pair_columns=32 controls=5 child_jump_explicit no_new_kappa')