Prove the maximal reserved-scratch echo equality band (no new κ)

research/dirty-echo-maximal-equality/PROOF.md

@@ -0,0 +1,148 @@
+# The maximal equality interval for reserved-scratch dirty echoes
+
+This scoped combinatorial proof is produced by Nick Petalas. The tree model,
+echo semantics and universal lower bound are inherited from Alexander
+Schwartzman's [PR784](https://github.com/CrocSwap/integer-mult-bounds/pull/784).
+Gareth Davidson's [PR887](https://github.com/CrocSwap/integer-mult-bounds/pull/887)
+formalizes the preceding sufficient equality interval. Neither predecessor
+claims that interval is maximal. The contribution here is the exact maximal
+interval and the complete recursive equality characterization.
+
+## Model and theorem
+
+An ordered tree has no unary nodes. A leaf has factor count n=1, completed
+call count N=1 and scratch requirement S=0. A node with k>=2 children obeys
+
+```
+n = sum n_i,
+N = 2 N_1 + 4 sum_(1<i<k) N_i + 2 N_k,
+S = k-1 + max S_i.
+```
+
+These are the static all-arity echoes that reserve every parent connector
+throughout every child invocation. Factors stay ordered. All signed leaf
+invocations, including inverse and restoration calls, are counted. Unit leaf
+prices, sequential child execution and a disjoint deeper scratch pool are
+part of the model. The inherited echo identity is not reverified here.
+
+For a nonnegative integer budget s, define
+
+```
+B_s(n) = 2^(s+1)n - 4^s,
+a_s = ceil(2^(s+1)/3).
+```
+
+The predecessor proves capacity n<=2^s and N>=B_s(n) whenever S<=s.
+The new theorem is
+
+```
+there exists a tree with S<=s, n leaves and N=B_s(n)
+    if and only if a_s <= n <= 2^s.
+```
+
+In this interval the exact minimum completed call count is B_s(n). Outside
+it, no feasible tree attains that affine bound. The statement includes s=0,
+where the unique equality tree is one leaf, and s=1, where it is a binary
+pair. Every equality tree uses the full available budget.
+
+For example s=4,n=11 has exact minimum 96. Its ternary root has child leaf
+counts (4,3,4), child calls (16,8,16) and child budgets (2,2,2). Thus the
+root bill is 2*16+4*8+2*16=96, with four reserved scratch arrays. The prior
+sufficient interval at s=4 started at n=12. PR784 already tabulates finite
+optima; this example illustrates the new general theorem and is not claimed
+as a newly discovered numerical minimum.
+
+## Exact slack identity and all equality trees
+
+Let delta_s(T)=N(T)-B_s(n(T)). For a leaf,
+
+```
+delta_s(leaf) = (2^s-1)^2.
+```
+
+For an internal root of arity k, put r=s-k+1, p=2^r, t=2^(k-1),
+and w_1=w_k=2, with interior weights w_i=4. Every child has S_i<=r,
+so r>=0. Direct substitution gives the exact identity
+
+```
+delta_s(T) = sum_i w_i delta_r(T_i)
+           + 2p sum_i (t-w_i)(p-n_i)
+           + p^2 (t-2)(t-2k+2).                  (1)
+```
+
+Indeed sum w_i=4k-4 and 2^s=pt. Expanding the right side cancels the
+constant and linear terms to N(T)-2pt sum n_i+p^2 t^2.
+All three terms on the right are nonnegative: the predecessor's bound gives
+child slack, capacity gives n_i<=p, t>=w_i, and t>=2k-2 for k>=2.
+For k>=4, t>2k-2 and t>2, so the final term is strictly positive.
+This extracts equality conditions from the inherited inequality without
+assuming the predecessor's sufficient construction is exhaustive.
+
+Consequently every equality tree, and only such a tree, follows these rules
+with the indicated contextual budget:
+
+1. At s=0 it is a leaf. A leaf at any s>0 is not tight.
+2. A binary root at s>=1 has two equality children at budget s-1.
+3. A ternary root at s>=2 has three equality children at budget s-2,
+   and its first and last children each have exactly 2^(s-2) leaves.
+4. No node with arity at least four occurs.
+
+For rule 3, the endpoint coefficients t-w_i equal 2, while the middle
+coefficient is zero. This proves necessity and sufficiency directly in (1).
+A tree of capacity 2^r at budget r is the unique perfect binary tree of
+height r. To see this, a root of arity k>=3 has at most
+k*2^(r-k+1)<2^r leaves; a binary root must have both children at capacity,
+and induction finishes. Thus the endpoint subtrees in rule 3 are uniquely
+specified. The classification concerns ordered shapes, not uniqueness of
+all equality trees or of schedules in a larger reversible-program class.
+Induction on these rules also gives S=s for every equality tree.
+
+## Exact interval, necessity and constructive sufficiency
+
+Let E_s be the set of equality leaf counts. The classification yields
+
+```
+E_0 = {1}, E_1 = {2},
+E_s = (E_(s-1) + E_(s-1)) union (2^(s-1) + E_(s-2)), s>=2,       (2)
+```
+
+where the first plus is the set of pairwise sums and the second translates
+a set. Both directions of (2) are constructive because children occupy
+consecutive factor intervals. Endpoint perfect binary trees use no extra
+space beyond their prescribed child budgets.
+
+Inductively suppose E_j=[a_j,2^j] over the integers for smaller budgets.
+The binary part of (2) is the whole interval
+[2a_(s-1),2^s]. The ternary part is
+[2^(s-1)+a_(s-2),3*2^(s-2)]. The lower ternary endpoint equals a_s,
+since subtracting the integer 2^(s-1) from 2^(s+1)/3 leaves 2^(s-1)/3.
+The lower binary endpoint is either a_s or a_s+1. For completeness,
+
+```
+2 ceil(2^s/3) = a_s + 1, if s is even,
+2 ceil(2^s/3) = a_s,     if s is odd.
+```
+
+Also a_s<=3*2^(s-2), because the expression on the right is an integer
+at least 2^(s+1)/3. Hence these two integer intervals overlap or are
+adjacent, their union is exactly [a_s,2^s], and no smaller leaf count is
+possible. This proves the claimed maximal interval for every s.
+
+An explicit constructor uses a binary root whenever n>=2a_(s-1).
+Set the first child size to max(a_(s-1),n-2^(s-1)) and the second to the
+remaining size. Both lie in [a_(s-1),2^(s-1)]. If this test fails, use a
+ternary root with endpoint sizes 2^(s-2) and middle size n-2^(s-1).
+The interval argument places that middle size in E_(s-2). Repeat down
+to s=0. The implementation uses a bounded iterative worklist.
+
+## Scope
+
+This is an all-size written theorem about a specified tree grammar, with
+finite exact corroboration. It supplies no new multiplication exponent,
+physical supplier, tape implementation, weighted-price optimum, precision
+bound, nonlinear-gate statement or full multiplication theorem. Connector
+reuse, clean checkpoints, changing the echo word, interleaved lifetimes,
+borrowing ancestor arrays and arbitrary reversible programs are outside it.
+The predecessor's unfavorable full-supplier bill is unchanged. The proof is
+not checked by a formal kernel; the earlier Lean theorem has not been
+extended or rerun. No predecessor audit is a deliverable of this package.

research/dirty-echo-maximal-equality/README.md

@@ -0,0 +1,105 @@
+# The exact maximal equality band for dirty echoes
+
+For the ordered reserved-parent-scratch echo grammar of Alexander
+Schwartzman's [#784](https://github.com/CrocSwap/integer-mult-bounds/pull/784),
+the affine lower bound is attained exactly when
+
+```
+ceil(2^(s+1)/3) <= n <= 2^s,
+min N = 2^(s+1)n - 4^s.
+```
+
+This extends the preceding sufficient band `3*2^(s-2) <= n <= 2^s`.
+[PROOF.md](PROOF.md) also characterizes every equality tree. Its exact slack
+identity permits binary nodes with tight children and ternary nodes with
+capacity-saturating endpoints; larger arities have positive slack.
+At four scratch arrays the new theorem includes eleven factors and 96
+complete calls. The predecessor's finite table already includes this
+numerical optimum. The contribution is the all-size maximality theorem,
+not a replay or recount of that table.
+
+Claim type: scoped proof with exact finite corroboration. No new kappa,
+physical supplier or complete multiplication theorem is claimed.
+This contribution is produced by Nick Petalas. Independent human and
+formal proof-kernel review are unclaimed.
+
+## 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 scripts/research_package.py --package research/dirty-echo-maximal-equality
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/check_research_commit.py --package research/dirty-echo-maximal-equality --check-source-history
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/dirty-echo-maximal-equality/verify.py
+```
+
+The first command runs both registered checks. A portable reviewer can replace
+the absolute interpreter path with their CPython 3.12 executable. The scientific
+verifier also runs outside Git. It compares every field of the generated
+[RESULT.json](RESULT.json), including source hashes, and prints
+`PASS_DIRTY_ECHO_MAXIMAL_EQUALITY`. `--write /absolute/new/file.json` creates
+an exclusive generated receipt and refuses an existing path.
+
+[oracle.py](oracle.py) independently minimizes over every root arity and
+positive child-size composition, without using the new equality threshold.
+It checks all budgets 0..8 and factor counts 1..256. A separate whole-tree
+enumerator checks the recursive characterization on every ordered tree through
+eight leaves, including nonoptimal shapes and every fitting budget through
+eight. The constructor supplies every equality size through budget eight.
+Boundary and corruption controls run under optimized Python as well.
+Finite checks support the written proof; they do not establish its universal
+quantifiers by enumeration. Exact coverage is generated in RESULT.json.
+No predecessor verifier, Lean build or supplier replay is run.
+
+## Credit and source boundary
+
+Alexander Schwartzman #784 supplies the lower bound and sufficient equality
+family. Gareth Davidson #887 supplies its scoped Lean formalization, explicitly
+without maximality. The original multiway echo and restoration semantics are
+androolloyd's #673. Credit Koroffstrogov #758 for the all-arity optimizer,
+Sagar Thakrar #730 for ordered binary/ternary optimization, Dillon Amburgey
+#689 for the balanced ternary baseline, and the retained Chafik Boukhalfa
+#628 leaf lineage. No predecessor implementation is copied or imported.
+[SOURCES.json](SOURCES.json) pins the statements as historical provenance.
+The model and the necessary definitions are stated completely in PROOF.md.
+The source contexts are cited premises; their computations are not rechecked.
+
+The entry cached scan covered 379 open PRs and 3,859 Discussion records,
+with complete reported pagination. Its local corpus included only 102 of
+6,319 tracked notes. Relevant predecessor notes were then materialized.
+Live handoffs, relevant PR bodies, merged-term searches and all-main README
+searches supplement the scan. They do not cover unpublished work or prove
+literature novelty. The canonical claim is in
+[handoffs #1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133745).
+New files are Apache-2.0.
+
+## Limits and verification policy
+
+The theorem keeps unit leaf prices, all inverse/restoration calls, ordered
+factors, static trees and parent-reserved dirty arrays. It does not cover
+connector reuse, clean checkpoints or arbitrary reversible programs. The full
+supplier bill remains a separate, unfavorable predecessor interface; local
+call optimality does not improve kappa. A formal-kernel extension, physical
+caller and weighted analogue remain unrun or unresolved.
+
+The new Python code has bounded inputs and iterative traversals. Functions
+fit within 60 physical lines. Explicit exceptions remain active under `-O`.
+Managed Python and itertools allocate at runtime, a Power of Ten deviation;
+fixed domains of at most 256 leaves, budget eight and eight-leaf exhaustive
+trees bound live data. Strict-warning normal/optimized runs and corruption
+controls provide the applicable diagnostics. The local oracle import uses one explicit path and the receipt binds its
+bytes. Rejection controls dispatch only to two named validation functions.
+These bounded Python mechanisms are documented deviations from the strict
+metaprogramming and indirect-call rules. No static type checker is configured
+for this standalone integer verifier; syntax compilation and strict-warning
+execution are the available language diagnostics.
+
+## Open next questions
+
+- Determine a closed form for the number of equality trees at each `(s,n)`.
+  Start from the disjoint binary/ternary shape recurrence in PROOF.md.
+  This would distinguish existence from schedule multiplicity; no physical
+  caller is needed, but no such count is proved here.
+- Find a useful analytic bound for unequal leaf prices under the same scratch
+  contract. Start with one fixed ordered price vector and keep all restoration
+  multipliers. The maximal unit-price equality band alone does not solve it.

research/dirty-echo-maximal-equality/RESULT.json

@@ -0,0 +1,69 @@
+{
+  "controls": {
+    "rejected_inputs": 22,
+    "structural_controls": 2
+  },
+  "examples": [
+    {
+      "budget": 4,
+      "calls": 96,
+      "leaves": 11,
+      "postfix_sha256": "c2ef8701595d8fec3daf5c9bf73d14a704b9a4a824b8a15e34adf56cb2d82245",
+      "scratch": 4
+    },
+    {
+      "budget": 6,
+      "calls": 1408,
+      "leaves": 43,
+      "postfix_sha256": "170fe6ff4215c2414a59d88554ef5f8ed44288005728da345265bd0e6b061d6a",
+      "scratch": 6
+    },
+    {
+      "budget": 8,
+      "calls": 22016,
+      "leaves": 171,
+      "postfix_sha256": "f3060db63c8c36e92101a97734bcae5a629596c72a3ca4c4acde415fa3ad0bc9",
+      "scratch": 8
+    }
+  ],
+  "minima": {
+    "cells": 2304,
+    "equality_sizes_per_budget": [
+      1,
+      1,
+      2,
+      3,
+      6,
+      11,
+      22,
+      43,
+      86
+    ],
+    "transitions": 51374,
+    "witnesses": 175
+  },
+  "schema_version": 1,
+  "scope": "Scoped written theorem; finite exact corroboration only",
+  "shapes": {
+    "equality_occurrences": 9,
+    "tree_budget_comparisons": 48960,
+    "trees": 5440,
+    "trees_per_size": [
+      1,
+      1,
+      3,
+      11,
+      45,
+      197,
+      903,
+      4279
+    ]
+  },
+  "source_sha256": {
+    "PROOF.md": "9994f4350e550abd2c31417e8ef4e6846729d9f55bc4159ac0eb68811348580d",
+    "oracle.py": "f3dcd19bb3286e8fb904ad9fa72308af910911eb0eedeb61bf50f91dc1949d86",
+    "test_package.py": "397c1040ba0d2a0b72f1aeb55e61195ceee5419014b40c7d26743cc8935d0274",
+    "verify.py": "c5e3443a901a781f8f8a74343f47f8ded7d16720071db70eaf6acdc9f23abf40"
+  },
+  "status": "PASS_DIRTY_ECHO_MAXIMAL_EQUALITY"
+}

research/dirty-echo-maximal-equality/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/dirty-echo-space-budget/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "3a7c2f4c84b06592c54a518441f554210867b9f0",
+      "sha256": "b3c290eb501ac3c806838677aaa50546d2443e638d6f67ac37711c0646fe30ac"
+    },
+    {
+      "path": "research/lean-dirty-echo-budget/README.md",
+      "usage": "provenance",
+      "git_blob": "3727dca7f51ec11fa2543eaaa4c76261e1a58db1",
+      "sha256": "1795505e18337bcc041eaf579ef666ca3789f85a6ab45da9f5b382d2290cd362"
+    }
+  ]
+}