Attain the depth-four chain connector floor 4m for every 33 ≤ m ≤ 64, via an exact row model (no new κ)

research/depth4-chain-rowmodel/README.md

@@ -0,0 +1,186 @@
+# Depth-four chain connector: a row model and the 4m minimum for 33 <= m <= 64
+
+This package extends open question 1 of
+[#4263](https://github.com/CrocSwap/integer-mult-bounds/pull/4263) from
+characteristic 32 to characteristic 64. The contribution was produced by Nick
+Petalas.
+
+The complete calls are `z_l += B_l z_{l-1}` for l = 1, 2, 3, 4, with x = z_0
+immutable and z_1, z_2, z_3 and y = z_4 holding arbitrary dirty data. The maps
+are arbitrary and the coefficients lie in a nonzero unital ring of exact
+characteristic m. For a nonzero residue c the word must restore z_1, z_2 and
+z_3 and add `c B4 B3 B2 B1 x` to y. There are no sign or inverse calls.
+
+```text
+shortest length = 4m   for every 33 <= m <= 64 and every c != 0 (mod m)
+```
+
+| m | 2 | 3 | 4 | 5 | 6 to 32 | 33 to 64 |
+|---|---:|---:|---:|---:|---:|---:|
+| shortest length | 12 | 18 | 20 | 25 | 4m | 4m |
+| source | #4249 | #4249 | #4249 | #4249 | #4263 | this package |
+
+The new results are:
+
+1. **Finite certificate.** One witness for each of the 1,520 pairs (m, c) with
+   33 <= m <= 64 and 1 <= c < m, each using every call exactly m times.
+2. **Scoped proof (Lemma 2).** An exact criterion for a balanced word in terms
+   of a partition and two monotone profiles. It holds for every m and is what
+   makes the witnesses compact and quick to find.
+3. **Scoped proof (Lemma 3).** For prime m, the partition needs at least three
+   rows strictly between 0 and m.
+
+With #4249 and #4263, which are open and not rechecked here, the depth-four
+minimum is known exactly for 2 <= m <= 64. No all-m theorem, no new κ, no
+supplier admission and no change to the selected frontier.
+
+## Argument
+
+**Lemma 1 (floor; #4249).** A word is correct for c iff every scattered
+subword count N[i..j] of i(i+1)...j is 0 mod m, except N[1..4], which is c mod
+m. So each call appears a positive multiple of m times, and every correct word
+has at least 4m calls. A word with exactly m copies of each call is *balanced*.
+
+**Lemma 2 (row model).** Call 1 commutes with calls 3 and 4, and call 4 with
+calls 1 and 2. So a balanced word is fixed, up to its action, by three objects:
+
+- the subword of calls 2 and 3. Let f(p) be the number of calls 2 before the
+  p-th call 3. The cells above this lattice path form a partition λ in the
+  m × m box: column p has height m − f(p). Write ℓ(q) for its row lengths,
+  q = 1..m, top row first.
+- the levels of the calls 1. A call 1 with a calls 2 before it has row level
+  r = m − a. Let ρ(q) be the number of calls 1 with r >= q.
+- the levels of the calls 4. A call 4 with b calls 3 before it has level b.
+  Let β(p) be the number of calls 4 with b >= p, and B(L) = β(1) + ... + β(L).
+
+Conversely, every partition λ in the box and every pair of nonincreasing
+profiles ρ, β with values in [0, m] come from a balanced word. The word is
+correct for c iff
+
+```text
+(i)   Σ_q ℓ(q)        ≡ 0        (iv)  Σ_q ρ(q) ℓ(q)     ≡ 0
+(ii)  Σ_q ρ(q)        ≡ 0        (v)   Σ_q B(ℓ(q))       ≡ 0
+(iii) Σ_p β(p)        ≡ 0        (vi)  Σ_q ρ(q) B(ℓ(q))  ≡ −c      (mod m)
+```
+
+*Proof.* Count each interval by the calls that complete it. N[2..3] = Σ f(p) =
+m² − |λ|. A call 1 at level a precedes m − a calls 2, so N[1..2] = Σ ρ(q), and
+N[3..4] = Σ b = Σ β(p). For N[1..3], N[2..4] and N[1..4] use
+
+```text
+Σ_{p <= b} (f(p) − a)^+ = b (m − a) − C(m − a, b),
+```
+
+where C(r, b) is the number of cells of λ in rows 1..r and columns 1..b. This
+holds because column p has (m − a) − (f(p) − a)^+ cells in rows 1..m − a.
+Summing over the calls gives N[1..3] = m N[1..2] − Σ ρ(q) ℓ(q),
+N[2..4] = m N[3..4] − Σ B(ℓ(q)) and N[1..4] = N[1..2] N[3..4] − Σ ρ(q) B(ℓ(q)).
+Reduce mod m. ∎
+
+A row of length m drops out of (i), (iv), (v) and (vi) once (iii) holds. It
+contributes only to (ii). So each witness here has one full row, used to settle
+(ii), and three to five rows strictly between 0 and m. The witnesses store
+(λ, ρ, β) directly.
+
+**Lemma 3 (two short rows are not enough for prime m).** Let m be prime. If λ
+has at most two rows with 0 < ℓ < m, every correct word has c ≡ 0.
+
+*Proof.* Rows of length 0 and m drop out of (i), (iv), (v) and (vi). One short
+row contradicts (i). Two short rows ℓ_1 >= ℓ_2 must satisfy ℓ_1 + ℓ_2 = m. Then
+(iv) reads (ρ_1 − ρ_2) ℓ_1 ≡ 0. Since ℓ_1 is a unit, ρ_1 ≡ ρ_2, and (vi) becomes
+ρ_1 (B(ℓ_1) + B(ℓ_2)) ≡ 0 by (v). ∎
+
+### What did not give an all-m law
+
+A uniform family was looked for and not found. These local searches are not
+part of the package:
+
+- Designs whose block lengths are all small constants or m minus small
+  constants, with at most four blocks per letter in the 2/3 path and up to three
+  levels each for calls 1 and 4, gave no witness that works for the same c at
+  m = 101, 103 and 107.
+- One full row, three short rows, ρ = 0 on the last short row, and calls 4 at
+  one level b plus filler at level 1, covers only some residues: none at m = 7
+  and m = 8, and 5 of the 10 nonzero residues at m = 11.
+- The constraint that blocks a simple parametric proof is the budget: ρ(1) and
+  the number of calls 4 must stay at most m while (ii) and (iii) hold.
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth4-chain-rowmodel/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/depth4-chain-rowmodel/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/depth4-chain-rowmodel
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/depth4-chain-rowmodel --check-source-history
+```
+
+Any CPython 3.12 can replace the local interpreter path. The verifier writes no
+files and runs in about a second. It prints a JSON receipt with the SHA-256 of
+every package file and input, then
+`PASS_DEPTH4_CHAIN_ROWMODEL moduli=32 witnesses=1520`. It checks:
+
+- For every witness: the shapes of λ, ρ and β, the five vanishing sums of
+  Lemma 2 and the predicted coefficient c.
+- The word built from the record: length 4m and exactly m copies of each call,
+  the interval conditions of Lemma 1 by one counting pass, and separately the
+  UT5(Z/m) product I + c e_{1,5}.
+- One literal replay per witness with dirty registers in (Z/m)^2 and random
+  2x2 maps, which generally do not commute. It checks that z_1, z_2 and z_3 are
+  restored and y gains exactly c B4 B3 B2 B1 x.
+- Lemma 2 on 4,000 random records with 2 <= m <= 9: the sums decide
+  correctness exactly as direct counting does, and give the same c when the
+  word is correct. Lemma 3 on random records with two short rows and prime m.
+- Five rejection controls on the witness for (m, c) = (37, 5): a wrong
+  coefficient, a changed ρ(1), a shortened row, a moved call-4 level and a
+  dropped call.
+
+The witnesses were found by a randomized solver in the row model: draw the
+short rows and the call-4 level, keep draws that satisfy (i) and (v), and solve
+(iv) and (vi) for the top two values of ρ. The solver is not part of the
+package. The verifier checks the records and the words themselves, so it does
+not matter how they were found.
+
+## Limitations
+
+The certificate covers only 33 <= m <= 64. It is a finite certificate per
+(m, c), not an all-m theorem. The values for m <= 32 come from #4249 and #4263
+and are not rechecked here. Lemmas 2 and 3 are proved in this README and only
+spot-checked by the verifier. Independent human and formal proof-kernel review
+are unclaimed. Every call carries its complete implementation price.
+Admission, dispatch, routing of the three intermediates and word-dependent
+physical costs are extra. No supplier caller, precision analysis, outer
+multiplication theorem or new κ is supplied.
+
+## Open next questions
+
+The structured questions in [TASK.json](TASK.json) give first steps and
+blockers.
+
+1. Is the depth-four minimum exactly 4m for every m >= 6? Lemma 2 turns this
+   into a question about one partition and two profiles. A parametric choice of
+   four short rows, ρ and β that keeps ρ(1) <= m and at most m calls 4 for
+   every c would settle it.
+2. Is three short rows enough for every prime m >= 7? Lemma 3 shows two are
+   not. 436 of the 1,520 witnesses here use three.
+3. Does a row model of the same kind describe depth five, with two interior
+   paths, and give the floor 5m there?
+
+## Attribution and scope
+
+The chain model, the interval-count reduction, the floor and the m <= 5
+depth-four minima come from
+[#4249](https://github.com/CrocSwap/integer-mult-bounds/pull/4249). The
+witnesses for 6 <= m <= 32 and the three-interleaving lemma come from
+[#4263](https://github.com/CrocSwap/integer-mult-bounds/pull/4263). Ross
+Richardson's [#943/#934 lineage](../universal-connector-boundary/README.md)
+supplies the complete-call dirty-connector interface. The new results here are
+the row model of Lemma 2, Lemma 3 and the 1,520 witnesses for 33 <= m <= 64.
+Subword counts, unitriangular matrices and lattice-path partitions are
+classical tools; no novelty is claimed for them. Exact pins are in
+[SOURCES.json](SOURCES.json).
+
+The `connector-alphabet-change` card is explicitly changed to this side
+question, as in #4249 and #4263. The alphabet stays unsigned and complete.
+Apache-2.0.

research/depth4-chain-rowmodel/SOURCES.json

@@ -0,0 +1,38 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/universal-connector-boundary/README.md",
+      "usage": "input",
+      "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f",
+      "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476"
+    }
+  ],
+  "context_only": [
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4263",
+      "head_commit": "2183322b32a5975ecb4a6aec2ec8f43ac08b1aec",
+      "credit": "Nick Petalas",
+      "role": "Depth-four minimum 4m for 6 <= m <= 32 by explicit witnesses, Lemma 2 (three interleavings) and the recorded failed uniform families. Its open question 1 is extended here to 33 <= m <= 64; no executable dependency."
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4249",
+      "head_commit": "03b8a19d7442edebb3565064631f6ca2408d731e",
+      "credit": "Nick Petalas",
+      "role": "Chain model, interval-count reduction, the 4m floor, and the depth-four minima 12, 18, 20, 25 at m = 2..5; no executable dependency."
+    }
+  ]
+}

research/depth4-chain-rowmodel/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Extend the exact minimum of the unsigned depth-four dirty chain connector z_l += B_l z_{l-1} (l = 1..4, z_0 = x immutable, z_1..z_3 and y = z_4 dirty) over characteristic m from 6 <= m <= 32 (PR #4263) to 33 <= m <= 64: the per-call floor 4m is attained for every nonzero residue c, by explicit witnesses. Also prove an exact row-model criterion for balanced words (README Lemma 2) and that prime m needs at least three short rows (Lemma 3).",
+  "scope_change_reason": "The card asks about one extension of the connector alphabet. This package keeps the unsigned complete-call alphabet and the one-source depth-four chain of PRs #4249 and #4263, and continues open question 1 of #4263. It does not extend a source-count census or claim a supplier improvement.",
+  "bottleneck_link": "A recursive boundary that routes through three dirty intermediates pays this call count. The small-characteristic premium of #4249 (m <= 5) stays absent through m = 64. Side result: no consumer, paid profile or kappa change is supplied.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after explicit witnesses for every (m, c) in a bounded range with literal dirty replay and source-bound publication checks. A uniform all-m family was searched for part of the session and not found; no all-m theorem is claimed.",
+  "outcome": "completed",
+  "evidence": "witnesses.json stores one row-model record (lambda, rho, beta) for each of the 1,520 pairs (m, c), 33 <= m <= 64, 1 <= c < m. verify.py checks the Lemma 2 sums of each record, builds the word and checks it has exactly m copies of each call, the interval subword counts, the UT5(Z/m) product and one literal dirty replay with random noncommuting 2x2 maps; it spot-checks Lemmas 2 and 3 on random records, runs five rejection controls and prints a receipt with package and input SHA-256 values. The 4m floor is Lemma 1 (from #4249).",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is the depth-four minimum exactly 4m for every m >= 6?",
+      "why_it_matters": "It would make the depth-four premium a small-characteristic effect, m <= 5 only.",
+      "first_step": "In the row model of README Lemma 2, fix one full row and four short rows with lengths that are linear in m, and look for rho and beta profiles linear in c that keep rho(1) <= m and at most m calls 4.",
+      "blocked_by": "The uniform small-constant designs and the three-short-row family tried here fail; the binding constraint is the budget on rho(1) and on the number of calls 4."
+    },
+    {
+      "question": "Are three short rows enough for every prime m >= 7?",
+      "why_it_matters": "Lemma 3 shows two are not; a positive answer would give the smallest row-model witnesses for prime m.",
+      "first_step": "Search the row model with exactly three short rows and general rho and beta for primes 7 to 61.",
+      "blocked_by": "Only the restricted three-row family (rho = 0 on the last short row, calls 4 at one level plus filler) was searched; it is incomplete at m = 7 and 11."
+    },
+    {
+      "question": "Does a row model of the same kind describe depth five and give the floor 5m there?",
+      "why_it_matters": "It would carry the compact witness format to longer dirty chains.",
+      "first_step": "Write the depth-five word as calls 1 and 5 inserted into a 2/3/4 word and express N[1..5] through that word's prefix and suffix counts.",
+      "blocked_by": "No depth-five reduction was attempted here."
+    }
+  ]
+}

research/depth4-chain-rowmodel/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/universal-connector-boundary/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Every row-model witness for 33 <= m <= 64 and 1 <= c < m: the Lemma 2 sums, then the built word (exactly m copies of each call, interval subword counts, UT5(Z/m) product, one literal dirty noncommuting replay); Lemma 2 and Lemma 3 on random records; five rejection controls; source hashes."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "The same checks with Python assertions disabled; all contracts use explicit exceptions."
+    }
+  ]
+}