Prove N(c) ≥ ⌊5c/2⌋ for the unsigned connector via five-source depth-two blocks in every c ≥ 5 (no new κ)

research/connector-five-halves-growth/CERTIFICATE.json

@@ -0,0 +1,46 @@
+{
+  "schema_version": 1,
+  "interface": "PR #4231 unsigned dirty connector; PR #4248 prefix criterion over Z/c",
+  "sources": 5,
+  "depth": 2,
+  "template_walk": [
+    0,
+    2,
+    1,
+    4,
+    3,
+    2,
+    0,
+    3,
+    1,
+    0,
+    4,
+    1,
+    4,
+    4,
+    2,
+    0,
+    3,
+    3,
+    1,
+    2,
+    4,
+    3,
+    1,
+    2,
+    0,
+    4,
+    3,
+    1,
+    2,
+    0
+  ],
+  "template_cut": [
+    3,
+    3,
+    2,
+    2,
+    3
+  ],
+  "template_rule": "For every c >= 5, replace the (template_cut[j]+1)-th event of source j by a run of c-5 copies of j; at c=5 that event is deleted."
+}

research/connector-five-halves-growth/README.md

@@ -0,0 +1,165 @@
+# Unsigned connector: a five-source depth-two block in every c ≥ 5, so N(c) ≥ ⌊5c/2⌋
+
+Take the unsigned dirty connector of
+[#4231](https://github.com/CrocSwap/integer-mult-bounds/pull/4231) over a ring
+of characteristic c, with k immutable sources and all 2^k − 1 nonzero
+binary-mask outputs. Every legal word needs at least c(k + 2^k − 1) complete
+calls. Let N(c) be the largest k at which that floor is attained.
+[#4248](https://github.com/CrocSwap/integer-mult-bounds/pull/4248) proved
+N(c) ≥ 2c for every c by concatenating depth-one two-source blocks. Its open
+question 2 asks how N(c) grows, and names a depth-d block with more than 2d
+sources, valid for every large c, as the way to raise the constant.
+[#4271](https://github.com/CrocSwap/integer-mult-bounds/pull/4271) showed that
+no five-source depth-two block exists at c = 4.
+
+This package shows:
+
+- **Theorem T** (proof, finite core checked): one explicit 30-event template
+  gives a five-source depth-two block in **every** characteristic c ≥ 5.
+- **Corollary** (proof): N(c) ≥ ⌊5c/2⌋ for every c ≥ 5. This improves 2c by
+  ⌊c/2⌋, for example N(5) ≥ 12, N(6) ≥ 15, N(7) ≥ 17 and N(8) ≥ 20.
+
+The claims are a scoped proof plus a finite certificate. There is no new κ,
+no consumer, no selected-frontier change and no multiplication theorem.
+Characteristic four is untouched: 9 ≤ N(4) ≤ 17 stands.
+
+## 1. Interface and depth
+
+The interface, prefix criterion and depth notion are #4248's. A floor word has
+a source walk w of length ck that uses each source exactly c times. Let
+q_t ∈ (Z/c)^k count source events modulo c after t steps. The word is correct
+exactly when every nonzero mask m has readout boundaries t_1 ≤ … ≤ t_c with
+q_(t_1) + … + q_(t_c) = m in (Z/c)^k. A walk has **depth d** if every
+nonzero mask is a sum of at most d prefixes. #4248's concatenation lemma joins
+walks on disjoint source sets whose depths sum to at most c into a floor walk;
+spare readouts go to boundary 0.
+
+## 2. Theorem T: the lifted template
+
+[CERTIFICATE.json](CERTIFICATE.json) gives the base walk on sources 0–4,
+each used six times,
+
+```text
+W = 0 2 1 4 3 2 0 3 1 0 4 1 4 4 2 0 3 3 1 2 4 3 1 2 0 4 3 1 2 0
+```
+
+and cut positions a = (3, 3, 2, 2, 3). Let n_t(j) be the number of events of
+source j among the first t events of W. Define the **lifted prefix**
+L_t ∈ Z^5 by L_t(j) = n_t(j) if n_t(j) ≤ a_j, and n_t(j) − 6 otherwise. So
+coordinate j runs 0, 1, …, a_j, then a_j − 5, …, −1, 0.
+
+**Template identity** (finite check). For every nonzero m ∈ {0,1}^5 there are
+base boundaries t_1 ≤ t_2 with L_(t_1) + L_(t_2) = m **as integer vectors**.
+The verifier finds a pair for all 31 masks.
+
+**Expansion.** For c ≥ 5, form W_c by replacing the (a_j + 1)-th event of each
+source j with a run of c − 5 copies of j. At c = 5 that event is deleted.
+Each source then occurs 6 − 1 + (c − 5) = c times.
+
+**Proof of Theorem T.** Let τ(t) be the boundary of W_c that follows the first
+t events of W (after the whole run, if event t is expanded). Count source j at
+τ(t). If n_t(j) ≤ a_j, the expanded event has not occurred and the count is
+n_t(j) = L_t(j). Otherwise it is n_t(j) − 1 + (c − 5) = n_t(j) + c − 6, which
+is L_t(j) modulo c. Hence q_(τ(t)) ≡ L_t (mod c). For a mask m with
+L_(t_1) + L_(t_2) = m in Z^5, reduction modulo c gives
+q_(τ(t_1)) + q_(τ(t_2)) = m. So W_c has depth two on five sources. ∎
+
+The argument needs c − 5 ≥ 0. It cannot reach c = 4, where #4271 excludes
+every five-source depth-two block.
+
+## 3. Corollary: N(c) ≥ ⌊5c/2⌋ for every c ≥ 5
+
+Concatenate ⌊c/2⌋ copies of W_c on disjoint five-source sets. For odd c,
+append #4248's depth-one block a b a^(c−1) b^(c−1) on two more sources. The
+total depth is at most c, so #4248's concatenation lemma gives a floor walk on
+5⌊c/2⌋ + 2(c mod 2) = ⌊5c/2⌋ sources. #4248's deletion lemma makes the
+attaining set an initial segment, so the floor is attained for every
+k ≤ ⌊5c/2⌋.
+
+| c | #4248: 2c | this package: ⌊5c/2⌋ | counting: first excluded k (#4248) |
+|---:|---:|---:|---:|
+| 5 | 10 | **12** | 30 |
+| 6 | 12 | **15** | 38 |
+| 7 | 14 | **17** | 47 |
+| 8 | 16 | **20** | 55 (#4255) |
+
+The counting column is #4248's and #4255's upper bound, quoted, not rechecked.
+
+## 4. What the verifier checks
+
+[verify.py](verify.py) uses only the standard library and takes about 2 s.
+
+1. The template identity for all 31 masks, with integer arithmetic.
+2. For every 5 ≤ c ≤ 64: W_c uses each source c times, every nonzero mask is
+   a sum of two prefixes modulo c by direct search, and each lifted readout
+   pair maps through τ to a correct readout. Item 1 is the only finite step the
+   proof needs; item 2 is a control.
+3. For c = 5, 6, 7: the concatenated floor walks on 12, 15 and 17 sources. It
+   builds the literal words of 20,535, 196,692 and 917,616 calls and simulates
+   them with generic coefficients over Z/c, following #4248's simulator. Every
+   output must equal its mask, the connector must return to its dirty value,
+   and every operator must be called exactly c times.
+4. Five mutation controls must be rejected: the unexpanded c = 6 block read in
+   characteristic seven, the c = 5 block read in characteristic four, every cut
+   moved one event later, three depth-two blocks at c = 5, and a floor word
+   with one readout call dropped.
+
+Expected marker:
+`PASS_CONNECTOR_FIVE_HALVES depth_two_k5_every_c>=5 N(c)>=floor(5c/2)`.
+It also prints a receipt hash bound to all six package files.
+
+## 5. Search notes (local only, not proofs)
+
+The template came from simulated annealing over 30-event base walks and cut
+vectors under the integer criterion. The same search with five events per
+source (cuts of a 25-event walk) peaked at 28 of 31 masks over 30 runs, which
+matches the c = 4 obstruction of #4271. Direct searches modulo c found
+depth-two five-source blocks at c = 5, 6, 7 and 8 separately. The search
+programs and logs are not committed.
+
+## 6. Reproduction
+
+From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/connector-five-halves-growth/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/connector-five-halves-growth
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/connector-five-halves-growth --check-source-history
+```
+
+## 7. Limitations
+
+The result covers only the unsigned, immutable-source, complete-call interface
+of #4231, and relies on #4248's prefix criterion, concatenation lemma and
+deletion lemma, which are cited and not re-derived. Theorem T is proved for
+every c ≥ 5; the direct block check runs for c ≤ 64 and the literal word
+simulation for c ≤ 7. Fixed call prices must include their full
+implementation. Input admission, coefficient preparation, dispatch and physical
+costs are additional and unknown. No consumer is instantiated. N(c) for c ≥ 5
+remains open between ⌊5c/2⌋ and the counting bound. Proof-kernel checks and
+independent human review are not claimed.
+
+## Open next questions
+
+These are recorded with first steps in [TASK.json](TASK.json).
+
+1. Does any characteristic admit a depth-two block on six or more sources?
+   One valid for all large c would give N(c) ≥ 3c. The lifted integer
+   criterion with more cut points per source is a direct first search.
+2. Is there a depth-three block on eight or more sources valid for every large
+   c? It would give density 8/3 > 5/2.
+3. Is N(c)/c unbounded? Counting gives O(c log c); this package gives ⌊5c/2⌋.
+4. Does any concrete consumer use a characteristic-c batch at a favorable
+   complete invoice? The abstract call counts change no supplier or κ.
+
+## Credit
+
+This package was produced by Nick Petalas. It builds on the interface and lower
+bound of #4231, the prefix criterion, depth notion, concatenation and deletion
+lemmas and N(c) ≥ 2c of #4248, the deletion lemma of
+[#4232](https://github.com/CrocSwap/integer-mult-bounds/pull/4232), the
+counting bounds of #4248 and
+[#4255](https://github.com/CrocSwap/integer-mult-bounds/pull/4255), and the
+c = 4 depth-two obstruction of #4271. The word builder and generic simulator
+in verify.py are adapted from research/connector-depth-blocks/verify.py.
+New work is Apache-2.0.

research/connector-five-halves-growth/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "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"
+    }
+  ]
+}

research/connector-five-halves-growth/TASK.json

@@ -0,0 +1,91 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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": "For the unsigned dirty connector of PR4231 over a ring of characteristic c, with N(c) the largest source count attaining the floor c(k+2^k-1), give one five-source depth-two walk template valid in every characteristic c>=5 and conclude N(c)>=floor(5c/2) for every c>=5 with PR4248's concatenation and deletion lemmas. Answers part of PR4248 open question 2 (growth of N(c)).",
+  "scope_change_reason": "Keeps the PR4231 alphabet and increases the source count, a scope-change trigger on the card. PR4248 asked how N(c) grows and named a depth-d block with more than 2d sources valid for every large c as the route; PR4271 excludes such a depth-two block at c=4 only.",
+  "bottleneck_link": "Side result on the complete-call interface floor: it raises the batch size at which a characteristic-c connector consumer can pay exactly c calls per operator. No physical consumer, admission or transfer is supplied, so no kappa change follows.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after one uniform depth-two five-source template with an all-c proof, direct checks over a finite range of c and literal floor words for small c. Report searches for larger blocks only as search notes.",
+  "outcome": "completed",
+  "evidence": "CERTIFICATE.json gives a 30-event base walk and per-source cut positions. verify.py checks the integer two-prefix identity for all 31 masks (the finite core of the all-c proof), checks the expanded block directly modulo c and through the lifted readouts for every 5<=c<=64, builds the concatenated floor walks on 12, 15 and 17 sources for c=5,6,7 and simulates the literal 20,535-, 196,692- and 917,616-call words with generic coefficients, and rejects five mutation controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does any characteristic c admit a depth-two block on six or more sources, or is five the maximum for every c?",
+      "why_it_matters": "A six-source depth-two block valid for all large c would raise the lower bound to N(c)>=3c.",
+      "first_step": "Run the same lifted integer criterion on six-source base walks with several cut positions per source, or extend PR4271's depth-two counting to general c.",
+      "blocked_by": "No search or upper bound for six-source depth-two blocks is recorded here."
+    },
+    {
+      "question": "Is there a depth-three block on eight or more sources valid for every large c?",
+      "why_it_matters": "Eight sources at depth three would give density 8/3 > 5/2 sources per readout.",
+      "first_step": "Search lifted base walks with seven or eight events per source under the integer three-prefix criterion.",
+      "blocked_by": "PR4248 reports a 125-of-127 search failure for seven sources at depth three in characteristic four only."
+    },
+    {
+      "question": "Is N(c)/c unbounded? Counting gives N(c)=O(c log c) and this package gives N(c)>=floor(5c/2).",
+      "why_it_matters": "It decides whether high-characteristic batches can stay at the floor with superlinear source counts.",
+      "first_step": "Look for a block family whose sources-per-depth ratio grows with depth, or a parity-type upper bound linear in c.",
+      "blocked_by": "No construction with ratio above 5/2 and no linear upper bound is known."
+    },
+    {
+      "question": "Does any concrete consumer use a characteristic-c batch at a favorable complete invoice?",
+      "why_it_matters": "The abstract call counts change no recursive supplier or kappa by themselves.",
+      "first_step": "Identify an immutable-source, unobserved-output caller with coefficients of characteristic c and price every primitive, admission and dispatch.",
+      "blocked_by": "No selected-supplier consumer is instantiated."
+    }
+  ],
+  "predecessor_handoff": {
+    "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4248",
+    "author": "Nick Petalas",
+    "usage": "Prefix criterion, depth and concatenation lemma, deletion lemma, N(c)>=2c and open question 2; word builder and generic simulation adapted from research/connector-depth-blocks/verify.py. No executable dependency."
+  },
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19230522",
+    "upstream_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+    "overlap_scope": "Open and merged PR searches for unsigned connector, N(c), depth-two block and connector floor walk; merged README grep for N(c) and N(4); last handoff comments and the batch claim list. Related packages: connector-depth-blocks (PR4248), connector-char4-floor-bounds (PR4255), connector-char4-floor-obstructions (PR4271), universal-connector-boundary (PR943), PR4231 and PR4232.",
+    "family_decision": "Local interface result; stop. No construction round is justified without a consumer."
+  }
+}

research/connector-five-halves-growth/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Integer two-prefix template identity for all 31 masks; expanded five-source depth-two blocks for every 5<=c<=64, directly and through the lifted readouts; literal floor words on 12, 15 and 17 sources for c=5,6,7 with generic coefficients; five rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Repeat every check under optimized Python; checks use explicit exceptions."
+    }
+  ]
+}