diff --git a/research/shorter-native-phase-witness/README.md b/research/shorter-native-phase-witness/README.md new file mode 100644 index 0000000000..5b68f6be4a --- /dev/null +++ b/research/shorter-native-phase-witness/README.md @@ -0,0 +1,186 @@ +# Shorter constructive witnesses for native monomial identities + +This package improves the sufficient tensor-width bound for the affine/quadratic +Gaussian monomial grammar in [PR #5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369). +For n>=2 axes, the general cutoff is 2n+3. For three axes, an exact finite +character calculation improves it further to seven. Thus widths 7,8,9,10 +decide every fixed three-axis identity in this grammar. The complete kappa +calculation is unchanged. + +## Contract and result + +Retain the input-phase action and fixed external coefficients: + +```text +U(g,q)e_x = i^q(x) e_g(x), +q(x) = c + sum_j a_j x_j + 2 sum_(j=2 and f>=2n+3 imply ker(rho_f)=I_(f mod 4). +n=3 and f>=7 imply ker(rho_f)=I_(f mod 4). +``` + +Consequently four consecutive widths starting at either sufficient cutoff +decide equality for a single fixed P at all positive widths. The same result +applies entrywise to complete register endpoints. All independent dirty inputs +and all specified returned roles remain part of the endpoint. A width-dependent +program cannot be promoted to an all-width identity by four tests. + +For nine axes the sufficient window changes from 22..25 to 21..24. This changes +an algebraic test bound. It does not reduce a physical supplier's paid cost. +The sharp two-axis cutoff six in PR #5522 remains stronger in that dimension. +No least representation cutoff for n>=3 is claimed here. + +## A nonalternating Gram form saves one column + +A phase character has statistics (r,u,v), where r and u_j are modulo four and +v_jk are modulo two. As in the predecessor, set the binary symmetric matrix M +by M_jj=u_j mod 2 and M_jk=v_jk. A tuple of points must have Gram matrix M, +coordinate counts u modulo four, length r modulo four and full affine span. + +Choose an invertible binary matrix B whose column sum s differs from u modulo +two. This is possible for n>=2: use B=I unless u mod 2 is the all-ones vector; +in that case replace its first column e_1 by e_1+e_2. Start the tuple with zero +and the n columns of B. It already has full affine span. The residual Gram +matrix R=M+BB^t has diagonal u+s, which is nonzero. Thus R is nonalternating. + +Every nonalternating symmetric binary matrix R has a factor YY^t=R with +exactly rank(R)<=n columns. Here is an explicit proof and algorithm. Symmetric +elimination splits the form into unit lines, hyperbolic pairs and a radical. +There is at least one unit line. A unit z and a hyperbolic pair e,f can be +replaced by z+e, z+f, z+e+f; these three vectors are orthonormal. Repeat to +obtain an orthonormal basis v_i for a complement to the radical. Then + +```text +R = sum_i (R v_i)(R v_i)^t. +``` + +Indeed the orthonormal vectors resolve the bilinear form on the quotient by +its radical. This gives the columns of Y and uses polynomial binary linear +algebra. Nonalternation is essential: a nonzero alternating form can require +an extra Gram column. The rank lower bound also proves that this factor width +is exact for the chosen R. Binary symmetric factorization is classical. + +Append the columns of Y. The tuple now has the required Gram matrix and length +at most 2n+1. If its coordinate counts are w modulo four, then u-w is even. +Append two copies of the single vector z with coordinates (u_j-w_j)/2 modulo +two, unless z is zero. This changes the coordinate counts as required and +preserves all pair parities. The length is at most 2n+3. + +For any f>=2n+3 with f congruent to r modulo four, append zero points to reach +f. They preserve coordinate counts, pair counts and affine span. The resulting +tuple realizes every character at every such f. This proves the improved +constructive bound. + +## Why character witnesses decide the complete endpoint + +The predecessor's Fourier argument is retained. Write P as a sum over affine +maps g and diagonal phases. At a fixed residue r, combine the constant phase +coefficients. If P is outside I_r, finite Fourier inversion gives an affine +bucket and a nonconstant phase character with a nonzero Fourier coefficient. +Use a tuple X with that character and full affine span, and put Y=gX. +A different affine map cannot send X to Y. The matrix entry from X to Y is +therefore exactly the nonzero Fourier coefficient. Conversely every element +of I_r evaluates to zero at residue r. This proves the displayed kernel bounds. +The four residue ideals have zero intersection, which proves the four-test +statement. This step neither assumes nor proves that full affine span is +necessary for representation faithfulness. + +## Exact three-axis character calculation + +For n=3 there are 2048 characters including the constant residue. For a +multiplicity vector m on the eight binary addresses, write m=a+4t with +0<=a_x<=3 and t_x>=0. Define its character by + +```text +r = sum_x a_x modulo 4, +u_j = sum_x a_x x_j modulo 4, +v_jk = sum_x a_x x_j x_k modulo 2. +``` + +Let d(a) be the affine dimension of its positive support, with d=-1 for the +empty support. The exact shortest full-span realization of this residue vector +has length + +```text +L(a) = sum_x a_x + 4(3-d(a)). +``` + +Each new supported point requires four copies and increases affine dimension +by at most one. Conversely any affine subspace extends to the full space by +exactly 3-d new points. These two facts prove the formula, including empty +support. Therefore the exact minimum for a character is the minimum of L(a) +over its residue vectors a in {0,1,2,3}^8. Four-copy zero padding preserves the +character and full span at every later width of that residue. + +The executable checks all 65536 residue vectors and all 2048 characters. The +maxima of these exact minima, ordered by residue 0,1,2,3, are + +```text +(8,9,10,7). +``` + +A separate enumeration of all 43758 nonnegative multiplicity vectors of total +width at most ten gives exactly the same 2048 minima. Every minimum also has +an explicit full-span witness. This finite exact certificate and the padding +argument prove that the three-axis representation has stabilized by width +seven. They do not exclude stabilization before the full-span witness bound; +that would require a separate analysis of nontrivial affine stabilizers. + +## Evidence and reproduction + +```sh +python3.12 -B scripts/research_package.py --package research/shorter-native-phase-witness +``` + +Python 3.12 and the standard library suffice. Normal and optimized warning-strict +runs print `PASS_SHORTER_NATIVE_PHASE_WITNESS`; the launcher prints +`PASS_REGISTERED_RESEARCH_PACKAGE`. Each run checks 1023 nonalternating binary +forms through dimension four, 2624 constructed characters through 17 axes, +17408 literal Gaussian-phase identities, the two complete three-axis censuses +above and seven controls. The controls reject an alternating input and show +that Gram parity alone misses a two-unit linear phase change. + +No predecessor executable is imported. These finite checks corroborate the +all-dimension written proof; no independent human or proof-kernel acceptance +is claimed. The selected cold replay, native physical emission, full compiler, +precision, stock, movement and outer-transfer checks were not run. + +## Sources and related work + +Ali Romman's [pinned PR #5369 proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/native-tensor-cutoff/PROOF.md) +supplies the exact grammar, Fourier reduction, pair correction, four residues +and full endpoint contract. It retains Jose Manuel (@jmbarrancoml), Douglas +Colkitt, ywz65, Chris R (@Clear1nsight), JoyboyBrian, Cinna Davis and the native +source lineage. The adaptive initial basis is the change to that construction. + +Hiroki KUMAZAKI (@kumagi) supplies the sharp two-axis result in +[PR #5522](https://github.com/CrocSwap/integer-mult-bounds/pull/5522) and its +[pinned proof](https://github.com/kumagi/integer-mult-bounds/blob/ffb5adf6a2509a7c99f564d13b74fc82a51b5adc/research/two-axis-native-cutoff/PROOF.md). +Its multiplicity method and warning about the representation-kernel gap guide +the three-axis calculation. [PR #5521](https://github.com/CrocSwap/integer-mult-bounds/pull/5521) +audits the general proof and settles one axis. [PR #5526](https://github.com/CrocSwap/integer-mult-bounds/pull/5526) +treats the larger full-Clifford group; the present grammar excludes Hadamards. +No result or source in those contributions is edited. + +## Open next questions + +Determine whether the three-axis representation already stabilizes before +width seven. Start with the affine pointwise stabilizers for characters whose +full-span minimum exceeds the width, and compute their common group-algebra +kernel. A character-realization minimum alone is not a lower bound for the +complete representation. Physical application still needs a source-bound +complete endpoint and its full paid invoice. + +## Credit + +Finite Fourier inversion, binary form classification and affine basis methods +are classical. Predecessor methods retain the credit above. New proof and +checks by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. +No general literature-priority claim is made. diff --git a/research/shorter-native-phase-witness/SOURCES.json b/research/shorter-native-phase-witness/SOURCES.json new file mode 100644 index 0000000000..ddfddba43f --- /dev/null +++ b/research/shorter-native-phase-witness/SOURCES.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/native-tensor-cutoff/PROOF.md", + "usage": "provenance", + "git_blob": "2d92f17cd8e1064028656cd4ff06c1d38f14ebc0", + "sha256": "b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041" + } + ], + "external_provenance": [ + { + "repository": "kumagi/integer-mult-bounds", + "commit": "ffb5adf6a2509a7c99f564d13b74fc82a51b5adc", + "path": "research/two-axis-native-cutoff/PROOF.md", + "git_blob": "68c7f71040bac9afc22246892ff60aedf25363bb", + "usage": "Read-only proof and scoped handoff; no executable import." + } + ] +} diff --git a/research/shorter-native-phase-witness/TASK.json b/research/shorter-native-phase-witness/TASK.json new file mode 100644 index 0000000000..a6cbc6b52b --- /dev/null +++ b/research/shorter-native-phase-witness/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Lower the general native monomial cutoff and certify the three-axis sufficient window.", + "scope_change_reason": "Take the sharper-bound handoff in PR5369, preserving PR5522 exact two-axis result.", + "bottleneck_link": "Reduce sufficient algebraic identity-test widths under the complete native endpoint contract.", + "budget_minutes": 60, + "stop_rule": "Prove the adaptive-basis bound and exact three-axis phase witnesses; do not claim a sharp representation cutoff or physical supplier.", + "outcome": "completed", + "evidence": "Written proof, exact binary factors and two independent complete multiplicity censuses.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance.", + "open_questions": [ + { + "question": "Does the three-axis representation stabilize before width seven?", + "why_it_matters": "The sufficient full-span witness bound need not be the exact representation threshold.", + "first_step": "Compute the common group-algebra kernel of the relevant affine pointwise stabilizers.", + "blocked_by": "The two-axis sign argument does not supply necessity in three axes." + } + ] +} diff --git a/research/shorter-native-phase-witness/VERIFY.json b/research/shorter-native-phase-witness/VERIFY.json new file mode 100644 index 0000000000..ed51afe17f --- /dev/null +++ b/research/shorter-native-phase-witness/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Binary factors, full native phase characters and two independent three-axis multiplicity censuses." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Binary factors, full native phase characters and two independent three-axis multiplicity censuses." + } + ] +} diff --git a/research/shorter-native-phase-witness/verify.py b/research/shorter-native-phase-witness/verify.py new file mode 100644 index 0000000000..e192625ff9 --- /dev/null +++ b/research/shorter-native-phase-witness/verify.py @@ -0,0 +1,206 @@ +#!/usr/bin/env python3 +"""Check shorter native phase witnesses with exact binary arithmetic. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from itertools import product, combinations +import json + + +def require(c, message): + if not c: + raise ValueError(message) + + +def rank(vectors): + pivots = {} + for v in vectors: + while v: + k = v.bit_length() - 1 + if k in pivots: + v ^= pivots[k] + else: + pivots[k] = v + break + return len(pivots) + + +def affine_dimension(points): + return rank([x ^ points[0] for x in points]) if points else -1 + + +def pairing(rows, x, y): + return sum(((rows[j] & y).bit_count() & 1) for j in range(len(rows)) if x >> j & 1) & 1 + + +def gram(columns, n): + return [sum((sum(((v >> j) & 1) * ((v >> k) & 1) for v in columns) & 1) << k + for k in range(n)) for j in range(n)] + + +def factor_nonalternating(rows): + n = len(rows) + require(any(rows[j] >> j & 1 for j in range(n)), 'alternating input') + todo = [1 << j for j in range(n)] + units, pairs = [], [] + while todo: + pivot = next((x for x in todo if pairing(rows, x, x)), None) + if pivot is not None: + units.append(pivot) + todo.remove(pivot) + todo = [x ^ pivot if pairing(rows, x, pivot) else x for x in todo] + continue + pair = next(((x, y) for x, y in combinations(todo, 2) if pairing(rows, x, y)), None) + if pair is None: + break + x, y = pair + todo.remove(x) + todo.remove(y) + todo = [z ^ (x if pairing(rows, z, y) else 0) ^ (y if pairing(rows, z, x) else 0) for z in todo] + pairs.append(pair) + for x, y in pairs: + z = units.pop() + units.extend((z ^ x, z ^ y, z ^ x ^ y)) + columns = [sum(((row & v).bit_count() & 1) << j for j, row in enumerate(rows)) for v in units] + require(len(columns) == rank(rows) and gram(columns, n) == rows, 'binary factorization') + return columns + + +def statistics(points, n): + u = tuple(sum(x >> j & 1 for x in points) % 4 for j in range(n)) + v = tuple(sum((x >> j & 1) * (x >> k & 1) for x in points) % 2 for j, k in combinations(range(n), 2)) + return len(points) % 4, u, v + + +def witness(n, u, v, width): + require(n >= 2 and width >= 2 * n + 3, 'outside general witness domain') + columns = [1 << j for j in range(n)] + parity = sum((x & 1) << j for j, x in enumerate(u)) + if parity == (1 << n) - 1: + columns[0] ^= 2 + points = [0] + columns + M = [(u[j] & 1) << j for j in range(n)] + for bit, (j, k) in zip(v, combinations(range(n), 2)): + M[j] |= bit << k + M[k] |= bit << j + start = gram(columns, n) + points += factor_nonalternating([a ^ b for a, b in zip(M, start)]) + current = statistics(points, n)[1] + z = sum((((u[j] - current[j]) % 4) // 2) << j for j in range(n)) + if z: + points += [z, z] + require(len(points) <= 2 * n + 3, 'witness width') + points += [0] * (width - len(points)) + return points + + +def count_statistics(counts): + return (sum(counts) % 4, + tuple(sum(counts[x] * (x >> j & 1) for x in range(8)) % 4 for j in range(3)), + tuple(sum(counts[x] * (x >> j & 1) * (x >> k & 1) for x in range(8)) % 2 + for j, k in combinations(range(3), 2))) + + +def three_axis_minima(): + minima, chosen = {}, {} + for counts in product(range(4), repeat=8): + support = [x for x in range(8) if counts[x]] + length = sum(counts) + 4 * (3 - affine_dimension(support)) + key = count_statistics(counts) + if length < minima.get(key, 100): + minima[key], chosen[key] = length, counts + require(len(minima) == 2048, 'complete character inventory') + for key, counts in chosen.items(): + counts = list(counts) + support = [x for x in range(8) if counts[x]] + while affine_dimension(support) < 3: + x = next(x for x in range(8) if affine_dimension(support + [x]) > affine_dimension(support)) + counts[x] += 4 + support.append(x) + require(sum(counts) == minima[key] and count_statistics(counts) == key, 'minimum witness') + direct = {} + compositions = 0 + for width in range(11): + for bars in combinations(range(width + 7), 7): + endpoints = (-1,) + bars + (width + 7,) + counts = tuple(endpoints[i + 1] - endpoints[i] - 1 for i in range(8)) + compositions += 1 + if affine_dimension([x for x in range(8) if counts[x]]) == 3: + direct.setdefault(count_statistics(counts), width) + require(direct == minima, 'independent total-width census') + thresholds = [max(value for key, value in minima.items() if key[0] == r) for r in range(4)] + require(thresholds == [8, 9, 10, 7], 'three-axis residue thresholds') + return thresholds, compositions + + +def phase(points, n, c, a, b): + return sum(c + sum(a[j] * (x >> j & 1) for j in range(n)) + + 2 * sum(bit * (x >> j & 1) * (x >> k & 1) + for bit, (j, k) in zip(b, combinations(range(n), 2))) for x in points) % 4 + + +def general_checks(): + factors = characters = phase_checks = 0 + for n in range(1, 5): + positions = list(combinations(range(n), 2)) + [(j, j) for j in range(n)] + for bits in product(range(2), repeat=len(positions)): + rows = [0] * n + for bit, (j, k) in zip(bits, positions): + rows[j] |= bit << k + rows[k] |= bit << j + if any(rows[j] >> j & 1 for j in range(n)): + factor_nonalternating(rows) + factors += 1 + for n in (2, 3): + for u in product(range(4), repeat=n): + for v in product(range(2), repeat=n * (n - 1) // 2): + for r in range(4): + F = 2 * n + 3 + width = F + (r - F) % 4 + points = witness(n, u, v, width) + require(statistics(points, n) == (r, u, v) and affine_dimension(points) == n, 'complete witness contract') + characters += 1 + for seed in range(8): + c = seed % 4 + a = [(seed + 3 * j) % 4 for j in range(n)] + b = [(seed + j) % 2 for j in range(len(v))] + expected = (r * c + sum(x * y for x, y in zip(u, a)) + 2 * sum(x * y for x, y in zip(v, b))) % 4 + require(phase(points, n, c, a, b) == expected, 'literal Gaussian phase') + phase_checks += 1 + for n in range(4, 18): + for seed in range(32): + u = tuple((seed * (j + 1) + j * j) % 4 for j in range(n)) + v = tuple(((seed + 1) * (j + 3) + j // 3) % 2 for j in range(n * (n - 1) // 2)) + width = 2 * n + 3 + seed % 4 + points = witness(n, u, v, width) + require(statistics(points, n) == (width % 4, u, v) and affine_dimension(points) == n, 'larger witness') + characters += 1 + return factors, characters, phase_checks + + +def main(): + factors, characters, phase_checks = general_checks() + thresholds, compositions = three_axis_minima() + controls = 0 + try: + factor_nonalternating([2, 1]) + except ValueError: + controls += 1 + else: + raise ValueError('alternating input accepted') + for n in (2, 3, 9): + u, v = (1,) * n, (0,) * (n * (n - 1) // 2) + points = witness(n, u, v, 2 * n + 3) + require(phase(points, n, 1, [0] * n, [0] * len(v)) == len(points) % 4, 'constant phase') + controls += 1 + changed = points + [1, 1] + require(statistics(changed, n)[1] != u and gram(changed, n) == gram(points, n), 'parity-only false witness') + controls += 1 + print('PASS_SHORTER_NATIVE_PHASE_WITNESS ' + json.dumps(dict(binary_factorizations=factors, + constructed_characters=characters, literal_phase_checks=phase_checks, normal_forms=65536, + independent_compositions=compositions, three_axis_characters=2048, + three_axis_residue_thresholds=thresholds, controls=controls), sort_keys=True)) + + +if __name__ == '__main__': + main()