From 1c98c7261ccb03e089c61f006c29ba0a47d3f42f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 00:09:47 +0100 Subject: [PATCH] feat(research): prove a Fibonacci paid-scan floor --- research/fibonacci-scan-floor/PROOF.md | 134 ++++++++++++ research/fibonacci-scan-floor/README.md | 102 +++++++++ research/fibonacci-scan-floor/RESULT.json | 231 +++++++++++++++++++++ research/fibonacci-scan-floor/SOURCES.json | 36 ++++ research/fibonacci-scan-floor/TASK.json | 68 ++++++ research/fibonacci-scan-floor/VERIFY.json | 34 +++ research/fibonacci-scan-floor/verify.py | 212 +++++++++++++++++++ 7 files changed, 817 insertions(+) create mode 100644 research/fibonacci-scan-floor/PROOF.md create mode 100644 research/fibonacci-scan-floor/README.md create mode 100644 research/fibonacci-scan-floor/RESULT.json create mode 100644 research/fibonacci-scan-floor/SOURCES.json create mode 100644 research/fibonacci-scan-floor/TASK.json create mode 100644 research/fibonacci-scan-floor/VERIFY.json create mode 100644 research/fibonacci-scan-floor/verify.py diff --git a/research/fibonacci-scan-floor/PROOF.md b/research/fibonacci-scan-floor/PROOF.md new file mode 100644 index 0000000000..61e416024d --- /dev/null +++ b/research/fibonacci-scan-floor/PROOF.md @@ -0,0 +1,134 @@ +# A Fibonacci support bound for two output banks + +## Exact model + +Let K be a field and let m>=2 banks each contain N coordinates. All mN +initial coordinates are independent variables. In particular, extra banks +contain arbitrary dirty data. A program is a finite composition of these gates: + +1. A monomial map within one bank, and a permutation of whole banks. These + may be arbitrary and may depend on N. We grant them zero cost in the bound. +2. A charged ADD scan `x_i <- x_i + c M x_j`, with i distinct from j, c in K + and M monomial. It changes only bank i. Let S count these gates. +3. A unary gate `x_i <- U x_i`, where every row of U has at most `2^r` + nonzero entries, for an assigned nonnegative integer r. Let R be the sum + of these assigned exponents. Unary native gates are covered when their + actual row supports satisfy this hypothesis. + +Monomial means a permutation times an invertible diagonal matrix. Each gate +acts on the full bank volume. Invertibility of the unary gates is unnecessary +for the lower bound, although reversible applications require it. General +free bank GL, additions with source and destination in the same bank, +multi-bank native gates and partial-volume operations are outside this model. +An ADD with several summands must count each separate scan. + +For each bank i, let sigma_i be the maximum number of nonzero coefficients +in any scalar row of its current linear map from all initial coordinates. +Write A and B for the largest and second largest sigma_i, counting banks +with multiplicity. Thus two equally large banks give A=B. Initially A=B=1. +Zero rows are permitted later. Define F_0=0, F_1=1 and F_(k+2)=F_(k+1)+F_k. + +## Theorem + +At every program cut, + +``` +A <= 2^R F_(S+2), B <= 2^R F_(S+1). (1) +``` + +Consequently, if each of two distinct required output banks has a row with +at least D nonzero old-input coefficients, every implementation satisfies + +``` +2^R F_(S+1) >= D. (2) +``` + +This holds for every finite m. Restoring arbitrary dirty helpers only adds +endpoint requirements, so cannot invalidate the necessary inequality. +The count S is a serial gate count, not a parallel depth or a count of +traversals that fuse several ADDs. + +## Proof + +A monomial map only reorders and rescales scalar rows, so preserves sigma_i. +A bank permutation preserves the sorted support profile. + +Consider one ADD with distinct banks i,j. Each new row of bank i is the sum +of one old row of i and one scaled old row of j. Cancellations can only +decrease support. Thus sigma_i' <= sigma_i+sigma_j <= A+B. All other bank +support sizes are unchanged. After changing one bank, the second largest +size is at most A, regardless of whether the changed bank becomes largest. +Therefore + +``` +A' <= A+B, B' <= A. +``` + +If (1) holds before this gate, the Fibonacci recurrence proves it afterwards +with S replaced by S+1 and R unchanged. + +A unary gate of exponent r replaces each scalar row by a linear combination +of at most 2^r old rows of its own bank. Its support size grows by at most +2^r. Every bank's size is therefore bounded by 2^r times its previous size, +including the unchanged banks. Sorting preserves componentwise inequalities, +so A'<=2^r A and B'<=2^r B. This proves (1) after replacing R by R+r. +The initial profile satisfies (1) with S=R=0. Induction over the finite gate +list proves (1). Two required dense banks force B>=D and give (2). + +The argument applies to total row support across all initial banks. If the +required density is already present in one particular old-input block, it +also lower-bounds this total support. Unknown dirty inputs cannot be treated +as zero to erase those coefficients. + +## Two full chirps + +The paid scan escape in Ross Richardson's #4023 uses, on L internal bits, + +``` +alpha=(1+i)/2, beta=(1-i)/2, +C=[[alpha,beta],[beta,alpha]], C_L=C tensor ... tensor C. +``` + +Both alpha and beta are nonzero. Every row of C_L has exactly 2^L nonzero +entries. The inverse exchanges alpha and beta and has the same density. +Thus either endpoint `diag(C_L,C_L)` or `diag(C_L^-1,C_L)` on two arbitrary +independent banks, with restored dirty helpers if used, requires + +``` +2^R F_(S+1) >= 2^L. (3) +``` + +With no unary native gates, define +`s_L=min { s>=0 : F_(s+1)>=2^L }`. Then S>=s_L. The first working example +is L=3: F_4=3, F_5=5, F_6=8, so S>=5. The earlier single-maximum +support argument gives S>=3 here. Since F_(L+1)<2^L for every L>=1, +the new integer floor strictly improves that estimate. We claim no +implementation attaining s_L. + +For L>=1, the elementary induction F_(s+1)<=phi^s, where +`phi=(1+sqrt(5))/2`, gives the exact real inequality +`S >= L log(2)/log(phi)` when R=0. The displayed integer minimum is the +stronger usable statement. Hence no number of these inter-bank ADD scans +bounded independently of L can produce both chirps without native queries. +For general R, (3) is a necessary tradeoff, not an independent native-query +optimum. Any separate query lower bound keeps its own alphabet hypotheses. + +## Why the distinct-bank premise matters + +Allow a buffered same-bank update `x <- (I+2X_j)x` over F5, where X_j flips +address bit j. It is invertible because its two eigenvalues are 3 and -1. +Three such updates on one eight-coordinate bank give row support eight. +One inter-bank ADD into a second independent bank gives supports 8 and 9. +If all four updates were charged as the theorem's ADDs with R=0, its second +support bound would be F_5=5, which fails. Those first three gates instead +have to be excluded or counted as unary support exponents. This is an +explicit alphabet boundary, not a counterexample to (1). + +## Evidence boundary + +This is a scoped written proof. The finite verifier enumerates support-size +relaxations and executes separate exact F5 matrices as corroboration. +Neither establishes a complete multiplication theorem or a physical tape +cost. The chirp tensor is used only for its density, with its predecessor +construction and invoice cited rather than replayed. Formal proof-kernel +and independent human review are unclaimed. diff --git a/research/fibonacci-scan-floor/README.md b/research/fibonacci-scan-floor/README.md new file mode 100644 index 0000000000..f715e02b8b --- /dev/null +++ b/research/fibonacci-scan-floor/README.md @@ -0,0 +1,102 @@ +# A Fibonacci paid-scan floor for two dense dirty outputs + +For any finite number of arbitrary dirty banks, S inter-bank monomial ADD +scans and unary gates of total row-support exponent R can produce two +output banks of row support D only if + +``` +2^R F_(S+1) >= D, F_0=0, F_1=F_2=1. +``` + +This scoped proof strengthens the earlier single-maximum support bound by +tracking the two largest bank support sizes. Arbitrary per-bank monomial +address/phase maps and permutations of whole banks are granted free. Every +ADD has distinct source and destination banks. [PROOF.md](PROOF.md) states +the full alphabet, induction and its same-bank boundary. + +For the two full L-bit chirps in Ross Richardson's #4023, D=2^L. With no +native gates the necessary scan count is the least s with F_(s+1)>=2^L. +For L=3 this gives five ADDs instead of the inherited support-doubling floor +of three. This is a lower bound; no matching optimal word is claimed. +The selected kappa is unchanged. + +## Evidence and reproduction + +From the repository root, use CPython 3.12 and the standard library: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fibonacci-scan-floor +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fibonacci-scan-floor --check-source-history +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/fibonacci-scan-floor/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/fibonacci-scan-floor/verify.py +``` + +Expected markers are `PASS_FIBONACCI_SCAN_FLOOR` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. The generated [RESULT.json](RESULT.json) +contains all finite counts and SHA256 hashes of the proof, verifier and +metadata. Default replay compares the complete receipt, including JSON +types, and writes nothing. The verifier works in a Git-free package copy. + +The finite evidence includes every distinct sorted support-size relaxation +profile through seven gates for two through five banks, with unary exponents +one and two and total exponent at most four. Distinct-bank shears include +every ordered bank choice. Independent dense F5 executions test actual +cancellation, address permutations and unary operations. Tensor entries +corroborate chirp density through seven internal bits. One-fewer-scan, +invalid-input and same-bank-alphabet controls must reject. + +The all-parameter conclusion rests on the written induction. No predecessor +verifier, native recipe, complete supplier, selected cold replay or proof +assistant is run. General free bank GL, buffered same-bank ADDs counted as +ordinary scans, multi-bank native gates, variable bank volumes and fused +traversals require separate models. Physical routing, precision, restoration +cost and actual runtime remain separate obligations. + +## Scope and sources + +Canonical base `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. +The connector-alphabet-change card changes scope to its cost-aware controller +boundary. Its old connector pairing fixture is not relevant to this alphabet +and is not replayed. The first new fixture is L=3 with two output banks. +The family decision is narrow: retain this quantitative obstruction and stop; +no further construction campaign or frontier change follows from it. + +Ross Richardson's [#4023](https://github.com/CrocSwap/integer-mult-bounds/pull/4023) +supplies the paid two-chirp escape and its explicitly open constant-scan +question. His [#4082](https://github.com/CrocSwap/integer-mult-bounds/pull/4082) +and [#4057](https://github.com/CrocSwap/integer-mult-bounds/pull/4057) supply +the earlier support-doubling and paid-endpoint bounds in their respective +models. The standard union-of-support argument and Fibonacci recurrence +are not claimed as new methods. The new step is the two-bank order-statistic +invariant and the resulting paid-scan/native-support tradeoff. +[SOURCES.json](SOURCES.json) pins predecessor documentation as historical +provenance; no executable predecessor dependency is imported. + +The live overlap scan covered 411 open PRs and 3,920 Discussion records at +2026-10-22 23:04 UTC. Sparse local notes were incomplete. Separate all-main +README and merged-PR searches covered the distinctive object and Fibonacci +terms. This coverage is not a novelty certificate. The canonical +[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134252) +records the question and scope. + +## Open next questions + +1. Find the exact ADD optimum between this lower bound and #4023's cited + six-per-bit construction. Start at L=1 with two banks and explicit + monomial shears. Exact feasibility may depend on available coefficients; + no matching construction is supplied here. +2. Derive a weighted support bound for partial-volume or fused traversals. + Start with a declared row-update and movement tariff. The present count + charges full-bank serial shears, so supplies no runtime price in that model. + +## Credit + +This contribution was produced by Nick Petalas. Apache-2.0. Credit Ross +Richardson for the predecessor constructions, support arguments and open +question, with their retained native and compiler lineage. Independent human +and formal proof-kernel review are unclaimed. + +The verifier uses managed Python allocations. Its fixed finite domains and +explicit profile-capacity check bound live data; no constant-allocation +claim is made. All loops have finite domain bounds and no recursion is used. +Warning-strict normal and optimized replay check the committed artifact. diff --git a/research/fibonacci-scan-floor/RESULT.json b/research/fibonacci-scan-floor/RESULT.json new file mode 100644 index 0000000000..03f6f55a28 --- /dev/null +++ b/research/fibonacci-scan-floor/RESULT.json @@ -0,0 +1,231 @@ +{ + "abstract_layers": [ + [ + 2, + 0, + 1 + ], + [ + 2, + 1, + 3 + ], + [ + 2, + 2, + 16 + ], + [ + 2, + 3, + 63 + ], + [ + 2, + 4, + 226 + ], + [ + 2, + 5, + 727 + ], + [ + 2, + 6, + 2086 + ], + [ + 2, + 7, + 5473 + ], + [ + 3, + 0, + 1 + ], + [ + 3, + 1, + 3 + ], + [ + 3, + 2, + 17 + ], + [ + 3, + 3, + 91 + ], + [ + 3, + 4, + 476 + ], + [ + 3, + 5, + 2339 + ], + [ + 3, + 6, + 10432 + ], + [ + 3, + 7, + 42817 + ], + [ + 4, + 0, + 1 + ], + [ + 4, + 1, + 3 + ], + [ + 4, + 2, + 17 + ], + [ + 4, + 3, + 92 + ], + [ + 4, + 4, + 537 + ], + [ + 4, + 5, + 3074 + ], + [ + 4, + 6, + 17028 + ], + [ + 4, + 7, + 91394 + ], + [ + 5, + 0, + 1 + ], + [ + 5, + 1, + 3 + ], + [ + 5, + 2, + 17 + ], + [ + 5, + 3, + 92 + ], + [ + 5, + 4, + 538 + ], + [ + 5, + 5, + 3202 + ], + [ + 5, + 6, + 19102 + ], + [ + 5, + 7, + 116012 + ] + ], + "abstract_states": 315884, + "chirp_rows": [ + [ + 1, + 2, + 2 + ], + [ + 2, + 4, + 4 + ], + [ + 3, + 8, + 5 + ], + [ + 4, + 16, + 7 + ], + [ + 5, + 32, + 8 + ], + [ + 6, + 64, + 10 + ], + [ + 7, + 128, + 11 + ] + ], + "larger_floors": [ + [ + 8, + 13 + ], + [ + 16, + 24 + ], + [ + 32, + 47 + ], + [ + 64, + 93 + ] + ], + "literal_prefixes": 2304, + "rejection_controls": 10, + "schema": "two-bank-fibonacci-support/v1", + "source_sha256": { + "PROOF.md": "a6475f2145437f5863c30027240c395582bddfdbd8c0c1262a673e9835b5ff36", + "README.md": "df2a41acdc72832eac67350a7d3871299e963a78f6bf4e31717cbda6ee060fc2", + "SOURCES.json": "8b2e217af09d3732bdfd692e120dff5ff52a23bde97fc0755375c6cd7b41fa61", + "TASK.json": "df19e3619166aad33dbdaddd3686eef44d35b92b88fa039d46d05cb1c5667c1e", + "VERIFY.json": "51e04d102ce421450124301bea8da63fde9faa3231c738fa3558491aab1cd0f2", + "verify.py": "e7f9c7b224cf0081a71a32d7efd92dac0e88273a7c076bdd081a76e5dc35d9d2" + } +} diff --git a/research/fibonacci-scan-floor/SOURCES.json b/research/fibonacci-scan-floor/SOURCES.json new file mode 100644 index 0000000000..5fe4a01505 --- /dev/null +++ b/research/fibonacci-scan-floor/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/coupled-tail-support-floor/README.md", + "usage": "provenance", + "git_blob": "b151bb966d6761b1acfc786513e36cf7c18602ff", + "sha256": "3317a2c14b7c9c6cf8ee4bd15189452ea1f84aba3661b096d4f23433c6398890" + }, + { + "path": "research/fixed-support-unary-query-bounds/README.md", + "usage": "provenance", + "git_blob": "29e1f2ba643e36ef43d566d32242bf6950b2ab27", + "sha256": "58f4675f0b6694177bba3a2c8de7bf7d9445f6e87437356e2cf1e33bb090f3d4" + }, + { + "path": "research/fixed-support-unary-query-bounds/ZERO-HELPER-SCAN-COUNTEREXAMPLE.md", + "usage": "provenance", + "git_blob": "96922db4362ef21917424879a49cc23d368097e8", + "sha256": "fef9f157318932c43bf5570c59811bb7e84030315800b9b3e2c021822680e560" + } + ] +} diff --git a/research/fibonacci-scan-floor/TASK.json b/research/fibonacci-scan-floor/TASK.json new file mode 100644 index 0000000000..3e21a20824 --- /dev/null +++ b/research/fibonacci-scan-floor/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the two-bank Fibonacci row-support invariant and its paid ADD/native-support tradeoff for two full dirty chirps.", + "scope_change_reason": "The fixed-support predecessor explicitly leaves a quantitative constant-scan ADDRESS model open; this contribution charges inter-bank monomial shears rather than enlarging the old connector alphabet.", + "bottleneck_link": "Refines the exponential support floor for paid controllers; no complete supplier or exponent gain is inferred.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved two-bank support improvement with finite exact corroboration; do not seek a matching optimal word.", + "outcome": "completed", + "evidence": "PROOF.md supplies the quantified induction; verify.py regenerates the source-bound RESULT.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact inter-bank ADD optimum for two full L-bit chirps?", + "why_it_matters": "The necessary Fibonacci floor and the cited six-per-bit construction need not match.", + "first_step": "Solve L=1 with two banks, explicit monomial shears and exact coefficients.", + "blocked_by": "No matching construction or stronger exact-cost proof is supplied." + }, + { + "question": "What weighted support bound holds for partial-volume or fused traversals?", + "why_it_matters": "A serial full-bank ADD count does not price a different movement model.", + "first_step": "Declare one exact row-update alphabet and its physical movement tariff.", + "blocked_by": "The current model has equal volumes and one paid ADD per scan." + } + ] +} diff --git a/research/fibonacci-scan-floor/VERIFY.json b/research/fibonacci-scan-floor/VERIFY.json new file mode 100644 index 0000000000..1d55276ab4 --- /dev/null +++ b/research/fibonacci-scan-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 support-profile enumeration, literal F5 traces, tensor density, strict threshold and alphabet controls, full source-bound receipt" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete mathematical and source-bound receipt under optimized Python" + } + ] +} diff --git a/research/fibonacci-scan-floor/verify.py b/research/fibonacci-scan-floor/verify.py new file mode 100644 index 0000000000..7deaaa704f --- /dev/null +++ b/research/fibonacci-scan-floor/verify.py @@ -0,0 +1,212 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the two-bank support bound. Apache-2.0.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +MAX_STATES = 200_000 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def fibonacci(index): + require(type(index) is int and 0 <= index <= 4096, "Fibonacci index") + left, right = 0, 1 + for _ in range(index): + left, right = right, left + right + return left + + +def scan_floor(density, exponent=0): + require(type(density) is int and 1 <= density <= 2**1024, "density") + require(type(exponent) is int and 0 <= exponent <= 1024, "exponent") + for scans in range(2049): + if 2**exponent * fibonacci(scans + 1) >= density: + return scans + raise ValueError("bounded Fibonacci search exhausted") + + +def check_profile(profile, scans, exponent): + scale = 2**exponent + require(profile[0] <= scale * fibonacci(scans + 2), "largest bank") + require(profile[1] <= scale * fibonacci(scans + 1), "second bank") + + +def successors(profile, scans, exponent): + """Overapproximate row-support unions, including every bank choice.""" + for target, source in itertools.permutations(range(len(profile)), 2): + sizes = list(profile) + sizes[target] += sizes[source] + yield tuple(sorted(sizes, reverse=True)), scans + 1, exponent + for rank in (1, 2): + if exponent + rank <= 4: + for target in range(len(profile)): + sizes = list(profile) + sizes[target] *= 2**rank + yield tuple(sorted(sizes, reverse=True)), scans, exponent + rank + + +def abstract_profiles(): + layers = [] + for banks in range(2, 6): + states = {((1,) * banks, 0, 0)} + for depth in range(8): + for profile, scans, exponent in states: + check_profile(profile, scans, exponent) + layers.append([banks, depth, len(states)]) + if depth < 7: + following = set() + for profile, scans, exponent in states: + following.update(successors(profile, scans, exponent)) + require(len(following) <= MAX_STATES, "profile capacity") + states = following + return layers + + +def support(matrix, width): + sizes = [] + for start in range(0, len(matrix), width): + sizes.append(max(sum(value != 0 for value in row) + for row in matrix[start:start + width])) + return tuple(sorted(sizes, reverse=True)) + + +def shear(matrix, width, target, source, shift, scalar): + require(target != source, "distinct shear banks") + for row in range(width): + old = matrix[target * width + row] + incoming = matrix[source * width + (row + shift) % width] + matrix[target * width + row] = [ + (a + scalar * b) % 5 for a, b in zip(old, incoming, strict=True) + ] + + +def unary(matrix, width, bank, axis): + """Invertible I+2X_axis over F5, with row support two.""" + saved = [row[:] for row in matrix[bank * width:(bank + 1) * width]] + for row in range(width): + matrix[bank * width + row] = [ + (a + 2 * b) % 5 + for a, b in zip(saved[row], saved[row ^ (1 << axis)], strict=True) + ] + + +def identity(dimension): + return [[int(row == column) for column in range(dimension)] + for row in range(dimension)] + + +def literal_traces(): + checked = 0 + for banks, bits, seed in itertools.product(range(2, 6), range(1, 5), range(6)): + width = 2**bits + matrix = identity(banks * width) + scans, exponent = 0, 0 + for step in range(24): + target = (seed + step) % banks + if step % 5 == 2: + unary(matrix, width, target, (seed + step) % bits) + exponent += 1 + else: + source = (target + 1 + step % (banks - 1)) % banks + shear(matrix, width, target, source, step % width, 1 + step % 4) + scans += 1 + # A per-bank address permutation does not change support. + start = target * width + matrix[start:start + width] = matrix[start:start + width][::-1] + check_profile(support(matrix, width), scans, exponent) + checked += 1 + return checked + + +def chirp_densities(): + """Direct tensor entries of C=[[alpha,beta],[beta,alpha]], modulo five.""" + rows = [] + for bits in range(1, 8): + width = 2**bits + for output in range(width): + entries = [] + for incoming in range(width): + entry = 1 + for axis in range(bits): + entry = entry * (2 if (output ^ incoming) >> axis & 1 else 4) % 5 + entries.append(entry) + require(all(entries), "dense chirp tensor row") + rows.append([bits, width, scan_floor(width)]) + return rows + + +def boundary_controls(): + rejected = 0 + for density, exponent in ((2, 0), (8, 0), (16, 0), (8, 1), (128, 2)): + floor = scan_floor(density, exponent) + require(floor > 0, "positive control floor") + require(2**exponent * fibonacci(floor) < density, "one fewer scan rejects") + rejected += 1 + for args in ((0, 0), (True, 0), (8, -1), (8, True)): + try: + scan_floor(*args) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid argument accepted") + # Permitting buffered same-bank additions invalidates this alphabet. + matrix = identity(16) + for axis in range(3): + unary(matrix, 8, 0, axis) + shear(matrix, 8, 1, 0, 0, 1) + require(support(matrix, 8)[1] == 8 > fibonacci(5), "same-bank boundary") + try: + check_profile(support(matrix, 8), 4, 0) + except ValueError: + rejected += 1 + else: + raise ValueError("same-bank mutant accepted") + return rejected + + +def build_receipt(): + layers = abstract_profiles() + result = { + "schema": "two-bank-fibonacci-support/v1", + "abstract_layers": layers, + "abstract_states": sum(row[2] for row in layers), + "literal_prefixes": literal_traces(), + "chirp_rows": chirp_densities(), + "rejection_controls": boundary_controls(), + "larger_floors": [[bits, scan_floor(2**bits)] for bits in (8, 16, 32, 64)], + } + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result["source_sha256"] = { + name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() for name in names + } + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="author a new, source-bound receipt") + args = parser.parse_args() + result = build_receipt() + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.write is not None: + with args.write.open("x", encoding="utf-8") as stream: + require(stream.write(encoded) == len(encoded), "complete receipt write") + else: + expected = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + require(json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + "complete source-bound receipt mismatch") + print("PASS_FIBONACCI_SCAN_FLOOR " + json.dumps({ + key: value for key, value in result.items() if key not in ("source_sha256", "abstract_layers") + }, sort_keys=True)) + + +if __name__ == "__main__": + main()