Prove the sharp common reserve for PR6472's row menu (no κ)

research/sharp-adaptive-reserve/ORIGIN.json

@@ -0,0 +1,10 @@
+{
+  "source_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/6472",
+  "author": "Ali Romman / aliromman",
+  "repository": "aliromman/integer-mult-bounds",
+  "commit": "6621e59b773b179a0340627eadbe295eb5254d07",
+  "path": "research/adaptive-row-bill/example.json",
+  "retained_path": "inputs/example6472.json",
+  "sha256": "8819bb327b318bed314cc6cd12781e4ad148a18a4cf77fa749167bc7b1c3c3b4",
+  "usage": "The four allowed rows only. No predecessor executable or scientific replay is imported."
+}

research/sharp-adaptive-reserve/PROOF.md

@@ -0,0 +1,125 @@
+# Sharp common reserve for the PR6472 example
+
+This is a scoped mathematical proof, produced by Nick Petalas.
+It answers the common-ratio optimization question posed by Ali Romman in
+[PR6472](https://github.com/CrocSwap/integer-mult-bounds/pull/6472), exact head
+`6621e59b773b179a0340627eadbe295eb5254d07`. That package supplies the menu,
+the adaptive row contract, the exact total `u=(5,3)` and its reserve ratio `4/5`.
+Those are credited inputs, not new results of this package.
+
+## Contract and claim
+
+The two type menus are
+
+```text
+R_1 = {(0,6/5), (1/5,1)}
+R_2 = {(2/5,0), (0,1/4)}.
+T(x)_i = max_{r in R_i} r x.
+```
+
+For a positive real weight `w=(x,y)`, let `q(w)` be the smallest number such
+that `r w <= q(w) w_i` for every row of type `i`. All four rows are retained.
+The new exact optimum is
+
+```text
+min_{w>0} q(w) = lambda = (1+sqrt(41))/10.
+```
+
+Its minimizing weights have the unique ratio
+`x/y=(1+sqrt(41))/4`. Consequently no positive rational weight attains the
+minimum. A rational certificate `w=(37,20)` gives `q=137/185 < 4/5`.
+
+For the finite-depth adaptive unit-toll totals
+`x_0=0`, `x_{d+1}=1+T(x_d)`, this certificate gives
+
+```text
+0 <= u-x_d <= (137/185)^d (111/20,3),
+max_i (u_i-x_{d,i})/u_i <= (111/100)(137/185)^d.
+```
+
+These are componentwise inequalities. They imply the relative tolerance
+`2^-64` at depth 149. The cited `4/5` reserve bound first implies that
+tolerance at depth 199. These are exact cutoffs for the two bounds, not a
+claim that the actual nonlinear recurrence first meets tolerance at 149.
+
+## Lower bound for every positive real weight
+
+Put `t=x/y>0`. Directly from the four rows,
+
+```text
+q(w) = max(6/(5t), 1/5+1/t, 2t/5, 1/4).
+```
+
+In particular `q>1/5`, `1/t <= q-1/5` and `t <= 5q/2`.
+Multiplying the last two positive inequalities gives
+`1 <= (q-1/5)(5q/2)`, hence
+
+```text
+5q^2-q-2 >= 0.
+```
+
+The polynomial has exactly one positive root, `lambda`, so `q>=lambda`.
+This argument quantifies over every positive real weight; the finite
+rational-weight checks do not supply this quantifier.
+
+## Attainment and uniqueness
+
+Choose `t=(1+sqrt(41))/4=5 lambda/2`. The equation
+`5 lambda^2-lambda-2=0` gives
+`1/5+1/t=lambda=2t/5`. Also `t>1`, so
+`6/(5t) <= 1/5+1/t`; and `1/4<lambda`. Thus all four rows satisfy the
+bound with equality on the two coupled rows.
+
+If `q=lambda`, equality must hold in both inequalities that were multiplied
+above. This forces `t=5 lambda/2`. Since 41 is not a square, `t` is irrational.
+Positive rational weights therefore cannot attain the optimum. Density and
+continuity show that the infimum restricted to rational weights is still
+`lambda`.
+
+## Rational certificate and all-depth tail
+
+For `w=(37,20)`, the four row ratios are exactly
+
+```text
+24/37, 137/185, 37/50, 1/4.
+```
+
+Their maximum is `137/185`. Scaling to `v=(111/20,3)` preserves the ratio,
+and `v>=u`. For arbitrary vectors `a,b`, the elementary maximum inequality
+and nonnegative rows give
+
+```text
+|T(a)_i-T(b)_i| <= max_{r in R_i} r |a-b|.
+```
+
+The cited total satisfies `u=1+T(u)`. Starting with `0<=u-x_0=u<=v`, the
+displayed inequality proves inductively
+`0<=u-x_d<=q^d v` for every integer `d>=0`. Division by `u` gives the
+relative bound, since `max_i v_i/u_i=111/100`.
+
+The new componentwise bound is smaller than the cited bound for every `d>=2`.
+It suffices to check
+`(111/100)(137/148)^2<1`; larger `d` only decrease this expression.
+The exact 64-bit cutoff assertions reduce to four rational comparisons:
+
+```text
+(111/100)(137/185)^149 <= 2^-64 < (111/100)(137/185)^148,
+(4/5)^199 <= 2^-64 < (4/5)^198.
+```
+
+The verifier performs these comparisons with integer-backed fractions.
+
+## Credit and scope
+
+Weighted maximum norms, nonnegative matrix theory, and positive-vector
+contraction arguments are classical. The selected two coupled rows also
+give the classical Perron-root interpretation. No general theorem priority
+is claimed. The new contribution is the sharp source-specific reserve
+optimization, its rational certificate and the resulting cutoff comparison.
+PR6472 retains credit for the row menu, total-bill interface and its proofs.
+
+This synthetic example does not identify a physical supplier menu. Every
+actual caller would still need complete child, adapter and restoration
+charges, legal independent row choices, native realization, compiler,
+storage, precision/tape and outer applicability. All five selected framework
+assumptions remain. There is no new kappa or selected-frontier change.

research/sharp-adaptive-reserve/README.md

@@ -0,0 +1,54 @@
+# Sharp reserve for an adaptive two-type bill
+
+Scoped proof with exact finite corroboration, produced by Nick Petalas.
+
+For the exact synthetic row menu of Ali Romman's [PR6472](https://github.com/CrocSwap/integer-mult-bounds/pull/6472), the optimal common positive-weight contraction ratio is
+
+```text
+lambda = (1+sqrt(41))/10.
+```
+
+The minimizing weight ratio is uniquely `(1+sqrt(41))/4`, so no positive rational weights attain it. The explicit rational weights `(37,20)` certify ratio `137/185`. Every allowed source row is retained. This answers the source's open common-ratio optimization question; it does not audit or replay the existing total-bill result.
+
+Using the cited exact total `u=(5,3)`, the new all-depth tail bound is
+
+```text
+0 <= u-x_d <= (137/185)^d (111/20,3).
+```
+
+It certifies relative error at most `2^-64` at depth 149. The source's `4/5` bound first certifies it at depth 199. These are cutoffs of the two certified bounds; neither is asserted to be the actual first successful depth of the recurrence. The [proof](PROOF.md) establishes the optimum over every positive real weight and the tail inequality for every depth.
+
+## Reproduce
+
+From the repository root, use CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/sharp-adaptive-reserve/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/sharp-adaptive-reserve/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sharp-adaptive-reserve
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sharp-adaptive-reserve --check-source-history
+```
+
+Another CPython 3.12 interpreter can replace that path. Expected markers are `PASS_SHARP_ADAPTIVE_RESERVE`, `PASS_REGISTERED_RESEARCH_PACKAGE`, and `PASS_RESEARCH_COMMIT_BYTES`. The direct verifier prints a generated receipt bound to all nine package files. An optional `--receipt /absolute/scratch/path.json` writes it outside the package. No receipt is hand-written or required as an input.
+
+The verifier compares literal source-row products with the reduced ratio formula for all 4,096 integer weight pairs in `1..64` squared. It checks 257 exact nonlinear finite-depth prefixes against a separate two-by-two matrix recurrence, the tail inequalities and minimality of both stated cutoffs. False reserve, invalid precision and source-corruption controls must reject. These finite checks corroborate the written proof; they do not establish its universal quantifiers.
+
+## Sources and scope
+
+[ORIGIN.json](ORIGIN.json) identifies the exact PR6472 commit and source file. Its four-row example is retained byte for byte in [inputs/example6472.json](inputs/example6472.json), authenticated before parsing. The package imports no predecessor executable and does not require the pending source commit in local Git history. [SOURCES.json](SOURCES.json) binds the canonical base and historical task catalogue.
+
+The chosen card is `complex-rank-shape-decoder`, explicitly changed to this analytical side question. Common reserves can control compiler tail cutoffs, but this example is synthetic. The metadata binding baseline passed for selected PR6030. Live handoffs, open and merged PRs, source/formula searches on main, and the bounded overlap cache were checked. Unpublished work, arbitrary historical diffs and uninspected replies remain coverage limits.
+
+No physical supplier, native word, compiler admission, complete cost invoice, precision/stock/tape result, new kappa or selected-frontier change is supplied. All five selected framework assumptions remain. Selected cold replay, Lean and Docker were not run. Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+Can a complete source-compatible supplier row menu use optimized reserves to lower a real compiler cutoff? First extract a named caller's complete row menu and required tail tolerance, including all adapters, restoration and extra fees. Actual row legality, native realization, compiler applicability, storage, precision/tape and outer costs remain blockers. Structured fields are in [TASK.json](TASK.json).
+
+## Attribution
+
+The new reserve optimization and proof were produced by Nick Petalas. Ali Romman / PR6472 supplies the exact menu, adaptive contract, total `u=(5,3)`, original `4/5` reserve and the explicit next question. Classical weighted norms, nonnegative matrix and Perron theory retain credit; no general literature-priority claim is made. The source package retains its full predecessor attribution, including its fixed-matrix, observed-forcing and synchronized-switching interfaces. None is recertified here. Apache-2.0.
+
+## Implementation limits
+
+The retained input is fixed, has two types and four rows, and is hash-checked before parsing. All loops have explicit finite bounds. Cutoff requests accept 1..128 precision bits, search at most 1,025 depths and reject exhaustion. Verification checks use explicit exceptions, so optimized Python preserves every check. Functions remain below 60 physical lines. Python's managed fractions, JSON and hashing allocate dynamically, a rule-3 deviation bounded here by the fixed input, 4,096 weight pairs, 257 prefix depths and at most 1,025 cutoff iterations. This is a finite exact-arithmetic check, not a fixed-memory embedded implementation. The normal and optimized warning-strict registered commands are the diagnostics; no separate Python static analyzer is configured for this package. A future configurable or native implementation must revisit these resource bounds.

research/sharp-adaptive-reserve/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/sharp-adaptive-reserve/TASK.json

@@ -0,0 +1,75 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Optimize the common positive-weight contraction ratio for the exact two-type example of Ali Romman PR6472, and improve its certified finite-depth relative tail cutoff.",
+  "scope_change_reason": "This is a scoped analytical side result answering PR6472's explicit reserve-ratio open question, rather than a new physical decoder or productive-target itinerary.",
+  "bottleneck_link": "Common contraction reserves control finite compiler tails. This synthetic row menu is not a selected physical supplier, so the result supplies no native, compiler or outer admission.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first proved exact reserve improvement; package its proof and finite corroboration without extending to other menus.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; reserve.py; verify.py; generated hash-bound stdout receipt.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a complete source-compatible supplier row menu use an optimized reserve to lower a real compiler tail cutoff?",
+      "why_it_matters": "The displayed 64-bit cutoff improvement is synthetic until a real caller supplies every row and extra charge.",
+      "first_step": "Extract one named caller's complete row menu and its required tail tolerance; include adapters, restoration and every additional fee before optimizing weights.",
+      "blocked_by": "No physical supplier menu, compiler applicability, native realization, storage, precision/tape or outer bill is bound in this package."
+    }
+  ]
+}

research/sharp-adaptive-reserve/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact sharp-ratio polynomial, all four row inequalities, rational reserve, literal finite-depth tails, exact cutoff minimality, invalid certificates and source corruption."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Identical complete coverage with Python assertions disabled."
+    }
+  ]
+}

research/sharp-adaptive-reserve/inputs/example6472.json

@@ -0,0 +1,7 @@
+{
+  "schema": "adaptive-row-bill/v1",
+  "rows": [
+    [[0, "6/5"], ["1/5", 1]],
+    [["2/5", 0], [0, "1/4"]]
+  ]
+}

research/sharp-adaptive-reserve/reserve.py

@@ -0,0 +1,70 @@
+"""Exact common reserves for the retained two-type row menu."""
+
+from fractions import Fraction
+from hashlib import sha256
+import json
+
+Row = tuple[Fraction, Fraction]
+Menu = tuple[tuple[Row, ...], tuple[Row, ...]]
+Vector = tuple[Fraction, Fraction]
+SOURCE_SHA256 = "8819bb327b318bed314cc6cd12781e4ad148a18a4cf77fa749167bc7b1c3c3b4"
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+def parse_menu(data: bytes) -> Menu:
+    """Authenticate the exact source bytes before parsing their four rows."""
+    require(sha256(data).hexdigest() == SOURCE_SHA256, "source hash mismatch")
+    raw = json.loads(data)
+    require(raw["schema"] == "adaptive-row-bill/v1", "unexpected schema")
+    groups = raw["rows"]
+    require(len(groups) == 2, "expected two types")
+    parsed = []
+    for group in groups:
+        require(len(group) == 2, "expected two rows per type")
+        rows = []
+        for row in group:
+            require(len(row) == 2, "expected two coefficients")
+            a, b = (Fraction(value) for value in row)
+            require(a >= 0 and b >= 0, "negative row")
+            rows.append((a, b))
+        parsed.append(tuple(rows))
+    return parsed[0], parsed[1]
+
+
+def common_ratio(menu: Menu, weight: Vector) -> Fraction:
+    require(len(weight) == 2 and min(weight) > 0, "positive two-type weight required")
+    return max(
+        (row[0] * weight[0] + row[1] * weight[1]) / weight[i]
+        for i in range(2)
+        for row in menu[i]
+    )
+
+
+def check_certificate(menu: Menu, weight: Vector, ratio: Fraction) -> None:
+    require(0 <= ratio < 1, "ratio must be in [0,1)")
+    require(common_ratio(menu, weight) <= ratio, "row exceeds claimed ratio")
+
+
+def next_prefix(menu: Menu, value: Vector) -> Vector:
+    require(len(value) == 2 and min(value) >= 0, "nonnegative prefix required")
+    values = tuple(
+        1 + max(row[0] * value[0] + row[1] * value[1] for row in group)
+        for group in menu
+    )
+    return values[0], values[1]
+
+
+def first_cutoff(ratio: Fraction, prefactor: Fraction, bits: int) -> int:
+    require(0 < ratio < 1 and prefactor >= 1, "invalid tail bound")
+    require(type(bits) is int and 1 <= bits <= 128, "bits outside 1..128")
+    threshold = Fraction(1, 2**bits)
+    tail = prefactor
+    for depth in range(1025):
+        if tail <= threshold:
+            return depth
+        tail *= ratio
+    raise ValueError("cutoff exceeds the explicit 1024-depth limit")