diff --git a/research/prefix-encoder-metric-loss/PROOF.md b/research/prefix-encoder-metric-loss/PROOF.md new file mode 100644 index 0000000000..efb76b1c6d --- /dev/null +++ b/research/prefix-encoder-metric-loss/PROOF.md @@ -0,0 +1,132 @@ +# The sharp boundary loss of the prefix encoder + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +Let G be any finite group, with identity e and order q. The physical column +alphabet and virtual state space are both G. All vector spaces in this proof +are complex Hilbert spaces with their coordinate inner products. Define + + T[y,x]_(a,b) = 1 if y = a x and b = y, and 0 otherwise, + F = e_e*, B = sum_(b in G) e_b. + +For every positive width f the physical endpoint is + + E_f[Y,X] = F T[y_1,x_1] ... T[y_f,x_f] B. + +This uses the fixed physical-table convention of zxv's [PR5441](https://github.com/CrocSwap/integer-mult-bounds/pull/5441). +For G=C2 it is the standard prefix-XOR encoder in that package. We use the +table definition, not any claimed physical implementation or paid cost. + +## Claim and certificate being optimized + +The endpoint E_f is a permutation matrix, so ||E_f||_op=1 at every positive f. +For the following specific sufficient certificate, however, the least uniform +squared bound is exactly q. This remains true after grouping any fixed positive +number k of columns and after any fixed invertible change of virtual basis. + +The certificate is Ali Romman's [PR5451](https://github.com/CrocSwap/integer-mult-bounds/pull/5451) +metric criterion. Write L_k for the full local operator whose block from physical +input X to output Y is T[y_1,x_1] ... T[y_k,x_k]. It asks for a positive definite +Hermitian P and nonnegative scalars A,H,c, with c<=1, satisfying + + F*F <= A P, B* P B <= H, + L_k* (P tensor I_(q^k)) L_k <= c (P tensor I_(q^k)). + +The tensor factors here are ordered virtual then physical. Permuting both +sides gives exactly the source's physical-then-virtual block convention. +The resulting bound at f=k m is A H c^m. Its uniform positive-m bound is +A H c. The theorem below optimizes precisely these inequalities. It neither +asserts that all uniform bounds have this form nor alleges an error in the +source's sufficient theorem. + +## 1. The endpoint and local operator are unitary + +For an initial state a and input X=(x_1,...,x_k), the only surviving path is + + y_j = a x_1 ... x_j, b = y_k. + +With a=e and the final state summed by B, E_f is the prefix-product map. +Its inverse is x_1=y_1 and x_j=y_(j-1)^(-1) y_j for j>=2. Thus it is a +permutation on G^f, including for noncommutative G. + +The direction of the virtual indices matters. As an operator L_k, the input +virtual state is the terminal b, and the output virtual state is a. +For each input (b,X), set a=b (x_1 ... x_k)^(-1), then form the unique Y above. +This defines one output (a,Y). Conversely, (a,Y) determines X by successive +group differences and determines b=y_k. Therefore L_k is itself a permutation +matrix on q^(k+1) coordinates. In particular it is unitary. + +## 2. A contractive positive metric is scalar + +Put W=P tensor I_(q^k). Its trace is positive. Since L_k is unitary, + + Tr(L_k* W L_k) = Tr(W). + +The contraction inequality and c<=1 imply Tr(W)<=c Tr(W), hence c=1. +The positive semidefinite difference W-L_k* W L_k has trace zero, so it is zero. +Equivalently, L_k preserves the full metric W exactly. + +Consider two input coordinates (b,X) and (b',X) with the same physical X +and distinct b,b'. Their output physical words Y,Y' are distinct because their +last letters are b,b'. Consequently + + (L_k* W L_k)_((b,X),(b',X)) = 0, + W_((b,X),(b',X)) = P_(b,b'). + +Metric invariance forces every off-diagonal entry of P to vanish, including +its imaginary part. On a diagonal coordinate (b,X), invariance then says + + P_(b,b) = P_(a,a), a=b (x_1 ... x_k)^(-1). + +At every k>=1 the product x_1 ... x_k ranges over all G. Thus all diagonal +entries agree. Positive definiteness gives P=t I_q with t>0. Conversely every +such metric is preserved by the permutation L_k. This characterizes all +feasible positive metrics, rather than searching a finite subset of them. + +## 3. The exact optimum is q + +For P=t I_q, the left inequality forces A>=1/t by evaluating it on e_e. +The right inequality forces H>=q t because B has q unit entries. Thus + + A H c >= (1/t) (q t) = q. + +Equality is attained at P=t I_q, A=1/t, H=q t, c=1. Hence the least certified +squared bound is q, although the actual squared operator norm is one. +The multiplicative loss in operator norm is exactly sqrt(q). It persists at +every fixed blocking length. For a residual epsilon E_f with epsilon nonzero, +the same argument gives the least squared bound q |epsilon|^2. + +## 4. A virtual basis change cannot remove the loss + +Let S be any invertible complex q-by-q matrix, and set + + T'[y,x]=S^(-1) T[y,x] S, F'=F S, B'=S^(-1) B. + +Products telescope at every block length. A certificate for the primed table +with metric P' is exactly a certificate for the original table with +P=S^(-*) P' S^(-1), with the same A,H,c. Congruence by an invertible matrix +preserves positive definiteness and semidefinite order in both directions. +All feasible primed metrics are therefore P'=t S* S, and the optimum is q. +This permits arbitrary conditioning of S. It is an algebraic statement, not +a claim that a basis change has zero physical or precision cost. + +## Consequence and scope + +For a desired norm tolerance tau, an error epsilon E_f can satisfy the actual +bound |epsilon|<=tau while this certificate demands sqrt(q)|epsilon|<=tau. +Searching more positive metrics, or blocking more columns within this same +representation and criterion, cannot close that gap. A useful next method +must retain boundary correlation, use a different representation, or change +the certificate. Those possibilities are not excluded by this proof. + +The example is a complete algebraic physical endpoint, not a materialized +native/tape implementation. It supplies no paid supplier, dirty-workspace +program, compiler closure, recovery budget, new kappa or multiplication +theorem. No claim is made about arbitrary transfer tables, augmented virtual +spaces, width-dependent metrics, or position-dependent metric sequences. + +The trace and congruence arguments and weighted operator norms are classical. +The additional result is this exact optimum, its positive-metric rigidity, +and its permanence under blocking and virtual gauges for the named encoder. +Finite checks in verify.py corroborate the proof and do not replace its +universal quantifiers or constitute formal proof-kernel acceptance. diff --git a/research/prefix-encoder-metric-loss/README.md b/research/prefix-encoder-metric-loss/README.md new file mode 100644 index 0000000000..d6a59f2a0b --- /dev/null +++ b/research/prefix-encoder-metric-loss/README.md @@ -0,0 +1,105 @@ +# A sharp boundary loss in uniform transfer-metric certificates + +This scoped written proof with exact finite corroboration was produced by Nick Petalas. +For the standard prefix-product encoder on any finite group G of order q, +every complete physical endpoint is unitary. Its true operator norm is one. +The least uniform operator-norm bound obtainable from Ali Romman's +[PR5451](https://github.com/CrocSwap/integer-mult-bounds/pull/5451) fixed positive +transfer-metric criterion is exactly sqrt(q). Every fixed positive blocking +length and every invertible complex virtual basis change retains that loss. + +The new [proof](PROOF.md) characterizes all feasible metrics. The local blocked +operator is a permutation, so its contraction inequality forces c=1 and exact +metric invariance. Physical output separation then forces P=t I. The two +boundary inequalities have product at least q, with an attaining certificate. +This is a sharp limit of that sufficient criterion, not a counterexample to +its theorem. No new kappa or selected-frontier change is claimed. + +For the prefix-XOR example in zxv's +[PR5441](https://github.com/CrocSwap/integer-mult-bounds/pull/5441), the loss is +sqrt(2). Searching more positive metrics or blocking more columns cannot make +that certificate sharp. A boundary-aware method or a changed representation +is a separate question. + +## Evidence and reproduction + +The independent local implementation imports no predecessor executable. It +checks complete endpoint entries by literal one-column contraction, complete +blocked local permutations, exact ranks of the metric-invariance equations, +explicit negative quadratic-form witnesses for non-scalar real and complex +metrics, and rational gauge certificates. Six groups include noncommutative S3. +The universal statement rests on the written proof, not extrapolation from +these finite groups or block lengths. Generated stdout receipts bind all seven +package files and both exact source-document inputs by SHA256. + +The fixed replay enumerates 21 blocked tables and 787 literal blocked paths, +85,873 metric-commutator entries, 17,792 complete endpoint entries, 45 negative +metric witnesses and 12 gauge certificates. Its 63 controls comprise seven +invalid group/block cases, a changed terminal boundary, an imaginary +off-diagonal metric and 54 strict boundary/rate underclaim witnesses. + +From the repository root, use CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/prefix-encoder-metric-loss/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/prefix-encoder-metric-loss/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/prefix-encoder-metric-loss +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/prefix-encoder-metric-loss --check-source-history +``` + +Other machines may substitute their CPython 3.12 interpreter. The verifier +prints `PASS_PREFIX_ENCODER_METRIC_LOSS` in its JSON receipt and writes no files. +Both warning-strict modes are registered. The source-history check is a +publication integrity check, separate from the mathematics. A Git-free export +needs this package and the two inputs declared in VERIFY.json. + +## Scope and credit + +Ali Romman supplies the sufficient metric criterion and its stated limitations. +zxv supplies the concrete fixed-transfer contract and prefix-XOR example, with +the retained weighted-automata, matrix-product, native and phase lineage. +Trace invariance, congruence and weighted operator norms are classical. The +additional result is the sharp optimized loss and its metric rigidity under +blocking and virtual gauges. No predecessor result is audited or replayed. +Source documents, Git blobs and hashes are pinned in [SOURCES.json](SOURCES.json). +New work is Apache-2.0. Independent human and formal proof-kernel review are unclaimed. + +The `formal-interface-lemma` card is explicitly changed to this certificate +obstruction. It explains a limitation of one possible route to uniform error +control, without discharging a selected framework assumption. The result +fixes this representation and certificate. Larger or different virtual +representations, position-dependent metrics and boundary-aware certificates +remain open. Physical synthesis, dirty restoration, native costs, the complete +paid invoice, compiler closure, tape/precision and exact recovery are outside +scope. No selected cold replay, native suite, Lean or Docker build was run. + +## Open next questions + +1. Can a boundary-aware finite certificate attain norm one for this encoder + while still controlling small complete residuals? Start with the reachable + boundary subspaces and retain coherent physical input sums. The obstruction + here only applies to the single fixed positive metric criterion. +2. Does another finite transfer representation of the same endpoint remove + the loss? Start by allowing a changed virtual dimension and explicit boundary + maps. An invertible basis change in the present dimension is already covered. + +## Verifier constraints + +All functions have fewer than sixty physical lines, with structured iterative +control flow and explicit exception checks that remain active under optimization. +Groups have at most six elements; blocked local permutations have at most 216 +coordinates; exact constraint elimination has at most 36 variables and 2592 +distinct relations. Dense gauge matrices have at most 36 rows. Fixed fixture +loops and these caps bound the complete run. The verifier has no subprocess, +network or input-file argument. Source and package files are capped at one MB. + +Power of Ten rule 3 deviation: CPython allocates managed integers, Fractions and +collections during this bounded one-shot check. The fixed domains above bound +live data; no unbounded search or external resource is retained. Both registered +modes exercise those domains. A fixed-allocation implementation would require +a different arithmetic runtime. Rule 8/9 deviation: isolated execution uses one +explicit file-based import of the package-local encoder.py. The only dynamic +target is that fixed sibling file, which is included in the receipt and committed +source. No external plugin or generated code is loaded. Reassess these controls +before adding an external frontend. Warning-strict execution and AST compilation +are the local diagnostics; no external static analyzer is claimed. diff --git a/research/prefix-encoder-metric-loss/SOURCES.json b/research/prefix-encoder-metric-loss/SOURCES.json new file mode 100644 index 0000000000..cac02e86bd --- /dev/null +++ b/research/prefix-encoder-metric-loss/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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/finite-memory-lifting/README.md", + "usage": "input", + "git_blob": "5ce4fa86af1d5487f9a639acdc9fa0177c76c192", + "sha256": "ca0be421d5cb1835a8814685907db78a7a3ea24b7e1e474f3038c87b0e46498e" + }, + { + "path": "research/transfer-metric-error-bound/README.md", + "usage": "input", + "git_blob": "d0642b7857a1e6f14517f366ef9eade202a23a3d", + "sha256": "60d86e24f2efafe4e2e3600a7e8a49b6ce5f45d4bf3892d84f1f48bb475c6d9d" + } + ] +} diff --git a/research/prefix-encoder-metric-loss/TASK.json b/research/prefix-encoder-metric-loss/TASK.json new file mode 100644 index 0000000000..616b968632 --- /dev/null +++ b/research/prefix-encoder-metric-loss/TASK.json @@ -0,0 +1,142 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "Sharp sqrt(|G|) loss of the fixed positive transfer-metric certificate for the standard prefix-product encoder, invariant under fixed blocking and virtual similarity.", + "scope_change_reason": "An original certificate obstruction replaces an audit or formalization of a predecessor. It identifies a method that cannot give a sharp uniform error estimate for this complete unitary family.", + "bottleneck_link": "Side result for uniform numerical certification, relevant to precision_tape. No selected assumption or kappa is discharged.", + "budget_minutes": 60, + "stop_rule": "Package the first verified sharp obstruction. Do not extend to a new certificate method or physical supplier.", + "outcome": "completed", + "evidence": "PROOF.md and the read-only exact normal/optimized verify.py checks.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a boundary-aware certificate attain the true unit norm?", + "why_it_matters": "Avoids the proved sqrt(q) loss in a recovery-error budget.", + "first_step": "Track the reachable boundary subspaces while retaining coherent physical inputs.", + "blocked_by": "A new finite soundness theorem for complete residuals." + }, + { + "question": "Can a different virtual representation remove the loss?", + "why_it_matters": "The rigidity only covers this representation and its invertible gauges.", + "first_step": "Supply explicit enlarged tables and boundary maps for the same endpoint.", + "blocked_by": "Representation search and a complete endpoint proof." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19247053", + "question_source": "PR #5451", + "question_source_author": "aliromman", + "scientific_base": "721c03822c421b7f7fcbb2598993b947c4d88419", + "preserved_branch": "research/w14-1022aj-query-floor", + "preserved_head": "5e09c60005dd6ae454eef8271c0c2d2dba62c12e", + "playbook": "Investigation", + "environment": { + "python": "3.12.15" + }, + "overlap": { + "live_open_pr_snapshot": "2026-10-28T16:15:28.060013+00:00", + "open_pr_records": 407, + "discussion_snapshot": "2026-10-28T16:16:39.899759+00:00", + "discussion_records": 5829, + "limitations": "Sparse local notes; arbitrary historical diffs and unpublished work are not exhausted. Main README and merged PR term searches supplemented the cache.", + "source_checks": "No this-account PR returned for source5451. Same-account recent targets and current locks were excluded.", + "related_open_work": "No open PR located on this specific metric optimum; PR5451 and PR5441 are merged predecessors.", + "final_check": "Refetched unchanged canonical main; repeated exact-object/formula/main and merged-PR searches; read current locks and newly opened PRs through #6156. No competing metric-optimum result located." + }, + "claim_type": "scoped written proof with exact finite corroboration", + "verification_summary": { + "groups": 6, + "blocked_tables": 21, + "literal_blocked_paths": 787, + "metric_commutator_entries": 85873, + "complete_endpoint_entries": 17792, + "negative_metric_witnesses": 45, + "gauge_certificates": 12, + "controls": { + "invalid_group_or_block": 7, + "changed_terminal_boundary": 1, + "imaginary_off_diagonal_metric": 1, + "strict_boundary_or_rate_underclaim": 54 + } + }, + "upstream_refresh": { + "commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "checked_at": "2026-10-28T16:27:05.660499+00:00", + "guidance_changed": false + } +} diff --git a/research/prefix-encoder-metric-loss/VERIFY.json b/research/prefix-encoder-metric-loss/VERIFY.json new file mode 100644 index 0000000000..1458503b98 --- /dev/null +++ b/research/prefix-encoder-metric-loss/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/finite-memory-lifting/README.md", + "research/transfer-metric-error-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete literal endpoints, blocked metric-commutant rank, complex negative witnesses, gauge certificates and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete literal endpoints, blocked metric-commutant rank, complex negative witnesses, gauge certificates and rejection controls." + } + ] +} diff --git a/research/prefix-encoder-metric-loss/encoder.py b/research/prefix-encoder-metric-loss/encoder.py new file mode 100644 index 0000000000..7dc1a93ba4 --- /dev/null +++ b/research/prefix-encoder-metric-loss/encoder.py @@ -0,0 +1,145 @@ +"""Exact finite prefix-encoder tables and metric obstruction witnesses. + +Produced by Nick Petalas. Apache-2.0. +""" + +from fractions import Fraction as Q +from itertools import product + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def group(table): + """Validate a small Cayley table, with identity labelled zero.""" + q = len(table) + require(1 <= q <= 6, "group order outside 1..6") + require(all(len(row) == q for row in table), "Cayley shape") + require(all(type(x) is int and 0 <= x < q for row in table for x in row), + "Cayley entries") + require(all(table[0][a] == a == table[a][0] for a in range(q)), "identity") + for a in range(q): + require(any(table[a][b] == 0 == table[b][a] for b in range(q)), "inverse") + for a, b, c in product(range(q), repeat=3): + require(table[table[a][b]][c] == table[a][table[b][c]], "associativity") + return q + + +def encode(word, q): + result = 0 + for letter in word: + result = q * result + letter + return result + + +def prefixes(table, initial, word): + current = initial + output = [] + for letter in word: + current = table[current][letter] + output.append(current) + return tuple(output) + + +def local_permutation(table, block): + """Columns (final virtual state, input); rows (initial state, output).""" + q = group(table) + require(type(block) is int and 1 <= block <= 6, "positive block length <=6") + m = q ** block + require(q * m <= 216, "local state capacity 216") + permutation = [-1] * (q * m) + for initial in range(q): + for word in product(range(q), repeat=block): + output = prefixes(table, initial, word) + column = output[-1] * m + encode(word, q) + row = initial * m + encode(output, q) + require(permutation[column] == -1, "duplicate physical column") + permutation[column] = row + require(sorted(permutation) == list(range(q * m)), "local unitarity") + return tuple(permutation), m + + +def metric_relations(permutation, m, q): + """All coefficient equations of L* (P tensor I) L = P tensor I.""" + n = len(permutation) + require(n == q * m and n <= 216, "metric dimensions") + require(sorted(permutation) == list(range(n)), "invalid permutation") + relations = set() + for i in range(n): + ai, yi = divmod(permutation[i], m) + bi, xi = divmod(i, m) + for j in range(n): + aj, yj = divmod(permutation[j], m) + bj, xj = divmod(j, m) + row = {} + if yi == yj: + row[ai * q + aj] = 1 + if xi == xj: + key = bi * q + bj + row[key] = row.get(key, 0) - 1 + nonzero = tuple(sorted((key, val) for key, val in row.items() if val)) + if nonzero: + relations.add(nonzero) + return tuple(sorted(relations)), n * n + + +def relation_rank(relations, variables): + require(1 <= variables <= 36 and len(relations) <= 2592, "rank capacity") + basis = {} + for sparse in relations: + row = [Q(0)] * variables + for key, value in sparse: + row[key] = Q(value) + for pivot in sorted(basis): + factor = row[pivot] + row = [a - factor * b for a, b in zip(row, basis[pivot])] + pivot = next((i for i, value in enumerate(row) if value), None) + if pivot is not None: + factor = row[pivot] + basis[pivot] = tuple(value / factor for value in row) + return len(basis) + + +def defect_entry(real, imaginary, permutation, m, i, j): + """Entry of Q = P tensor I - L* (P tensor I) L.""" + bi, xi = divmod(i, m) + bj, xj = divmod(j, m) + ai, yi = divmod(permutation[i], m) + aj, yj = divmod(permutation[j], m) + re = real[bi][bj] if xi == xj else Q(0) + im = imaginary[bi][bj] if xi == xj else Q(0) + if yi == yj: + re -= real[ai][aj] + im -= imaginary[ai][aj] + return re, im + + +def negative_witness(real, imaginary, permutation, m): + """Return a rational Gaussian vector with negative contraction residual.""" + q = len(real) + require(1 <= q <= 6 and len(imaginary) == q, "Hermitian metric dimension") + require(all(len(row) == q for row in real + imaginary), "metric shape") + for i, j in product(range(q), repeat=2): + require(real[i][j] == real[j][i] and imaginary[i][j] == -imaginary[j][i], + "metric must be Hermitian") + n = len(permutation) + require(n == q * m and n <= 216, "witness capacity") + diagonal = [defect_entry(real, imaginary, permutation, m, i, i)[0] + for i in range(n)] + require(sum(diagonal) == 0, "unitary trace identity") + for i, value in enumerate(diagonal): + if value < 0: + return ((i, Q(1), Q(0)),), value + require(all(value == 0 for value in diagonal), "nonnegative trace zero") + for i in range(n): + for j in range(i + 1, n): + re, im = defect_entry(real, imaginary, permutation, m, i, j) + if re: + sign = -1 if re > 0 else 1 + return ((i, Q(1), Q(0)), (j, Q(sign), Q(0))), -2 * abs(re) + if im: + sign = 1 if im > 0 else -1 + return ((i, Q(1), Q(0)), (j, Q(0), Q(sign))), -2 * abs(im) + return (), Q(0) diff --git a/research/prefix-encoder-metric-loss/verify.py b/research/prefix-encoder-metric-loss/verify.py new file mode 100644 index 0000000000..ed01b36a44 --- /dev/null +++ b/research/prefix-encoder-metric-loss/verify.py @@ -0,0 +1,258 @@ +#!/usr/bin/env python3 +"""Finite corroboration of the sharp prefix-encoder metric loss. + +Produced by Nick Petalas. Apache-2.0. No predecessor executable is imported. +""" + +import hashlib +import importlib.util +import json +from fractions import Fraction as Q +from itertools import permutations, product +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location("prefix_encoder_local", HERE / "encoder.py") +if SPEC is None or SPEC.loader is None: + raise ValueError("local encoder loader unavailable") +E = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(E) + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def eye(n): + check(1 <= n <= 36, "dense matrix capacity") + return [[Q(i == j) for j in range(n)] for i in range(n)] + + +def transpose(a): + return [list(column) for column in zip(*a)] + + +def multiply(a, b): + check(1 <= len(a) <= 36 and 1 <= len(b) <= 36, "multiply capacity") + check(all(len(row) == len(b) for row in a), "multiply dimensions") + return [[sum(x * y for x, y in zip(row, col)) for col in zip(*b)] for row in a] + + +def groups(): + result = [("C" + str(q), tuple(tuple((i + j) % q for j in range(q)) + for i in range(q))) for q in range(1, 5)] + result.append(("V4", tuple(tuple(i ^ j for j in range(4)) for i in range(4)))) + elements = list(permutations(range(3))) + table = tuple(tuple(elements.index(tuple(a[b[i]] for i in range(3))) + for b in elements) for a in elements) + result.append(("S3", table)) + return tuple(result) + + +def literal_entry(table, inputs, outputs, final=None, initial=0): + """Multiply the one-column tables independently of the blocked constructor.""" + q = len(table) + row = [Q(i == initial) for i in range(q)] + for x, y in zip(inputs, outputs): + next_row = [Q(0)] * q + for a, b in product(range(q), repeat=2): + transition = int(y == table[a][x] and b == y) + next_row[b] += row[a] * transition + row = next_row + return sum(row) if final is None else row[final] + + +def endpoint_checks(table, max_width): + q = len(table) + entries = 0 + for width in range(1, max_width + 1): + words = tuple(product(range(q), repeat=width)) + images = [] + for inputs in words: + expected = [] + for index in range(width): + value = 0 + for letter in inputs[:index + 1]: + value = table[value][letter] + expected.append(value) + images.append(tuple(expected)) + for outputs in words: + check(literal_entry(table, inputs, outputs) == int(outputs == tuple(expected)), + "literal complete endpoint differs from prefix permutation") + entries += 1 + check(len(set(images)) == len(words), "endpoint is not unitary") + return entries + + +def quadratic(real, imaginary, permutation, m, vector): + """Evaluate z* Q z independently by the two weighted norms.""" + before = Q(0) + after = Q(0) + for i, ir, ii in vector: + for j, jr, ji in vector: + bi, xi = divmod(i, m) + bj, xj = divmod(j, m) + ai, yi = divmod(permutation[i], m) + aj, yj = divmod(permutation[j], m) + cr, ci = ir * jr + ii * ji, ir * ji - ii * jr + if xi == xj: + before += cr * real[bi][bj] - ci * imaginary[bi][bj] + if yi == yj: + after += cr * real[ai][aj] - ci * imaginary[ai][aj] + return before - after + + +def metric_checks(table, block): + q = len(table) + permutation, m = E.local_permutation(table, block) + words = tuple(product(range(q), repeat=block)) + for column, row in enumerate(permutation): + terminal, xi = divmod(column, m) + initial, yi = divmod(row, m) + check(literal_entry(table, words[xi], words[yi], terminal, initial) == 1, + "blocked path disagrees with literal one-column table product") + relations, entries = E.metric_relations(permutation, m, q) + rank = E.relation_rank(relations, q * q) + check(rank == q * q - 1, "contractive metric commutant is not scalar") + for relation in relations: + check(sum(value for key, value in relation if key // q == key % q) == 0, + "identity metric is not in the kernel") + witnesses = 0 + for mode in range(3): + vr = [Q((i + 1) * (mode + 1), 3) for i in range(q)] + vi = [Q((i % 2) * mode, 5) for i in range(q)] + real = [[Q(i == j) + vr[i] * vr[j] + vi[i] * vi[j] + for j in range(q)] for i in range(q)] + imaginary = [[vi[i] * vr[j] - vr[i] * vi[j] + for j in range(q)] for i in range(q)] + # P = I + v v* is positive definite without a numerical eigenvalue test. + vector, value = E.negative_witness(real, imaginary, permutation, m) + if q == 1: + check(not vector and value == 0, "trivial group metric") + else: + check(value < 0 and quadratic(real, imaginary, permutation, m, vector) == value, + "explicit noncontractive metric witness") + witnesses += 1 + return entries, len(relations), witnesses, len(permutation) + + +def gauge_checks(table): + q = len(table) + permutation, _ = E.local_permutation(table, 1) + n = q * q + local = [[Q(permutation[j] == i) for j in range(n)] for i in range(n)] + count = 0 + for mode in range(2): + s, inverse = eye(q), eye(q) + if mode == 0: + for i in range(q): + s[i][i], inverse[i][i] = Q(i + 1), Q(1, i + 1) + elif q > 1: + s[0][1], inverse[0][1] = Q(2, 3), Q(-2, 3) + check(multiply(s, inverse) == eye(q), "gauge inverse") + metric = multiply(transpose(s), s) + lift = [[s[i // q][j // q] * int(i % q == j % q) + for j in range(n)] for i in range(n)] + unlift = [[inverse[i // q][j // q] * int(i % q == j % q) + for j in range(n)] for i in range(n)] + transformed = multiply(unlift, multiply(local, lift)) + weight = [[metric[i // q][j // q] * int(i % q == j % q) + for j in range(n)] for i in range(n)] + check(multiply(transpose(transformed), multiply(weight, transformed)) == weight, + "gauge metric does not contract isometrically") + left = [s[0]] + right = [[sum(row)] for row in inverse] + left_dual = multiply(multiply(left, multiply(inverse, transpose(inverse))), + transpose(left))[0][0] + right_bound = multiply(transpose(right), multiply(metric, right))[0][0] + check(left_dual == 1 and right_bound == q, "gauge boundary factor") + count += 1 + return count + + +def reject_controls(): + count = 0 + cases = (((), 1), (((0, 1), (1, 0)), 0), (((0, 1), (1, 0)), 7), + (((0, 1), (1, 1)), 1), (((0, 2), (1, 0)), 1), + (((0, 1),), 1), (((0, 1), (1, 0)), 1.0)) + for table, block in cases: + try: + E.local_permutation(table, block) + except ValueError: + count += 1 + else: + raise ValueError("invalid group or block accepted") + table = ((0, 1), (1, 0)) + check(literal_entry(table, (1,), (1,), final=0) == 0, "terminal-state mutant") + count += 1 + permutation, m = E.local_permutation(table, 1) + re, im = eye(2), [[Q(0), Q(1, 3)], [Q(-1, 3), Q(0)]] + vector, value = E.negative_witness(re, im, permutation, m) + check(value < 0 and quadratic(re, im, permutation, m, vector) == value, + "imaginary off-diagonal mutant not rejected") + check(all(re[i][i] == 1 for i in range(2)), "diagonal-only false positive") + count += 1 + for q in range(1, 7): + for t in (Q(1, 3), Q(1), Q(7, 2)): + check((1 / t - Q(1, 100)) * t - 1 < 0, "left-bound underclaim") + check(q * t - (q * t - Q(1, 100)) > 0, "right-bound underclaim") + check(Q(999, 1000) * q - q < 0, "rate below one underclaim") + count += 3 + return count + + +def authenticated_hashes(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + root = HERE.parents[1] + pins = {} + for row in sources["files"]: + if row["usage"] != "input": + continue + path = root / row["path"] + check(path.stat().st_size <= 1_000_000, "source input size") + digest = hashlib.sha256(path.read_bytes()).hexdigest() + check(digest == row["sha256"], "changed source input: " + row["path"]) + pins[row["path"]] = digest + own = {} + for path in sorted(HERE.iterdir()): + if path.is_file(): + check(path.stat().st_size <= 1_000_000, "package file size") + own[path.name] = hashlib.sha256(path.read_bytes()).hexdigest() + check(len(own) == 7 and len(pins) == 2, "package/input inventory") + return own, pins + + +def main(): + own, pins = authenticated_hashes() + entries = relations = witnesses = endpoints = gauges = blocks = paths = 0 + summaries = [] + for name, table in groups(): + q = E.group(table) + widths = (1, 2, 3, 4, 5, 6) if q <= 2 else ((1, 2, 3) if q <= 4 else (1, 2)) + for block in widths: + if q ** (block + 1) > 216: + continue + n_entries, n_relations, n_witnesses, n_paths = metric_checks(table, block) + entries += n_entries + relations += n_relations + witnesses += n_witnesses + paths += n_paths + blocks += 1 + endpoints += endpoint_checks(table, 4 if q <= 3 else (3 if q <= 4 else 2)) + gauges += gauge_checks(table) + summaries.append({"group": name, "order": q, "true_squared_norm": 1, + "least_certified_squared_bound": q}) + controls = reject_controls() + print(json.dumps({"status": "PASS_PREFIX_ENCODER_METRIC_LOSS", "groups": summaries, + "blocked_tables": blocks, "commutator_entries": entries, + "sum_distinct_relations_per_table": relations, + "blocked_path_entries": paths, "negative_metric_witnesses": witnesses, + "complete_endpoint_entries": endpoints, "gauge_certificates": gauges, + "rejecting_controls": controls, "package_sha256": own, + "source_sha256": pins}, sort_keys=True)) + + +if __name__ == "__main__": + main()