From f39226f49486f44e9771b88121ad11f9d0b76eee Mon Sep 17 00:00:00 2001 From: Johnny Franks Date: Tue, 13 Oct 2026 00:59:12 -0400 Subject: [PATCH] Add uniform proof and exact checks for archived stage bound --- .github/workflows/cross-shear-stage-bound.yml | 36 + research/cross-shear-stage-bound/CLAIM.json | 55 ++ research/cross-shear-stage-bound/README.md | 220 ++++++ research/cross-shear-stage-bound/RESULT.json | 684 ++++++++++++++++++ .../cross-shear-stage-bound/SOURCE-PINS.json | 28 + .../cross-shear-stage-bound/VALIDATION.json | 111 +++ .../evidence/M-RESULT.md | 298 ++++++++ .../evidence/NOTICE.md | 13 + research/cross-shear-stage-bound/verify.py | 306 ++++++++ 9 files changed, 1751 insertions(+) create mode 100644 .github/workflows/cross-shear-stage-bound.yml create mode 100644 research/cross-shear-stage-bound/CLAIM.json create mode 100644 research/cross-shear-stage-bound/README.md create mode 100644 research/cross-shear-stage-bound/RESULT.json create mode 100644 research/cross-shear-stage-bound/SOURCE-PINS.json create mode 100644 research/cross-shear-stage-bound/VALIDATION.json create mode 100644 research/cross-shear-stage-bound/evidence/M-RESULT.md create mode 100644 research/cross-shear-stage-bound/evidence/NOTICE.md create mode 100644 research/cross-shear-stage-bound/verify.py diff --git a/.github/workflows/cross-shear-stage-bound.yml b/.github/workflows/cross-shear-stage-bound.yml new file mode 100644 index 0000000000..12ccfbe89c --- /dev/null +++ b/.github/workflows/cross-shear-stage-bound.yml @@ -0,0 +1,36 @@ +name: Cross-shear stage bound + +on: + pull_request: + paths: + - 'research/cross-shear-stage-bound/**' + - 'research/experiment-log/campaign-100/**' + - 'research/e8-bit-r420/NOTICE.md' + - 'research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py' + - '.github/workflows/cross-shear-stage-bound.yml' + push: + paths: + - 'research/cross-shear-stage-bound/**' + - 'research/experiment-log/campaign-100/**' + - 'research/e8-bit-r420/NOTICE.md' + - 'research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py' + - '.github/workflows/cross-shear-stage-bound.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + verify: + runs-on: ubuntu-latest + timeout-minutes: 5 + strategy: + matrix: + python: ['3.11', '3.14'] + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: ${{ matrix.python }} + - run: python -I -B research/cross-shear-stage-bound/verify.py + - run: python -I -O -B research/cross-shear-stage-bound/verify.py diff --git a/research/cross-shear-stage-bound/CLAIM.json b/research/cross-shear-stage-bound/CLAIM.json new file mode 100644 index 0000000000..83eacd0589 --- /dev/null +++ b/research/cross-shear-stage-bound/CLAIM.json @@ -0,0 +1,55 @@ +{ + "track": "research consolidation", + "assignment_seed": 97, + "randomness": "Python secrets.randbelow(100), operating-system randomness", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "candidates": [ + { + "task": "Reconcile selected #626 Linux replay status", + "decision": "declined: open PR695 already covers it" + }, + { + "task": "Bind review-ledger decisions to source pins", + "decision": "declined: open PR704 already covers it" + }, + { + "task": "Resolve the uniform stage-count claim in archived campaign report M", + "decision": "selected" + } + ], + "seed_use": "Campaign idea 97 points to report M; focus on its finite-versus-uniform stage-count evidence rather than the newest bound.", + "object": "Report M section 1: k >= 2P+1 for P bank pairs, rank-v cross-block shears, arbitrary invertible within-block bridges", + "method": "Rank potential rank(A)+rank(D) for the two diagonal blocks; first-call zero progress; exact integer controller witnesses and finite-field negative controls", + "deliverable": "Scoped written proof, independent executable witness checks, source pins, and reconciliation of historical evidence scope; no new kappa", + "coordination": "No pinned issues exist; only open issue #650 concerns enabling Discussions. Local claim per sprint instructions.", + "open_pr_count_at_claim": 544, + "maximum_open_pr_at_claim": 725, + "overlap_review": [ + 288, + 397, + 446, + 657, + 695, + 704, + 705, + 720 + ], + "expected_finish_utc": "2026-10-13T05:31:00Z", + "status": "completed: uniform stage-count conclusion supported", + "contributor": "Johnny Franks (0xjohnnydev)", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human review claimed.", + "completed_utc": "2026-10-13T04:58:56+00:00", + "result": { + "statement": "Over every field, P pairs of v-dimensional blocks require at least 2P+1 rank-at-most-v cross shears, with arbitrary invertible within-block bridges; the existing borrowing chain attains the count.", + "link": "https://github.com/0xjohnnydev/integer-mult-bounds/blob/codex/reconcile-cross-shear-stage-bound/research/cross-shear-stage-bound/README.md", + "new_kappa": false, + "evidence": "Written uniform rank proof; 28 exact rational witnesses; 20160 binary prefixes; 362880 cross-call and 725760 bridge transitions; 276 endpoint mutation controls.", + "verification": "Clean-tree runs on Python 3.9.6, 3.12.14 and 3.14.8, normal and optimized; source/coverage corruption rejected.", + "overlap_refresh": { + "open_pr_count": 551, + "maximum_pr": 732, + "same_scope_found": false, + "cited_positive_identity_pr": 397 + } + } +} diff --git a/research/cross-shear-stage-bound/README.md b/research/cross-shear-stage-bound/README.md new file mode 100644 index 0000000000..b7b20d76ad --- /dev/null +++ b/research/cross-shear-stage-bound/README.md @@ -0,0 +1,220 @@ +# A uniform stage-count proof for the archived borrowing model + +**Research consolidation; no new kappa.** In the model below, swapping two +blocks of dimension `P*v` needs at least `2P + 1` cross-block calls when each +call has rank at most `v`. The existing borrowing chain attains this count. +This note supplies a short proof for every positive `P` and `v`, over every +field. It does not claim a new controller or a lower bound for multiplication. + +## The evidence discrepancy being resolved + +The archived campaign's [report M, section 1](evidence/M-RESULT.md) concludes +that fewer than `2P + 1` stages are impossible in its model. Its supporting +discussion gives a small-pattern rank argument for at most four calls and +reports finite searches for `P <= 3`. Its general count of at least `P` upper +and `P` lower calls gives only `2P`; the extra call needs a separate argument. +The proof below provides that argument. **The stage-count conclusion survives +this audit.** No counterexample to it, failed search, or new saving is reported. + +The original report and its notice are retained byte for byte. Their other +claims, historical timings, recommendations, and local paths are not audited +or adopted here. The campaign index already labels this material as historical +and distinguishes analysis from completed experiments. We preserve that scope. + +Assignment seed **97** selected research consolidation. Campaign idea 97 links +to report M, which led to this specific obligation. [CLAIM.json](CLAIM.json) +records the alternatives, overlap checks, and local claim. No pinned sprint +issue existed. Base commit: +`66849e1475c930fd7732b1a0067ffee7e1e95f60`. + +## Exact model + +Let `F` be any field, let `d = P*v`, and write the data as `(X,Y)` with +`X,Y in F^d`. A **shear** adds a linear function of one block to the other. +The counted calls are + +```text +L(E) = [ I 0 ] U(H) = [ I H ] + [ E I ] [ 0 I ], +``` + +where `rank(E) <= v` or `rank(H) <= v`. Rank means the number of independent +columns. A **bridge** is any `diag(S,T)` with `S,T` invertible `d` by `d` +matrices. Arbitrarily many bridges may occur anywhere, including at both ends. +Bridges can mix ports within a block. They are not limited to pairwise adds. + +The starting map is the identity. The required endpoint, **before the +designated terminal exchange**, is block antidiagonal: + +```text +[ 0 C ] +[ D 0 ], C and D invertible. +``` + +The usual controller has `C = -I`, `D = I`; the final signed exchange then +restores the data. The exchange is not an allowed bridge inside this model. +If the only endpoint requirement were identity, doing nothing would suffice. + +"Uncounted" bridges are a relaxation for this call-count lower bound. They +still require scalar work and legal frames in an implemented controller. +Auxiliary registers are not extra state in this model. To apply the result to +a supplier, each complete invocation must satisfy its normalized data-shear +contract; its helpers, restoration, frames, and physical costs remain separate +obligations. Calls that change both blocks at once are outside this model. + +## Uniform lower bound + +Write the matrix of a prefix as + +```text +M = [ A B ] + [ C D ] +``` + +and define `Phi(M) = rank(A) + rank(D)`. Initially `Phi = 2d`. At the required +endpoint `Phi = 0`. + +1. Left multiplication by a bridge replaces `A,D` by `S*A,T*D`. Both ranks + stay unchanged because `S,T` are invertible. +2. A lower call replaces `D` by `D + E*B` and leaves `A` unchanged. The rank + inequality `rank(R + Q) >= rank(R) - rank(Q)` and + `rank(E*B) <= rank(E)` show that its decrease in `Phi` is at most `v`. + An upper call replaces `A` by `A + H*C`, with the same conclusion. +3. Before the **first** counted call, all preceding bridges have left the + prefix block diagonal, so `B = C = 0`. The first call changes neither `A` + nor `D`. Its decrease in `Phi` is exactly zero. + +Zero counted calls cannot reach a block-antidiagonal invertible endpoint. +With `k >= 1` calls, summing the decreases gives + +```text +2d <= (k - 1)*v, hence k >= 1 + ceil(2d/v) = 2P + 1. +``` + +Intermediate increases in `Phi` do not affect this inequality. No reduction +modulo a prime, finite search, alternating-pattern assumption, or common port +basis is used. In particular, arbitrary invertible within-block bridges cannot +remove the first call's zero progress. + +The proof also gives the useful weighted statement: if the actual ranks of +the calls are `r_1,...,r_k`, then `sum(r_i for i >= 2) >= 2d`. We do not claim +that this bound is always attainable for a prescribed unequal rank list. + +## Why the existing count is sharp + +This is the existing Sussman borrowing chain, not a new construction. Index +the bank pairs by `j = 0,...,P-1`, each of width `v`. Start with `Y_0 += X_0`. +For each `j` in increasing order: + +1. Make the counted call `X_j -= Y_j`. +2. If there is a next pair, bridge with + `X_j += X_(j+1)` and `Y_(j+1) -= Y_j`. +3. Make the counted call `Y_j += X_j`. +4. If there is a next pair, bridge with + `X_j -= X_(j+1)` and `Y_(j+1) += Y_j`. + +Finally, for `j = P-2,...,0` in decreasing order, bridge with +`X_(j+1) += X_j` and `Y_j -= Y_(j+1)`. + +Here is an all-size scalar check. Let the original data be `(x_j,y_j)`, and +put `t_-1 = 0`, `t_j = y_j - t_(j-1)`. On entry to iteration `j`, the active +pair is `(x_j, x_j + t_j)`. Its exit values are +`X_j = -t_j` and `Y_j = x_j + x_(j+1)`, except that the last pair exits with +`Y_(P-1) = x_(P-1)`. The bridges prepare the next entry pair with +`t_(j+1) = y_(j+1) - t_j`. Descending cleanup then gives `X_j = -y_j` and +`Y_j = x_j` for every `j`. These identities hold over the integers and hence +over any field. Tensoring with `I_v` gives rank-`v` counted calls. + +There are exactly `2P + 1` counted calls and `6(P - 1)` elementary bridge +adds, followed by the terminal signed exchange. This establishes sharpness +of the call count only. It says nothing about optimal idle transitions, +helper stock, copied information, moment costs, or an optimal kappa. + +## Reproduce the finite evidence + +From the repository root, with Python 3.9 or newer: + +```sh +python3 -I -B research/cross-shear-stage-bound/verify.py +``` + +Expected final line: + +```text +PASS_CROSS_SHEAR_STAGE_BOUND 28 rational witnesses; 20160 F2 prefixes; 362880 cross-call and 725760 bridge transitions +``` + +The command uses only the standard library, performs no network requests, +writes no files, and compares every result with [RESULT.json](RESULT.json). +All rejection checks remain active under `-O`. `--write-result NEW_PATH` +instead saves freshly computed evidence and refuses to overwrite a file. +Recorded interpreter, clean-tree, and corruption checks are in +[VALIDATION.json](VALIDATION.json). The path-filtered workflow runs normal and +optimized checks on Linux with Python 3.11 and 3.14; its presence alone is not +evidence that hosted CI has passed. + +The checks cover: + +- Seven pinned input files, including the preserved historical report and + the controller source. Only its inspected `recipe` function is evaluated; + no supplier imports or replay jobs run. +- Equality of the independent, grouped-coordinate word with the pinned + recipe for every `P` from 1 through 16. This exercises the scalar recipe + beyond the physical driver's supported sizes; it does not certify those + physical layouts. +- Exact rational replay for `P = 1,...,16` at `v = 1`, and `P = 1,...,6` at + each of `v = 2,3`. Each witness attains every available potential decrease + and restores the data after the signed exchange. +- Every invertible four-by-four binary prefix: 20,160 matrices. For each, + all 18 nonzero rank-one cross-block calls satisfy the rank inequality and + all 36 invertible block-diagonal bridges preserve the potential. All 648 + first-call cases have zero progress. This uses a separate bit-packed rank + implementation, not rational elimination or any repository rank engine. +- Omission and sign reversal of every counted call and every elementary + bridge in the words with `P = 1,...,6`. These controls check the actual + wrong signed-swap endpoint, rather than merely rejecting a changed operation + count. Every omitted counted call also leaves a nonzero diagonal block, so + it fails even the more permissive antidiagonal endpoint condition. +- Hypothesis controls: a rank-two three-call swap defeats an incorrectly + applied rank-one five-call bound; a cross-block exchange and a singular + diagonal map can lower the potential if admitted as bridges; identity is + not the required endpoint. A matrix with different rational and binary + ranks checks the distinction between the two arithmetic implementations. + +This is a complete census of the stated finite domain, not a search for a +new construction. There is no solver or time-based stopping rule. The proof +above, rather than extrapolation from these tests, establishes the uniform +claim. No proof-assistant or independent human verification is claimed. + +## Sources, overlap, and scope + +[SOURCE-PINS.json](SOURCE-PINS.json) records exact source hashes. The original +report is from Rohan Arun's [PR368 at fa8ab946](https://github.com/rohanarun/integer-mult-bounds/blob/fa8ab946df57ebadae1a470b637c2a590a0a5317/research/campaign-100-results/reports/M-RESULT.md). +The main-branch campaign index is the later PR477 integration. The executable +recipe is the unchanged `global_k.py` preserved by #543 from the +#510/#463/#443/#436/#386 controller lineage. Its original notice retains +the contributor credit. + +Jacob Sussman's bridge construction and the #234/#363/#373/#375 lineage +already provide the borrowing mechanism. [PR397](https://github.com/CrocSwap/integer-mult-bounds/pull/397) +at `cb6455fa1e9af68be47c33948d3d1a6f0717a5e4` separately formalizes the +indexed scalar identity. That Lean package is cited, not imported or rebuilt; +we make no priority claim for the identity or its arbitrary-size validity. +The added result here is the explicit rank-potential lower-bound proof and +its reconciliation with the archived stage exclusion. + +The checked nearby PRs concern different obligations: #695 records Linux +execution provenance; #704 binds review-ledger metadata; #705 bounds complex +rank-homogeneous paths; #720 treats an abelian three-register bit model. +None is a dependency of this proof. #288 and #446 also remain distinct +model-specific obstruction packages. + +The selected conditional result remains +`51110230636731/31250000000000000`. No selected certificate, upstream source, +or construction is changed. All inherited compiler, physical realization, +hosting, restoration, precision/tape, and analytic obligations remain. + +Prepared by **Johnny Franks (0xjohnnydev)** with substantial **OpenAI Codex** +assistance in analysis, implementation, and writing. New work is Apache-2.0. +See the preserved [historical notice](evidence/NOTICE.md) and the pinned +controller notice for predecessor attribution and AI disclosures. diff --git a/research/cross-shear-stage-bound/RESULT.json b/research/cross-shear-stage-bound/RESULT.json new file mode 100644 index 0000000000..131bbedd2b --- /dev/null +++ b/research/cross-shear-stage-bound/RESULT.json @@ -0,0 +1,684 @@ +{ + "status": "PASS_CROSS_SHEAR_STAGE_BOUND", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "input_files_checked": 7, + "source_recipe_pairs_checked": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16 + ], + "rational_witnesses": [ + { + "pairs": 1, + "width": 1, + "paid_calls": 3, + "bridge_shears": 0, + "potential_after_paid": [ + 2, + 2, + 1, + 0 + ] + }, + { + "pairs": 2, + "width": 1, + "paid_calls": 5, + "bridge_shears": 6, + "potential_after_paid": [ + 4, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 3, + "width": 1, + "paid_calls": 7, + "bridge_shears": 12, + "potential_after_paid": [ + 6, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 4, + "width": 1, + "paid_calls": 9, + "bridge_shears": 18, + "potential_after_paid": [ + 8, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 5, + "width": 1, + "paid_calls": 11, + "bridge_shears": 24, + "potential_after_paid": [ + 10, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 6, + "width": 1, + "paid_calls": 13, + "bridge_shears": 30, + "potential_after_paid": [ + 12, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 7, + "width": 1, + "paid_calls": 15, + "bridge_shears": 36, + "potential_after_paid": [ + 14, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 8, + "width": 1, + "paid_calls": 17, + "bridge_shears": 42, + "potential_after_paid": [ + 16, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 9, + "width": 1, + "paid_calls": 19, + "bridge_shears": 48, + "potential_after_paid": [ + 18, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 10, + "width": 1, + "paid_calls": 21, + "bridge_shears": 54, + "potential_after_paid": [ + 20, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 11, + "width": 1, + "paid_calls": 23, + "bridge_shears": 60, + "potential_after_paid": [ + 22, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 12, + "width": 1, + "paid_calls": 25, + "bridge_shears": 66, + "potential_after_paid": [ + 24, + 24, + 23, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 13, + "width": 1, + "paid_calls": 27, + "bridge_shears": 72, + "potential_after_paid": [ + 26, + 26, + 25, + 24, + 23, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 14, + "width": 1, + "paid_calls": 29, + "bridge_shears": 78, + "potential_after_paid": [ + 28, + 28, + 27, + 26, + 25, + 24, + 23, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 15, + "width": 1, + "paid_calls": 31, + "bridge_shears": 84, + "potential_after_paid": [ + 30, + 30, + 29, + 28, + 27, + 26, + 25, + 24, + 23, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 16, + "width": 1, + "paid_calls": 33, + "bridge_shears": 90, + "potential_after_paid": [ + 32, + 32, + 31, + 30, + 29, + 28, + 27, + 26, + 25, + 24, + 23, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ] + }, + { + "pairs": 1, + "width": 2, + "paid_calls": 3, + "bridge_shears": 0, + "potential_after_paid": [ + 4, + 4, + 2, + 0 + ] + }, + { + "pairs": 1, + "width": 3, + "paid_calls": 3, + "bridge_shears": 0, + "potential_after_paid": [ + 6, + 6, + 3, + 0 + ] + }, + { + "pairs": 2, + "width": 2, + "paid_calls": 5, + "bridge_shears": 6, + "potential_after_paid": [ + 8, + 8, + 6, + 4, + 2, + 0 + ] + }, + { + "pairs": 2, + "width": 3, + "paid_calls": 5, + "bridge_shears": 6, + "potential_after_paid": [ + 12, + 12, + 9, + 6, + 3, + 0 + ] + }, + { + "pairs": 3, + "width": 2, + "paid_calls": 7, + "bridge_shears": 12, + "potential_after_paid": [ + 12, + 12, + 10, + 8, + 6, + 4, + 2, + 0 + ] + }, + { + "pairs": 3, + "width": 3, + "paid_calls": 7, + "bridge_shears": 12, + "potential_after_paid": [ + 18, + 18, + 15, + 12, + 9, + 6, + 3, + 0 + ] + }, + { + "pairs": 4, + "width": 2, + "paid_calls": 9, + "bridge_shears": 18, + "potential_after_paid": [ + 16, + 16, + 14, + 12, + 10, + 8, + 6, + 4, + 2, + 0 + ] + }, + { + "pairs": 4, + "width": 3, + "paid_calls": 9, + "bridge_shears": 18, + "potential_after_paid": [ + 24, + 24, + 21, + 18, + 15, + 12, + 9, + 6, + 3, + 0 + ] + }, + { + "pairs": 5, + "width": 2, + "paid_calls": 11, + "bridge_shears": 24, + "potential_after_paid": [ + 20, + 20, + 18, + 16, + 14, + 12, + 10, + 8, + 6, + 4, + 2, + 0 + ] + }, + { + "pairs": 5, + "width": 3, + "paid_calls": 11, + "bridge_shears": 24, + "potential_after_paid": [ + 30, + 30, + 27, + 24, + 21, + 18, + 15, + 12, + 9, + 6, + 3, + 0 + ] + }, + { + "pairs": 6, + "width": 2, + "paid_calls": 13, + "bridge_shears": 30, + "potential_after_paid": [ + 24, + 24, + 22, + 20, + 18, + 16, + 14, + 12, + 10, + 8, + 6, + 4, + 2, + 0 + ] + }, + { + "pairs": 6, + "width": 3, + "paid_calls": 13, + "bridge_shears": 30, + "potential_after_paid": [ + 36, + 36, + 33, + 30, + 27, + 24, + 21, + 18, + 15, + 12, + 9, + 6, + 3, + 0 + ] + } + ], + "exhaustive_f2": { + "invertible_prefixes": 20160, + "rank_one_transitions": 362880, + "bridge_transitions": 725760, + "first_call_checks": 648, + "rank_drop_histogram": { + "-1": 93312, + "0": 176256, + "1": 93312 + } + }, + "negative_controls": { + "endpoint_hypothesis_is_necessary": 1, + "omitted_free": 90, + "omitted_paid": 48, + "rank_cap_is_necessary": 1, + "rational_vs_binary_rank": 1, + "singular_bridge_changes_potential": 1, + "terminal_exchange_is_not_a_bridge": 1, + "wrong_sign_free": 90, + "wrong_sign_paid": 48 + }, + "scope": "Finite supporting evidence for the written rank proof; no physical supplier, all-size, or multiplication-theorem verification." +} diff --git a/research/cross-shear-stage-bound/SOURCE-PINS.json b/research/cross-shear-stage-bound/SOURCE-PINS.json new file mode 100644 index 0000000000..b4e0745a45 --- /dev/null +++ b/research/cross-shear-stage-bound/SOURCE-PINS.json @@ -0,0 +1,28 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "files": { + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8", + "research/e8-bit-r420/NOTICE.md": "12ba6e0845f222e9940b00f6c60d261db104246a8d3143da267682973479f811", + "research/experiment-log/campaign-100/README.md": "35231f9020c2d1dfd5a9a877c778d640f9c5a04101ea8e635ec98c7fa19b3e3c", + "research/experiment-log/campaign-100/analytic-theory.md": "43534dfec4f206ae91dda02e52e27ece94579128e5e9113293fa7e45690e1345", + "research/experiment-log/campaign-100/architectures-and-stages.md": "733ea7d90301081423ad6a4e5c26ce6005215ebd188688dec65567fd54a11f44", + "research/cross-shear-stage-bound/evidence/M-RESULT.md": "fd4b0f80eef427a6e5d8013ea19abe43c8a85f5826e7c8a22acc4655bebf3a68", + "research/cross-shear-stage-bound/evidence/NOTICE.md": "0713737458d843b8d51382d051d9f201196a9c7a4fcca773d2a61f65a9912454" + }, + "historical_source": { + "repository": "https://github.com/rohanarun/integer-mult-bounds", + "commit": "fa8ab946df57ebadae1a470b637c2a590a0a5317", + "pull_request": 368, + "paths": [ + "research/campaign-100-results/reports/M-RESULT.md", + "research/campaign-100-results/NOTICE.md" + ], + "preservation": "Complete original bytes retained under evidence/. Other historical claims are not audited here." + }, + "related_formalization": { + "pull_request": 397, + "head": "cb6455fa1e9af68be47c33948d3d1a6f0717a5e4", + "scope": "Predecessor scalar identity formalization; cited, not imported or rebuilt." + }, + "method": "Exact rational rank and integer row updates; separate bit-packed F2 elimination. No external dependencies." +} diff --git a/research/cross-shear-stage-bound/VALIDATION.json b/research/cross-shear-stage-bound/VALIDATION.json new file mode 100644 index 0000000000..c258323c0d --- /dev/null +++ b/research/cross-shear-stage-bound/VALIDATION.json @@ -0,0 +1,111 @@ +{ + "status": "focused verification passed", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "sha256": { + "verify.py": "55d1077d1af2345c037e4f07dee485f3686254f33fa4260a6f389fd00179ca17", + "RESULT.json": "6e54dd593f207062acc6bec3a4810b6ebad2e329a154e965f7fc10ecc94b5612", + "SOURCE-PINS.json": "b0be44290994e1aa9f5541645e1eddc2872687890415d07b0890526cd8cfed50" + }, + "portable_tree": "Only the declared input files, checker, input manifest and expected result; no .git, site packages or generated supplier output.", + "working_directory": "Outside the portable repository root", + "runs": [ + { + "case": "Python 3.14.8 isolated", + "flags": [ + "-I", + "-B" + ], + "returncode": 0, + "elapsed_seconds": 1.3279, + "observed": "PASS_CROSS_SHEAR_STAGE_BOUND 28 rational witnesses; 20160 F2 prefixes; 362880 cross-call and 725760 bridge transitions" + }, + { + "case": "Python 3.14.8 optimized", + "flags": [ + "-I", + "-O", + "-B" + ], + "returncode": 0, + "elapsed_seconds": 1.4158, + "observed": "PASS_CROSS_SHEAR_STAGE_BOUND 28 rational witnesses; 20160 F2 prefixes; 362880 cross-call and 725760 bridge transitions" + }, + { + "case": "Python 3.9.6 isolated", + "flags": [ + "-I", + "-B" + ], + "returncode": 0, + "elapsed_seconds": 2.1519, + "observed": "PASS_CROSS_SHEAR_STAGE_BOUND 28 rational witnesses; 20160 F2 prefixes; 362880 cross-call and 725760 bridge transitions" + }, + { + "case": "Python 3.9.6 optimized", + "flags": [ + "-I", + "-O", + "-B" + ], + "returncode": 0, + "elapsed_seconds": 2.1499, + "observed": "PASS_CROSS_SHEAR_STAGE_BOUND 28 rational witnesses; 20160 F2 prefixes; 362880 cross-call and 725760 bridge transitions" + }, + { + "case": "Python 3.12.14 isolated", + "flags": [ + "-I", + "-B" + ], + "returncode": 0, + "elapsed_seconds": 1.1944, + "observed": "PASS_CROSS_SHEAR_STAGE_BOUND 28 rational witnesses; 20160 F2 prefixes; 362880 cross-call and 725760 bridge transitions" + }, + { + "case": "Python 3.12.14 optimized", + "flags": [ + "-I", + "-O", + "-B" + ], + "returncode": 0, + "elapsed_seconds": 1.2462, + "observed": "PASS_CROSS_SHEAR_STAGE_BOUND 28 rational witnesses; 20160 F2 prefixes; 362880 cross-call and 725760 bridge transitions" + }, + { + "case": "damaged source rejected", + "flags": [ + "-I", + "-O", + "-B" + ], + "returncode": 1, + "elapsed_seconds": 0.1214, + "observed": "ValueError: source pin mismatch: research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py" + }, + { + "case": "incomplete coverage receipt rejected", + "flags": [ + "-I", + "-B" + ], + "returncode": 1, + "elapsed_seconds": 1.3186, + "observed": "ValueError: finite evidence differs from RESULT.json" + }, + { + "case": "optimized incomplete coverage receipt rejected", + "flags": [ + "-I", + "-O", + "-B" + ], + "returncode": 1, + "elapsed_seconds": 1.405, + "observed": "ValueError: finite evidence differs from RESULT.json" + } + ], + "workflow_syntax": "Parsed successfully with Ruby YAML; no hosted CI result implied.", + "scope": "The finite checks support the written proof; this is neither a proof-assistant result nor a full multiplication-theorem verification." +} diff --git a/research/cross-shear-stage-bound/evidence/M-RESULT.md b/research/cross-shear-stage-bound/evidence/M-RESULT.md new file mode 100644 index 0000000000..6f913c7d92 --- /dev/null +++ b/research/cross-shear-stage-bound/evidence/M-RESULT.md @@ -0,0 +1,298 @@ +# M-math — feasibility memos for the [math] items (18, 21, 26 in depth; 23, 20, 49, 50, 53/97, 59, 60; one-liners for 28, 8/46/47/48/51/52/54) + +Baseline: #325 package (`/private/tmp/imbwork/w325/research/five-stage-p10b-banks`, p = 10, h = 20, v = 960, m = 100, +κ = 7.69684039383334e-4). Histogram and sensitivities from the certificate agent +(`/tmp/radical/B-certificate-whatif/RESULT.md`): Δκ ≈ +3.8e-7 per unit of five-stage deficit, ≈ −2.9e-10 per +unit of five-stage J (per replica); five-stage J = 2,645,397 of which idle 225,855 (8.5 %), 5×local 2,419,542. +Nothing heavy was run. Three small exhaustive F₂/F₃ searches (seconds to minutes, one core) are in +`/tmp/radical/M/M_search.py`, `M_idle.py`, `M_idle2.py`, `M_portmix.py`, `M_p3k6.py`; their outputs are quoted below. + +## 0. The pricing chain in one paragraph (what every item has to go through) + +1. The local word's role chains are nested, ascending frame chains; every rank-d step is one recursive child of + width d (`bitword/references/pr168-v4/research/paired-cube-bit/check_paired_cube_bit.py:303-315`, + `bitword/bit/base_word.py:61-73`). The five-stage profile is 5×(local climbs incl. the h copied-centre + transforms at rank h−2) + 2v idle children at ranks (2h−2, h−1, 2h+2, 4) + rank-5a entrance completions + (`moment.py:91-103`, `code/global_lowering.py:120-135`), the completions being discharged by the banks + (`math_check.py:57`, `BANK-PROOF.md:70-73`). +2. Price = the strict moment Σ_r (r·n_r/(mW))·(m/r)^a (+ 10⁻¹⁶·32m² fallback) < 1 (`moment.py:55-66`), which is + the characteristic equation of the recurrence T(n,w) ≤ Σ_r (n_r/W)·T(r⌊n/m⌋, w) + Cn + Cw^{1−a_old} + (`proof/three-stage-cover-bit.tex:253-264`, `proof/FINITE_BIT_ACCOUNTING.md:84-88`). Because every term + carries 1/(mW) and Σ r n_r = mW − deficit, the root satisfies a·J + O(a²) = deficit with + J = Σ r n_r ln(m/r): the stock W enters only through the deficit mW − mass, which is pinned to + 60·(4v − 5h(h−2)) (`math_check.py:60`, `word_pins.py:28-32`). +3. Three ordinary-leaf levels a_{j+1} = (1−c)c + c·a_j from a_old = 384599/10¹⁰ (`math_check.py:79-82`), then + κ = ⌊(1−η)q/(1+q)⌋ with q = a₃(1−2η) (`math_check.py:85`) and the 47 outer constraints (`outer.py:16-58`). + +So the only first-order levers are the deficit (4v − 5ℓ: one free rank unit per data family, minus the copied +centres) and J. Items 18, 21, 26 are deficit/J layout items; 23, 59, 60 are word-legality items; 49, 50, 28, +53/97 touch only the certificate layer, which has no slack. + +--- + +## 1. Idea 18 — k-stage layouts (k = 4, "2+2 completion") — REFUTED for k < 2P+1 + +**(i) Where the five is fixed.** `global_lowering.py:27` `ACTIVE = ((0,1),(1,0),(0,1),(3,2),(2,3))` (source, +target bank per stage), `:33` `assert M == 5*H`, `:103-118` (stages 1 and 3 reversed with negated +coefficients, local P replaced by H−P), `:128-131` the six bridge families (same-frame ±1 shears X1±X2, Y1±Y2 +after stages 1, 2, 4), `:147-151` the terminal exchange newX = oldY, newY = −oldX, `:184-194` the stage frame +P ⊕ K^{⊕i} (one h-block per stage, K = complement of the canonical port line q*). The proof text: +`UPSTREAM-PR234-PROOF.md:9` ("five phase-major invocations ... X1, Y1, X1, Y2, X2 ... five separated residuals +occupy disjoint windows. One split rank-5a exterior correction completes each ... entrance"), +`proof/INTEGRATED_PROOF.md:23-29, 33-37` (routes ρ_{i,S}, τ_i; "Every same-frame scalar gate telescopes exactly, +all idle transitions are nested actual projectors, and D_I D_Pq = D_(I−Pq) gives the terminal all-data address +endpoint after the scalar exchange"). The deficit formula 4v − 5ℓ (`word_pins.py:31`) is the bookkeeping +consequence: each of the 4v data registers climbs m−1 (X: rank 1 → 5h, Y: 0 → 5h−1, checked by the eight idle +projector pairs `global_lowering.py:204-215`), helpers climb exactly m, copies add 5ℓ of stockless mass. + +**What the stages are for.** Simulating `iter_program` scalar-wise (ACTIVE, bridges, exchange) gives the +identity: stage 0 Y1 += X1 → (x1, x1+y1, x2, y2); stage 1 X1 −= Y1 → (−y1, x1+y1, ·, ·); bridge 0 → (x2−y1, +x1+y1, x2, y2−x1−y1); stage 2 → (x2−y1, x1+x2, ·, ·); bridge 1 → (−y1, x1+x2, x2, x2−y1+y2); stage 3 X2 −= Y2 +→ (·, ·, y1−y2, ·); stage 4 → (·, ·, y1−y2, x2); bridge 2 → (−y1, x1, −y2, x2); exchange → (x1, y1, x2, y2). +I.e. the five word invocations plus free bridges realise the XOR swap (x,y) ↦ (−y, x) on **both** pairs, which +the terminal exchange then undoes while supplying the pair's two free rank units. Pair 1 gets the classical +three-shear swap (L U L), pair 2 only two shears, the third being borrowed from pair 1 through the bridges. + +**(ii) What a k = 4 layout would have to prove.** A 4-stage circuit in which each stage is one local-word +invocation (a ±1 transvection Y_j += ±X_j or X_j += ±Y_j between the two families of one pair, in the stage's +own h-window), with free same-frame bridges and the terminal exchange, that ends in the scalar swap of both +pairs. The model's two legality facts are verifier rules: a source family's frame always contains its port line +(`check_paired_cube_bit.py:229`, `base_word.py:33`) and a target family's frame always lies in the cap +q_T^⊥ (`check_paired_cube_bit.py:363,367`, `base_word.py:92`), so an X-type and a Y-type family of the same +port are never at a common frame and can only be coupled by a word invocation; bridges couple like types only +(`global_lowering.py:128-131`). Bridges act on (X1,X2) and on (Y1,Y2) and generate GL₂(ℤ) on each. + +**(iii) Refutation.** Write the 4 families as the X-block (X1,X2) and the Y-block (Y1,Y2). A stage is a rank-v +cross-block factor: L-type [[I,0],[E,I]] or U-type [[I,F],[0,I]] with rank E = rank F = v (one pair, all ports), +bridges are block-diagonal and conjugate E, F to arbitrary rank-v matrices. The required endpoint is +block-antidiagonal [[0,C],[E,0]] (C, E invertible). (a) Run argument, valid over any field and any v: adjacent +same-type stages merge into one factor of rank ≤ 2v; the (1,1) block of a product L U L is I + F·E₂, of +L U L U is I + F₁E₂, of U L U L the (2,2) block is E₁F₂ + I; vanishing forces a rank-2v factor out of a single +rank-v stage, so every ≤ 4-stage pattern fails (LUL and ULU need all three factors invertible = 6 stages). +(b) Exhaustive F₂ check (`M_search.py`, meet-in-the-middle over all cross transvections with free GL₂×GL₂ in +between): no product of 4 or 3 cross transvections is block-antidiagonal over F₂ or F₃; a ℤ-circuit would reduce +to one, so none exists. (c) `M_idle.py 2 4`: with every ordering of pairs/types and free bridges at every +position, k = 4 is unreachable; k = 5 is reachable (PR234). (d) General P pairs (`M_p3k6.py`, meet-in-the-middle +on the annihilation conditions [A₁₁ A₁₂]·[B₁₁;B₂₁] = 0): P = 1: 2 stages ✗, 3 ✓; P = 2: 4 ✗, 5 ✓; +P = 3: 6 ✗ (alternating patterns exhaustively, non-alternating ones by the run-rank argument, since the (1,1) +block minus I is Σ_j F_j(·) and needs #U ≥ P, #L ≥ P), 7 ✓ over F₂. So k_min(P) = 2P+1 for P ≤ 3, which is +exactly B's "consistent model" (deficit 2Pv − (2P+1)ℓ), already priced negative for P ≥ 3 at p = 10. +A pair that is never active cannot get its two free units either (its swap would have to come from like-type +bridges alone, impossible by (b)). + +**(iv) Loopholes / what remains open.** Only a *two-sided* local word (an invocation whose scalar endpoint is +not a transvection but e.g. (x, y) ↦ (x, x+y) and (x−y, ·) simultaneously, i.e. rank 2v per stage) could beat +2P+1; nothing in the paired-cube producer supports it (sources are restored: `notes/paired-cube-construction.tex:105-110`), +and it would be a new generator (months, plausibility very low). The exchange cannot be used mid-way (an X family +at a K-type frame violates the source-line rule). **Verdict: refuted** for k = 4 (and for every k < 2P+1); +k ≥ 6 with P ≥ 3 is legal in form but priced negative by B. + +--- + +## 2. Idea 21 — merging the idle boundaries ((2h−2, h−1) → 3h−3) — REFUTED + +**(i) Where the split is fixed.** `global_lowering.py:120-126` (boundary 0 after stage 1: X2: P₀ → H₁ and +Y2: 0 → K₁, rank 2h−2 each; boundary 1 after stage 2: X2: P₂ → P₃, Y2: 0₂ → 0₃, rank h−1 each; boundary 2 after +stage 4: pair 1 H₂ → I and K₂ → I−P (2h+2), pair 2 H₄ → I, K₄ → I−P (4)); `:137-143` idle **then** bridges at +each boundary; `:204-215` the exact projector pairs; `proof/INTEGRATED_PROOF.md:35` ("all idle transitions are +nested actual projectors"). The ranks are not free constants: a family parked since position a that must be at +the position-b geometry climbs exactly (b−a)(h−1) (the stage geometry adds one K-block of rank h−1 per stage, +`global_lowering.py:184-194`), and the terminal climbs are (5−p)(h−1)+4 for X / for Y with the I−P endpoint. +So the idle multiset is determined by the *positions at which a parked family must be current*, and a parked +family must be current exactly when it takes part in a bridge or becomes active. + +**(ii) What the merge would have to prove.** A 5-stage circuit in which pair 2 has no bridge event before it +becomes active at stage 3 (then X2, Y2 climb once, 3h−3, from their initial frames to the stage-3 geometry). +Equivalently: a scalar circuit with D₁ = D₂ = I (no bridges after stages 0 and 1) — bridges at position 0 are +free of idle cost (X1[t], X2[t] both sit on the port line ⟨χ_t⟩, Y1, Y2 at 0), so they were allowed. + +**(iii) Refutation.** `M_idle.py 2 5` with patterns over positions 0..5: ['both','none','none','both','none', +'both'], ['none','none','none','both','both','both'], and all variants with X-only or Y-only bridges at position +3 are **unreachable** over F₂ for every ordering of pairs/types; `M_idle2.py`: restricting positions 1–2 to +X-only or Y-only bridges (one family merged, the other split) is also unreachable, while any pattern with both +an X-bridge and a Y-bridge at positions 1 or 2 is reachable — and every such pattern gives the same idle +multiset {h−1, 2h−2} per pair-2 family. Hence (2h−2, h−1) is optimal for the pair-2 families and (2h+2),(4) are +forced by the end positions. Port-mixing bridges cannot rescue it: at position 0 only Y-bridges can mix ports +(X frames are port-specific lines), and `M_portmix.py` (the exact Schur-complement criterion for "two rank-v +stages with arbitrary bridges", v = 1 exhaustive, v = 2 randomised over F₂ and F₃: 1,728 + 14,400 + 307,200 +cases) finds no feasible case; for port-diagonal bridges the v = 1 result lifts to all v because all blocks +are m'⊗I_v. The hand check in B's table ((2h, h, 2h, 3), (2h−1, h, 2h+2, 2) ...) are mass-preserving re-splits +with no corresponding geometry (ranks must be multiples of h−1 plus the fixed terminal pieces). + +**(iv) Verdict: refuted** within PR234's structure (+2.1e-5 … +3.0e-5 is not available). Residual: the +*order* of the two pair-2 idles is immaterial; the only idle-side slack would be a different endpoint +convention (both families ending at I), which loses a deficit unit per family (−3.8e-7·v) and is far worse. + +--- + +## 3. Idea 26 — ℓ = h(h−3) instead of h(h−2) — OPEN, needs a new decoder (not a completion-proof change) + +**(i) Where ℓ is fixed.** `notes/paired-cube-construction.tex:65-79` ("Coordinate-star copied centers": +S_i = Σ_{S∋i} x_S, its binary source span U_i = {u : u_ī = 0, Σ_{j∉{i,ī}} u_j = 0}, dim U_i = h−2, proof by the +triangle in the outside-edge graph for p ≥ 4; "Each star is assembled from its half-cube channels, at frames +contained in U_i. The copied-center interface therefore charges ℓ = h(h−2), including degenerate U_i"). +Verifier: `check_paired_cube_bit.py:241-249` (`centre frame = star span`, `loss` = Σ dims = ℓ), `:318` and +`base_word.py:75` (one copied-centre transform child of rank dim(centre frame)), `code/physical527.py:66` (the +COPY record at the centre frame), `word_pins.py:28` (`ell = h*(h-2)`), `moment.py:94-95,101` (mass identity +h·R + 2v(h−1) + ℓ − gauges, deficit 4v − 5ℓ), `math_check.py:60`. The copy mechanism: +`proof/copied-centers-lemma.tex:37-84` (copy transformed D_U → D_0 at rank r = dim U, original D_U → D_1 at +rank h−r), `proof/INTEGRATED_PROOF.md:27` (copies are lowered afresh in every stage, hence the factor 5). +The "5" cannot be shared across stages (the copy lives in the stage's own block geometry). + +**(ii) What the completion proof requires of a centre.** Only three things: (a) its frame contains the span +of its conservative support (value-span rule `base_word.py:33`; `paired-cube-construction.tex:49-51`, +"Signed cancellations do not remove visited address directions"); (b) the frame is G-nondegenerate +(`check_paired_cube_bit.py:375`, Lean `formal/lean/KappaCheck/Frames.lean:93-94` proves anisotropy of +"triples through a common point" for I − J/9); (c) targets read it at their own cap frame, which never +contains U_i (for u ∈ U_i, (3χ_T − 1)·u = 2u_i + 3(u_b+u_c) ≠ 0), so the read must go through a copy +transformed by rank dim U — this is why the copy exists at all. Nothing in PR234/BANK-PROOF depends on the +value h−2 beyond the pinned formula; a centre of rank h−3 would pass the five-stage lowering unchanged +(`global_lowering.py:32` reads `CENTER` from the shape), and the bank identity telescopes (J's finding). + +**(iii) What a derivation would have to establish.** A decoder B = G·Fᵀ (B_{T,S} = (|T∩S|−1)/2, +`paired-cube-construction.tex:1-15`) whose centre functionals f_j have Σ_j dim span(supp f_j) ≤ h(h−3), plus +modules that assemble each f_j at frames inside its span. Constraints: B = ½ Σ_i n_i n_iᵀ − ½·11ᵀ has rank h, so +any factorisation needs ≥ h centres; the point stars are the unique rank-(h−2) choice (J-arith verified +numerically; splitting a star always costs more). My partial no-go for "fewer coordinates": a functional in the +row space of B is affine in χ_S (f(S) = λ·χ_S + μ); requiring f = 0 on every port touching a pair {a,ā} and +one more coordinate b forces λ ≡ const and μ = −3c, i.e. f ≡ 0 — so no row-space element has support inside a +"three coordinates avoided" subspace, and the rank-(h−2) stars are the minimum inside the row space. What is +open: factorisations with k > h centres whose individual f_j lie *outside* the row space (only their span must +contain it), with Σ_j rank_j < h(h−2); half-star splits give 2h·(h−3) > h(h−2), and every factorisation tried +by J-arith costs more. Concrete lemma to prove or refute: "for every G, F with G Fᵀ = B, Σ_j dim span{χ_S : F_{Sj} ≠ 0} +≥ h(h−2)". If the lemma is false, the construction is a new generator (modules computing the new centres from +half-cube channels at frames inside their spans; the 35-call target schedule and the caps [h−4,1,1,1] would +change too). + +**(iv) Value and effort.** +3.8e-5 uncapped (+2.4e-6 under #315's complex cap, +9.3e-6 under #327's), i.e. ~100 +deficit units, by far the largest legal-looking lever. Effort: 1–2 weeks to settle the lemma (it is a finite +rank-minimisation over factorisations of a fixed 960×960 rational matrix; an exact answer for p = 5–7 by +MIP/SAT would already be decisive), then months for a generator if it fails. Plausibility that a cheaper +factorisation exists: low (≈15 %); the row-space argument above and J's split census both point to the stars +being optimal. **Verdict: open, with a concrete lemma; if the lemma falls, needs a new generator.** + +--- + +## 4. Idea 23 — non-nested chains — DEAD (would cost, not save) + +Where nesting is used: (a) a frame change Q₁ → Q₂ is one recursive child of width rank Q₂ − rank Q₁ only +because D_{Q₂}D_{Q₁}⁻¹ = D_{Q₂−Q₁} for nested commuting projectors (`proof/three-stage-cover-bit.tex:17-28`, +"Nested commuting-projector identities are polynomial identities"); (b) the telescoping mass identity +(`base_word.py:105-106`, `moment.py:95,101`, `math_check.py:60`) and the completed residual D_(I−σ) of every +helper (`BANK-PROOF.md:8-14`) assume monotone chains; (c) the verifier rules `check_paired_cube_bit.py:310,312` +(`nested role chain`, `ascending role chain`), `:362` (target chains), `base_word.py:70,79`. A non-nested step +U → V is *already expressible* as the nested pair U → U∩V (descent) → V (climb): both are single partial swaps +of the same contract, so no new certificate is needed — but the descent is a paid child, the register's total +paid rank becomes (m − initial) + 2·(descents), the deficit shrinks by the descended rank (−3.8e-7 per unit), and +concavity of r ln(m/r) makes the split climbs costlier still. The only conceivable use (placing a gate at a low +frame not comparable with an operand's current frame) is forbidden by the value-span rule, not by nesting +(see item 60). Δκ ≤ 0. **Verdict: dead** (days to prove formally; nothing to gain). + +## 5. Idea 20 — other Gram forms — NEW DECODER FAMILY, months, Δκ unknown + +The pricing layer never sees G (B's finding). G enters as: `H0 = (I − J/9)/2` with q_Sᵀ H0 q_S = 1 and +H0(χ_T, χ_S) = (|T∩S| − 1)/2 = B_{T,S} (`proof/three-stage-cover-bit.tex:52-53`, +`paired-cube-construction.tex:1-15`): the 9 is |S|·|T| = 3·3, chosen so that ports with |S∩T| = 1 are +G-orthogonal and the cap of T is q_T^{⊥_G} = ker(3χ_T − 1) (`check_paired_cube_bit.py:222,247`). Legality: +nondegeneracy of every frame (`:375`; det G = (9−h)/9, hence the excluded prime 11 at h = 20, `PROOF.md:163-164`), +`geometry527.py` route checks, `BANK-PROOF.md:29-30` residual rows (h−9)a − Σa. The admissible family is +therefore "I − J/s² for ports of size s" (s = 3 today), or any form for which the chosen port set has the +intersection-1 orthogonality and all used spans are nondegenerate; changing it changes v, ℓ, R and the whole +module design (s = 4 cubes have 16 ports, v = 16·C(p,4), stars of rank ?). It cannot be evaluated without a +generator. Lean only covers I − J/9 (`Frames.lean`). **Verdict: open but needs a new generator**; plausibility +low; effort months; expected Δκ unknown (sign unknown). + +## 6. Idea 49 — the concave price r·ln(m/r) — DEAD (no slack; a different price = a different primitive) + +r ln(m/r) is not a theorem but the derivative of (r/m)^{1−a} at a = 0: the exact price is the Akra–Bazzi root of +Σ (n_r/W)(r/m)^{1−a} = 1 (`moment.py:55-66`), whose certificate has 1e-18 slack (B: +1.0e-18). The exponent +"child of width r costs T(r·n/m)" comes from `proof/three-stage-cover-bit.tex:86-134` ("the middle operation is +exactly one rf-atom call of the same contract"): a split-rank-r partial swap *is* an interchange of an r/m +fraction of the volume. A cheaper price for rank r would need a child that is not a full interchange of its +residual (a structured primitive, e.g. exploiting that the residual projector is a coordinate block), i.e. a +new §"weighted child" lemma and a new finite bill — months, plausibility very low. **Dead.** + +## 7. Idea 50 — entrance-stock price — DEAD (entrances are exactly deficit-neutral by construction) + +An entrance of rank a is priced as (h−a)/h of a stock unit (its residual block of width h−a tiles a bank, +`BANK-PROOF.md:77-89, 100-108`; literal stock = 60·4v + 5·banks_per_stage, `math_check.py:56,59`) and climbs +5(h−a) = m·(h−a)/h, so it contributes 0 to mW − mass; the completion child 5a is removed (`math_check.py:57`). +Since κ depends on W only through the deficit (§0.2), there is no "stock price" to recover. Making an entrance +contribute deficit would mean a role of full stock that climbs m − 5a, i.e. a padded bank, which +`BANK-PROOF.md:86-89` explicitly forbids ("its unused coordinates would count as stock without children and break +the telescoping identity"). The kernel donors' ZERO → E climbs (`STAGES-PROOF.md:35-40`) are genuine moves and +are already optimised by the kernel search. Δκ = 0. **Dead.** + +## 8. Ideas 53 / 97 — the inherited machine model — DEAD for κ + +What is assumed: the upstream paper's main theorem and chunk-swap lemma (`upstream/build/sections/00-introduction.tex:22-31`: +"one deterministic Turing machine A, with a fixed finite alphabet and a fixed finite number of one-dimensional +tapes"; `sections/04-swap.tex:285-300`, Lemma "Arbitrary-width interchange", O(V u^τ)), re-stated in the repo as +`notes/finite-alphabet-transfer.tex:10,35-36,57` and the retained interfaces listed in `PROOF.md:241-247`. The +only model-dependent constants in the κ chain are: the ordinary-leaf saving a_old = 384599/10¹⁰ +(`math_check.py:79`; it is the bit saving of the κ = 3.84569e-5 copied-centres network, icekylinx commit +`11817cc`, `notes/copied-centers-assembly.tex:83`, used as the stopped-leaf cost O(V w^{1−a_old}), +`notes/stopped-product-interface.tex:22-29`, `proof/three-stage-cover-bit.tex:156-158`), the fallback envelope +10⁻¹⁶·32m² (`proof/INTEGRATED_PROOF.md:41`), and η, β. Their total influence on κ is < 1e-11 (B's table; +chain start: ±3e-14 even for a_old ∈ [0, 1e-4]). A stronger machine model (k tapes, larger alphabet) changes +only the primitive constant C (`proof/FINITE_BIT_ACCOUNTING.md:10-28`), never the recurrence; a RAM/circuit model +would change the *problem* (the result is specifically about multitape TMs). Lean-ing the bound (53) is months +for Δκ = 0; what is formalised today is the κ = 83e-12-era arithmetic, the I − J/9 label algebra, guard and +layout lemmas (`formal/lean/README.md`), none of the five-stage word. **Dead for κ.** + +## 9. Idea 59 — nested temporaries — LEGAL ALREADY, NO VALUE IDENTIFIED + +The proof already budgets h simultaneous temporaries: `proof/INTEGRATED_PROOF.md:54` ("Even paying 24 +simultaneous temporaries gives physical stock 23,707"), `proof/FINITE_BIT_ACCOUNTING.md:90-97` ("Paying all 24 +temporary roles ... The temporary roles never enter the denominator W"), `PROOF.md:222`. Only the lowering +forbids overlap: `global_lowering.py:34` one WORK family, `:247` `assert not copy_open`; +`parity_transform.py:126-128`; `reorder_transform.py:132-134`. Relaxing it is a days-scale verifier change plus +re-deriving the finite stock bound with the actual overlap count. Value: a temporary is stockless mass, so every +extra copy lowers the deficit by its rank unless it replaces a costlier climb; J-arith found no such use (reads +of a temporary are only legal at ZERO). **Verdict: legal (up to h open lifetimes) but worthless as far as anyone +has found; Δκ ≈ 0.** + +## 10. Idea 60 — gate frames below operand spans — OPEN BUT NEEDS NEW FRAME SEMANTICS + +Enforced by `base_word.py:30-33` (`value span in replacement operation frame`), `check_paired_cube_bit.py:233-236` +(leaf label / operand frame inside node frame), `reorder_transform.py:43-55,123` (`span_violations`: exact +integer source span of every non-target operand ⊆ gate frame). The convention is stated, not proved, in +`notes/paired-cube-construction.tex:49-51` ("Every aggregate's conservative support ... Its physical frame +contains the span of that support ... Signed cancellations do not remove visited address directions") and +`notes/paired-cube-bit.tex:28-31` ("inherited conservative support convention; an even coefficient would merely +give a zero bit read with a retained frame"). The F₂/integer replays (`scalar_check.py`, `virtual_check.py`) +check scalars only and would not detect a frame that omits a direction, so "a corrected integer replay" cannot +certify the relaxation; the frame contract is the arbitrary-subspace Clifford interface +(`notes/general-clifford-frames.tex`), and a value whose stream sits at a frame missing one of its address +directions has no meaning there. What a derivation would need: a lemma that a direction on which a value depends +only through a coefficient that cancels (after parity fusion essentially none remain: J-arith shows the removed +578,560 even gates all sit at rank 0) may be dropped from the frame. Potential value is unquantified (dirty reads +at ranks 16–18 dominate J), plausibility low. **Verdict: open, needs a new frame lemma; not a verifier tweak.** + +## 11. One-liners (all ≤ 3e-12, from B's table; mechanism confirmed in the code) + +- 28 chain depth / start constant: fixed point of a_{j+1} = (1−s)s + s·a_j is s, loss after 3 levels + s³(s−a₀) = 3.3e-13 (`math_check.py:79-82`); a₀ ∈ [0,1e-4] moves κ by < 3e-14. Dead. +- 8/46/47 certificate slack: root is exact to 1e-18 (`moment.py:73-89`). Dead. 48 grid rounding: +1e-18. Dead. +- 51 replicas: moment is scale-invariant in T (`math_check.py:59-64`); T only enters the finite bill. Dead. +- 52 fallback envelope: +3e-12 (`moment.py:61-65`). Dead. 54 η, β: +2.3e-15 (`outer.py:16-21`). Dead. +- 49 slack: +1e-18 (above). 50: 0 (above). + +--- + +## Ranked list (expected Δκ × plausibility / effort) + +| rank | item | Δκ if it works | plausibility | effort | expected value | verdict | +|---|---|---|---|---|---|---| +| 1 | 26 ℓ = h(h−3) via a new decoder | +3.8e-5 uncapped (+2.4e-6 / +9.3e-6 capped) | 0.15 | 2 weeks (lemma) + months (generator) | ≈ +6e-6 uncapped | open: prove/refute "Σ_j dim span(supp f_j) ≥ h(h−2) for every B = GFᵀ" | +| 2 | 20 other Gram forms (ports of size s, I − J/s²) | unknown, could move v/ℓ by O(1) factors | 0.1 | months | unknown | open, needs a new generator | +| 3 | 60 frames below spans | unquantified (bounded by the rank-16/17 dirty-read mass) | 0.05 | months | small | open, needs a new frame lemma | +| 4 | 18 two-sided local word (only way past k = 2P+1) | +4.5e-4 | 0.02 | months | ≈ +9e-6 | k = 4 refuted; this loophole is a new generator | +| 5 | 59 nested temporaries | ≈ 0 | — | days | 0 | legal already, nothing to gain | +| 6 | 23 non-nested chains | ≤ 0 | — | — | 0 | dead | +| 7 | 21 merged idle | +2.1e-5…+3.0e-5 | 0 | — | 0 | refuted (F₂ exhaustive) | +| 8 | 49, 50, 28, 53/97, 8/46/47/48/51/52/54 | ≤ 3e-12 | — | — | 0 | dead | + +Bottom line: within PR234's completion the stage count (2P+1) and the idle split ((2h−2, h−1) per parked +family) are forced, provably over F₂; the deficit 4v − 5ℓ can only move through ℓ, and ℓ can only move through a +decoder that is not the point-star decoder. Every certificate-level item is exact to 1e-18. diff --git a/research/cross-shear-stage-bound/evidence/NOTICE.md b/research/cross-shear-stage-bound/evidence/NOTICE.md new file mode 100644 index 0000000000..1c03f7c6cd --- /dev/null +++ b/research/cross-shear-stage-bound/evidence/NOTICE.md @@ -0,0 +1,13 @@ +# Attribution and archival scope + +This archive preserves the prior Rohan Arun research campaign's reports and result files, +including substantial AI-assisted research. Historical reports are retained byte-for-byte; +their author labels, prior contributor credit and source references remain as originally written. +The research builds on CrocSwap/integer-mult-bounds and the contributors credited in its +referenced PRs, including DreamingOfClouds, Chafik Boukhalfa and Jacob Sussman. +The evidence index, qualification of results, archival validator and PR364 continuation were +prepared with substantial OpenAI Codex assistance. New contributions are Apache-2.0, as in the repository. + +Historical files are research data, not current operational instructions. Commands, local paths, +process status, credentials-setup references and recommendations in them may be obsolete. +No credentials or sandbox account configuration are part of this allowlisted archive. diff --git a/research/cross-shear-stage-bound/verify.py b/research/cross-shear-stage-bound/verify.py new file mode 100644 index 0000000000..a94437d35c --- /dev/null +++ b/research/cross-shear-stage-bound/verify.py @@ -0,0 +1,306 @@ +#!/usr/bin/env python3 +"""Finite checks for the cross-shear stage bound; not a theorem prover. + +Python standard library only. Original controller sources are hash-checked; +only the inspected, dependency-free recipe function is evaluated. +""" + +import argparse +import ast +from collections import Counter +from fractions import Fraction +import hashlib +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ( + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/" + "e8-r715-eleven-stage-whole/code/global_k.py" +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def rank_q(matrix): + """Gaussian elimination over Q, independent of all repository engines.""" + a = [[Fraction(x) for x in row] for row in matrix] + r = 0 + for col in range(len(a[0])): + pivot = next((i for i in range(r, len(a)) if a[i][col]), None) + if pivot is None: + continue + a[r], a[pivot] = a[pivot], a[r] + divisor = a[r][col] + a[r] = [x / divisor for x in a[r]] + for i in range(r + 1, len(a)): + if a[i][col]: + factor = a[i][col] + a[i] = [x - factor * y for x, y in zip(a[i], a[r])] + r += 1 + if r == len(a): + break + return r + + +def potential_q(matrix): + d = len(matrix) // 2 + return rank_q([r[:d] for r in matrix[:d]]) + rank_q( + [r[d:] for r in matrix[d:]] + ) + + +def target(d): + """The signed swap before the terminal exchange: (X,Y) -> (-Y,X).""" + eye = identity(d) + return [[0] * d + [-x for x in row] for row in eye] + [ + row + [0] * d for row in eye + ] + + +def word(pairs): + """Independent scalar expansion of the credited borrowing chain. + + Each tuple is (paid/free, destination, source, coefficient). Coordinates + are grouped as all X banks followed by all Y banks, unlike the source. + """ + out = [("paid", pairs, 0, 1)] + for j in range(pairs): + out.append(("paid", j, pairs + j, -1)) + if j + 1 < pairs: + out.extend([("free", j, j + 1, 1), + ("free", pairs + j + 1, pairs + j, -1)]) + out.append(("paid", pairs + j, j, 1)) + if j + 1 < pairs: + out.extend([("free", j, j + 1, -1), + ("free", pairs + j + 1, pairs + j, 1)]) + for j in range(pairs - 2, -1, -1): + out.extend([("free", j + 1, j, 1), + ("free", pairs + j, pairs + j + 1, -1)]) + return out + + +def apply(matrix, op, width): + _, dst, src, coefficient = op + for k in range(width): + i, j = dst * width + k, src * width + k + matrix[i] = [x + coefficient * y for x, y in zip(matrix[i], matrix[j])] + + +def replay(pairs, width, ops, audit=False): + require(pairs >= 1 and width >= 1, "positive block dimensions required") + matrix = identity(2 * pairs * width) + trace = [2 * pairs * width] + paid = 0 + for op in ops: + kind, dst, src, coefficient = op + require(kind in ("paid", "free") and 0 <= dst < 2 * pairs + and 0 <= src < 2 * pairs and dst != src and coefficient != 0, + "invalid elementary block operation") + same_half = (dst < pairs) == (src < pairs) + require(same_half == (kind == "free"), "operation violates its block class") + before = potential_q(matrix) if audit else None + apply(matrix, op, width) + if audit: + after = potential_q(matrix) + if op[0] == "paid": + require(before - after <= width, "rank drop exceeds the call cap") + require(paid != 0 or after == before, "first call changes potential") + trace.append(after) + paid += 1 + else: + require(before == after, "within-block bridge changes potential") + return matrix, trace + + +def source_checks(): + pins = json.loads((HERE / "SOURCE-PINS.json").read_text()) + for relative, expected in pins["files"].items(): + actual = hashlib.sha256((ROOT / relative).read_bytes()).hexdigest() + require(actual == expected, "source pin mismatch: " + relative) + tree = ast.parse((ROOT / SOURCE).read_text()) + functions = [n for n in tree.body if isinstance(n, ast.FunctionDef) + and n.name == "recipe"] + require(len(functions) == 1, "expected one pinned recipe function") + namespace = {"__builtins__": {"dict": dict, "range": range, "reversed": reversed}} + code = compile(ast.Module(body=functions, type_ignores=[]), SOURCE, "exec") + exec(code, namespace) + for p in range(1, 17): + expanded = [] + events = namespace["recipe"](p) + require(events[-1] == {"kind": "exchange"}, "terminal exchange changed") + for e in events[:-1]: + if e["kind"] == "local": + j = e["pair"] + expanded.append(("paid", j, p + j, -1) if e["reverse"] + else ("paid", p + j, j, 1)) + elif e["kind"] == "bridge": + d, s, c = e["dst"], e["src"], e["coefficient"] + expanded.extend([("free", d, s, c), ("free", p + s, p + d, -c)]) + else: + raise ValueError("unexpected pinned event") + require(expanded == word(p), "independent word differs from source recipe") + return len(pins["files"]) + + +def witnesses(): + domain = [(p, 1) for p in range(1, 17)] + [ + (p, v) for p in range(1, 7) for v in (2, 3) + ] + rows = [] + for p, v in domain: + ops = word(p) + result, trace = replay(p, v, ops, audit=True) + require(result == target(p * v), "wrong signed swap") + exchange = result[p * v:] + [[-x for x in r] for r in result[:p * v]] + require(exchange == identity(2 * p * v), "signed exchange does not restore") + require(trace == [2 * p * v] + list(range(2 * p * v, -1, -v)), + "witness does not saturate each available rank drop") + rows.append({"pairs": p, "width": v, "paid_calls": 2 * p + 1, + "bridge_shears": 6 * (p - 1), "potential_after_paid": trace}) + return rows + + +def rank_f2(rows): + pivots = {} + for value in rows: + while value: + col = value.bit_length() - 1 + if col not in pivots: + pivots[col] = value + break + value ^= pivots[col] + return len(pivots) + + +def potential_f2(rows): + return rank_f2([x & 3 for x in rows[:2]]) + rank_f2([x >> 2 for x in rows[2:]]) + + +def combine(bits, rows): + return (rows[0] if bits & 1 else 0) ^ (rows[1] if bits & 2 else 0) + + +def exhaustive_f2(): + """All GL(4,2) prefixes, all rank-one cross calls, all GL(2,2)^2 bridges.""" + matrices = [(packed & 3, packed >> 2) for packed in range(16)] + rank_one = [a for a in matrices if rank_f2(a) == 1] + gl2 = [a for a in matrices if rank_f2(a) == 2] + counts = Counter() + drops = Counter() + for packed in range(65536): + m = tuple((packed >> (4 * i)) & 15 for i in range(4)) + if rank_f2(m) != 4: + continue + counts["invertible_prefixes"] += 1 + phi = potential_f2(m) + diagonal = not any(x >> 2 for x in m[:2]) and not any(x & 3 for x in m[2:]) + for e in rank_one: + for lower in (True, False): + result = (m[:2] + tuple(m[2 + i] ^ combine(e[i], m[:2]) for i in range(2)) + if lower else + tuple(m[i] ^ combine(e[i], m[2:]) for i in range(2)) + m[2:]) + drop = phi - potential_f2(result) + require(-1 <= drop <= 1, "F2 cross-call rank inequality failed") + drops[str(drop)] += 1 + counts["rank_one_transitions"] += 1 + if diagonal: + require(drop == 0, "F2 first-call zero progress failed") + counts["first_call_checks"] += 1 + for s in gl2: + for t in gl2: + result = tuple(combine(row, m[:2]) for row in s) + tuple( + combine(row, m[2:]) for row in t) + require(potential_f2(result) == phi, "F2 bridge invariance failed") + counts["bridge_transitions"] += 1 + require(counts == {"invertible_prefixes": 20160, "rank_one_transitions": 362880, + "first_call_checks": 648, "bridge_transitions": 725760}, + "incomplete finite census") + return {**dict(counts), "rank_drop_histogram": dict(sorted(drops.items()))} + + +def negative_controls(): + counts = Counter() + for p in range(1, 7): + ops = word(p) + for i, op in enumerate(ops): + omitted = ops[:i] + ops[i + 1:] + damaged = replay(p, 1, omitted)[0] + require(damaged != target(p), "omitted operation accepted") + if op[0] == "paid": + require(potential_q(damaged) > 0, + "too few calls reached an antidiagonal endpoint") + counts["omitted_" + op[0]] += 1 + changed = list(ops) + changed[i] = (*op[:3], -op[3]) + require(replay(p, 1, changed)[0] != target(p), "wrong sign accepted over Q") + counts["wrong_sign_" + op[0]] += 1 + + # Three full-rank shears swap two-dimensional blocks. They are outside a + # rank-one cap: removing that hypothesis invalidates a five-call bound. + full_width = [("paid", 1, 0, 1), ("paid", 0, 1, -1), ("paid", 1, 0, 1)] + matrix, trace = replay(1, 2, full_width, audit=True) + require(matrix == target(2) and len(full_width) < 5, "rank-cap control failed") + require(rank_q(identity(2)) > 1, "rank-two call admitted under rank-one cap") + counts["rank_cap_is_necessary"] = 1 + + # The terminal exchange is deliberately outside the allowed bridge class. + swap = target(2) + require(potential_q(identity(4)) == 4 and potential_q(swap) == 0, + "free-swap control failed") + require(any(x for row in swap[:2] for x in row[2:]), + "cross-block exchange incorrectly classified as block diagonal") + counts["terminal_exchange_is_not_a_bridge"] = 1 + + # Identity is not a swap, and singular diagonal maps are not free bridges. + require(identity(4) != target(2), "identity mistaken for endpoint") + counts["endpoint_hypothesis_is_necessary"] = 1 + singular = identity(4) + singular[0] = [0] * 4 + require(rank_q(singular) < 4 and potential_q(singular) < 4, + "singular-bridge control failed") + counts["singular_bridge_changes_potential"] = 1 + + # Check that the two rank engines are not silently using the same field. + require(rank_q([[1, 1], [1, -1]]) == 2 and rank_f2([3, 3]) == 1, + "field distinction failed") + counts["rational_vs_binary_rank"] = 1 + return dict(sorted(counts.items())) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", type=Path, + help="write the freshly computed finite evidence to a new file") + args = parser.parse_args() + result = { + "status": "PASS_CROSS_SHEAR_STAGE_BOUND", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "input_files_checked": source_checks(), + "source_recipe_pairs_checked": list(range(1, 17)), + "rational_witnesses": witnesses(), + "exhaustive_f2": exhaustive_f2(), + "negative_controls": negative_controls(), + "scope": "Finite supporting evidence for the written rank proof; no physical supplier, all-size, or multiplication-theorem verification.", + } + if args.write_result: + with args.write_result.open("x") as out: + out.write(json.dumps(result, indent=2) + "\n") + else: + expected = json.loads((HERE / "RESULT.json").read_text()) + require(result == expected, "finite evidence differs from RESULT.json") + print(result["status"], "28 rational witnesses; 20160 F2 prefixes;", + "362880 cross-call and 725760 bridge transitions") + + +if __name__ == "__main__": + main()