Show the short-field movement does not tighten the Strassen boundary …

research/pr4100-row-field-ledger/PROOF.md

@@ -0,0 +1,127 @@
+# Short-field movement sits above the Strassen boundary row
+
+Scoped substitution for one open question of
+`research/pr4100-row-field-movement`. No new κ. #4100 is not accepted.
+The selected record is unchanged.
+
+## What is substituted
+
+Lemma 3 of that package says that exposing one field of length `a ≥ 1`
+and real volume `V` moves strictly fewer than
+
+```text
+8 · max(1, ceil(log2 a)) · V
+```
+
+records on the forward-plus-undo schedule. The #4100 boundary sentence
+already charges
+
+```text
+O(V d W^(tau-1)/B polylog(p)),    tau = 45/16,
+```
+
+and the same paragraph's union movement is
+
+```text
+O(V d W/B polylog(p)).
+```
+
+PHASE-LAYOUT charges the layout itself as `O(log p)` times the boundary
+volume, not a transpose of the long spectator field. The open question
+was whether that count becomes the Strassen sentence only after the
+exposed length is set equal to the carving parameters `W` and `B`.
+
+## Pinned lengths
+
+Two lengths are named. Neither is the equality `a = W` or `a = B`.
+
+- FINE-PRIME.md and GAUSSIAN.md set `W = O(sqrt(p) polylog p)`. The
+  boundary-row field in PHASE-LAYOUT is that polynomial-width row, so
+  this reading has `a = O(p^{1/2} polylog p)`.
+- If the exposed field is instead the whole carved line, CAPPED-SIGNOFF
+  gives `|E_i| = O(L W/B polylog p + W polylog p)`, and GAUSSIAN.md sets
+  `L = 2^{ceil(400 log2 p)}`. Then `a` is still `p^{O(1)}`.
+
+In both readings `ceil(log2 a) = O(log p)`. Lemma 3 therefore multiplies
+the volume it actually exposes by a polylogarithmic factor. It does not
+change a `W` power.
+
+The volume it exposes is the boundary volume. GAUSSIAN.md gives that set
+density `O(W/B polylog(p))`, and FINE-PRIME.md §6 keeps the cost power
+`epsilon - xi + (tau-1)/2` because the density is still `W/B`. UNION-SCHEDULE
+records the same density as `mu = O((W/B) polylog p)`.
+
+## Exponent comparison
+
+FINE-PRIME.md §6–§7 uses one dictionary. A term
+
+```text
+O(V (d/B) W^alpha polylog p)
+```
+
+has cost power `epsilon - xi + alpha/2` and saving
+`1 - epsilon + xi - alpha/2`, because the worst-case bandwidth in that
+section satisfies `log_p W = 1/2`. That is why the printed union row
+(`alpha = 1`) has saving `xi + 1/2 - epsilon`, and the printed Strassen
+row (`alpha = tau - 1`) has saving `c + xi - epsilon` with
+`c = (3 - tau)/2`.
+
+Lemma 3, on the boundary volume, is the `alpha = 1` shape: the extra
+`ceil(log2 a)` factor is inside the polylog already written on the union
+sentence `O(V d W/B polylog(p))`. Its saving exceeds the Strassen saving by
+
+```text
+(xi + 1/2 - epsilon) - (c + xi - epsilon) = 1/2 - c = (tau - 2)/2.
+```
+
+The difference does not depend on `epsilon` or `xi`. For the stated
+`tau = 45/16`, one has `c = 3/32` and
+
+```text
+1/2 - 3/32 = 13/32.
+```
+
+`W = O(sqrt(p) polylog p)` contributes `o(1)` beyond the printed `1/2`,
+because `(log p)^k = p^{o(1)}`. A constant gap of `13/32` stays positive
+for all large `p`. This note does not compute that finite threshold; an
+explicit density constant would be needed for one. A separate movement
+row would still save `13/32 - o(1)` more than the Strassen boundary row,
+so it does not become the minimum. At the explicit §7 balance
+(`s = 10^{-64}`, boundary saving `= epsilon q + s`), the printed-power
+movement saving is that boundary saving plus `13/32`.
+
+The same arithmetic gives the monomial comparison used by the big-O.
+For every integer `W ≥ 1`,
+
+```text
+W^{29} ≥ W^{16},
+```
+
+so `W^{29/16} ≥ W`, and `W^{tau-1} ≥ W` at `tau = 45/16`. A movement of
+shape `K V (d/B) W (log p)^k` is at most `K (log p)^k` times the monomial
+inside `O(V d W^{tau-1}/B polylog p)`. The layout factor is absorbed by
+the polylog of the boundary sentence. It is not necessary to set `a`
+equal to `W` or to `B`.
+
+For the other printed exponent `tau_eff = 2 + 10^{-64}`, the same
+difference is `(tau_eff - 2)/2 = 5 · 10^{-65} > 0`, and `W^{tau_eff-1} ≥ W`
+for every integer `W ≥ 1`. Absorption holds for that exponent too. Which
+of the two exponents the ledger should state is a separate question.
+
+## The density is necessary
+
+If Lemma 3 were charged on the full tensor volume instead of the boundary
+volume, the `W/B` factor would drop out and the saving would fall to
+`1 - epsilon`. At the §7 parameters `epsilon = 9999999/10000000`, that
+saving is strictly smaller than the headline `epsilon q`. The boundary
+density is what keeps the movement off the binding row. The proof does
+not rerun the carving program that produces the density; it uses the
+density #4100 already writes.
+
+## Not proved
+
+This note does not prove the Strassen count, the seven-product circuit,
+conditioning, the row gap, or the choice between `tau = 45/16` and
+`tau_eff`. It does not replay the dyadic carving. It does not accept
+#4100 or change the selected exponent. The `O` constants inside the
+written density are not replaced by explicit integers.

research/pr4100-row-field-ledger/README.md

@@ -0,0 +1,95 @@
+# Short-field movement does not tighten the Strassen boundary row
+
+**Scoped exponent comparison. No new κ.** #4100 is not accepted, and the
+selected conditional result stays `0.00302015`.
+
+## Scope and evidence
+
+Card `uniform-transfer-audit`, scope **refined** to one substitution left
+open by the boundary-arithmetic layout lemma. That lemma bounds one exposed
+field by `8 max(1, ceil(log2 a))` times its real volume. #4100 already
+writes the Strassen boundary cost
+
+```text
+O(V d W^(tau-1)/B polylog(p)),    tau = 45/16,
+```
+
+and the union movement `O(V d W/B polylog(p))`. This package compares those
+two shapes after the layout factor is included. It does not replay the
+carving program.
+
+[PROOF.md](PROOF.md) records the argument. In the exponent dictionary of
+FINE-PRIME.md §6–§7, a term `O(V (d/B) W^alpha polylog p)` has saving
+`1 - epsilon + xi - alpha/2`. The layout movement is the `alpha = 1` shape,
+because `ceil(log2 a) = O(log p)` for both named lengths: the
+polynomial-width boundary row, using `W = O(sqrt(p) polylog p)`, and the
+carved line `|E_i| = O(L W/B polylog p + W polylog p)` with
+`L = 2^{ceil(400 log2 p)}`. Its saving exceeds the Strassen saving by
+
+```text
+1/2 - (3 - tau)/2 = 13/32
+```
+
+at `tau = 45/16`. The difference does not depend on `epsilon` or `xi`.
+The printed `1/2` is the worst-case `log_p W`; a polylogarithmic factor
+in `W` adds only `o(1)`, which does not close `13/32` for large `p`.
+For every integer `W ≥ 1`, `W^{29} ≥ W^{16}`, so
+`W^{tau-1} ≥ W` and the movement monomial is absorbed by the boundary
+big-O. The exposed length is not set equal to `W` or to `B`.
+
+The same gap is `5 · 10^{-65}` at the other printed exponent
+`tau_eff = 2 + 10^{-64}`. Both exponents absorb the movement. Choosing
+which exponent the ledger states is left open.
+
+Charging the same logarithm on the full tensor volume, dropping the
+written density `O(W/B polylog p)`, would leave saving `1 - epsilon`.
+At the §7 parameters that quantity is strictly below the headline
+`epsilon q`. The density is what keeps this charge off the binding row.
+
+`verify.py` recomputes the rational identities, the integer bandwidth
+comparison for `W = 1..256` and two larger widths, the named core-length
+logarithm, and the two rejecting controls (`tau = 2` is not strict;
+`tau = 7/4` makes movement the heavier row; the full-volume charge
+undercuts the headline).
+
+## Reproduce
+
+From the repository root, on CPython 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/pr4100-row-field-ledger --check-only
+python3.12 -B scripts/research_package.py --package research/pr4100-row-field-ledger
+```
+
+The registered command is `verify.py`. It uses the standard library and
+reads the pinned prose inputs. Expected first line:
+
+```text
+PASS_ROW_FIELD_LEDGER tau=45/16 c=3/32 movement_minus_boundary_saving=13/32 gap_independent_of_epsilon_and_xi=true integer_bandwidth_absorbed=true tau_eff_gap=5e-65 full_volume_charge_binds=true boundary_volume_charge_binds=false exposed_length_equals_W_or_B=false selected_decimal=0.00302015 no_new_kappa=true
+```
+
+## Open next questions
+
+1. **Choose the boundary exponent.** GAUSSIAN.md uses `tau = 45/16` for the
+   seven-product paragraph, while UNION-SCHEDULE §4 uses
+   `tau_eff = 2 + 10^{-64}`. Both absorb this movement. The ledger row
+   still has to name one of them before the layout lemma is copied in as
+   a numeric coefficient. First compare those two sentences with the
+   generated ledger at head `337d04939571a637aeab54a0f58f54fde811663a`.
+   Blocked here because that ledger is a different program.
+2. **Extract the density constant.** The `O(W/B polylog p)` factor is used
+   as written. An explicit `C` such that `mu ≤ C (W/B) (log p)^k` would
+   turn the `13/32` gap into a finite-`p` inequality. First pin `C` and
+   `k` from the carving proof, not from another asymptotic sentence.
+
+## Credit
+
+The boundary and union sentences are Cinna Davis's #4100. The layout lemma
+is `research/pr4100-row-field-movement` (unpaidmoon). The exponent table is
+FINE-PRIME.md §6–§7, and the carved-line bound is CAPPED-SIGNOFF.md. The
+coverage map that listed the row-field movement as unaudited is PR #4311
+(Ryanson Jonathan). PR #4376 proved the layout count and left this
+substitution open.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+No independent human review and no formal-kernel acceptance are claimed.

research/pr4100-row-field-ledger/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "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/capped-phase-fusion/CAPPED-SIGNOFF.md",
+      "usage": "input",
+      "git_blob": "fc3456387b9399c8108db75b46088f85c5c26f82",
+      "sha256": "70e9175ebde200f8b016236adc88c4a1c4858945e7c3e5c453a8b6a5f79a263a"
+    },
+    {
+      "path": "research/capped-phase-fusion/PHASE-LAYOUT-AUDIT.md",
+      "usage": "input",
+      "git_blob": "bbeeee7431720817f031360f67b2186abac5cd23",
+      "sha256": "54aafc7afd09fe1a5312e69fad09c87422690543ab75c6ae35f6cbcc26b3eb8a"
+    },
+    {
+      "path": "research/pr4100-row-field-movement/PROOF.md",
+      "usage": "input",
+      "git_blob": "8cb9097d216677e218c5e59d9d6e7e77801e8727",
+      "sha256": "9b20f66269383535d20f1f0a762710a393ea036471a9383b7dafc07db341d02b"
+    },
+    {
+      "path": "research/unconditional-batched-crt/GAUSSIAN.md",
+      "usage": "input",
+      "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b",
+      "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242"
+    },
+    {
+      "path": "research/unconditional-batched-crt/vendor/FINE-PRIME.md",
+      "usage": "input",
+      "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3",
+      "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce"
+    },
+    {
+      "path": "research/unconditional-batched-crt/vendor/UNION-SCHEDULE.md",
+      "usage": "input",
+      "git_blob": "b5eb03e6745804f465a536fc9ffa87c2515d1bfa",
+      "sha256": "aabb28c343bcb9697a4cac7058060132617073df17ee18e591d2bf4defe9e921"
+    }
+  ]
+}

research/pr4100-row-field-ledger/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "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_status": "refined",
+  "actual_scope": "Substitute the proved short-field move count into #4100's Strassen boundary cost O(V d W^(tau-1)/B polylog p) at tau=45/16, using the written boundary density, and decide whether that charge tightens the boundary row.",
+  "scope_change_reason": "PR #4376 proved the layout count and left the ledger substitution open. The coverage map listed the row-field movement as unaudited obligation 3; this package answers that obligation's first remaining question and does not reopen the move-count proof.",
+  "bottleneck_link": "Side result for the #4100 admission audit: the layout movement does not undercut the Strassen boundary row, so it is not a new obstruction to the proposed exponent. It does not move the selected frontier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the exponent comparison and the integer absorption check. Do not choose between tau=45/16 and tau_eff, and do not replay the carving program.",
+  "outcome": "completed",
+  "evidence": "PROOF.md derives the 13/32 saving gap. verify.py checks the rational identities, the integer bandwidth comparison, the source sentences, and the full-volume rejecting control.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance.",
+  "open_questions": [
+    {
+      "question": "Which printed boundary exponent, tau=45/16 or tau_eff=2+10^{-64}, does the #4100 ledger use when the layout lemma is copied in?",
+      "why_it_matters": "Both absorb this movement, but the numeric boundary row still has to name one exponent.",
+      "first_step": "Compare GAUSSIAN.md's seven-product sentence with UNION-SCHEDULE section 4 against the generated ledger at head 337d04939571a637aeab54a0f58f54fde811663a.",
+      "blocked_by": "The generated ledger is a different program and is not replayed here."
+    },
+    {
+      "question": "What explicit C and k satisfy mu <= C (W/B) (log p)^k in the carving proof?",
+      "why_it_matters": "An explicit constant would turn the 13/32 exponent gap into a finite-p inequality.",
+      "first_step": "Pin C and k from the carving argument rather than from another asymptotic sentence.",
+      "blocked_by": "The carving program is not replayed here; the written O bound is the input."
+    }
+  ]
+}

research/pr4100-row-field-ledger/VERIFY.json

@@ -0,0 +1,25 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/capped-phase-fusion/CAPPED-SIGNOFF.md",
+    "research/capped-phase-fusion/PHASE-LAYOUT-AUDIT.md",
+    "research/pr4100-row-field-movement/PROOF.md",
+    "research/unconditional-batched-crt/GAUSSIAN.md",
+    "research/unconditional-batched-crt/vendor/FINE-PRIME.md",
+    "research/unconditional-batched-crt/vendor/UNION-SCHEDULE.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact 13/32 saving gap at tau=45/16; integer check W^(tau-1) >= W; tau_eff gap; full-volume charge undercuts the headline; source-sentence binding; rejection controls for tau=2 and tau=7/4."
+    }
+  ]
+}