Prove exact canonical-checkpoint costs for cyclic output frames (no new κ)

research/cyclic-checkpoint-cost/README.md

@@ -0,0 +1,201 @@
+# Exact canonical-checkpoint costs for cyclic output frames
+
+This scoped proof answers the second **Open next question** in Ross
+Richardson's [PR1287](https://github.com/CrocSwap/integer-mult-bounds/pull/1287).
+It gives a closed form and an attaining schedule for any prescribed canonical
+cuts in that fixed-child batch, and the sharp price of one extra cut.
+No new kappa is claimed.
+
+For workspace/output rotation prices `A=3, B=1`, five children cost 8 boundary
+units. A canonical cut after child 2 still costs 8; a cut after child 1 costs 9.
+Eager restoration costs 15. Thus an internal canonical cut can retain the full
+boundary saving. These costs exclude the common child bodies. With the inherited
+six-ADD rotation backend, the two boundary passes in a complete echo save
+respectively 84 and 72 ADDs against eager restoration. No new rotation circuit
+is asserted.
+
+## Contract and exact formula
+
+Use the predecessor's fixed indivisible children
+
+```
+C_i(D,W) = (D + R_i W, P W),   R_i P = Q R_i,   P^3 = Q^3 = I.
+```
+
+`P,Q` rotate every workspace/output triple. Inputs and private child workspace
+are arbitrary dirty values. The parent applies only whole-register powers of
+`P,Q` between ordered complete children. Either nonidentity power costs `A>0`
+on workspace and `B>0` on output. The word must work uniformly over all admitted
+readers and arbitrary incoming output. Before each child the two phases must
+therefore agree. A canonical cut requires both phases zero. Cuts are read-only
+frame requirements, without mutation or adaptive changes to later children.
+
+Let `b(k)` be the minimum boundary cost for `k>=1` children, canonical at both
+ends, without internal cuts. For all positive real prices:
+
+```
+if A <= B: b(k) = k A
+if A >  B: b(k) = k B + f(k mod 3)
+
+f(0) = 0
+f(1) = A-B
+f(2) = min(2(A-B), A)
+```
+
+For prescribed cuts partitioning the children into positive segment lengths
+`k_1,...,k_s`, the exact optimum is `sum_j b(k_j)`.
+
+The extra cost of splitting one segment into lengths `u,v>=1` is
+`b(u)+b(v)-b(u+v)`. It is zero when `A<=B`. When `A>B`, its sharp maximum is
+
+```
+(A-B) + min(2(A-B), A).
+```
+
+Residues 1 and 2 in either order attain the maximum. Optimality concerns this
+macro alphabet and uniform reader class. Opening child bodies changes the model.
+
+## Proof
+
+The predecessor gives the aligned transition. If the phase before a child is
+`t` and the next aligned phase is `s`, put `d=s-t mod 3`. The child changes
+`(t,t)` to `(t+1,t)`, so its post-child powers and transition prices are
+
+```
+workspace: d-1 mod 3,   output: d,
+c(0)=A,  c(1)=B,  c(2)=A+B.
+```
+
+A nonzero entrance phase `(t,t)` costs `A+B`. Replace that entrance and its
+first post-child gap by a first transition from phase zero to the same next
+aligned phase `s`. That transition costs at most `A+B`, so is no dearer. The
+next state is identical and all children remain aligned. The uniform canonical
+map is preserved. Thus an optimum has zero entrance phase, including when the
+first child is followed by a canonical cut.
+
+Let `n_d` count the transitions of difference `d`. Order does not affect cost
+or the final phase. The constraints are
+
+```
+n_0+n_1+n_2 = k,   n_1+2n_2 = 0 mod 3,
+cost = n_0 A+n_1 B+n_2(A+B).
+```
+
+If `A<=B`, each transition costs at least `A`; all-zero differences attain
+`k A`. Suppose `A>B`. Replace two differences 2 by differences 0 and 1.
+Their sum modulo three is unchanged and cost falls by `A+B`. Replace a pair
+0 and 2 by two differences 1: the sum is unchanged and cost falls by
+`2A-B>0`. Hence an optimum has either no 2, or exactly one 2 and no 0.
+
+With no 2 the congruence requires `n_0=k mod 3`, modulo multiples of three.
+Cost increases with `n_0`, so the best such word has `r=k mod 3` zero
+differences and all others 1. Its cost is `k B+r(A-B)`. The other possibility
+has one difference 2 and all others 1. It is legal precisely when `r=2` and
+costs `A+k B`. Taking the smaller proves the formula and explicitly constructs
+an attaining word. Use the zero differences first, followed by the 1s; in the
+second case use the 2 first, followed by the 1s.
+
+Each prescribed cut has the canonical state. Restricting a legal word to each
+segment gives the lower bound `b(k_j)`. Concatenating the attaining segment
+words gives the upper bound, proving additivity.
+
+For the one-cut bound put `a=A-B>0`, `c=min(2a,A)`. The residue correction is
+`(0,a,c)`, where `a<=c<=2a`. A pair with a zero residue adds zero. The other
+pairs add `2a-c`, `a+c`, or `2c-a`. All lie between zero and `a+c`; residues
+1 and 2 attain `a+c`. This proves the bound and sharpness.
+
+## Evidence and reproduction
+
+The written proof establishes the quantified statement. The generated
+[RESULT.json](RESULT.json) supplies finite corroboration of the new formula:
+
+- All 16,320 cut-mask/price cases through eight children and integer prices
+  `1<=A,B<=8`, compared with a separately written nine-state optimizer that
+  permits every entrance and gap power.
+- All 9,216 pairs `1<=u,v<=12` at those prices, checking the one-cut bound and
+  its attained maximum; 72 exact rational-price cases.
+- All 756 cut-mask/dimension fixtures through six children, with `1<=m<=4`
+  workspace triples and `1<=n<=3` output triples. Periodic integer circulant
+  readers execute each schedule on every dirty input/output basis vector and
+  one signed rational probe. The 10,962 probes check the restored source and
+  canonical partial batch output at every prescribed cut.
+- Fourteen invalid-input/noncanonical-word rejections and three controls
+  distinguishing the residue-two alternatives and an ignored checkpoint.
+
+No predecessor code is imported or replayed. The receipt binds all five package
+source files by SHA-256. Ordinary verification recomputes it and writes nothing.
+From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/cyclic-checkpoint-cost/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/cyclic-checkpoint-cost/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cyclic-checkpoint-cost
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cyclic-checkpoint-cost --check-source-history
+```
+
+Expected marker: `PASS_CYCLIC_CHECKPOINT_COST`. Elsewhere substitute the local
+Python 3.12 path. `--write-result ABSENT_PATH` generates a new receipt and
+refuses to overwrite; it is not the ordinary verification command.
+
+## Limits and implementation bounds
+
+A canonical batch cut exposes `D_initial + sum R_i W_initial`. Inside the
+first batch of a source-only dirty echo this is not the completed partial
+update from the external source. That stronger observation can need extra
+copies, storage or a changed graph and is outside the theorem. Observation
+execution costs are outside the boundary bill.
+
+No selected supplier exposing these indivisible children is identified.
+Physical routing, coefficient access, preparation, precision, native hosting
+and all-size multiplication obligations remain open. The inherited child
+contract, alignment rule and six-ADD upper bound are cited premises. The proof
+is not checked by a formal proof kernel. The selected frontier is unchanged.
+
+The formula implementation accepts up to 4,096 children and positive exact
+integer/Fraction prices at most 4,096, with denominator at most 4,096. Schedule
+emission accepts up to 64 segments and 256 total children, using linear output
+space and emission work. These are implementation limits, not theorem limits.
+No runtime speedup is claimed. Every function is below 60 lines. There is no
+recursion, dynamic code or subprocess execution. Loops have explicit caps or
+fixed fixture dimensions. Managed Python allocations are a Power-of-Ten rule-3
+deviation, bounded by these caps. A fixed-storage implementation would be needed
+to remove that runtime deviation. Warning-strict normal and optimized runs
+exercise interpreter diagnostics; no separate static analyzer is configured.
+
+## Open next questions
+
+1. Can a literal consumer use a canonical partial batch record without requiring
+   the completed external-source partial echo? Identify the record and its
+   read-only use first. That missing consumer blocks an application of the
+   zero-surcharge cuts.
+2. What is the exact minimum when completed partial echoes are required at cuts?
+   Start with three children and one observation, charging every source
+   injection and restoration. Specify the stronger observed-output contract
+   before applying the present formula.
+
+## Scope, overlap and credit
+
+Base main is `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7.
+The `formal-interface-lemma` card is changed to a written exact interface proof
+with finite corroboration. The card's historical baseline fails with
+`KeyError: bit_lower`; the current selected-baseline source-binding command
+passes. Neither is scientific evidence for this theorem.
+
+Overlap checked live open PRs, this account's preceding-day PRs, the last 100
+handoff posts, active discussions, distinctive main README and merged-PR
+searches. The cached scan covered 379 open PRs and 3,852 Discussion records;
+local notes were sparse. No matching canonical-cut formula was found within
+that coverage. Unpublished work and arbitrary diffs remain outside it.
+The [public claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133719)
+records the target and stopping rule.
+
+This contribution was produced by Nick Petalas. Ross Richardson #1287 supplies
+the order-three contract, alignment implication, sharp recurrence and explicit
+checkpoint handoff. The new step is the closed form, arbitrary-cut optimum and
+sharp surcharge, with independently written finite checks. Credit Sagar Thakrar
+#1227 for paid output-sign frames, mightyOil/Philipp #1203 for compatible-reader
+boundaries, and Ross Richardson #1145 for the six-ADD rotation upper bound.
+Hanson Sun #1488 treats faithful S3 transport and cut policies; Cinna Davis #1391
+treats order-four transport. Their work and the retained restoration/echo
+lineage keep predecessor credit. No predecessor files or credits are changed.
+Independent human and formal proof-kernel review are unclaimed. Apache-2.0.

research/cyclic-checkpoint-cost/RESULT.json

@@ -0,0 +1,29 @@
+{
+  "claim_type": "scoped proof with finite corroboration",
+  "counts": {
+    "arbitrary_dirty_basis_and_rational_probes": 10962,
+    "checkpoint_optima": 16320,
+    "formula_mutant_controls": 3,
+    "literal_fixtures": 756,
+    "one_cut_pairs": 9216,
+    "rational_price_cases": 72,
+    "rejected_inputs_and_word_mutants": 14
+  },
+  "five_children_A3_B1": {
+    "cut_after_1": 9,
+    "cut_after_2": 8,
+    "eager": 15,
+    "no_cut": 8,
+    "one_cut_maximum": 5
+  },
+  "no_new_kappa": true,
+  "schema_version": 1,
+  "source_sha256": {
+    "README.md": "f4249104e6418596846ad3d6f05067b83b06d021b20edb0c2961b8a50d46ff0e",
+    "SOURCES.json": "cf6a94a6253a49c82b37ce0e3ee7c17ca8e50cfbe853b1be4bc415d8bab6c395",
+    "TASK.json": "1061c0c50300f0497750106c70e54432b30813f39e5ddf56472b6df94060c651",
+    "VERIFY.json": "3166e07deaa59e9b86d22ee887c25bbf589af6c01b5ec146cc4a4ea1f186967f",
+    "verify.py": "91e21e4c677421d24912a75f588ecfb23216172f36b0d2e97590e596e50ce256"
+  },
+  "status": "PASS_CYCLIC_CHECKPOINT_COST"
+}

research/cyclic-checkpoint-cost/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/cyclic-output-restoration/README.md",
+      "usage": "input",
+      "git_blob": "2cb99db015f3b24a1fc31158013cf408b75b0225",
+      "sha256": "fc56e55e76a4d41d9da442ee1af63b4032eb41267a80500814f81027cc0fd087"
+    }
+  ]
+}

research/cyclic-checkpoint-cost/TASK.json

@@ -0,0 +1,114 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "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": "Exact canonical-checkpoint optimum for the fixed order-three cyclic-equivariant child batch, with a closed form, attaining schedules and sharp one-cut surcharge.",
+  "scope_change_reason": "Follow Ross Richardson PR1287 Open next question 2. This is an original written interface theorem with finite corroboration, rather than a proof-assistant theorem-to-certificate binding.",
+  "bottleneck_link": "Determine exactly which canonical observations preserve a paid output-frame boundary saving. This is a scoped side interface result; no selected supplier or kappa improvement is claimed.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified closed form and attaining canonical-cut schedule; package without expanding to a physical caller or stronger observed-output contract.",
+  "outcome": "completed",
+  "evidence": "README.md proves the quantified optimum; verify.py compares the new formula with a nine-state optimizer and executes the new schedules on exact dirty-state inputs. RESULT.json is generated and source-hash-bound.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a literal consumer use a canonical partial batch record without requiring a completed external-source partial echo?",
+      "why_it_matters": "A real consumer is required to apply zero-surcharge cuts to an admitted supplier.",
+      "first_step": "Identify one exact record and specify its read-only use at a batch cut.",
+      "blocked_by": "No such consumer is identified."
+    },
+    {
+      "question": "What is the exact minimum when completed partial echoes must be available at cuts?",
+      "why_it_matters": "That stronger observation can add source injections and restoration absent from canonical batch frames.",
+      "first_step": "Specify the stronger output contract for three children and one cut; price every injection and restoration.",
+      "blocked_by": "The stronger observed-output contract and permitted graph must be fixed."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133719",
+  "upstream_checkpoint": {
+    "commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+    "priority_revision": 7,
+    "checked_at": "2026-10-22T22:11:44Z"
+  },
+  "overlap": {
+    "open_pr_records": 379,
+    "discussion_records": 3852,
+    "local_notes_complete": false,
+    "matching_new_result_found": false,
+    "limitations": "Unpublished work and arbitrary code diffs are not covered. Distinctive main README and merged searches were also performed."
+  }
+}