From b0cb9c60ac4c237ba498ce71ed8cf5597fb6062a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 22:25:58 +0000 Subject: [PATCH] feat(research): bound sharp growth in restoring unit-shear words --- research/restored-unit-shear-growth/PROOF.md | 129 +++++++++++++++++ research/restored-unit-shear-growth/README.md | 106 ++++++++++++++ .../restored-unit-shear-growth/SOURCES.json | 18 +++ research/restored-unit-shear-growth/TASK.json | 107 ++++++++++++++ .../restored-unit-shear-growth/VERIFY.json | 34 +++++ research/restored-unit-shear-growth/model.py | 83 +++++++++++ research/restored-unit-shear-growth/oracle.py | 48 +++++++ research/restored-unit-shear-growth/verify.py | 135 ++++++++++++++++++ 8 files changed, 660 insertions(+) create mode 100644 research/restored-unit-shear-growth/PROOF.md create mode 100644 research/restored-unit-shear-growth/README.md create mode 100644 research/restored-unit-shear-growth/SOURCES.json create mode 100644 research/restored-unit-shear-growth/TASK.json create mode 100644 research/restored-unit-shear-growth/VERIFY.json create mode 100644 research/restored-unit-shear-growth/model.py create mode 100644 research/restored-unit-shear-growth/oracle.py create mode 100644 research/restored-unit-shear-growth/verify.py diff --git a/research/restored-unit-shear-growth/PROOF.md b/research/restored-unit-shear-growth/PROOF.md new file mode 100644 index 0000000000..834ecb090f --- /dev/null +++ b/research/restored-unit-shear-growth/PROOF.md @@ -0,0 +1,129 @@ +# Sharp intermediate growth under exact restoration + +This proof and its application were produced by Nick Petalas. Apache-2.0. + +## Contract and theorem + +Let n>=2 and L>=0 be integers. A gate on n rows is exactly + +``` +x_i <- x_i + epsilon x_j, i != j, epsilon in {-1,1}. +``` + +All other rows stay fixed. A word has length ell<=L, and its complete +integer matrix is I_n. This is full restoration for every original input, +including every dirty workspace row. There is no scaling, self-addition, +native operator, rounding, source insertion or free operation. + +Set F_0=0, F_1=1 and F_(a+2)=F_(a+1)+F_a. Let P_k be the prefix matrix +after k gates, with P_0=I. Write |P|_max for its largest absolute entry, +and ||P||_infinity for its largest absolute row sum. + +**Theorem.** With d=min(k,ell-k), every cut satisfies + +``` +|P_k|_max <= F_(d+1), +||P_k||_infinity <= F_(d+2). +``` + +Consequently, over all allowed words and all their cuts, the exact maxima are + +``` +max |P_k|_max = F_(floor(L/2)+1), +max ||P_k||_infinity = F_(floor(L/2)+2). +``` + +Both maxima are attained by one word on two rows. Any additional rows stay +fixed, so allowing arbitrarily many dirty rows cannot increase the maxima. +These are maxima under an **at most L** budget. We do not assert an +identity word of every exact length, or sharpness at every specified cut. + +## One-way growth lemma + +First ignore the endpoint. For each row of a prefix matrix take its +absolute row sum, and sort these n nonnegative numbers. Let a>=b be +the two largest. Updating one row changes its norm to at most the sum +of the norms of two distinct old rows, hence at most a+b. The new +second largest norm is at most a, since only one row changes. Thus the +ordered pair of largest norms is componentwise bounded by + +``` +(a,b) -> (a+b,a). +``` + +Initially it is (1,1). Induction bounds it after t gates by +(F_(t+2),F_(t+1)), so ||P||_infinity<=F_(t+2). Decreases and sign +cancellations do not invalidate this upper bound. + +Apply the same argument to the absolute values in one fixed column. +Initially the two largest are (1,0). They are bounded after t gates by +(F_(t+1),F_t). Each column therefore has largest entry at most F_(t+1), +which proves |P|_max<=F_(t+1). This argument applies separately to each +column and does not assume independent signs across columns. + +## Use both sides of the cut + +Write S_k for the matrix of the remaining ell-k gates, so S_k P_k=I. +Then P_k=S_k^-1. A gate's inverse is another allowed gate, with its +sign negated. Reversing the remaining gates and negating their signs +therefore writes the **same P_k** as a word of length ell-k. + +The one-way lemma gives both bounds with t=k and with t=ell-k. +The Fibonacci numbers are nondecreasing, so taking the smaller gives +the two stated cut bounds. Since min(k,ell-k)<=floor(L/2), the global +bounds follow. No norm estimate on the final identity is substituted +for the inverse-word argument. + +## Attainment and the magnitude guard + +Put s=floor(L/2). Starting with two rows, alternate positive additions + +``` +x_0 += x_1, x_1 += x_0, x_0 += x_1, ... +``` + +for s gates. Execute their inverse gates in reverse order. The resulting +word has length 2s<=L and endpoint I. At its midpoint, its two row sums +are F_(s+2),F_(s+1), in one order. For s>=1 its largest entry is +F_(s+1), as follows by the same alternating recurrence in the two columns. +For s=0 the midpoint is I, with both maxima equal to one. This proves +attainment, simultaneously for both bounds. + +If every original real or integer input satisfies |x_i|<=H, the triangle +inequality gives the uniform intermediate magnitude cap + +``` +|x_i(k)| <= H F_(floor(L/2)+2). +``` + +For H>=0, set both active initial rows equal to H in the attaining word. +The larger midpoint row attains this cap exactly. Arbitrary spectator +inputs remain unchanged. Hence the cap is the least possible universal +cap from L and H alone for n>=2. If H is a nonnegative integer and +M=H F_(floor(L/2)+2), the smallest two's-complement width sufficient for +every state is 1+bit_length(M), with bit_length(0)=0. The positive +attainer also proves necessity of this symmetric-range width. + +This guard applies to exact row states. It does not bound the error of +rounded shears, local arithmetic temporaries with a different evaluation +order, coefficient preparation, tape movement, or native Gaussian gates. + +## Verification boundary and relevance + +The all-dimension and all-length assertions rest on the proof above. +The finite matrix census evaluates every signed unit ADD word through +length eight on two rows and length five on three rows. It tests each +identity word's individual cuts and reports their exact counts. The +separate oracle evaluates integer cube corners, without matrix operations +or imports from the model. Checking all corners determines identity and +the induced infinity norm over this characteristic-zero model, since +the corners span and each row's absolute sum is attained at a corner. +All words in the two declared oracle domains are enumerated too. + +The proof isolates an exact restoration-aware precision input. A complete +selected caller contains operations outside this alphabet, so there is no +automatic replacement of its existing precision guard or scalar allowance. +No source word, predecessor theorem, native map or historical count is +replayed as the contribution. Independent human and formal proof-kernel +review, physical implementation and all five framework assumptions remain +unclaimed. No new kappa follows. diff --git a/research/restored-unit-shear-growth/README.md b/research/restored-unit-shear-growth/README.md new file mode 100644 index 0000000000..795acfcf17 --- /dev/null +++ b/research/restored-unit-shear-growth/README.md @@ -0,0 +1,106 @@ +# Sharp growth inside a restoring unit-shear word + +This contribution was produced by Nick Petalas. Claim type: scoped written +proof with exact finite corroboration. Apache-2.0. No new kappa is claimed. + +For any finite number n>=2 of arbitrary dirty rows, take a word of at most +L gates `x_i += epsilon*x_j`, with i!=j and epsilon in {-1,1}, whose complete +endpoint is the identity. The exact largest possible intermediate values are + +``` +largest absolute matrix coefficient = F_(floor(L/2)+1) +largest absolute row sum = F_(floor(L/2)+2) +``` + +Here F_0=0 and F_1=1. Two rows attain both bounds: alternate positive ADDs +for floor(L/2) steps, then execute the literal inverse. Extra dirty rows +cannot improve the maxima. At cut k of a length-ell loop, replace floor(L/2) +by min(k,ell-k) in the upper bounds. + +For initial magnitudes at most H, the sharp universal intermediate cap is +`H*F_(floor(L/2)+2)`. The [proof](PROOF.md) also gives its exact signed-width +guard. The new step uses the restoring suffix to bound the same prefix from +the opposite end. Standard top-two Fibonacci majorization supplies the +one-way estimate. No global literature-priority claim is made. + +The changed card scope is explicit in [TASK.json](TASK.json). This is a +scalar precision side result, without selected-caller binding. It does not +audit a predecessor, admit a supplier or change the selected frontier. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/restored-unit-shear-growth +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/restored-unit-shear-growth/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/restored-unit-shear-growth/oracle.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/restored-unit-shear-growth --check-source-history +``` + +Any CPython 3.12 installation can replace the local interpreter path. The +registered normal and optimized runs print PASS_RESTORED_UNIT_SHEAR_GROWTH. +Direct oracle replay prints PASS_RESTORED_SHEAR_LITERAL_CUBE. + +The matrix census enumerates all 87,381 two-row words through length eight +and all 271,453 three-row words through length five. It finds 2,689 and 577 +identity words, respectively, and checks each cut. The independent oracle +uses literal integer cube corners, with no matrix-model import. It enumerates +5,461 two-row words through length six and 22,621 three-row words through +length four; every common identity count and maximum row norm agrees. +Empty exact-length classes have null maxima in the generated receipt. + +The replay checks 387 attaining loops at even budgets through 256, 128 odd +budget attainers, 231 literal magnitude/width guards and 12 controls. The +controls include invalid coefficients and indices, self-addition, inadequate +gate budgets, incomplete restoration and an undersized Fibonacci bound. +Explicit exceptions keep every check active under optimization. The receipt +binds every package file by SHA256 and is printed without writing files. + +## Limits + +The theorem uses an at-most gate budget and exact full identity restoration. +It excludes scales, coefficients beyond signed units, source insertions, +native operators and rounding. In particular, this is not an error bound +for rounded identity cycles or a bound on every arithmetic temporary. Real +selected callers contain excluded operations. Their source/frame/ownership, +physical tape, precision, compiler and analytic obligations remain separate. +No predecessor suite, selected cold replay, Lean or Docker build ran. +Independent human and formal proof-kernel review are unclaimed. + +The reference model accepts at most eight rows and 256 gates. The proof has +no such dimension or length restriction. Every loop has a finite bound from +these limits or the fixed census domains. No recursion, network, subprocess +or dynamic evaluation is used. Functions stay below 60 physical lines. +Python allocation during integer arithmetic is a Power-of-Ten rule 3 +deviation, bounded by the fixed domains and word lengths. The census streams +words and retains only one trace and per-length summaries. Warning-strict +normal and optimized replay supplies the available interpreted diagnostics; +no installed static type checker or linter was available. Explicit sibling +imports identify the two scientific modules; no predecessor is imported. + +## Open next questions + +1. Determine a sharp bound for one specified nonidentity endpoint. Begin + with forward growth and inverse-suffix multiplication by the endpoint. + This could cover useful scalar intervals, but no sharp classification + or selected interval is bound here. +2. Derive an error bound for a stated rounded implementation using the + exact inverse-prefix envelope. Specify every rounding point and increment + model first. Exact restoration alone does not prove rounded restoration + or dirt-independent increments. + +## Sources and credit + +Base: canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority +revision 8, selected PR6030. The selected record and catalogue are historical +provenance in [SOURCES.json](SOURCES.json), with no external scientific input. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361711) +records the original question. Live handoffs and reservations, open/account +PRs, main README and formula searches, merged PR searches and cached card +coverage were checked. Arbitrary historical diffs and unpublished work remain +outside that coverage. + +Elementary row operations, induced matrix norms and Fibonacci majorization +are classical. The new scoped contribution is the sharp restoration-aware +application and its rerunnable verification, produced by Nick Petalas. diff --git a/research/restored-unit-shear-growth/SOURCES.json b/research/restored-unit-shear-growth/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/restored-unit-shear-growth/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/restored-unit-shear-growth/TASK.json b/research/restored-unit-shear-growth/TASK.json new file mode 100644 index 0000000000..8881873fe6 --- /dev/null +++ b/research/restored-unit-shear-growth/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp coefficient and induced infinity-norm growth inside exact identity words of at most L signed unit row ADDs, in every finite dimension, with matching dirty-input magnitude and signed-width guards.", + "scope_change_reason": "The formal-interface card is changed to an original written scalar precision lemma. This package does not formalize a selected-caller implication or claim proof-kernel acceptance.", + "bottleneck_link": "Side result for precision_tape: exact restoration constrains the intermediate growth envelope through both sides of each cut. Actual selected callers also contain operations outside this alphabet and require a separate binding.", + "budget_minutes": 60, + "stop_rule": "Ship the first sharp restoration-aware envelope after the proof, exact bounded checks and controls pass; do not extend to rounded words or selected integration.", + "outcome": "completed", + "evidence": "PROOF.md; complete matrix and independent literal-cube censuses; attaining loops and guard checks; generated file-hash-bound receipts.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What sharp intermediate bound survives a specified nonidentity endpoint?", + "why_it_matters": "Selected scalar intervals need not restore the entire data state to identity.", + "first_step": "Specify a fixed endpoint T and compare the forward word with the inverse suffix followed by T; determine when the resulting product bound is attained.", + "blocked_by": "No sharp endpoint-dependent classification or selected-word binding is supplied." + }, + { + "question": "What rounded-error bound can exploit the exact restoration-aware envelope?", + "why_it_matters": "Exact magnitude control alone does not certify rounded cleanup.", + "first_step": "Fix rounding points and an allowed increment-error model, then bound the actual inverse-prefix propagation of each error.", + "blocked_by": "The exact identity argument does not assert a rounded identity endpoint or dirt-independent increments." + } + ], + "claim_type": "scoped mathematical proof with exact finite corroboration", + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361711", + "source": "original", + "coverage": "Live open/account PRs, handoffs, local reservations, merged/object/formula searches and a cached formal-interface card search; arbitrary historical diffs and unpublished work excluded." + } +} diff --git a/research/restored-unit-shear-growth/VERIFY.json b/research/restored-unit-shear-growth/VERIFY.json new file mode 100644 index 0000000000..1fcab9bc45 --- /dev/null +++ b/research/restored-unit-shear-growth/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": 180, + "checks": "Exhaustive exact matrix and independent scalar-cube censuses, sharp loops, signed guards and invalid-contract controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "The same complete scientific checks with assertions disabled." + } + ] +} diff --git a/research/restored-unit-shear-growth/model.py b/research/restored-unit-shear-growth/model.py new file mode 100644 index 0000000000..500df19ad6 --- /dev/null +++ b/research/restored-unit-shear-growth/model.py @@ -0,0 +1,83 @@ +"""Exact reference model for restoring signed unit row additions. + +Produced by Nick Petalas. Apache-2.0. +""" + +from __future__ import annotations + +MAX_ROWS = 8 +MAX_GATES = 256 +Gate = tuple[int, int, int] +Matrix = tuple[tuple[int, ...], ...] + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def fibonacci(index: int) -> int: + need(type(index) is int and 0 <= index <= MAX_GATES + 2, "Fibonacci index") + previous, current = 0, 1 + for _ in range(index): + previous, current = current, previous + current + return previous + + +def validate(n: int, word: tuple[Gate, ...]) -> None: + need(type(n) is int and 1 <= n <= MAX_ROWS, "row count") + need(type(word) is tuple and len(word) <= MAX_GATES, "word capacity") + for gate in word: + need(type(gate) is tuple and len(gate) == 3, "gate shape") + need(all(type(value) is int for value in gate), "integer gate") + target, source, sign = gate + need(0 <= target < n and 0 <= source < n, "row index") + need(target != source and sign in (-1, 1), "signed unit ADD") + + +def identity(n: int) -> Matrix: + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def apply(matrix: Matrix, gate: Gate) -> Matrix: + target, source, sign = gate + rows = list(matrix) + rows[target] = tuple(a + sign * b for a, b in zip(rows[target], rows[source])) + return tuple(rows) + + +def measures(matrix: Matrix) -> tuple[int, int]: + entry = max(abs(value) for row in matrix for value in row) + norm = max(sum(abs(value) for value in row) for row in matrix) + return entry, norm + + +def trace(n: int, word: tuple[Gate, ...]) -> tuple[Matrix, tuple[tuple[int, int], ...]]: + validate(n, word) + matrix = identity(n) + heights = [measures(matrix)] + for gate in word: + matrix = apply(matrix, gate) + heights.append(measures(matrix)) + return matrix, tuple(heights) + + +def check_loop(n: int, word: tuple[Gate, ...], budget: int) -> tuple[int, int]: + need(type(budget) is int and len(word) <= budget <= MAX_GATES, "gate budget") + endpoint, heights = trace(n, word) + need(endpoint == identity(n), "full arbitrary-input endpoint is not identity") + length = len(word) + for cut, (entry, norm) in enumerate(heights): + radius = min(cut, length - cut) + need(entry <= fibonacci(radius + 1), "coefficient envelope") + need(norm <= fibonacci(radius + 2), "row-norm envelope") + peak = tuple(max(pair[j] for pair in heights) for j in range(2)) + need(peak[0] <= fibonacci(budget // 2 + 1), "budget coefficient") + need(peak[1] <= fibonacci(budget // 2 + 2), "budget row norm") + return peak + + +def attaining_word(steps: int) -> tuple[Gate, ...]: + need(type(steps) is int and 0 <= steps <= MAX_GATES // 2, "attainer capacity") + outward = tuple((step % 2, 1 - step % 2, 1) for step in range(steps)) + return outward + tuple((i, j, -sign) for i, j, sign in reversed(outward)) diff --git a/research/restored-unit-shear-growth/oracle.py b/research/restored-unit-shear-growth/oracle.py new file mode 100644 index 0000000000..87538f5b20 --- /dev/null +++ b/research/restored-unit-shear-growth/oracle.py @@ -0,0 +1,48 @@ +"""Independent literal integer-cube oracle, without the matrix model. + +Produced by Nick Petalas. Apache-2.0. +""" + +from __future__ import annotations + +import itertools +import json + + +def scalar_census(n: int, depth: int) -> dict: + if (n, depth) not in ((2, 6), (3, 4)): + raise ValueError("oracle domain") + symbols = tuple((i, j, sign) for i in range(n) for j in range(n) + if i != j for sign in (-1, 1)) + corners = tuple(itertools.product((-1, 1), repeat=n)) + counts = [] + fib = [0, 1] + for _ in range(depth + 2): + fib.append(fib[-1] + fib[-2]) + for length in range(depth + 1): + words = closed = 0 + maximum = 1 + for instructions in itertools.product(symbols, repeat=length): + words += 1 + restores = True + cut_peaks = [1] * (length + 1) + for original in corners: + cells = list(original) + for cut, (target, source, sign) in enumerate(instructions, 1): + cells[target] += sign * cells[source] + cut_peaks[cut] = max(cut_peaks[cut], *map(abs, cells)) + restores = restores and tuple(cells) == original + if restores: + closed += 1 + for cut, actual in enumerate(cut_peaks): + if actual > fib[min(cut, length - cut) + 2]: + raise ValueError("literal cube exceeds closed-word guard") + maximum = max(maximum, *cut_peaks) + counts.append({"length": length, "words": words, "closed": closed, + "max_norm": maximum if closed else None}) + return {"rows": n, "depth": depth, "by_length": counts} + + +if __name__ == "__main__": + print(json.dumps([scalar_census(2, 6), scalar_census(3, 4)], sort_keys=True)) + print("PASS_RESTORED_SHEAR_LITERAL_CUBE") diff --git a/research/restored-unit-shear-growth/verify.py b/research/restored-unit-shear-growth/verify.py new file mode 100644 index 0000000000..fd36d5810c --- /dev/null +++ b/research/restored-unit-shear-growth/verify.py @@ -0,0 +1,135 @@ +"""Bounded exhaustive corroboration; no predecessor executable is imported. + +Produced by Nick Petalas. Apache-2.0. +""" + +from __future__ import annotations + +import hashlib +import itertools +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from model import attaining_word, check_loop, fibonacci, identity, need, trace +from oracle import scalar_census + + +def matrix_census(n: int, depth: int) -> dict: + need((n, depth) in ((2, 8), (3, 5)), "matrix census domain") + alphabet = tuple((i, j, sign) for i in range(n) for j in range(n) + if i != j for sign in (-1, 1)) + rows = [] + for length in range(depth + 1): + visited = closed = 0 + peak_entry = peak_norm = 1 + for word in itertools.product(alphabet, repeat=length): + endpoint, _ = trace(n, word) + visited += 1 + if endpoint != identity(n): + continue + closed += 1 + entry, norm = check_loop(n, word, length) + peak_entry, peak_norm = max(peak_entry, entry), max(peak_norm, norm) + need(visited == len(alphabet) ** length, "complete alphabet coverage") + rows.append({"length": length, "words": visited, "closed": closed, + "max_entry": peak_entry if closed else None, + "max_norm": peak_norm if closed else None}) + return {"rows": n, "depth": depth, "by_length": rows} + + +def sharpness() -> dict: + digest = hashlib.sha256() + checked = 0 + for steps in range(129): + word = attaining_word(steps) + expected = fibonacci(steps + 1), fibonacci(steps + 2) + for n in (2, 3, 8): + peak = check_loop(n, word, 2 * steps) + need(peak == expected, "sharp coefficient and norm") + endpoint, heights = trace(n, word) + need(endpoint == identity(n), "attainer dirty spectators") + digest.update(json.dumps([n, steps, heights]).encode()) + checked += 1 + if steps < 128: + need(check_loop(2, word, 2 * steps + 1) == expected, "odd budget") + return {"even_budget_attainers": checked, "odd_budget_attainers": 128, + "trace_sha256": digest.hexdigest()} + + +def controls() -> int: + valid = attaining_word(3) + invalid = ( + (2, valid[:-1], 5), + (2, ((0, 1, 1),), 1), + (2, ((0, 1, 2),), 1), + (2, ((0, 0, 1),), 1), + (2, ((0, 2, 1),), 1), + (2, ((0, 1, True),), 1), + (0, (), 0), + (9, (), 0), + (2, valid, 5), + (2, (), 257), + ) + rejected = 0 + for n, word, budget in invalid: + try: + check_loop(n, word, budget) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid loop was admitted") + need(check_loop(1, (), 0) == (1, 1), "one-row empty word") + need(check_loop(2, attaining_word(1), 2)[1] > fibonacci(2), + "one-index-too-small norm bound must fail") + return rejected + 2 + + +def compare_oracle(primary: dict, other: dict) -> None: + need(primary["rows"] == other["rows"], "oracle dimension") + for row in other["by_length"]: + observed = primary["by_length"][row["length"]] + for key in ("length", "words", "closed", "max_norm"): + need(observed[key] == row[key], "matrix/scalar oracle: " + key) + + +def magnitude_guards() -> int: + checked = 0 + for steps in range(33): + for height in (0, 1, 2, 3, 7, 8, 31): + cells = [height, height] + cap = height * fibonacci(steps + 2) + peak = height + for target, source, sign in attaining_word(steps): + cells[target] += sign * cells[source] + peak = max(peak, *map(abs, cells)) + need(cells == [height, height] and peak == cap, "literal sharp guard") + width = 1 + cap.bit_length() + need(cap <= 2 ** (width - 1) - 1, "signed width suffices") + if cap: + need(cap > 2 ** (width - 2) - 1, "smaller width fails") + checked += 1 + return checked + + +def main() -> None: + primary = [matrix_census(2, 8), matrix_census(3, 5)] + independent = [scalar_census(2, 6), scalar_census(3, 4)] + for matrix, scalar in zip(primary, independent): + compare_oracle(matrix, scalar) + result = {"claim_type": "scoped proof with finite corroboration", + "matrix_censuses": primary, "scalar_censuses": independent, + "sharpness": sharpness(), "controls": controls(), + "literal_magnitude_guards": magnitude_guards()} + here = Path(__file__).resolve().parent + result["file_sha256"] = { + p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(here.iterdir()) if p.is_file() + } + print(json.dumps(result, sort_keys=True)) + print("PASS_RESTORED_UNIT_SHEAR_GROWTH") + + +if __name__ == "__main__": + main()