diff --git a/research/terminal-approximation-floor/PROOF.md b/research/terminal-approximation-floor/PROOF.md new file mode 100644 index 0000000000..91165052d5 --- /dev/null +++ b/research/terminal-approximation-floor/PROOF.md @@ -0,0 +1,132 @@ +# A robust scalar-ADD floor for two-stage terminal codes + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped proof, conditional on the cited physical-code identity. +Independent human and formal proof-kernel review are unclaimed. + +## Contract and cited premise + +Use Cinna Davis's [PR5065 proof](../two-stage-coded-terminal/PROOF.md), +building on Dillon's PR4933 and Dugongue's PR4929. Its exact marker identity +is a premise here. We do not re-establish or independently validate it. + +For two distinct stage blocks and signs epsilon, eta in {+1,-1}, write + +```text +J_f = Q_f^-1 C_t,f^epsilon C_s,f^eta Q_f, +m = number of negative signs, +alpha_m = 1/(8*13^m), +R_f = 4^(f-1). +``` + +The cited proof restricts input digit column one to address zero and output +digit column one to address 2048, inside owner block (0,1). The resulting +submatrix is `-i alpha_m N^(tensor(f-1))`. Row zero of N has precisely the +four entries `(1,-i,i,1)/2`, on inputs `(0,1,16,17)`. Consequently the selected +row in the restriction has exactly R_f nonzeros, all of modulus +`alpha_m/sqrt(R_f)`, and squared Euclidean norm `alpha_m^2`. + +The row statement follows directly by tensoring the cited row. It needs no +new code census or assumption that an owner-coefficient sum is tensorized. + +The approximation model is a linear straight-line program using whole-field +scalar ADD/SCALE, monomial address maps and owned COPY/CLEAR. Its scalars may +be arbitrary complex numbers. It may use dirty helpers and owned scratch; +all arbitrary inputs are included as independent coordinates of its linear +map. Count every scalar ADD. No Gaussian transform, dense free linear map, +nonlinear rounding, intermediate measurement or free coordinate projection +is part of the alphabet. The projections above are proof devices only. + +Let A_f denote the program's designated output map. Compare it with J_f on +the required bank coordinates, extended by zero coefficients on independent +scratch inputs. The norm below is the induced Euclidean operator norm. In +particular, the claim concerns a uniform linear approximation on arbitrary +inputs, not accuracy at a finite list of test inputs. + +## The quantitative bound + +For every integer f >= 1 and every such program using g >= 0 ADDs, + +```text +||A_f - J_f||_(2->2)^2 + >= alpha_m^2 max(0, 1 - 2^g/R_f). (1) +``` + +Initially each scalar state coordinate depends on at most one independent +input coordinate. A monomial permutes those coordinates and multiplies them +by scalars; SCALE preserves their support; COPY and CLEAR cannot enlarge the +maximum support. One ADD forms a union of two supports, and hence at most +doubles that maximum. After g ADDs, every output row has support at most +2^g. Arbitrary coefficients, cancellations and dirty scratch do not invalidate +this upper bound. + +Restrict A_f to the same input and output coordinates used in the cited +marker identity. A row restriction cannot increase its support. If 2^g=R_f, nonnegativity proves (1). +This also covers f=1, where the displayed lower bound is zero. + +The sparse-row inequality used here is sharp: retain any s of the R_f exact +target coefficients, and set all other coefficients to zero. Its squared +error is exactly alpha_m^2(1-s/R_f). This is sharpness of the row argument. +It does not construct a full decoder or prove attainability of (1) by a word. + +## A fixed positive tolerance preserves the exact floor + +For f>=2, suppose g<2(f-1). Integrality gives +`2^g <= R_f/2`. Therefore (1) implies + +```text +||A_f-J_f||_(2->2) >= alpha_m/sqrt(2). (2) +``` + +Every error tolerance strictly less than alpha_m/sqrt(2), including +alpha_m/2, forces `g>=2(f-1)`. The strict endpoint matters: (2) does not +exclude equality at alpha_m/sqrt(2). For f=1, the ADD floor is zero. + +The actual negative banks 0 and 8 in the cited proof have terminal codes +`C_32 C_31^-1` and `C_1^-1 C_0`. Their unique exact postdecoders reverse +the factors and invert them, so each still has exactly one negative sign. +For both actual postdecoder targets, m=1 and alpha_m=1/104. Thus even the +relaxed requirement + +```text +||A_f - required_postdecoder_f||_(2->2) <= 1/208 +``` + +requires at least `2(f-1)` ADDs at every positive width. This is the same +ADD floor previously available only for exact decoding. + +For any fixed g, (1) also gives +`liminf_(f->infinity) ||A_f-J_f||_(2->2) >= alpha_m`. +The program and its scalar coefficients may vary with f while its ADD budget +stays fixed. Thus even width-dependent coefficients cannot supply a uniform +linear approximation with error bounded strictly below 1/104 for the two +actual postdecoders. The liminf assertion is a lower bound, not an optimum. + +## Scope and evidence + +The new step is (1), its quantitative tolerance and its actual-bank +specialization. The marker identity, physical bank labels and exact support +obstruction retain Cinna Davis's credit. Dillon, Dugongue, JoyboyBrian, +Cao Yifan, zxv, Jacob Alan Sussman, Ryanson Jonathan and the retained +native/controller/compiler lineage retain their predecessor credit. + +The exact verifier checks the new sparse-row inequality using every support +through sixteen columns, Gaussian coefficient perturbations, bounded tensor +rows and integer corollary comparisons. These are finite corroboration of +the written proof. It authenticates, but never executes, the cited predecessor +proof. No predecessor result is audited or recertified by this contribution. + +We do not prove a paid Gaussian decoder minimum, a bound for nonlinear rounded +programs, a relative error bound for the entire terminal operator, or a whole +controller obstruction. A changed entrance/exit, recursive job family or +operation alphabet requires a different argument. Physical precision, storage, +routing, native all-column correctness, compiler and outer admission remain +inherited or unresolved. The selected frontier is unchanged. diff --git a/research/terminal-approximation-floor/README.md b/research/terminal-approximation-floor/README.md new file mode 100644 index 0000000000..47276528f7 --- /dev/null +++ b/research/terminal-approximation-floor/README.md @@ -0,0 +1,121 @@ +# Approximate terminal decoding still needs growing scalar work + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped proof with finite exact corroboration. Independent human +and formal proof-kernel review are unclaimed. + +For the two-stage inverse postdecoder targets in the actual negative banks +0 and 8 of Dillon's PR4933, **Euclidean operator error at most `1/208` still +requires at least `2(f-1)` scalar ADDs** at every positive digit-column width f. +Cinna Davis's [PR5065](../two-stage-coded-terminal/README.md) proved this +floor for exact decoding. The new result makes that obstruction quantitative +for uniform linear approximation, using the same operation alphabet. + +For all four forward/inverse sign choices, let m be the number of inverse +factors, alpha=1/(8*13^m) and R=4^(f-1). Every linear scalar/monomial program +using g ADDs obeys + +```text +||approximation - terminal_operator||_(2->2)^2 + >= alpha^2 max(0, 1 - 2^g/R). +``` + +For the actual inverse postdecoder targets, m=1 and alpha=1/104. Any fixed +ADD budget has limiting inferior error at least 1/104 as f grows, even if +the program's coefficients vary with f. The sparse-row inequality is sharp; +attainability by a complete decoder is unclaimed. See [PROOF.md](PROOF.md). + +## Evidence and predecessor boundary + +The proof cites PR5065's isolated marker tensor identity and four-entry flat +row. It adds the sparse approximation inequality, projection argument and +positive-tolerance corollary. The predecessor identity is a premise, not a +newly audited or replayed deliverable. The verifier hashes its exact README +and proof bytes and never executes predecessor code. + +The standalone verifier uses exact integer and rational arithmetic. It checks +all support subsets of the new flat-row fixtures through sixteen coordinates, +a complete finite Gaussian coefficient box, tensor-row truncations through +width six, and bounded integer instances of the all-width corollary. It also +checks invalid arguments and discriminating false-strengthening controls. +[RESULT.json](RESULT.json) is generated by the verifier and binds the package +and cited inputs by SHA256. Universal coverage comes from the written proof, +not these finite fixtures. + +## Reproduce + +From the repository root with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/terminal-approximation-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/terminal-approximation-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/terminal-approximation-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/terminal-approximation-floor --check-source-history +``` + +The first two commands print `PASS_TERMINAL_APPROXIMATION_FLOOR`. +The registered hook runs both modes, each with a 60-second limit. A portable +Python 3.12 interpreter can replace the absolute path. Direct replay needs +the package and its two declared inputs at their relative paths, without Git +or network access. `--emit /absolute/new/scratch/result.json` generates a new +receipt; normal replay writes nothing. + +## Scope and implementation bounds + +This is an algebraic boundary result on the changed complex-rank-shape-decoder +card. Its old fixed-profile packing ceiling is inapplicable. The historical +first command was attempted and fails with `KeyError: 'complex_profile'` on +the selected schema. The current `research_selected_baseline.py` orientation +passes source bindings only. Neither run certifies a supplier. + +The model permits arbitrary complex scalars, monomial maps, owned COPY/CLEAR +and arbitrary independent dirty scratch, counting every scalar ADD. It is a +linear operator-approximation model. Nonlinear rounded execution, approximation +of the composed caller in a different norm, paid Gaussian decoding, changed +recursive job types and complete physical costs are outside the theorem. +Native all-column, ownership, routing, storage, precision/tape, compiler and +outer assumptions remain unresolved or inherited. No new kappa or selected +frontier change is claimed. + +Only this new package changes. Code uses direct calls without recursion, +subprocesses, network access or predecessor imports. Tensor fixtures have at +most 1,024 entries; the support census visits at most 65,536 subsets per row; +the coefficient box has 9^4 rows. Corollary loops use width at most 200 and +at most 398 ADD counts per sign case. The arithmetic entry point rejects +widths above 1,000 and ADD budgets above 2,000. Every function is below sixty +physical lines. Both registered modes enable warning errors, and explicit +exceptions keep invariants active under optimization. No external static +analyzer or formal proof kernel is claimed. + +Power of Ten rule 3 deviation: CPython allocates arithmetic objects and +collections. These bounded one-shot checks cannot prohibit runtime allocation. +At most one tensor row, its approximation and one current census candidate +are live; integer sizes are bounded by the enforced inputs. Both execution +modes exercise the endpoint limits. A future native steady-operation port +would need fixed-capacity storage before removing this deviation. + +## Open next questions + +1. Can a linear scalar/monomial word attain a comparable whole-operator error + with O(f) ADDs? Start with the isolated block, then require all owner blocks + and dirty restoration. A sharp row inequality alone is not such a word. +2. Can this operator floor be translated to final Gaussian-output error for + the actual caller? First bind the entrance operator's least singular value + and the caller's norm and precision contract. Conditioning and complete + physical costs remain blockers; this result makes no such transfer claim. + +## Sources and credit + +Canonical base is `81e9bd69e4a5b00ba9c713a1620e36d576d5522e`, priority revision 7. +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19142720) +records the changed premise and bounded stop rule. Source pins are in +[SOURCES.json](SOURCES.json); scope and coverage are in [TASK.json](TASK.json). + +Credit Cinna Davis/PR5065 for the exact marker identity, bank-specific support +obstruction and operation alphabet; Dillon Amburgey/PR4933 for the actual +signed monomial normalizers and coded caller; Dugongue/mdumitrean/PR4929 for +the center-free producer and code; JoyboyBrian/PR5036/#5069 for the physical +substitution boundary and paid inverse-coded pair. Retain Cinna Davis's +PR4694/#4698/#4440/#4470, Cao Yifan/intqwq/PR4610, zxv, Jacob Alan Sussman, +Ryanson Jonathan and all retained native, Clifford, query, ownership, +compiler and precision contributors. Their files and credit lines are unchanged. diff --git a/research/terminal-approximation-floor/RESULT.json b/research/terminal-approximation-floor/RESULT.json new file mode 100644 index 0000000000..ebe9c511d9 --- /dev/null +++ b/research/terminal-approximation-floor/RESULT.json @@ -0,0 +1,59 @@ +{ + "actual_bank_inverse_count": 1, + "actual_bank_scale": "1/104", + "actual_bank_sufficient_error_tolerance": "1/208", + "claim_type": "scoped proof with exact finite corroboration", + "coefficient_rows": 6561, + "controls": { + "false_strengthenings": 6, + "invalid_arguments": 8 + }, + "corollary_comparisons": 119400, + "package_sha256": { + "PROOF.md": "36328319e54d046e9969c382b204d1aa716f0fae7665af51fb5890803ed8b361", + "README.md": "90e45c756cdc1988070a52f7ba2d7e256081a554bbe1c8572c33b3bf7be546ea", + "SOURCES.json": "e969993c5bee3670595255e17dd7d6e94615d9f77e687871d6461cd8ddb8b81c", + "TASK.json": "fb4b71196883a6774a96abca0e390a9245954941e67dc5b3f82575828f4e6f4c", + "VERIFY.json": "e413e4d8c5df12c632438db4d9b54631bd17ff8f6a5423284697b9a4b7adc79f", + "verify.py": "a6caa68dcbdb5ff2f19d307ec1359436ce4bc6c6fcf08fd0a6c6f77b8914496d" + }, + "premise_inputs": { + "research/two-stage-coded-terminal/PROOF.md": "5a8d0b3f6179c6b5892d55638a6cb8d58ab0135224da07ac181b6edad4cf4e8e", + "research/two-stage-coded-terminal/README.md": "1547a1b5fbb4b919fa90c6b2c3e476e51e52ca8f99c39a5f6a268757eced1365" + }, + "schema_version": 1, + "selected_kappa_unchanged": "60403/20000000", + "support_subsets": [ + 2, + 16, + 65536 + ], + "tensor_boundary_witnesses": [ + { + "half_support_error_squared_relative": "1/2", + "support": 4, + "width": 2 + }, + { + "half_support_error_squared_relative": "1/2", + "support": 16, + "width": 3 + }, + { + "half_support_error_squared_relative": "1/2", + "support": 64, + "width": 4 + }, + { + "half_support_error_squared_relative": "1/2", + "support": 256, + "width": 5 + }, + { + "half_support_error_squared_relative": "1/2", + "support": 1024, + "width": 6 + } + ], + "tensor_truncation_fixtures": 27 +} diff --git a/research/terminal-approximation-floor/SOURCES.json b/research/terminal-approximation-floor/SOURCES.json new file mode 100644 index 0000000000..b3fb77f052 --- /dev/null +++ b/research/terminal-approximation-floor/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/two-stage-coded-terminal/PROOF.md", + "usage": "input", + "git_blob": "228baac8d81081e32995a3596e9a913924801d9a", + "sha256": "5a8d0b3f6179c6b5892d55638a6cb8d58ab0135224da07ac181b6edad4cf4e8e" + }, + { + "path": "research/two-stage-coded-terminal/README.md", + "usage": "input", + "git_blob": "86e7af1c02878abd03e2287fa6c87f94d3371ef1", + "sha256": "1547a1b5fbb4b919fa90c6b2c3e476e51e52ca8f99c39a5f6a268757eced1365" + } + ] +} diff --git a/research/terminal-approximation-floor/TASK.json b/research/terminal-approximation-floor/TASK.json new file mode 100644 index 0000000000..4adb97608d --- /dev/null +++ b/research/terminal-approximation-floor/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Quantitative operator-norm error floor for scalar/monomial approximations to the two-stage physical terminal postdecoders of PR5065.", + "scope_change_reason": "Replace exact terminal decoding by uniform linear approximation; cite the existing marker identity and prove a new robust obstruction rather than audit it or optimize the old paid profile.", + "bottleneck_link": "Closes the possibility of uniformly accurate fixed-scalar-word postdecoding of these actual coded banks; this is a local interface obstruction, not supplier admission.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved positive-tolerance ADD floor; do not expand to Gaussian decoder synthesis or complete caller admission.", + "outcome": "completed", + "evidence": "Written sparse-row/operator-norm proof, exact bounded support and coefficient censuses, tensor fixtures and half-scale tolerance checks.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a full scalar/monomial word attain comparable whole-operator error using O(f) ADDs?", + "why_it_matters": "Distinguishes the sharp row argument from an attainable decoding price.", + "first_step": "Construct the isolated block, then include all owner blocks and dirty restoration.", + "blocked_by": "A whole-operator construction and complete physical bill." + }, + { + "question": "Can the postdecoder operator floor transfer to final Gaussian-output error?", + "why_it_matters": "Connects the scoped algebraic result to the actual caller precision contract.", + "first_step": "Bind the entrance least singular value and caller norm.", + "blocked_by": "Source-specific conditioning and complete physical costs." + } + ], + "overlap": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19142720", + "open_pr_snapshot_utc": "2026-10-23T09:27:33.727877+00:00", + "open_pr_records": 320, + "discussion_snapshot_utc": "2026-10-23T09:28:53.790400+00:00", + "discussion_records": 4236, + "remote_complete_pagination": true, + "local_notes_searched": 121, + "local_notes_at_head": 6824, + "limitations": "Sparse local note coverage; arbitrary diffs, unpublished work and later activity are not exhaustively searched. Distinctive all-main README and merged PR searches separately covered the target." + }, + "environment": { + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + } +} diff --git a/research/terminal-approximation-floor/VERIFY.json b/research/terminal-approximation-floor/VERIFY.json new file mode 100644 index 0000000000..3f4b8ca522 --- /dev/null +++ b/research/terminal-approximation-floor/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/two-stage-coded-terminal/PROOF.md", + "research/two-stage-coded-terminal/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact new sparse-row and coefficient inequalities, tensor fixtures, robust ADD corollary, rejecting inputs and source-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same new-result evidence with optimization and warnings as errors." + } + ] +} diff --git a/research/terminal-approximation-floor/verify.py b/research/terminal-approximation-floor/verify.py new file mode 100644 index 0000000000..f0dc4b3d1e --- /dev/null +++ b/research/terminal-approximation-floor/verify.py @@ -0,0 +1,218 @@ +#!/usr/bin/env python3 +"""Exact corroboration of a terminal approximation floor. Apache-2.0.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import sys + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SEED = ((1, 0), (0, -1), (0, 1), (1, 0)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def bounded_integer(value, lower, upper, name): + need(type(value) is int and lower <= value <= upper, name) + + +def error_squared(width, adds, inverse_count): + """Universal squared operator-error lower bound, not an optimum.""" + bounded_integer(width, 1, 1000, 'width outside executable budget') + bounded_integer(adds, 0, 2000, 'ADD count outside executable budget') + bounded_integer(inverse_count, 0, 2, 'invalid inverse count') + support = 4 ** (width - 1) + missed = max(0, support - 2 ** adds) + return Fraction(missed, support * (8 * 13 ** inverse_count) ** 2) + + +def multiply(left, right): + a, b = left + c, d = right + return a * c - b * d, a * d + b * c + + +def tensor_row(degree): + bounded_integer(degree, 0, 5, 'tensor fixture exceeds capacity') + row = [(1, 0)] + for _ in range(degree): + row = [multiply(x, y) for x in row for y in SEED] + need(len(row) == 4 ** degree, 'tensor support length') + need(all(a * a + b * b == 1 for a, b in row), 'flat Gaussian phases') + return row, 2 ** degree + + +def distance_squared(target, approximation, denominator): + need(len(target) == len(approximation) <= 1024, 'row dimensions') + need(type(denominator) is int and denominator > 0, 'denominator') + numerator = sum((a - c) ** 2 + (b - d) ** 2 + for (a, b), (c, d) in zip(target, approximation)) + return Fraction(numerator, denominator ** 2) + + +def support_census(): + """Literal best truncations on every support through sixteen columns.""" + counts = [] + for degree in range(3): + row, denominator = tensor_row(degree) + size = len(row) + for mask in range(1 << size): + approximation = [value if mask >> i & 1 else (0, 0) + for i, value in enumerate(row)] + actual = distance_squared(row, approximation, denominator) + expected = Fraction(size - mask.bit_count(), size) + need(actual == expected, 'nearest-support distance') + counts.append(1 << size) + return counts + + +def coefficient_census(): + """All 9^4 rows in a Gaussian-integer coefficient box, with cancellations.""" + row, denominator = tensor_row(1) + alphabet = tuple(product(range(-1, 2), repeat=2)) + count = 0 + for approximation in product(alphabet, repeat=len(row)): + used = sum(value != (0, 0) for value in approximation) + actual = distance_squared(row, approximation, denominator) + need(actual >= Fraction(4 - used, 4), 'arbitrary-coefficient floor') + count += 1 + return count + + +def tensor_fixtures(): + count, witnesses = 0, [] + for degree in range(6): + row, denominator = tensor_row(degree) + size = len(row) + need(distance_squared(row, [(0, 0)] * size, denominator) == 1, + 'normalized row energy') + for used in sorted({0, 1, size // 2, size - 1, size}): + approximation = row[:used] + [(0, 0)] * (size - used) + actual = distance_squared(row, approximation, denominator) + need(actual == Fraction(size - used, size), 'sharp row truncation') + if used: + a, b = approximation[0] + approximation[0] = (a + 3, b - 2) + perturbed = distance_squared(row, approximation, denominator) + need(perturbed == actual + Fraction(13, denominator ** 2), + 'retained-coordinate orthogonality') + count += 1 + if degree: + approximation = row[:size // 2] + [(0, 0)] * (size // 2) + need(distance_squared(row, approximation, denominator) == Fraction(1, 2), + 'one-fewer-ADD row boundary') + witnesses.append({'width': degree + 1, 'support': size, + 'half_support_error_squared_relative': '1/2'}) + return count, witnesses + + +def corollary_census(): + count = 0 + for width in range(2, 201): + for inverses in range(3): + scale_squared = Fraction(1, (8 * 13 ** inverses) ** 2) + for adds in range(2 * (width - 1)): + lower = error_squared(width, adds, inverses) + need(lower >= scale_squared / 2 > scale_squared / 4, + 'half-scale tolerance preserves ADD floor') + count += 1 + need(error_squared(width, 2 * (width - 1), inverses) == 0, + 'lower bound vanishes at exact support threshold') + need(error_squared(1, 0, 1) == 0, 'width-one vacuous bound') + need(error_squared(1000, 2000, 2) == 0, 'executable upper endpoint') + return count + + +def controls(): + invalid = [(0, 0, 1), (1001, 0, 1), (True, 0, 1), (2, -1, 1), + (2, 2001, 1), (2, False, 1), (2, 0, -1), (2, 0, 3)] + for values in invalid: + try: + error_squared(*values) + except ValueError: + continue + raise ValueError('invalid argument accepted') + row, denominator = tensor_row(1) + half = row[:2] + [(0, 0)] * 2 + half_error = distance_squared(row, half, denominator) + need(half_error != 1, 'reject omitted support allowance') + need(half_error != 0, 'reject a dimension-free zero-error claim') + need(error_squared(3, 0, 0) != error_squared(3, 0, 1), + 'reject omitted inverse scaling') + need(error_squared(3, 0, 1) != error_squared(3, 0, 2), + 'reject a squared inverse-count substitution') + need(error_squared(3, 2, 1) != error_squared(2, 2, 1), + 'reject omission of the marker-column loss') + need(distance_squared([(2, 0), (0, 0), (0, 0), (0, 0)], + [(2, 0), (0, 0), (0, 0), (0, 0)], 2) == 0, + 'nonflat negative fixture') + return {'invalid_arguments': len(invalid), 'false_strengthenings': 6} + + +def input_hashes(): + manifest = json.loads((PACKAGE / 'SOURCES.json').read_text()) + hashes = {} + for entry in manifest['files']: + if entry['usage'] == 'input': + path = entry['path'] + digest = sha256((ROOT / path).read_bytes()).hexdigest() + need(digest == entry['sha256'], 'cited premise changed: ' + path) + hashes[path] = digest + need(len(hashes) == 2, 'exactly two cited premise inputs') + return hashes + + +def result(): + inputs = input_hashes() + tensor_count, witnesses = tensor_fixtures() + output = { + 'schema_version': 1, + 'claim_type': 'scoped proof with exact finite corroboration', + 'premise_inputs': inputs, + 'support_subsets': support_census(), + 'coefficient_rows': coefficient_census(), + 'tensor_truncation_fixtures': tensor_count, + 'tensor_boundary_witnesses': witnesses, + 'corollary_comparisons': corollary_census(), + 'controls': controls(), + 'actual_bank_inverse_count': 1, + 'actual_bank_scale': '1/104', + 'actual_bank_sufficient_error_tolerance': '1/208', + 'selected_kappa_unchanged': '60403/20000000', + } + need(input_hashes() == inputs, 'premise inputs changed during replay') + own_files = ('PROOF.md', 'README.md', 'TASK.json', 'SOURCES.json', + 'VERIFY.json', 'verify.py') + output['package_sha256'] = { + name: sha256((PACKAGE / name).read_bytes()).hexdigest() for name in own_files + } + return output + + +def main(): + arguments = sys.argv[1:] + need(arguments == [] or len(arguments) == 2 and arguments[0] == '--emit', + 'usage: verify.py [--emit NEW_SCRATCH_FILE]') + output = result() + if arguments: + destination = Path(arguments[1]) + need(destination.is_absolute() and not destination.exists(), + 'receipt destination must be a new absolute scratch path') + with destination.open('x') as stream: + stream.write(json.dumps(output, indent=2, sort_keys=True) + '\n') + else: + expected = json.loads((PACKAGE / 'RESULT.json').read_text()) + need(output == expected, 'receipt mismatch') + print('PASS_TERMINAL_APPROXIMATION_FLOOR actual_bank_tolerance=1/208 ' + 'minimum_ADDs=2(f-1) no_new_kappa') + + +if __name__ == '__main__': + main()