diff --git a/research/dyadic-basis-conditioning/PROOF.md b/research/dyadic-basis-conditioning/PROOF.md new file mode 100644 index 0000000000..4da01c2153 --- /dev/null +++ b/research/dyadic-basis-conditioning/PROOF.md @@ -0,0 +1,125 @@ +# Optimal conditioning with a prescribed dyadic row and column + +This contribution was produced by Nick Petalas. Apache-2.0. + +Write D=Z[1/2]. Let a=(a_1,a_2) be a real dyadic row and b=(b_1,b_2)^T +a real dyadic column with ab=1. A compatible completion is R in GL_2(D) +such that aR=e_1^T and Re_1=b. Equivalently, the first column of R is b +and the first row of R^{-1} is a. The Euclidean condition number is +cond_2(R)=||R||_2 ||R^{-1}||_2. Set A=a_1^2+a_2^2 and B=b_1^2+b_2^2. +Both are positive and AB>=1 by Cauchy-Schwarz. + +## Theorem + +Every compatible completion has the unique form + + R_{k,s} = [ b, s 2^k (-a_2,a_1)^T ], k in Z, s in {1,-1}. + +Put q_k=A 2^k+B 2^{-k}. Then + + cond_2(R_{k,s}) = (q_k+sqrt(q_k^2-4))/2. + +The optimal exponents are exactly the integers satisfying + + 2^{2k-1} <= B/A <= 2^{2k+1}. + +There is one such integer except when B/A is an odd power of two, +meaning 2^{2j+1} for an integer j. In that case j and j+1 both minimize. +The sign s is free. These are all minimizers, with no hidden choice of +another basis vector. + +## Proof of the classification + +The first-column constraint writes R=[b,z]. The other constraint says az=0. +Since a is nonzero, the real kernel of a is the line spanned by +(-a_2,a_1)^T, so z=t(-a_2,a_1)^T for a unique real t. Directly, + + det R = t(a_1 b_1+a_2 b_2) = t. + +Because R is a dyadic matrix, its determinant belongs to D. Invertibility +over D requires that determinant to be a unit. The units of D are exactly +s 2^k: a dyadic number and its reciprocal both have power-of-two +denominators exactly when its reduced numerator has no odd prime factor. +Thus t=s 2^k. Conversely every displayed R has dyadic entries, unit +determinant, first column b and aR=(1,0), so it is a compatible completion. +This also proves the asserted inverse-row characterization. + +## Proof of the condition number and optimum + +Let the singular values be sigma_1>=sigma_2>0, and put c=sigma_1/sigma_2. +Their squared sum is the squared Frobenius norm B+t^2 A. Their product is +|det R|=|t|. Therefore + + c+c^{-1} = (sigma_1^2+sigma_2^2)/(sigma_1 sigma_2) + = B/|t|+A|t| = q_k. + +Solving c^2-q_k c+1=0 with c>=1 proves the formula. This expression is +strictly increasing in q>=2. Hence minimizing q suffices. Its successive +differences have the sign of A 2^{2k+1}-B, because + + q_{k+1}-q_k = A 2^k-B 2^{-k-1}. + +The differences are negative before their single sign change and positive +afterward. Comparing k with its two neighbors gives precisely the two +displayed inequalities. They cover all positive B/A, overlap only at the +stated equality boundaries, and exclude every other exponent globally. +This is an all-integer proof, rather than a bounded search. + +An exact implementation needs two candidates. Let e=floor(log_2(B/A)), +computed by bit lengths and a rational comparison. The candidates are +floor(e/2) and floor(e/2)+1. Comparing their rational q values retains all +ties and requires neither logarithmic approximation nor eigenvalue rounding. + +## Dyadic reversibility can cost more than real completion + +If R is allowed to be any real invertible matrix with the same two +constraints, its parameter t can be any nonzero real number. Arithmetic- +geometric mean gives q(t)>=2 sqrt(AB), with equality exactly when +|t|=sqrt(B/A). Its optimum condition number is therefore + + sqrt(AB)+sqrt(AB-1). + +The dyadic optimum equals that real optimum exactly when sqrt(B/A) is a +power of two. Otherwise the dyadic optimum is strictly greater. A dyadic +matrix that is merely invertible over Q need not be invertible over D; +allowing an odd determinant silently changes the arithmetic contract. + +## The source pair + +Ali Romman's PR5611 supplies a=(3,5), b=(2,-1)^T as a legal pair with no +individual unit entry in a, and gives the compatible completion +[[2,5],[-1,-3]]. That constructor and its correctness are cited, not audited. +The new optimization has A=34, B=5. At k=-1, + + R = [[2,-5/2],[-1,3/2]], det R=1/2, q=27, + cond_2(R)=(27+sqrt(725))/2. + +Indeed 1/8 < 5/34 < 1/2, so k=-1 is the unique optimal exponent. +Its two determinant signs are the only optimal completions. The cited +unit-determinant completion has q=39, so the new one is strictly better. +The unconstrained real optimum is sqrt(170)+13 and is strictly smaller +than the dyadic optimum, since 27^2>4*170. The example shows a genuine +arithmetic conditioning penalty rather than a numerical eigenvalue artifact. + +At a=(1,0), b=(1,1)^T, B/A=2. Both k=0 and k=1 minimize, with q=3. +This is an exact tie control for the optimizer. + +## Helper-interface scope + +The source dual-pair interface is the motivation and the compatible input +contract. This theorem optimizes its two-role endpoint basis, without extra +roles. For arbitrary independent complex banks of the same positive size, +R tensor I and its inverse have these same Euclidean norms and condition +number, because their Gram matrices tensor the corresponding scalar Gram +matrix with I. This is a scalar bank change, not a tensor power of R. + +Endpoint conditioning alone does not certify intermediate scalar growth, +componentwise rounded error, a gate-count optimum, a physically legal helper +cut, source delivery, dirty restoration in a complete word, frames, ownership, +stock, tape cost, compiler closure or outer funding. More workspace changes +the optimization domain. No selected assumption, complete multiplication +theorem, supplier admission or new kappa follows. The all-pair result is this +written proof; the accompanying finite checker corroborates it. Classical +two-by-two singular-value identities and dyadic-unit algebra are not claimed +as new general tools. Independent human and formal proof-kernel review are +unclaimed. diff --git a/research/dyadic-basis-conditioning/README.md b/research/dyadic-basis-conditioning/README.md new file mode 100644 index 0000000000..75deeccf87 --- /dev/null +++ b/research/dyadic-basis-conditioning/README.md @@ -0,0 +1,136 @@ +# Sharp conditioning of two-role dyadic helper completion + +This contribution was produced by Nick Petalas. Apache-2.0. + +For every dyadic row a and column b of length two with ab=1, the least +Euclidean condition number of a compatible invertible dyadic basis has an +exact formula. Write A=||a||_2^2 and B=||b||_2^2. Choose every integer k with + + 2^(2k-1) <= B/A <= 2^(2k+1). + +Then q=A*2^k+B*2^(-k), and the optimum is + + cond_2(R) = (q+sqrt(q^2-4))/2, + R = [b, ±2^k*(-a_2,a_1)^T]. + +There are at most two optimal exponents. The optimizer finds them by two +exact rational comparisons, without numerical logarithms or eigenvalues. +[PROOF.md](PROOF.md) classifies every compatible completion and proves +global optimality over all integer exponents, including ties. + +This is a scoped mathematical proof with exact finite corroboration. +It builds on the dual-pair interface of Ali Romman's merged +[PR #5611](https://github.com/CrocSwap/integer-mult-bounds/pull/5611). +That source constructs legal completions and leaves their growth and +precision costs payable. Its constructor is cited, not audited or replayed. +The new result optimizes endpoint conditioning in the two-role contract. + +For its pair a=(3,5), b=(2,-1)^T, the unique optimal determinant magnitude +is 1/2, with R=[[2,-5/2],[-1,3/2]]. The condition number is exactly +(27+sqrt(725))/2. The cited unit-determinant completion has q=39; the new +one has q=27, hence strictly smaller condition number. Real completions +without the dyadic inverse requirement reach sqrt(170)+13, strictly below +the dyadic optimum. Thus arithmetic reversibility can impose a genuine +conditioning penalty. At a=(1,0), b=(1,1)^T, both k=0 and k=1 are optimal. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/dyadic-basis-conditioning/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/dyadic-basis-conditioning/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dyadic-basis-conditioning +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dyadic-basis-conditioning --check-source-history +``` + +Other hosts may substitute their CPython 3.12 interpreter. The last command +checks the committed publication. Normal and optimized scientific commands +print `PASS_DYADIC_BASIS_CONDITIONING` and a generated SHA256-bound receipt. +The launcher prints `PASS_REGISTERED_RESEARCH_PACKAGE`. No receipt is +handwritten. The scientific verifier writes no files, imports no predecessor +code, and runs without Git or the network, including from a standalone export. + +The finite domain contains all 308 integer dual pairs with each coordinate +in [-5,5], with seven reciprocal dyadic rescalings per pair. These 2,156 +presentations are compared against 71,148 directly constructed exponent +matrices. Both determinant signs give 4,760 checked optimal representatives; +224 presentations have tied exponents. A separate second-column oracle +enumerates 56,628 literal matrices over 52 smaller dual pairs, finding 488 +compatible grid matrices and the same optima. Four size-boundary pairs and +14 rejection controls cover malformed inputs, odd denominators, size limits, +bad duality, a nonunit determinant, wrong endpoints, exponents and spectral +proxies. All checks remain active under Python optimization. These finite +counts corroborate the proof and do not replace its universal argument. + +## Scope and credit + +Scientific base is canonical main +19fdb086ea96af9a9f87936a2b888e10af4ed810, priorities revision 8. The current +selected-source binding check passed after sparse inputs were materialized. +The originating card is explicitly changed from a physical helper-inventory +construction to this endpoint precision-interface theorem. It supplies no +new productive targets or favorable complete signed moment. Discovery stopped +at this first result. [TASK.json](TASK.json) records the scope change and +[SOURCES.json](SOURCES.json) pins provenance; there are no live source inputs. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228475) +preceded substantive work. + +Credit Ali Romman #5611 for the completed dual-pair interface, its explicit +nonunit-entry pair and open growth/precision obligation; #5602 and #5599 for +the helper-splitting context and their retained P104/native/controller/compiler +lineage. Nick Petalas #5115 supplies earlier row preparation in a different +single-hub interface. The dyadic-unit classification, Cauchy-Schwarz and +two-by-two singular-value identities are classical. Their application to this +exact constrained optimum and the optimizer are the new contribution. +Predecessor files and credit lines are unchanged. Independent human and +formal proof-kernel review are unclaimed. + +Live PR lists and bodies, recent account work, handoffs, local reservations, +merged searches and distinctive all-main README searches were checked. +The cached card search had complete remote pagination but sparse local notes; +direct Git-tree searches supplemented that limit. These are bounded overlap +checks, not proof of novelty or coverage of unpublished work. + +The theorem fixes exactly two roles, real dyadic scalar coefficients, +the prescribed row and column, dyadic invertibility and the Euclidean norm. +It also applies to the same scalar basis tensored with an identity on banks. +It does not optimize extra workspace, scalar instructions, intermediate growth +or rounded error. No physical cut, frames, ownership/restoration, source access, +stock, tape, native costs, compiler, supplier admission, complete multiplication +theorem or new kappa is claimed. Lean, Docker and the selected complete cold +replay are unrun. The selected frontier is unchanged. + +## Open next questions + +- Can one actual helper cut use this optimal basis while keeping intermediate + scalar growth and the full paid/target invoice favorable? Start with its + exact two-role pair and emit a chronological scalar schedule. Physical + compatibility, rounding, restoration and the complete bill are blockers. +- What is the exact optimum with at least three prescribed helper roles? + Start with one three-coordinate dual pair. The complementary basis is no + longer a single scalar parameter, so the dyadic determinant restriction + alone does not solve the problem. No higher-dimensional optimum is claimed. + +## Executable bounds + +Build the Lever led to the reusable exact optimizer. Prove It Works led to +the separate direct-column oracle and dense Gram/inverse checks. Foundational +Thinking kept the endpoint contract as a row/column pair and separated it +from physical schedules. Power of Ten inspection covers the two new Python +files. There is no recursion, generated code, network, subprocess or callback +dispatch. Functions have at most 28 physical lines. External coordinates are +integers or Fractions with at most 64 numerator bits and 64 denominator bits +after the binary point. The optimizer's loops have at most two entries and +its powers are bounded by 260 in magnitude. The finite oracle uses fixed +domains, including at most 261 candidate exponents, 1,089 second columns +and 308 stored integer pairs. Package hashing reads seven files of at most +256 KiB each. + +Python allocation is a rule 3 managed-runtime deviation confined to this +bounded offline command. The fixed coordinate, matrix and enumeration limits +bound live data; no steady service is supplied. A lower-level runtime would +need fixed storage before widening these limits. Warning-strict normal and +optimized execution plus in-memory compilation provide local diagnostics; +no separate Python linter is available on PATH. No shared configuration or +predecessor code is changed. diff --git a/research/dyadic-basis-conditioning/SOURCES.json b/research/dyadic-basis-conditioning/SOURCES.json new file mode 100644 index 0000000000..ca2a2989e2 --- /dev/null +++ b/research/dyadic-basis-conditioning/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/dyadic-helper-basis-completion/PROOF.md", + "usage": "provenance", + "git_blob": "8c51201534aaab80b2cefe1ef12c3a1048ce3f36", + "sha256": "a909d7b909edffb5babec3e937a3d13052aeaf87852ec73a37dac9802b6d9734" + }, + { + "path": "research/dyadic-helper-basis-completion/README.md", + "usage": "provenance", + "git_blob": "595d586859ca22e488a675bb1b78985fa8157d36", + "sha256": "6eec44155e30cf8b100cfd2e6378d0dd60da1cdf496e3b88251a40018fe9bcb3" + } + ] +} diff --git a/research/dyadic-basis-conditioning/TASK.json b/research/dyadic-basis-conditioning/TASK.json new file mode 100644 index 0000000000..67177ee728 --- /dev/null +++ b/research/dyadic-basis-conditioning/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "productive helper", + "target refinement", + "5599", + "5614" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact minimum Euclidean conditioning of every two-role dyadic completion with prescribed row a and column b satisfying ab=1.", + "scope_change_reason": "The helper card is narrowed to an original endpoint precision-interface optimization prompted by the growth and precision obligation of Ali Romman PR5611; it does not construct a physical helper split.", + "bottleneck_link": "Legal helper bases still need numerical and physical budgets. This theorem gives the sharp two-role endpoint condition number and shows the extra restriction caused by a dyadic inverse. It supplies neither new targets nor a complete moment gain.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved two-role optimum and explicit improving completion; put physical scheduling and higher-dimensional optimization in Open next questions.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-pair classification and sharp optimum. verify.py checks 2156 presentations against 71148 exponent matrices, 56628 independent second-column matrices, four size-boundary pairs and fourteen rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one actual helper cut realize the optimal basis within a favorable full scalar-growth and paid/target bill?", + "why_it_matters": "Endpoint conditioning is one precision obligation; a physical gain requires the whole supplier interface.", + "first_step": "Bind one exact two-role pair and emit its chronological scalar implementation with intermediate rounding and restoration.", + "blocked_by": "No actual cut, physical schedule or complete invoice is supplied." + }, + { + "question": "What is the exact optimal Euclidean conditioning for a three-coordinate dyadic dual pair?", + "why_it_matters": "Larger helper groups have additional complementary-basis freedom absent from the two-role theorem.", + "first_step": "Specify one three-coordinate pair and characterize all compatible complementary bases over Z[1/2].", + "blocked_by": "The complement is not a scalar line; the present determinant optimization does not classify it." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228475", + "source_question": { + "pr": 5611, + "author": "aliromman", + "scope": "Coefficient-growth and precision obligation of the dyadic dual-pair basis interface." + }, + "environment": { + "python": "CPython 3.12.15", + "dependencies": "Python standard library", + "local_interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + } +} diff --git a/research/dyadic-basis-conditioning/VERIFY.json b/research/dyadic-basis-conditioning/VERIFY.json new file mode 100644 index 0000000000..10f95a4c94 --- /dev/null +++ b/research/dyadic-basis-conditioning/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Full exact dual-pair/exponent census, independent direct-column oracle, source and tie fixtures, input and semantic rejection controls, generated source-bound receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The identical complete scientific checks with optimization enabled; all failures use explicit exceptions." + } + ] +} diff --git a/research/dyadic-basis-conditioning/optimize.py b/research/dyadic-basis-conditioning/optimize.py new file mode 100644 index 0000000000..43d21dc678 --- /dev/null +++ b/research/dyadic-basis-conditioning/optimize.py @@ -0,0 +1,74 @@ +"""Exact two-role dyadic completion optimizer; no numerical eigenvalues.""" + +from fractions import Fraction + + +MAX_BITS = 64 + + +class Completion: + __slots__ = ("exponent", "q", "matrix") + + def __init__(self, exponent: int, q: Fraction, matrix: tuple): + self.exponent = exponent + self.q = q + self.matrix = matrix + + +def power_two(exponent: int) -> Fraction: + if not isinstance(exponent, int) or isinstance(exponent, bool): + raise ValueError("integer exponent required") + if not -260 <= exponent <= 260: + raise ValueError("exponent outside executable range") + if exponent >= 0: + return Fraction(1 << exponent) + return Fraction(1, 1 << -exponent) + + +def pair(values: tuple) -> tuple[Fraction, Fraction]: + if not isinstance(values, (tuple, list)) or len(values) != 2: + raise ValueError("exactly two coordinates required") + result = [] + for value in values: + if not isinstance(value, (int, Fraction)) or isinstance(value, bool): + raise ValueError("integer or Fraction coordinates required") + coordinate = Fraction(value) + denominator = coordinate.denominator + if denominator & (denominator - 1): + raise ValueError("coordinates must be dyadic") + if abs(coordinate.numerator).bit_length() > MAX_BITS: + raise ValueError("numerator exceeds executable bound") + if denominator.bit_length() - 1 > MAX_BITS: + raise ValueError("denominator exceeds executable bound") + result.append(coordinate) + return result[0], result[1] + + +def optimal_completions(a: tuple, b: tuple) -> tuple[Completion, ...]: + """Return positive-determinant representatives at every optimal exponent. + + The opposite sign of the second column gives all negative-determinant + minimizers. The proof has no bit-size limit; this executable does. + """ + row, column = pair(a), pair(b) + if sum(row[i] * column[i] for i in range(2)) != 1: + raise ValueError("the prescribed row and column must pair to one") + aa = sum(x * x for x in row) + bb = sum(x * x for x in column) + ratio = bb / aa + exponent = ratio.numerator.bit_length() - ratio.denominator.bit_length() + if ratio < power_two(exponent): + exponent -= 1 + first = exponent // 2 + candidates = [] + for k in (first, first + 1): + scale = power_two(k) + matrix = ((column[0], -scale * row[1]), + (column[1], scale * row[0])) + q = aa * scale + bb / scale + candidates.append(Completion(k, q, matrix)) + minimum = min(item.q for item in candidates) + result = tuple(item for item in candidates if item.q == minimum) + if not result or minimum < 2: + raise ArithmeticError("invalid completion invariant") + return result diff --git a/research/dyadic-basis-conditioning/verify.py b/research/dyadic-basis-conditioning/verify.py new file mode 100644 index 0000000000..9c2b235513 --- /dev/null +++ b/research/dyadic-basis-conditioning/verify.py @@ -0,0 +1,199 @@ +"""Independent finite corroboration of the written all-pair theorem.""" + +import hashlib +import itertools +import json +from fractions import Fraction as F +from pathlib import Path + +from optimize import Completion, optimal_completions, power_two + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def determinant(matrix: tuple) -> F: + return matrix[0][0] * matrix[1][1] - matrix[0][1] * matrix[1][0] + + +def gram(matrix: tuple) -> tuple: + return tuple(tuple(sum(matrix[k][i] * matrix[k][j] for k in range(2)) + for j in range(2)) for i in range(2)) + + +def unit(value: F) -> bool: + numerator = abs(value.numerator) + denominator = value.denominator + return (numerator > 0 and numerator & (numerator - 1) == 0 + and denominator & (denominator - 1) == 0) + + +def inspect_completion(a: tuple, b: tuple, item: Completion) -> F: + matrix = item.matrix + det = determinant(matrix) + require(unit(det), "nonunit completion determinant") + require(abs(det) == power_two(item.exponent), "wrong determinant exponent") + require(tuple(matrix[i][0] for i in range(2)) == b, "wrong first column") + require(tuple(sum(a[i] * matrix[i][j] for i in range(2)) + for j in range(2)) == (1, 0), "wrong prescribed row") + inverse = ((matrix[1][1] / det, -matrix[0][1] / det), + (-matrix[1][0] / det, matrix[0][0] / det)) + require(inverse[0] == a, "wrong inverse row") + for i, j in itertools.product(range(2), repeat=2): + product = sum(matrix[i][k] * inverse[k][j] for k in range(2)) + require(product == int(i == j), "inverse product") + gg = gram(matrix) + require(determinant(gg) == det * det, "Gram determinant") + q = (gg[0][0] + gg[1][1]) / abs(det) + require(q == item.q and q >= 2, "wrong spectral proxy") + return q + + +def integer_pairs(bound: int) -> tuple: + require(bound in (2, 5), "unsupported census bound") + pairs = [] + for values in itertools.product(range(-bound, bound + 1), repeat=4): + a, b = values[:2], values[2:] + if sum(a[i] * b[i] for i in range(2)) == 1: + pairs.append((tuple(map(F, a)), tuple(map(F, b)))) + return tuple(pairs) + + +def exhaustive_exponents(a: tuple, b: tuple, exponents: range) -> tuple: + scores = [] + for k in exponents: + t = F(2) ** k + matrix = ((b[0], -t * a[1]), (b[1], t * a[0])) + gg = gram(matrix) + scores.append(((gg[0][0] + gg[1][1]) / abs(determinant(matrix)), k)) + minimum = min(q for q, _ in scores) + return tuple(k for q, k in scores if q == minimum) + + +def check_pairs() -> dict: + counts = {"integer_dual_pairs": 0, "scaled_pairs": 0, + "exponent_matrices": 0, "optimal_representatives": 0, + "tied_pairs": 0} + pairs = integer_pairs(5) + counts["integer_dual_pairs"] = len(pairs) + for original_a, original_b in pairs: + for scale in range(-3, 4): + a = tuple(x * F(2) ** scale for x in original_a) + b = tuple(x / F(2) ** scale for x in original_b) + result = optimal_completions(a, b) + oracle = exhaustive_exponents(a, b, range(-16, 17)) + require(tuple(item.exponent for item in result) == oracle, + "exhaustive determinant comparison") + aa, bb = sum(x*x for x in a), sum(x*x for x in b) + for item in result: + inspect_completion(a, b, item) + require(F(2)**(2*item.exponent-1) <= bb/aa + <= F(2)**(2*item.exponent+1), "global optimality window") + opposite = tuple((row[0], -row[1]) for row in item.matrix) + inspect_completion(a, b, Completion(item.exponent, item.q, opposite)) + counts["scaled_pairs"] += 1 + counts["exponent_matrices"] += 33 + counts["optimal_representatives"] += 2 * len(result) + counts["tied_pairs"] += int(len(result) == 2) + return counts + + +def check_grid() -> dict: + pairs = integer_pairs(2) + columns = tuple(itertools.product((F(i, 4) for i in range(-16, 17)), repeat=2)) + examined, compatible = 0, 0 + for a, b in pairs: + scores = [] + for z in columns: + examined += 1 + matrix = ((b[0], z[0]), (b[1], z[1])) + det = determinant(matrix) + if sum(a[i] * z[i] for i in range(2)) != 0 or not unit(det): + continue + compatible += 1 + gg = gram(matrix) + scores.append((gg[0][0] + gg[1][1]) / abs(det)) + require(scores, "empty direct column oracle") + expected = optimal_completions(a, b) + require(min(scores) == expected[0].q, "direct second-column minimum") + for item in expected: + require(tuple(row[1] for row in item.matrix) in columns, + "optimal column absent from oracle grid") + return {"grid_pairs": len(pairs), "grid_matrices": examined, + "compatible_grid_matrices": compatible} + + +def check_fixtures() -> dict: + a, b = (F(3), F(5)), (F(2), F(-1)) + result = optimal_completions(a, b) + require(len(result) == 1, "source optimum multiplicity") + item = result[0] + require((item.exponent, item.q) == (-1, 27), "source optimum") + require(item.matrix == ((2, F(-5, 2)), (-1, F(3, 2))), "source matrix") + require(gram(item.matrix) == ((5, F(-13, 2)), (F(-13, 2), F(17, 2))), + "literal source Gram") + require(27*27 > 4*170 and 27 < 39, "strict arithmetic and baseline gaps") + tie = optimal_completions((1, 0), (1, 1)) + require(tuple(x.exponent for x in tie) == (0, 1), "exact tie") + require(all(x.q == 3 for x in tie), "tie proxy") + extremes = (((2**63, 1), (0, 1)), ((0, 1), (2**63, 1)), + ((F(1, 2**64), 1), (0, 1)), ((1, 0), (1, F(1, 2**64)))) + for row, column in extremes: + aa, bb = tuple(map(F, row)), tuple(map(F, column)) + found = optimal_completions(aa, bb) + require(tuple(x.exponent for x in found) + == exhaustive_exponents(aa, bb, range(-130, 131)), "size boundary") + for candidate in found: + inspect_completion(aa, bb, candidate) + return {"source_q": 27, "cited_completion_q": 39, + "tie_exponents": [0, 1], "size_boundary_pairs": len(extremes)} + + +def check_controls() -> int: + invalid = (((1,), (1, 0)), ((0, 0), (0, 0)), ((1, 0), (0, 1)), + ((F(1, 3), 1), (0, 1)), ((1, 0), (1, F(1, 3))), + ((2**64, 1), (0, 1)), ((1, 0), (1, F(1, 2**65))), + ((True, 0), (1, 0)), ((1.0, 0), (1, 0)), (None, (1, 0))) + count = 0 + for a, b in invalid: + try: + optimal_completions(a, b) + except ValueError: + count += 1 + else: + raise ValueError("invalid dual pair accepted") + a, b = (F(3), F(5)), (F(2), F(-1)) + corrupt = (Completion(-1, F(26), ((2, F(-5, 2)), (-1, F(3, 2)))), + Completion(0, F(27), ((2, F(-5, 2)), (-1, F(3, 2)))), + Completion(0, F(39), ((2, 5), (1, -3))), + Completion(0, F(1), ((2, -15), (-1, 9)))) + for item in corrupt: + try: + inspect_completion(a, b, item) + except ValueError: + count += 1 + else: + raise ValueError("corrupted completion accepted") + return count + + +def main() -> None: + counts = check_pairs() | check_grid() | check_fixtures() + counts["rejected_controls"] = check_controls() + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "optimize.py", "verify.py") + hashes = {} + for name in names: + require((package / name).stat().st_size <= 262144, "source file too large") + data = (package / name).read_bytes() + require(len(data) <= 262144, "package source exceeds hash bound") + hashes[name] = hashlib.sha256(data).hexdigest() + print(json.dumps({"counts": counts, "sha256": hashes}, sort_keys=True)) + print("PASS_DYADIC_BASIS_CONDITIONING") + + +if __name__ == "__main__": + main()