Prove exact weighted five-node clean scratch (no new κ)

research/weighted-five-node-chain/README.md

@@ -0,0 +1,171 @@
+# Exact weighted scratch for a five-node clean chain
+
+This package proves a closed form for a reversible dependency chain with
+arbitrary positive real node widths. The claim is a scoped mathematical proof
+with exact finite corroboration. It is a side result about clean scratch
+scheduling. It supplies no selected stock coefficient, physical implementation
+or new kappa.
+
+Let nodes 1 through 5 form a path. Node 1 has no parent; node i has parent i-1.
+A move computes an absent node or erases a present node, and its parent must be
+present for either move. External inputs remain available outside the scratch
+count. Begin empty and end with exactly node 5. The scratch usage of a state S
+is the sum of its positive widths w_i. Arbitrarily many recomputations are
+allowed, provided the schedule is finite.
+
+The exact minimum peak scratch is
+
+```text
+C(w) = w5 + max(w1+w2, w3+w4, w2+w3+min(w1,w4)).
+```
+
+Thus one of two fixed schedules is optimal for every width tuple. If w1<w4,
+use the first schedule below; otherwise use the second. At equality either
+works. This is a space optimum. No minimum operation-count claim is made.
+
+## Proof of the lower bound
+
+Take any successful finite schedule. Consider its last computation of node 5.
+The suffix starts with nodes 4 and 5 present, and node 5 remains present
+throughout. Node 4 must eventually be erased. At its first erasure in this
+suffix, nodes 3, 4 and 5 are present. Every successful schedule therefore has
+peak at least w3+w4+w5.
+
+At that erasure of node 4, if node 2 is present, the schedule visits a superset
+of {2,3,4,5}. If node 2 is absent, node 3 remains present just after the
+erasure. Node 3 cannot be erased before node 2 has been computed. At the first
+subsequent computation of node 2, its parent 1 is present and node 3 is still
+present. The schedule then visits a superset of {1,2,3,5}. Consequently it must
+visit at least one of these two four-node sets.
+
+Every successful schedule also visits a superset of {1,2,5}. In the preceding
+case where node 2 is initially absent, this already follows from its subsequent
+computation. When node 2 is present at the first erasure of node 4, it must
+eventually be erased, and that erasure requires node 1 while node 5 remains
+present.
+
+Positivity of the widths turns these mandatory sets into the lower bound
+
+```text
+max(w1+w2+w5, w3+w4+w5,
+    min(w1+w2+w3+w5, w2+w3+w4+w5)) = C(w).
+```
+
+The argument uses the suffix after the final computation of node 5. It covers
+schedules that compute and erase node 5 earlier, extra visits to any state, and
+arbitrary recomputation of the other nodes.
+
+## Two attaining schedules
+
+A positive integer denotes computation and a negative integer denotes erasure.
+Every displayed move has its parent present. All other states are subsets of
+one of the two maximal states listed for that schedule.
+
+```text
+Via node 3, 13 moves:
+  1, 2, 3, -2, -1, 4, 5, -4, 1, 2, -3, -2, -1
+  maximal states: {1,2,3,5}, {3,4,5}
+  peak A = w5 + max(w1+w2+w3, w3+w4)
+
+Via node 2, 11 moves:
+  1, 2, -1, 3, 4, 5, -4, -3, 1, -2, -1
+  maximal states: {1,2,5}, {2,3,4,5}
+  peak B = w5 + max(w1+w2, w2+w3+w4)
+```
+
+If w1<=w4, the four-node sum for A is the smaller one, and
+w1+w2<=w1+w2+w3. Hence A=C(w). If w4<=w1, the four-node sum for B is the smaller
+one, and w3+w4<=w2+w3+w4. Hence B=C(w). This attains the lower bound for every
+positive real width tuple. For unit widths the optimum is four. Widths
+(1,1,1,10,1) favor the first schedule, and (10,1,1,1,1) favor the second;
+their respective peak charges are 12 versus 13.
+
+## Reproduce and interpret the evidence
+
+From the repository root, use the actual CPython 3.12 interpreter:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/weighted-five-node-chain/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/weighted-five-node-chain/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/weighted-five-node-chain
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/weighted-five-node-chain --check-source-history
+```
+
+The verifier builds every legal edge on all 32 states, independently of the two
+supplied schedules. For every one of the 16,807 integer tuples in {1,...,7}^5,
+a bottleneck shortest-path oracle agrees with C(w), a separate set-based
+schedule replay attains it, and a capacity-bounded reachability check rejects
+every strictly smaller capacity. Three width-independent separating-state
+checks corroborate the proof's mandatory-set argument.
+
+Controls reject nine invalid width inputs and seven invalid schedules. They
+also distinguish merely visiting node 5, which needs three unit pebbles, from
+the clean endpoint, which needs four. Weighted controls distinguish both
+attaining branches, and the integer-width limit is exercised. All checks remain
+enabled under optimized Python. The bounded numeric interface accepts integer
+widths in 1..10^12. The written proof establishes the real-width theorem.
+
+Standard output is a generated JSON receipt with the interpreter version,
+counts, separating-state components and SHA256 hashes of every package file.
+Use `--receipt /absolute/scratch/path/receipt.json` to save it outside the
+package. Direct verification also works without Git or repository imports.
+SOURCES.json pins only catalogue and selected-record provenance. No pending
+predecessor source is needed to run this verifier.
+
+## Scope, predecessor and credit
+
+The operation contract is the pure reversible-pebble model in Ali Romman's
+[PR #5780](https://github.com/CrocSwap/integer-mult-bounds/pull/5780), head
+`0ed431c52085852999a5817e80b508c1b3c63f75`. Its
+[model guide](https://github.com/aliromman/integer-mult-bounds/blob/0ed431c52085852999a5817e80b508c1b3c63f75/docs/research/reversible-pebble-schedules.md)
+poses source-DAG and budget applications. That work supplies an exact bounded
+planner for a supplied numerical instance. This contribution gives a universal
+five-width threshold and two attaining schedules. Its verifier imports no
+predecessor code and does not replay the predecessor's examples or tests.
+Classical reversible pebbling retains its original credit.
+
+This changes the `selected-stock-envelope` card to a small analytical side
+result about a declared DAG. It does not bind that DAG to the selected producer.
+A clean pebble represents stored pure data. It is not an arbitrary productive
+dirty helper. Scratch charges exclude external inputs and the implementation
+of compute/erase operations. Native legality, precision, physical movement,
+dirty restoration, caller charges and all five framework assumptions remain
+separate. No Lean, formal proof kernel, native replay, selected cold replay or
+full multiplication theorem is claimed.
+
+The formula, proof and finite corroboration were produced by Nick Petalas.
+New material is Apache-2.0. Independent human and formal proof-kernel review
+are unclaimed.
+
+## Open next questions
+
+- Extract an actual five-node pure dependency chain from a supplier, with legal
+  compute and erase routines. Insert its widths into the formula and price the
+  selected schedule's full operations. Native and dirty-state contracts are the
+  blockers; the formula alone does not reduce selected stock.
+- Determine the minimum operation charge at the optimal scratch capacity when
+  computation and erasure have different prices. Begin with the same 32-state
+  graph and retain both schedules as upper bounds. This package optimizes space
+  only and does not claim either schedule minimizes those charges.
+
+## Verifier bounds
+
+The graph has 32 vertices and 96 directed edges. Each reachability queue removes
+at most 32 distinct states. Each minimax run has at most 97 heap removals, since
+each directed edge can relax only after its source is settled. The width sweep
+has exactly 7^5 iterations. Supplied schedule length is capped at 31. Each
+function is under 60 physical lines. Warning-strict ordinary/optimized replay
+and source compilation provide the available Python diagnostics.
+
+Python's managed runtime dynamically allocates objects, so Power of Ten rule 3
+requires a deviation. The deviation is confined to this terminating verifier:
+the graph, all queues and all state tables have the preceding fixed bounds,
+widths are at most 10^12, and each tuple is released before the next one. The
+compensating checks are the complete sweep and explicit exhaustion guards.
+A fixed-memory implementation would be needed if this were reused inside a
+runtime with allocation restrictions.
+
+The failure-control helper uses indirect calls to exactly two local functions,
+`capacity` and `replay`. This is a rule 9 deviation confined to the sixteen
+invalid-input controls. Both call targets are explicit and their exceptions
+are checked. Direct checks would replace this helper if either API changed.

research/weighted-five-node-chain/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}

research/weighted-five-node-chain/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "selected-stock-envelope",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "selected-stock-envelope",
+    "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?",
+    "starting_points": [
+      "research/selected-bootstrap-stock-audit/README.md",
+      "research/bootstrap-cutoff-time-space-split/README.md",
+      "certificates/selected-result.json",
+      "docs/research/community-efficient1000-review.md",
+      "research/stock-margin-chain/README.md"
+    ],
+    "methods": [
+      "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.",
+      "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope."
+    ],
+    "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.",
+    "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": "Choose one actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.",
+    "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.",
+    "allowed_variations": [
+      "One stage or one explicit reserve/depth implication.",
+      "An independently checked same-domain proof repair, retaining all remaining assumptions."
+    ],
+    "scope_change_triggers": [
+      "Importing the historical 57604 or 252 allowance without a selected-producer binding.",
+      "Calling a conditional fit lemma a full outer-proof adoption.",
+      "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality."
+    ],
+    "overlap_terms": [
+      "selected stock",
+      "stock envelope",
+      "bootstrap cutoff",
+      "1956",
+      "1965",
+      "1990",
+      "2972",
+      "stock-margin-chain",
+      "actual_stock_coefficient"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.",
+        "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation",
+        "remaining": "Derive one actual reserve/depth coefficient from the selected producer.",
+        "status": "reviewed",
+        "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact minimum peak clean scratch for a five-node reversible path, for every positive real width tuple, with arbitrary finite recomputation.",
+  "scope_change_reason": "Take the scratch-budget application boundary of PR5780 as a small analytical side result. Replace selected-producer coefficient extraction with a universal width-parametric clean-chain theorem. No selected source binding is claimed.",
+  "bottleneck_link": "Side result: a closed-form scratch budget can price a legal five-node pure sub-DAG once a supplier provides it. It does not establish a selected reserve coefficient.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first exact threshold with attaining schedules and complete finite-state corroboration; do not extend to longer chains or operation-price optimization.",
+  "outcome": "completed",
+  "evidence": "Written suffix lower bound, two attaining schedules, all 16807 width tuples in 1..7 checked against full-state minimax and strict-capacity reachability, separating-state checks and input/endpoint controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual supplier provide a five-node pure chain with legal compute and erase routines?",
+      "why_it_matters": "Only a source binding can turn the side lemma into a supplier stock budget.",
+      "first_step": "Extract one five-node path with node widths and price every move of the attaining schedule.",
+      "blocked_by": "Native, dirty-state, delivery and cleanup contracts."
+    },
+    {
+      "question": "What is the minimum operation charge at optimal capacity with unequal compute and erase prices?",
+      "why_it_matters": "A space-optimal schedule need not have the cheapest complete instruction bill.",
+      "first_step": "Use exact weighted shortest paths on the same 32-state graph at the proved capacity.",
+      "blocked_by": "A declared source operation-price contract; not attempted here."
+    }
+  ],
+  "predecessor": {
+    "pr": 5780,
+    "author": "Ali Romman",
+    "head": "0ed431c52085852999a5817e80b508c1b3c63f75",
+    "use": "Cited model and scratch-budget question only; no implementation or numerical result is imported."
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19215657"
+}

research/weighted-five-node-chain/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Universal-threshold finite corroboration over 16807 tuples, attaining schedules, full-state oracle, strict-capacity exclusion and semantic controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same complete verification with optimization enabled; all proof checks use explicit exceptions."
+    }
+  ]
+}