Prove sharp 7TP table travel for skew-radix cached chirps (no new κ)

research/chirp-radix-order/PROOF.md

@@ -0,0 +1,135 @@
+# Largest-radix-first cached chirp table movement
+
+This is a scoped written proof. It concerns the sequential table tape of
+Ryanson Jonathan's PR #4325 suffix-product chirp enumerator, with a changed
+axis layout. It does not audit that package or Cinna Davis's PR #4100.
+
+## Contract
+
+There are d >= 1 axes of dyadic lengths t_0,...,t_(d-1), each at least two,
+and T is their product. The tape contains the tables in that order. Each
+entry occupies P >= 1 consecutive cells. Table k starts at
+O_k = P sum_(i<k) t_i. The table head starts at zero.
+
+The mixed-radix counter enumerates axis zero fastest. At the first record,
+read entry zero of tables d-1,...,0 to fill the suffix-product cache. At a
+later record, if the carry stops at axis j, read the new entries of tables
+j,j-1,...,0 and recompute those suffix products. To read an entry, move to
+its first cell and sweep forward P cells. After the final record, return
+the table head to cell zero. All table contents are read-only.
+
+Cache arithmetic, cache-tape actions, the counter and payload are separate
+from this table-head metric. Products of exact phases commute, so the
+cache returns the same phase at each named coordinate after an axis
+permutation. Finite-precision multiplication need not commute or associate
+exactly; a rounded service must use its stated error contract.
+
+## Exact movement identity
+
+Write L_k = product_(i<k) t_i, so L_0=1 and L_d=T.
+For the full enumeration including setup and final return, table movement is
+
+```
+Q/P = 2 t_0
+      + 2 sum_(k=0)^(d-2) (t_k+1) T/L_(k+1)
+      +   sum_(j=1)^(d-1) (t_j-1) T/L_j.                 (1)
+```
+
+Empty sums are zero. This identity in fact requires only integer t_i >= 2.
+
+To prove it, first omit the final return. The last table read is the final
+entry of table zero, so the final head is t_0 P. If B is the total backward
+distance in units of P, the total distance before return is t_0 P+2BP.
+Returning adds another t_0 P.
+
+For each k < d-1, the reverse table traversal crosses from table k+1 to
+entry zero of table k exactly T/L_(k+1) times, including initialization.
+Its baseline backward distance is t_k+1. If the carry stops at j=k+1,
+the newly read entry of table j has index b in 1,...,t_j-1, so this one
+crossing has an additional backward distance b. Each such b occurs
+T/L_(j+1) times. Thus
+
+```
+B = sum_(k=0)^(d-2) (t_k+1) T/L_(k+1)
+    + sum_(j=1)^(d-1) [t_j(t_j-1)/2] T/L_(j+1).
+```
+
+Substitution proves (1). Every forward sweep, initial seek and final
+return is included; counting only the distance between entry starts would
+give a different identity.
+
+## Sharp uniform bound after choosing a fastest axis
+
+Choose any largest radix M as t_0. The remaining axes can stay in their
+relative order. Then
+
+```
+Q <= 7 T P.                                            (2)
+```
+
+No bound on max(t_i)/min(t_i) is needed. For d=1, Q=2TP.
+For d>=2 put b=2^(-(d-1)). Since t_i>=2 and t_i<=M,
+
+```
+2M/T <= 2b,
+2 sum_(k=0)^(d-2) (t_k+1)/L_(k+1)
+  = 2 sum_(k=0)^(d-2) (1+1/t_k)/L_k
+ <= 2 + 2/M + (6/M)(1-2b),
+sum_(j=1)^(d-1) (t_j-1)/L_j
+ <= (2-2/M)(1-b).
+```
+
+The middle sum over k>=1 is empty when d=2, and the displayed bound then
+has 1-2b=0. Adding gives the explicit stronger estimate
+
+```
+Q/(TP) <= 4 + 6/M - 10b/M <= 7,
+```
+
+because M>=2 and b>0. This proves (2).
+
+The constant seven cannot be decreased uniformly in d. With every t_i=2,
+(1) gives the exact formula
+
+```
+Q/P = 7*2^d - 10,
+Q/(TP) = 7 - 10/2^d.
+```
+
+It approaches seven from below. This is sharpness of one specified table
+schedule, not an optimality theorem over every possible tape algorithm.
+
+## First application and boundary
+
+On the skew two-axis layout (2,512), (1) gives Q=264708P. Choosing the
+512-axis fastest gives (512,2) and Q=3078P, with T=1024. The latter is
+1539/512 emitted word volumes. Both counts include the table-head return.
+PR #4325's displayed 258.5 ratio omits that final return and rounds the
+ratio; the metrics should not be silently mixed.
+
+The exact phase at an original named coordinate x is the product of the
+same one-axis factors in either order. The new enumeration emits those
+coordinates in the new order. A consumer must already accept that order,
+or separately pay for layout conversion. This proof supplies no free
+transpose, physical encoded controller, table construction, cache cleanup,
+multiplier implementation, supplier admission or new kappa.
+
+## Executable scope
+
+The independent literal counter executes every table read and carry. The
+closed-form implementation never calls that counter. Complete small
+dyadic domains compare both, and a separate exact quadratic-exponent cache
+checks the association of emitted phases with original axis names. The
+binary family is checked through 64 axes by exact arithmetic. The written
+argument, rather than that finite range, proves the all-size assertion.
+
+Executable inputs have at most 64 axes, radices at most 65536, word width
+at most 64 and product bit length at most 1025. Literal enumerations are
+capped at 131072 records; phase checks at 4096. These are verifier resource
+bounds. All loops have finite bounds, and all contracts remain enabled
+under optimized Python. Functions are below 60 lines. There is no recursion,
+dynamic loading, network, or write path. Python's managed integer, JSON and
+dictionary allocations are a Power-of-Ten rule-3 deviation, bounded by the
+input and fixture limits. Standard-library iterator and key callbacks have
+fixed targets and no shared mutable state. Warning-strict execution is the
+available interpreted diagnostic; no global analyzer configuration changes.

research/chirp-radix-order/README.md

@@ -0,0 +1,64 @@
+# Sharp table travel for skew-radix cached chirps
+
+Choosing a largest radix as the fastest axis gives table-head movement
+`Q <= 7TP` for the complete cached chirp enumeration, including initialization
+and the final return to cell zero. Here `T` is the number of tensor records
+and each table entry has `P` cells. There is no largest/smallest radix-ratio
+restriction. The constant seven is sharp for this specified schedule: with
+`d` binary axes, `Q/P = 7*2^d - 10`.
+
+On the two-axis layout `(2,512)`, the exact closed table walk costs
+`264708P`. Putting the 512-axis first costs `3078P`, with the same 1024
+records. This is a count of unit head moves, not a timing measurement.
+
+Claim type: scoped written mathematical proof with exact finite
+corroboration. [PROOF.md](PROOF.md) gives the exact movement identity,
+its all-size bound, sharpness family and physical boundary. No new kappa
+or selected-frontier change is claimed.
+
+## Reproduction
+
+From the repository root, CPython 3.12 and the standard library suffice:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/chirp-radix-order/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/chirp-radix-order
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/chirp-radix-order --check-source-history
+```
+
+The standalone verifier prints `PASS_CHIRP_RADIX_ORDER` with exact counts
+and SHA256 hashes of all six package files. It compares a literal complete
+table walker with a separately implemented closed formula, checks the sharp
+binary family through 64 axes, and executes exact quadratic-phase caches
+against direct values at every original named coordinate in five fixtures.
+The registered replay runs both normal and optimized warning-strict checks.
+No predecessor executable or numerical certificate is replayed.
+
+## Scope and credit
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Ryanson Jonathan, `pinterbanget`, supplies the sequential table layout and
+suffix-product cache model in [PR #4325](https://github.com/CrocSwap/integer-mult-bounds/pull/4325),
+retained as [pr4100-chirp-odometer-tariff](../pr4100-chirp-odometer-tariff/README.md).
+Cinna Davis supplies the underlying chirp construction in PR #4100 and
+Douglas Colkitt the retained compact-control ancestry. Their results and
+notices are unchanged. The predecessor's balanced-radix travel and rounding
+results are cited premises. The new result is the exact closed table-walk
+identity and sharp uniform bound after changing the fastest axis.
+
+The bound covers table-head movement only. Counter and cache actions,
+arithmetic, setup, cleanup and allocation remain separately chargeable.
+The phase stream is exact symbolic arithmetic; no rounded-word equality is
+asserted. A physical consumer must accept the changed named-coordinate
+order or pay for its conversion. No free transpose, encoded controller,
+complete multiplier or discharge of the five selected assumptions is supplied.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+Can an actual chirp consumer use the largest-radix-fastest payload order
+without an extra full transpose? Start by writing the complete input/output
+layout and movement bill for one real caller. The missing physical producer
+and consumer, rather than this table-movement estimate, are the blocker.
+The structured question is in [TASK.json](TASK.json).

research/chirp-radix-order/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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"
+    },
+    {
+      "path": "research/pr4100-chirp-odometer-tariff/README.md",
+      "usage": "input",
+      "git_blob": "c0f8b2a006965074c38484964d05f0a9cc1f3008",
+      "sha256": "6ed0793017d3c84003b0c7921c7b9598b868c48f05e46b8c0a88c52cfb843ff5"
+    }
+  ]
+}

research/chirp-radix-order/TASK.json

@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "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"
+    ],
+    "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "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": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "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": "Scoped all-size proof of the sharp table-tape movement bound Q <= 7TP for a largest-radix-first cached chirp enumerator, without a radix-ratio restriction; exact travel formula and independent finite counter.",
+  "scope_change_reason": "The selected card concerns the five selected-caller assumptions. This is a side result on a changed layout in the PR4325/PR4100 chirp interface, not admission of a selected assumption or an audit of the predecessor.",
+  "bottleneck_link": "Side result for precision_tape: arbitrary radix skew need not cause superlinear cached phase table movement when the caller supplies a largest-axis-fastest layout. Layout conversion and the other physical charges remain open.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified sharp uniform table-movement improvement; do not optimize further axis orders or extend to a complete supplier.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the exact movement identity, uniform constant seven and sharp binary family. verify.py independently executes complete table walks and exact named-coordinate phase streams and emits a receipt bound to package file hashes.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual chirp consumer accept a largest-radix-fastest payload layout without an added full transpose?",
+      "why_it_matters": "The movement saving is useful only after the physical payload order is funded.",
+      "first_step": "Specify one original payload layout and its complete changed producer/consumer order, including all data movement.",
+      "blocked_by": "No physical layout conversion or consumer is supplied by this table-only theorem."
+    }
+  ]
+}

research/chirp-radix-order/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/pr4100-chirp-odometer-tariff/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact closed travel identity against literal complete table walks; sharp binary family; named-coordinate quadratic chirps; rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same scientific checks with optimized Python and active runtime contracts."
+    }
+  ]
+}