diff --git a/research/joint-gaussian-transition-floor/PROOF.md b/research/joint-gaussian-transition-floor/PROOF.md new file mode 100644 index 0000000000..870ce16fa2 --- /dev/null +++ b/research/joint-gaussian-transition-floor/PROOF.md @@ -0,0 +1,147 @@ +# Exact joint transition cost + +This proof was produced by Nick Petalas. Apache-2.0. + +## Contract and theorem + +Take any finite number h of independent complex helpers. Write helper j as +two real coordinates and prescribe multiplication by + +`g_j = 2^(a_j) (1 + epsilon_j i)^(b_j)`, + +where a_j is any integer, b_j belongs to {0,1}, and epsilon_j belongs to +{-1,1}. The complete required real map is block diagonal, with blocks + +`T_j = 2^a [[1, -epsilon*b], [epsilon*b, 1]]`. + +Any finite number of extra real registers may contain arbitrary independent +dirty inputs. They must return exactly unchanged, without leaking into or +receiving data from the helpers at exit. Thus the complete endpoint is +`T = diag(T_1,...,T_h,I_dirty)` on every real input. + +The charged elementary operations are signed unit ADDs `x_r += +/- x_s` +with r != s, and individual doublings or halvings. Each costs one. Coordinate +permutations and negations are granted free. Every operation may connect any +two registers, including workspace. No other scalar coefficients, constants, +COPY, clear, nonlinear operation, or larger native map is free. + +Every implementing word needs at least + +`S = sum_j |2a_j+b_j|` doublings/halvings, and +`A = 2 sum_j b_j` signed ADDs. + +One explicit word attains both bounds simultaneously. Consequently its exact +minimum total charge is `S+A`, even with arbitrary cross-helper mixing and +any finite restored dirty workspace. The inverse endpoint has exactly the +same two minima. + +This answers the pure joint-transition question of Sagar Thakrar's PR1566. +It does not price a transition fused with a different surrounding operation. + +## A lattice-index distance counts scales + +For two full rational lattices L,M in Q^n, define + +`d(L,M) = log_2([L:L intersect M] [M:L intersect M])`. + +All these indices are finite. Applying the same invertible rational map to +both lattices preserves them. Also d satisfies the triangle inequality. +Indeed, for a third lattice N, + +`[L:L intersect N] <= [L:L intersect M] [M:M intersect N]`. + +To see this, insert the smaller subgroup L intersect M intersect N, split +its index at L intersect M, and inject the latter quotient into +M/(M intersect N). Apply the same inequality with L and N exchanged and +multiply the two bounds. Taking logarithms proves the triangle inequality. +This is a standard lattice-index argument, not a claimed new metric. + +Let Z denote Z^n and let P be the current rational matrix. A next gate G +satisfies + +`d(GPZ,Z) <= d(GPZ,GZ) + d(GZ,Z) = d(PZ,Z) + d(GZ,Z)`. + +A signed ADD, permutation or negation maps Z onto itself and has last term +zero. A single doubling or halving has last term one. Starting from P=I +therefore gives + +`number of scales >= d(TZ,Z)`. + +This uses a distance between lattices, rather than the absolute valuation of +the determinant. Opposite expansions and contractions cannot cancel it. + +For b=0, the two-coordinate block lattice is 2^a Z^2. Its distance from +Z^2 is 2|a|. For b=1 put + +`B_epsilon = [[1,-epsilon],[epsilon,1]]`, +`B_epsilon^-1 = (1/2) [[1,epsilon],[-epsilon,1]]`. + +If a >= 0, `2^a B_epsilon Z^2` lies inside Z^2 with index +`2^(2a+1)`. If a <= -1, its inverse matrix is integral, so the block lattice +contains Z^2, with index in the opposite direction `2^(-2a-1)`. +In either case the distance is |2a+1|. Intersections of direct-product +lattices are direct products and their indices multiply. Restored dirty +registers contribute zero. Hence `d(TZ,Z)=S` as asserted. + +## Row support counts ADDs + +Call a row mixed when it has at least two nonzero entries. The initial +identity has no mixed rows. A doubling, halving, negation or coordinate +permutation preserves the number of mixed rows. A signed ADD changes only +one row and can increase that number by at most one. At the required +endpoint exactly the two rows of each b=1 block are mixed; the other helper +and dirty rows each have support one. Thus every word needs at least A ADDs. + +This argument remains valid when temporary rows have large support, when +mixing is undone, and when arbitrary dirty registers are used. The scale +and ADD arguments apply to disjoint charged gate types, so their bounds add. + +## Simultaneous attainment + +For b=0, scale both coordinates by 2^a, using 2|a| individual scales. +For b=1 and a >= 0, the three operations + +```text +x -= epsilon*y +y *= 2 +y += epsilon*x +``` + +produce `(x-epsilon*y, epsilon*x+y)`. Scale both outputs by 2^a. +There are two ADDs and 2a+1 scales. + +For b=1 and a <= -1, instead use + +```text +x -= epsilon*y +x /= 2 +y += epsilon*x +``` + +This produces half of that same block. Scale both outputs by 2^(a+1). +There are two ADDs and -2a-1 scales. Execute these words independently on +all helpers and leave all workspace unchanged. They attain S and A. + +The inverse of a b=0 block replaces a by -a. The inverse of a b=1 block +replaces `(a,epsilon)` by `(-a-1,-epsilon)`. This stays in the stated +family and preserves |2a+b| and b, proving the inverse claim. + +## The requested reciprocal boundary + +For `(g_1,g_2) = (1+i, (1+i)^-1)`, the parameters are +`(a,b,epsilon)=(0,1,1),(-1,1,-1)`. Thus S=2, A=4 and the exact cost is +six. The determinant of the combined four-coordinate map is one, so its +determinant valuation alone gives zero. The lattice distance is two. +Arbitrary dirty workspace cannot lower six; a separately required return +costs six more. This is a boundary cost, not a lower bound on a fused round +trip whose only required endpoint is the identity. + +## Scope of the conclusion + +The quantified result is this written proof; finite software checks are +corroboration. General unit phases beyond the stated conjugate family, +nonunit odd coefficients, singular clean workspace, COPY/clear, alternative +native primitives and endpoints fused with an original SCALE or ADD require +separate analysis. Physical routing, precision, coefficient production, +compiler admission, productive targets and recursive costs are not supplied. +No new kappa or complete multiplication theorem is claimed. diff --git a/research/joint-gaussian-transition-floor/README.md b/research/joint-gaussian-transition-floor/README.md new file mode 100644 index 0000000000..9090119a12 --- /dev/null +++ b/research/joint-gaussian-transition-floor/README.md @@ -0,0 +1,140 @@ +# Joint Gaussian transitions cannot cancel their scale charges + +This contribution was produced by Nick Petalas. Apache-2.0. + +For any finite set of complex helpers, prescribe multiplication of helper j +by `2^(a_j) (1+epsilon_j*i)^(b_j)`, where a_j is an integer, b_j is zero or +one, and epsilon_j is either sign. Permit arbitrary signed unit ADDs between +any real coordinates, doublings and halvings, with free permutations and +negations and any finite amount of restored dirty workspace. The exact +minimum is + +```text +doublings/halvings = sum_j |2a_j+b_j| +signed ADDs = 2 sum_j b_j +total = their sum +``` + +Both lower bounds are attained by the same word, and apply separately to +its inverse. This is a **scoped proof with exact finite corroboration**. +It answers Open next question 2 of Sagar Thakrar's +[PR #1566](https://github.com/CrocSwap/integer-mult-bounds/pull/1566), which +leaves joint Gaussian transitions outside its separate-transition theorem. +The new result is the joint lower bound; the standalone transition words and +Gaussian-gauge setting retain their predecessor credit. + +In particular, the requested reciprocal pair `(1+i), (1+i)^-1` costs exactly +six primitives, comprising four ADDs and two scales. Its determinant is one. +Using only the total determinant valuation would miss both necessary scales. +The same endpoint cost applies to the return; a round trip with no required +intermediate boundary can of course be the empty word. + +## Proof and finite evidence + +[PROOF.md](PROOF.md) uses the classical index distance between rational +lattices. A signed ADD preserves the integer lattice; a scale changes the +distance by at most one. The final block-product distance adds the absolute +block valuations, including opposite signs. Separately, each odd Gaussian +block needs two mixed rows and every ADD can create at most one. Explicit +three-operation words plus scalar powers attain both bounds. The proof +covers all integer exponents, helper counts and finite restored dirty +workspace. It does not depend on a finite search or a predecessor replay. + +The standalone verifier checks exact rational matrices, all-input inverse +restoration and literal primitive counts. A separate finite quotient enumerates +the lattice intersections directly. Short arbitrary words test both invariants +on endpoints outside the target family. Controls remove a scale or ADD, +change the conjugate, leave workspace unrestored, or violate the input domain. +The fixed run checks 1,011 attaining endpoints, 42 finite lattices, 216 lattice +triangles, all 4,681 short words and 14 rejecting controls. The largest +checked attaining word has eighteen gates. Counts come from enumeration; +the universal theorem comes from the written proof. +[RESULT.json](RESULT.json) is generated by the verifier and binds every other +package file by SHA256; default replay compares the entire generated result. + +## Reproduction + +From the repository root, CPython 3.12 and its standard library suffice: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/joint-gaussian-transition-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/joint-gaussian-transition-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/joint-gaussian-transition-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/joint-gaussian-transition-floor --check-source-history +``` + +Other machines may substitute their CPython 3.12 interpreter. Expected marker +is `PASS_JOINT_GAUSSIAN_TRANSITION_FLOOR no_new_kappa`. Both normal and +optimized checks are registered with a 120-second timeout. To regenerate +the receipt without changing package files, add `--emit-result` and redirect +stdout to an external file. No Git, network, solver or imported predecessor +code is needed by the scientific verifier. SOURCES.json pins the predecessor +README, catalogue and selected record as historical provenance at canonical +main `19fdb086ea96af9a9f87936a2b888e10af4ed810`; there are no live inputs. + +## Scope and implementation limits + +The `complex-new-helper-inventory` card is explicitly changed to this scalar +compiler side question. The selected baseline binding control passed; this +was orientation, not a scientific selected replay. Pure joint transitions +cannot evade the stated charge through cross-helper determinant cancellation. +The result stops here; it does not justify more gauge searches in this class. + +General phases outside the conjugate family, nonunit odd coefficients, +clean initialized workspace with singular operations, COPY/clear and fused +non-block-diagonal endpoints are outside scope. So are rounding, routing, +coefficient production, physical ownership, native admission, full-word +scalar optimization, complete paid profiles, compiler/stock/outer premises +and a complete multiplication theorem. No new kappa or selected-frontier +change is claimed. Independent human and formal proof-kernel review are +unclaimed. No Lean, Docker or selected cold replay was run. + +The finite checker allows at most four helpers, four extra real coordinates, +dimension twelve and even-block exponents from -8 through 8. Odd-block +exponents run from -8 through 7, a domain closed under inversion. Stored words +are capped at 256 gates; the fixed tests use a smaller domain. The lattice +enumerator uses at most 4^4 residue points, and the short-word census uses +eight gates through length four. There is no recursion, subprocess, network, +dynamic code evaluation or shared mutable output. Functions fit in 60 lines. +Input receipts and each source file are capped at one MiB. + +Power of Ten rule 3 has a managed-runtime deviation in verify.py. Python +allocates exact integers, fractions, lists and sets during this offline +finite check. The preceding enforced bounds cap all live data; only one +case or short word is processed at a time. Warning-strict normal and +optimized replays check the same bounded path. A fixed-buffer implementation +would be required if allocation guarantees become a caller requirement. +Rule 9 has the corresponding standard-library arithmetic-dispatch deviation, +limited to integers and Fractions with visible direct calls. No separate +static type checker or linter is a dependency; warning-strict execution is +registered in CI. No shared build settings are changed. + +Local execution used CPython 3.12.15 on macOS 27.0.1 arm64. Hosted replay +and source-history availability are separate publication checks. + +## Open next questions + +Can a transition fused with an actual signed SCALE or ADD beat the complete +corresponding real-gauge invoice? This would change the pure block-diagonal +endpoint, which is the boundary of this proof. Start with one literal +surrounding operation, its complete dirty-input map and an attaining word. +A source-bound fused endpoint and complete caller invoice remain missing. +The same question and blockers are recorded in TASK.json. + +## Credit and coordination + +Sagar Thakrar / thakrarsagar supplies PR1566's temporal-gauge setting, +standalone bounds and explicit joint-transition question. Hanson Sun / +bbMisk's PR1490 supplies the static Gaussian common-rounding argument and +unit classification. PR1259/1380 and the scalar PR696 lowerer retain their +temporal and coefficient lineage. The lattice-index argument, row-support +count and elementary butterfly identities are classical methods; only their +joint arbitrary-dirty-workspace consequence for this interface is claimed +here. No predecessor result is audited or reverified. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19227539) +followed live PR/Discussion and batch reservations, searches of main READMEs, +merged-PR searches and recent account contributions. The cached scan covered +377 open PRs and 5,597 Discussion records with complete remote pagination; +sparse local notes and unsearched diffs limit that coverage. No literature-wide +novelty or acceptance is inferred from it. diff --git a/research/joint-gaussian-transition-floor/RESULT.json b/research/joint-gaussian-transition-floor/RESULT.json new file mode 100644 index 0000000000..92d0994a3c --- /dev/null +++ b/research/joint-gaussian-transition-floor/RESULT.json @@ -0,0 +1,22 @@ +{ + "attaining_cases": 1011, + "claim_type": "scoped proof with exact finite corroboration", + "finite_lattices": 42, + "lattice_triangles": 216, + "maximum_checked_word_length": 18, + "reciprocal_pair": { + "adds": 4, + "scales": 2, + "total": 6 + }, + "rejecting_controls": 14, + "short_words": 4681, + "source_sha256": { + "PROOF.md": "e2e2f759f99f43b3be361f0c603c4491a6d685940f390e114ff816a2a730dec9", + "README.md": "29c75fd37cb4a32287bf51f5b834c06019e2182417f053e9e1c59c705ff2b4da", + "SOURCES.json": "8c9df4284591c98f29881ef2b36c75cffe38e3bbaa934c07a0804cabac85937b", + "TASK.json": "f76f4f99f94baeb2eb2f9ebc9b3a9e026a2d996de08a4bb902487e4cba5aa6ca", + "VERIFY.json": "6eccb9abad76892b8ac6e50f94daea8da558fbd19a0d2d0f663d1f10978b78b7", + "verify.py": "f5b60c589e6522997d24e1f2a51d7c360fd1d48d975f9aee294e719a64de7915" + } +} diff --git a/research/joint-gaussian-transition-floor/SOURCES.json b/research/joint-gaussian-transition-floor/SOURCES.json new file mode 100644 index 0000000000..fdc292ffe5 --- /dev/null +++ b/research/joint-gaussian-transition-floor/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/temporal-gaussian-rounding-seed22/README.md", + "usage": "provenance", + "git_blob": "aec4f45e0ff936fce434c3293670ecbfdcfdd4c9", + "sha256": "49f0bf08574a36e2810bcbea99ab60d3550cd043f8c2f0339fbe5a1780bed4cf" + } + ] +} diff --git a/research/joint-gaussian-transition-floor/TASK.json b/research/joint-gaussian-transition-floor/TASK.json new file mode 100644 index 0000000000..875a4aa73b --- /dev/null +++ b/research/joint-gaussian-transition-floor/TASK.json @@ -0,0 +1,74 @@ +{ + "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 primitive cost of joint block-diagonal Gaussian-dyadic gauge transitions with arbitrary restored dirty workspace.", + "scope_change_reason": "PR1566 Open next question 2 asks whether joint transitions evade its separately charged transition bound. This is a scalar compiler side result rather than a changed paid helper inventory.", + "bottleneck_link": "Closes the proposed cross-helper cancellation of Gaussian transition charges in the stated elementary alphabet. It does not change a recursive paid profile or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified joint-transition obstruction and package it; no surrounding-word optimization.", + "outcome": "negative-result", + "evidence": "PROOF.md exact all-parameter lower and upper bounds; verify.py exact attaining words, finite lattice-index checks and controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a Gaussian transition fused with an actual signed SCALE or ADD beat the separately charged complete boundary?", + "why_it_matters": "The exact result covers a pure block-diagonal transition, so only a changed endpoint can evade it.", + "first_step": "Name one literal surrounding operation and its joint endpoint; compare a complete attaining word with the corresponding real-gauge alternative.", + "blocked_by": "An actual source-bound fused endpoint and full invoice are missing." + } + ] +} diff --git a/research/joint-gaussian-transition-floor/VERIFY.json b/research/joint-gaussian-transition-floor/VERIFY.json new file mode 100644 index 0000000000..22ca8f749b --- /dev/null +++ b/research/joint-gaussian-transition-floor/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": "Exact joint endpoints, inverse restoration, lattice-index and mixed-row lower bounds, exhaustive short words and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete check with optimized Python; acceptance uses explicit exceptions." + } + ] +} diff --git a/research/joint-gaussian-transition-floor/verify.py b/research/joint-gaussian-transition-floor/verify.py new file mode 100644 index 0000000000..bb7d8c6437 --- /dev/null +++ b/research/joint-gaussian-transition-floor/verify.py @@ -0,0 +1,270 @@ +#!/usr/bin/env python3 +"""Joint Gaussian transition checks. Produced by Nick Petalas. Apache-2.0.""" +from fractions import Fraction as F +from hashlib import sha256 +from itertools import product +from math import gcd +from pathlib import Path +import json +import sys + +ROOT = Path(__file__).resolve().parent +SOURCE_NAMES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") +MAX_DIM = 12 +MAX_WORD = 256 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + need(type(n) is int and 1 <= n <= MAX_DIM, "matrix dimension") + return [[F(i == j) for j in range(n)] for i in range(n)] + + +def validate(specs, dirty): + need(type(dirty) is int and 0 <= dirty <= 4, "dirty workspace bound") + need(1 <= len(specs) <= 4 and 2 * len(specs) + dirty <= MAX_DIM, "helper bound") + for a, b, epsilon in specs: + need(type(a) is int and -8 <= a <= 8, "finite verifier exponent bound") + need(type(b) is int and b in (0, 1), "Gaussian parity") + need(b == 0 or a <= 7, "odd-block domain closed under inverse") + need(type(epsilon) is int and epsilon in (-1, 1), "conjugation sign") + + +def endpoint(specs, dirty=0): + validate(specs, dirty) + matrix = identity(2 * len(specs) + dirty) + for j, (a, b, epsilon) in enumerate(specs): + x, y = 2 * j, 2 * j + 1 + scale = F(2) ** a + matrix[x][x] = matrix[y][y] = scale + matrix[x][y] = -epsilon * b * scale + matrix[y][x] = epsilon * b * scale + return matrix + + +def recipe(specs, dirty=0): + validate(specs, dirty) + word = [] + for j, (a, b, epsilon) in enumerate(specs): + x, y = 2 * j, 2 * j + 1 + residual = a + if b: + word.append(("add", x, y, -epsilon)) + word.append(("scale", y if a >= 0 else x, 1 if a >= 0 else -1)) + word.append(("add", y, x, epsilon)) + residual = a if a >= 0 else a + 1 + for coordinate in (x, y): + for _ in range(abs(residual)): + word.append(("scale", coordinate, 1 if residual > 0 else -1)) + need(len(word) <= MAX_WORD, "word capacity") + return word + + +def execute(word, matrix): + need(len(word) <= MAX_WORD, "word capacity") + n = len(matrix) + need(1 <= n <= MAX_DIM and all(len(row) == n for row in matrix), "square matrix") + rows = [row[:] for row in matrix] + for gate in word: + if gate[0] == "add": + _, destination, source, sign = gate + need(0 <= destination < n and 0 <= source < n and destination != source, "ADD roles") + need(sign in (-1, 1), "signed unit ADD") + rows[destination] = [x + sign * y for x, y in zip(rows[destination], rows[source])] + else: + need(gate[0] == "scale" and len(gate) == 3, "gate alphabet") + _, destination, exponent = gate + need(0 <= destination < n and exponent in (-1, 1), "unit scale") + rows[destination] = [x * F(2) ** exponent for x in rows[destination]] + return rows + + +def inverse_word(word): + return [gate[:-1] + (-gate[-1],) for gate in reversed(word)] + + +def inverse_specs(specs): + return [(-a - b, b, -epsilon) for a, b, epsilon in specs] + + +def floors(specs): + return sum(abs(2 * a + b) for a, b, _ in specs), 2 * sum(b for _, b, _ in specs) + + +def counts(word): + return sum(g[0] == "scale" for g in word), sum(g[0] == "add" for g in word) + + +def require_budget(specs, scales, adds): + scale_floor, add_floor = floors(specs) + need(scales >= scale_floor and adds >= add_floor, "insufficient transition budget") + + +def mixed_rows(matrix): + return sum(sum(x != 0 for x in row) >= 2 for row in matrix) + + +def check_case(specs, dirty): + target = endpoint(specs, dirty) + word = recipe(specs, dirty) + n = len(target) + need(execute(word, identity(n)) == target, "literal attaining endpoint") + need(counts(word) == floors(specs), "simultaneous scale and ADD optimum") + need(mixed_rows(target) == floors(specs)[1], "mixed-row lower bound") + need(execute(inverse_word(word), target) == identity(n), "all-input inverse restoration") + need(execute(recipe(inverse_specs(specs), dirty), target) == identity(n), "separate inverse recipe") + return len(word) + + +def power_log(value): + need(type(value) is int and value > 0 and value & (value - 1) == 0, "positive power of two") + return value.bit_length() - 1 + + +def finite_lattice(specs): + """Enumerate L/(2 Z^n) inside ((1/2) Z^n)/(2 Z^n).""" + n = 2 * len(specs) + need(1 <= len(specs) <= 2 and all(a in (-1, 0) for a, _, _ in specs), "finite lattice domain") + matrix = endpoint(specs) + inv = endpoint(inverse_specs(specs)) + need(all((2 * x).denominator == 1 for row in matrix for x in row), "L below half-grid") + need(all((2 * x).denominator == 1 for row in inv for x in row), "L contains twice-grid") + elements, integers = set(), set() + for point in product(range(4), repeat=n): + if all(v % 2 == 0 for v in point): + integers.add(point) + preimage = [sum(row[j] * F(point[j], 2) for j in range(n)) for row in inv] + if all(x.denominator == 1 for x in preimage): + elements.add(point) + return elements, integers + + +def distance(left, right): + common = len(left & right) + need(common > 0 and len(left) % common == 0 and len(right) % common == 0, "lattice indices") + return power_log(len(left) // common) + power_log(len(right) // common) + + +def lattice_checks(): + types = [(a, b, e) for a in (-1, 0) for b in (0, 1) for e in ((1,) if b == 0 else (-1, 1))] + checked = 0 + for helpers in (1, 2): + for specs in product(types, repeat=helpers): + lattice, integers = finite_lattice(specs) + need(distance(lattice, integers) == floors(specs)[0], "enumerated lattice floor") + checked += 1 + one = [finite_lattice((spec,))[0] for spec in types] + triangles = 0 + for left, middle, right in product(one, repeat=3): + need(distance(left, right) <= distance(left, middle) + distance(middle, right), "triangle inequality") + triangles += 1 + return checked, triangles + + +def two_dimensional_distance(matrix): + """Classical 2x2 Smith invariants, only for short-word controls.""" + denominator = max(x.denominator for row in matrix for x in row) + integers = [int(x * denominator) for row in matrix for x in row] + divisor = gcd(*integers) + determinant = abs(integers[0] * integers[3] - integers[1] * integers[2]) + first = power_log(divisor) - power_log(denominator) + second = power_log(determinant // divisor) - power_log(denominator) + return abs(first) + abs(second) + + +def short_word_checks(): + alphabet = [("add", i, 1 - i, e) for i in range(2) for e in (-1, 1)] + alphabet += [("scale", i, e) for i in range(2) for e in (-1, 1)] + checked = 0 + for length in range(5): + for word in product(alphabet, repeat=length): + matrix = execute(word, identity(2)) + scales, adds = counts(word) + need(two_dimensional_distance(matrix) <= scales, "arbitrary short-word scale floor") + need(mixed_rows(matrix) <= adds, "arbitrary short-word ADD floor") + checked += 1 + return checked + + +def rejection_checks(): + rejected = 0 + invalid = [([(0, 2, 1)], 0), ([(0, 1, 0)], 0), ([(F(1, 2), 1, 1)], 0), + ([(9, 1, 1)], 0), ([(8, 1, 1)], 0), + ([(0, 1, 1)], -1), ([(0, 1, 1)] * 5, 0)] + for specs, dirty in invalid: + try: + recipe(specs, dirty) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid boundary accepted") + pair = [(0, 1, 1), (-1, 1, -1)] + word, target = recipe(pair, 1), endpoint(pair, 1) + need(floors(pair) == (2, 4), "reciprocal six-call fixture") + need(abs(sum(2 * a + b for a, b, _ in pair)) == 0, "determinant-cancellation control") + mutants = [word[1:], word[:-1], word + [("add", 4, 0, 1)], + recipe([(0, 1, 1), (-1, 1, 1)], 1)] + for mutant in mutants: + need(execute(mutant, identity(5)) != target, "bad endpoint must reject") + rejected += 1 + for scales, adds in ((0, 4), (1, 4), (2, 3)): + try: + require_budget(pair, scales, adds) + except ValueError: + rejected += 1 + else: + raise ValueError("false resource budget accepted") + return rejected + + +def source_hashes(): + result = {} + for name in SOURCE_NAMES: + data = (ROOT / name).read_bytes() + need(len(data) <= 1024 * 1024, "source size bound") + result[name] = sha256(data).hexdigest() + return result + + +def scientific_result(): + types = [(a, b, e) for a in range(-3, 4) for b in (0, 1) for e in ((1,) if b == 0 else (-1, 1))] + cases, largest = 0, 0 + for helpers in (1, 2): + for specs in product(types, repeat=helpers): + for dirty in (0, 2): + largest = max(largest, check_case(specs, dirty)) + cases += 1 + for specs in product(((-1, 1, -1), (0, 1, 1), (1, 0, 1)), repeat=4): + largest = max(largest, check_case(specs, 2)) + cases += 1 + boundaries = [(-8, 0, 1), (8, 0, 1), (-8, 1, -1), (-8, 1, 1), (7, 1, -1), (7, 1, 1)] + for spec in boundaries: + largest = max(largest, check_case((spec,), 4)) + cases += 1 + lattices, triangles = lattice_checks() + return {"claim_type": "scoped proof with exact finite corroboration", "attaining_cases": cases, + "maximum_checked_word_length": largest, "finite_lattices": lattices, + "lattice_triangles": triangles, "short_words": short_word_checks(), + "rejecting_controls": rejection_checks(), "reciprocal_pair": {"scales": 2, "adds": 4, "total": 6}, + "source_sha256": source_hashes()} + + +def main(): + need(sys.argv[1:] in ([], ["--emit-result"]), "only --emit-result is supported") + result = scientific_result() + if sys.argv[1:]: + print(json.dumps(result, sort_keys=True, indent=2)) + return + raw = (ROOT / "RESULT.json").read_bytes() + need(len(raw) <= 1024 * 1024, "receipt size bound") + need(json.dumps(result, sort_keys=True) == json.dumps(json.loads(raw), sort_keys=True), "complete generated receipt") + print(json.dumps(result, sort_keys=True)) + print("PASS_JOINT_GAUSSIAN_TRANSITION_FLOOR no_new_kappa") + + +if __name__ == "__main__": + main()