Prove sharp Fibonacci growth inside restoring unit-shear words (no κ)

research/restored-unit-shear-growth/PROOF.md

@@ -0,0 +1,129 @@
+# Sharp intermediate growth under exact restoration
+
+This proof and its application were produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Let n>=2 and L>=0 be integers. A gate on n rows is exactly
+
+```
+x_i <- x_i + epsilon x_j,       i != j, epsilon in {-1,1}.
+```
+
+All other rows stay fixed. A word has length ell<=L, and its complete
+integer matrix is I_n. This is full restoration for every original input,
+including every dirty workspace row. There is no scaling, self-addition,
+native operator, rounding, source insertion or free operation.
+
+Set F_0=0, F_1=1 and F_(a+2)=F_(a+1)+F_a. Let P_k be the prefix matrix
+after k gates, with P_0=I. Write |P|_max for its largest absolute entry,
+and ||P||_infinity for its largest absolute row sum.
+
+**Theorem.** With d=min(k,ell-k), every cut satisfies
+
+```
+|P_k|_max       <= F_(d+1),
+||P_k||_infinity <= F_(d+2).
+```
+
+Consequently, over all allowed words and all their cuts, the exact maxima are
+
+```
+max |P_k|_max        = F_(floor(L/2)+1),
+max ||P_k||_infinity = F_(floor(L/2)+2).
+```
+
+Both maxima are attained by one word on two rows. Any additional rows stay
+fixed, so allowing arbitrarily many dirty rows cannot increase the maxima.
+These are maxima under an **at most L** budget. We do not assert an
+identity word of every exact length, or sharpness at every specified cut.
+
+## One-way growth lemma
+
+First ignore the endpoint. For each row of a prefix matrix take its
+absolute row sum, and sort these n nonnegative numbers. Let a>=b be
+the two largest. Updating one row changes its norm to at most the sum
+of the norms of two distinct old rows, hence at most a+b. The new
+second largest norm is at most a, since only one row changes. Thus the
+ordered pair of largest norms is componentwise bounded by
+
+```
+(a,b) -> (a+b,a).
+```
+
+Initially it is (1,1). Induction bounds it after t gates by
+(F_(t+2),F_(t+1)), so ||P||_infinity<=F_(t+2). Decreases and sign
+cancellations do not invalidate this upper bound.
+
+Apply the same argument to the absolute values in one fixed column.
+Initially the two largest are (1,0). They are bounded after t gates by
+(F_(t+1),F_t). Each column therefore has largest entry at most F_(t+1),
+which proves |P|_max<=F_(t+1). This argument applies separately to each
+column and does not assume independent signs across columns.
+
+## Use both sides of the cut
+
+Write S_k for the matrix of the remaining ell-k gates, so S_k P_k=I.
+Then P_k=S_k^-1. A gate's inverse is another allowed gate, with its
+sign negated. Reversing the remaining gates and negating their signs
+therefore writes the **same P_k** as a word of length ell-k.
+
+The one-way lemma gives both bounds with t=k and with t=ell-k.
+The Fibonacci numbers are nondecreasing, so taking the smaller gives
+the two stated cut bounds. Since min(k,ell-k)<=floor(L/2), the global
+bounds follow. No norm estimate on the final identity is substituted
+for the inverse-word argument.
+
+## Attainment and the magnitude guard
+
+Put s=floor(L/2). Starting with two rows, alternate positive additions
+
+```
+x_0 += x_1, x_1 += x_0, x_0 += x_1, ...
+```
+
+for s gates. Execute their inverse gates in reverse order. The resulting
+word has length 2s<=L and endpoint I. At its midpoint, its two row sums
+are F_(s+2),F_(s+1), in one order. For s>=1 its largest entry is
+F_(s+1), as follows by the same alternating recurrence in the two columns.
+For s=0 the midpoint is I, with both maxima equal to one. This proves
+attainment, simultaneously for both bounds.
+
+If every original real or integer input satisfies |x_i|<=H, the triangle
+inequality gives the uniform intermediate magnitude cap
+
+```
+|x_i(k)| <= H F_(floor(L/2)+2).
+```
+
+For H>=0, set both active initial rows equal to H in the attaining word.
+The larger midpoint row attains this cap exactly. Arbitrary spectator
+inputs remain unchanged. Hence the cap is the least possible universal
+cap from L and H alone for n>=2. If H is a nonnegative integer and
+M=H F_(floor(L/2)+2), the smallest two's-complement width sufficient for
+every state is 1+bit_length(M), with bit_length(0)=0. The positive
+attainer also proves necessity of this symmetric-range width.
+
+This guard applies to exact row states. It does not bound the error of
+rounded shears, local arithmetic temporaries with a different evaluation
+order, coefficient preparation, tape movement, or native Gaussian gates.
+
+## Verification boundary and relevance
+
+The all-dimension and all-length assertions rest on the proof above.
+The finite matrix census evaluates every signed unit ADD word through
+length eight on two rows and length five on three rows. It tests each
+identity word's individual cuts and reports their exact counts. The
+separate oracle evaluates integer cube corners, without matrix operations
+or imports from the model. Checking all corners determines identity and
+the induced infinity norm over this characteristic-zero model, since
+the corners span and each row's absolute sum is attained at a corner.
+All words in the two declared oracle domains are enumerated too.
+
+The proof isolates an exact restoration-aware precision input. A complete
+selected caller contains operations outside this alphabet, so there is no
+automatic replacement of its existing precision guard or scalar allowance.
+No source word, predecessor theorem, native map or historical count is
+replayed as the contribution. Independent human and formal proof-kernel
+review, physical implementation and all five framework assumptions remain
+unclaimed. No new kappa follows.

research/restored-unit-shear-growth/README.md

@@ -0,0 +1,106 @@
+# Sharp growth inside a restoring unit-shear word
+
+This contribution was produced by Nick Petalas. Claim type: scoped written
+proof with exact finite corroboration. Apache-2.0. No new kappa is claimed.
+
+For any finite number n>=2 of arbitrary dirty rows, take a word of at most
+L gates `x_i += epsilon*x_j`, with i!=j and epsilon in {-1,1}, whose complete
+endpoint is the identity. The exact largest possible intermediate values are
+
+```
+largest absolute matrix coefficient = F_(floor(L/2)+1)
+largest absolute row sum            = F_(floor(L/2)+2)
+```
+
+Here F_0=0 and F_1=1. Two rows attain both bounds: alternate positive ADDs
+for floor(L/2) steps, then execute the literal inverse. Extra dirty rows
+cannot improve the maxima. At cut k of a length-ell loop, replace floor(L/2)
+by min(k,ell-k) in the upper bounds.
+
+For initial magnitudes at most H, the sharp universal intermediate cap is
+`H*F_(floor(L/2)+2)`. The [proof](PROOF.md) also gives its exact signed-width
+guard. The new step uses the restoring suffix to bound the same prefix from
+the opposite end. Standard top-two Fibonacci majorization supplies the
+one-way estimate. No global literature-priority claim is made.
+
+The changed card scope is explicit in [TASK.json](TASK.json). This is a
+scalar precision side result, without selected-caller binding. It does not
+audit a predecessor, admit a supplier or change the selected frontier.
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/restored-unit-shear-growth
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/restored-unit-shear-growth/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/restored-unit-shear-growth/oracle.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/restored-unit-shear-growth --check-source-history
+```
+
+Any CPython 3.12 installation can replace the local interpreter path. The
+registered normal and optimized runs print PASS_RESTORED_UNIT_SHEAR_GROWTH.
+Direct oracle replay prints PASS_RESTORED_SHEAR_LITERAL_CUBE.
+
+The matrix census enumerates all 87,381 two-row words through length eight
+and all 271,453 three-row words through length five. It finds 2,689 and 577
+identity words, respectively, and checks each cut. The independent oracle
+uses literal integer cube corners, with no matrix-model import. It enumerates
+5,461 two-row words through length six and 22,621 three-row words through
+length four; every common identity count and maximum row norm agrees.
+Empty exact-length classes have null maxima in the generated receipt.
+
+The replay checks 387 attaining loops at even budgets through 256, 128 odd
+budget attainers, 231 literal magnitude/width guards and 12 controls. The
+controls include invalid coefficients and indices, self-addition, inadequate
+gate budgets, incomplete restoration and an undersized Fibonacci bound.
+Explicit exceptions keep every check active under optimization. The receipt
+binds every package file by SHA256 and is printed without writing files.
+
+## Limits
+
+The theorem uses an at-most gate budget and exact full identity restoration.
+It excludes scales, coefficients beyond signed units, source insertions,
+native operators and rounding. In particular, this is not an error bound
+for rounded identity cycles or a bound on every arithmetic temporary. Real
+selected callers contain excluded operations. Their source/frame/ownership,
+physical tape, precision, compiler and analytic obligations remain separate.
+No predecessor suite, selected cold replay, Lean or Docker build ran.
+Independent human and formal proof-kernel review are unclaimed.
+
+The reference model accepts at most eight rows and 256 gates. The proof has
+no such dimension or length restriction. Every loop has a finite bound from
+these limits or the fixed census domains. No recursion, network, subprocess
+or dynamic evaluation is used. Functions stay below 60 physical lines.
+Python allocation during integer arithmetic is a Power-of-Ten rule 3
+deviation, bounded by the fixed domains and word lengths. The census streams
+words and retains only one trace and per-length summaries. Warning-strict
+normal and optimized replay supplies the available interpreted diagnostics;
+no installed static type checker or linter was available. Explicit sibling
+imports identify the two scientific modules; no predecessor is imported.
+
+## Open next questions
+
+1. Determine a sharp bound for one specified nonidentity endpoint. Begin
+   with forward growth and inverse-suffix multiplication by the endpoint.
+   This could cover useful scalar intervals, but no sharp classification
+   or selected interval is bound here.
+2. Derive an error bound for a stated rounded implementation using the
+   exact inverse-prefix envelope. Specify every rounding point and increment
+   model first. Exact restoration alone does not prove rounded restoration
+   or dirt-independent increments.
+
+## Sources and credit
+
+Base: canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority
+revision 8, selected PR6030. The selected record and catalogue are historical
+provenance in [SOURCES.json](SOURCES.json), with no external scientific input.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361711)
+records the original question. Live handoffs and reservations, open/account
+PRs, main README and formula searches, merged PR searches and cached card
+coverage were checked. Arbitrary historical diffs and unpublished work remain
+outside that coverage.
+
+Elementary row operations, induced matrix norms and Fibonacci majorization
+are classical. The new scoped contribution is the sharp restoration-aware
+application and its rerunnable verification, produced by Nick Petalas.

research/restored-unit-shear-growth/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}

research/restored-unit-shear-growth/TASK.json

@@ -0,0 +1,107 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Sharp coefficient and induced infinity-norm growth inside exact identity words of at most L signed unit row ADDs, in every finite dimension, with matching dirty-input magnitude and signed-width guards.",
+  "scope_change_reason": "The formal-interface card is changed to an original written scalar precision lemma. This package does not formalize a selected-caller implication or claim proof-kernel acceptance.",
+  "bottleneck_link": "Side result for precision_tape: exact restoration constrains the intermediate growth envelope through both sides of each cut. Actual selected callers also contain operations outside this alphabet and require a separate binding.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first sharp restoration-aware envelope after the proof, exact bounded checks and controls pass; do not extend to rounded words or selected integration.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; complete matrix and independent literal-cube censuses; attaining loops and guard checks; generated file-hash-bound receipts.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What sharp intermediate bound survives a specified nonidentity endpoint?",
+      "why_it_matters": "Selected scalar intervals need not restore the entire data state to identity.",
+      "first_step": "Specify a fixed endpoint T and compare the forward word with the inverse suffix followed by T; determine when the resulting product bound is attained.",
+      "blocked_by": "No sharp endpoint-dependent classification or selected-word binding is supplied."
+    },
+    {
+      "question": "What rounded-error bound can exploit the exact restoration-aware envelope?",
+      "why_it_matters": "Exact magnitude control alone does not certify rounded cleanup.",
+      "first_step": "Fix rounding points and an allowed increment-error model, then bound the actual inverse-prefix propagation of each error.",
+      "blocked_by": "The exact identity argument does not assert a rounded identity endpoint or dirt-independent increments."
+    }
+  ],
+  "claim_type": "scoped mathematical proof with exact finite corroboration",
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361711",
+    "source": "original",
+    "coverage": "Live open/account PRs, handoffs, local reservations, merged/object/formula searches and a cached formal-interface card search; arbitrary historical diffs and unpublished work excluded."
+  }
+}

research/restored-unit-shear-growth/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Exhaustive exact matrix and independent scalar-cube censuses, sharp loops, signed guards and invalid-contract controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "The same complete scientific checks with assertions disabled."
+    }
+  ]
+}