Bound the unsigned F3 connector floor for every source count: attained for n ≤ 6, impossible for n ≥ 14 (no new κ)

research/f3-n-source-connector-floor/CERTIFICATE.json

@@ -0,0 +1,19 @@
+{
+  "schema_version": 1,
+  "field": "F3",
+  "readout_rule": "three unsigned A_m readouts at source-path boundaries a<=b<=c, lexicographically first triple whose prefix-count sum mod 3 equals the binary mask of m",
+  "floor_paths": {
+    "1": [0, 0, 0],
+    "2": [0, 1, 1, 0, 1, 0],
+    "3": [1, 2, 2, 1, 1, 0, 2, 0, 0],
+    "4": [2, 3, 0, 2, 1, 2, 1, 3, 1, 0, 3, 0],
+    "5": [0, 1, 0, 2, 3, 1, 1, 4, 4, 2, 3, 4, 0, 3, 2],
+    "6": [0, 1, 2, 3, 1, 1, 3, 3, 2, 4, 2, 4, 4, 5, 0, 5, 5, 0]
+  },
+  "seven_source_upper": {
+    "path": [6, 0, 5, 5, 4, 0, 0, 3, 4, 4, 2, 3, 3, 1, 2, 2, 6, 1, 1, 5, 6],
+    "uncovered_triple_mask": 127,
+    "six_readout_boundaries": [0, 0, 1, 2, 8, 14],
+    "calls": 405
+  }
+}

research/f3-n-source-connector-floor/README.md

@@ -0,0 +1,156 @@
+# Unsigned F3 connector: the three-call floor for n sources
+
+For n immutable sources and all 2^n − 1 nonzero binary-mask outputs over F3,
+every legal word needs at least 3(n + 2^n − 1) complete calls. This package
+shows:
+
+- **Attained for n ≤ 6** (finite certificate): explicit restored source paths
+  give words of 6, 15, 30, 57, 108 and 207 calls, each operator called exactly
+  three times.
+- **Deletion lemma** (proof): if the floor is attained for n sources, it is
+  attained for n − 1. The attaining set is therefore an initial segment
+  {1, …, N}.
+- **Fails for every n ≥ 14** (proof): at most C(3n+3, 3) readout triples
+  exist, and C(45, 3) = 14,190 < 16,383 = 2^14 − 1.
+- **Seven sources, upper bound 405** (finite certificate): one 21-event path
+  serves 126 of 127 masks with three readouts; the all-ones mask takes six.
+  The seven-source optimum is 402 or 405.
+
+So 6 ≤ N ≤ 13. Whether N = 6 is open (see Open next questions). The claims are a
+scoped proof plus a finite certificate. There is no new κ, no selected-frontier
+change and no multiplication theorem.
+
+This extends the five-source result of
+[#4225](https://github.com/CrocSwap/integer-mult-bounds/pull/4225) (head
+`397025101d23195a5193c7912e6cd384eccdbf1c`) and the one-source alphabet and
+handoff of Riquelme Soares's
+[#4189](https://github.com/CrocSwap/integer-mult-bounds/pull/4189) (head
+`5fb3936dfc8082f438f21c72dd6ca49ff4366ae7`). The interface and the
+prefix-boundary readout criterion follow Ross Richardson's
+[#943](../universal-connector-boundary/README.md), whose characteristic-two floor
+fails at five sources.
+
+## 1. Interface
+
+The rows are n read-only sources x_j, 2^n − 1 outputs y_m and one borrowed dirty
+connector z. For arbitrary F3-linear maps B_j and A_m of compatible
+dimension, the word must implement
+
+```text
+y_m += sum_(j: bit_j(m)=1) A_m B_j x_j   for m = 1, ..., 2^n - 1;
+x_j and z unchanged.
+```
+
+The only calls are unsigned `B_j: z += B_j x_j` and `A_m: y_m += A_m z`, with
+the complete-call contract of #4225. Signed calls, extra connectors, scaling,
+source mutation, frame changes and free copies are not admitted. The maps may
+be singular and need not commute.
+
+## 2. Lower bound for every n
+
+This is #4225's argument applied to general n. Specialise to scalar identity
+maps. If B_j occurs b_j times, restoring z forces 3 | b_j. If A_m occurs a_m
+times, output m receives a_m·z0, so 3 | a_m. Every count is positive, so
+each is at least three and the total is at least 3(n + 2^n − 1). Every count is
+a multiple of three, so a word that misses the floor has at least
+3(n + 2^n − 1) + 3 calls.
+
+## 3. Floor words are source paths with triple readouts
+
+A floor word has a source path w of length 3n that uses each source three
+times. Let q_t ∈ F3^n count source events modulo three after t steps. Three
+A_m readouts at boundaries a ≤ b ≤ c add A_m(3z0 + Σ_j (q_a + q_b + q_c)_j
+B_j x_j). The word is correct exactly when every nonzero binary mask equals
+some q_a + q_b + q_c. Readouts at one boundary commute.
+
+**Window form.** For source j, let n2 and n3 count its events in the windows
+[a, b) and [b, c). Then (q_a + q_b + q_c)_j ≡ n3 − n2 (mod 3). Mask m is
+served when, for every j, n3 − n2 ≡ m_j and never ≡ 2.
+
+**Deletion lemma.** Remove the three events of source j from a floor path. Each
+old boundary maps to a new boundary with the same counts on the other sources.
+A mask with bit j zero keeps its triple, so every mask of the n − 1 remaining
+sources is served. The verifier checks all 20 single-source deletions of the
+certified paths as a control.
+
+**Counting.** A path of length 3n has 3n + 1 boundaries and C(3n+3, 3) readout
+triples with repetition. That number is at least 2^n − 1 for n ≤ 13
+(C(42, 3) = 11,480 ≥ 8,191) and smaller for n = 14. The deletion lemma extends
+the failure to all n ≥ 14. The verifier also checks the table directly up to
+n = 64.
+
+## 4. Certificate
+
+[CERTIFICATE.json](CERTIFICATE.json) lists one path for each n = 1..6. For
+example, the six-source path is
+
+```text
+0 1 2 3 1 1 3 3 2 4 2 4 4 5 0 5 5 0
+```
+
+The verifier regenerates the lexicographically first triple for every mask,
+builds the literal word, and simulates it with generic coefficients: z is held
+as a formal sum over z0 and the B_j x_j terms. Every output must receive
+exactly its mask row with no z0 term, and z must restore. This identity uses
+no commutation of A_m with B_j.
+
+For seven sources, the path
+
+```text
+6 0 5 5 4 0 0 3 4 4 2 3 3 1 2 2 6 1 1 5 6
+```
+
+serves all masks except 127 with three readouts. Mask 127 uses six readouts
+at boundaries (0, 0, 1, 2, 8, 14). The literal word has 21 + 3·126 + 6 = 405
+calls, the next multiple of three above the floor of 402.
+
+## 5. Search evidence for n = 7 (local only, not a proof)
+
+These runs are search failures, not exclusions. Simulated annealing over
+restored 21-event paths reached at most 126 of 127 masks in eight runs. For
+n = 8, 9 and 10 the best runs reached 224/255, 366/511 and 430/1023. A direct
+SAT encoding found floor paths for n = 5 and 6 in under a second. For n = 7 it
+did not finish within its time limit. These scripts and logs are not
+committed, and no unsatisfiability certificate exists.
+
+## 6. Reproduction
+
+From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/f3-n-source-connector-floor/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/f3-n-source-connector-floor
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/f3-n-source-connector-floor --check-source-history
+```
+
+Expected marker:
+`PASS_F3_N_SOURCE_CONNECTOR_FLOOR attained_n=1..6 counting_excludes_n>=14 n7_upper=405`.
+The verifier is standard-library only and prints a receipt hash bound to all
+six package files. Five mutation controls must be rejected: a dropped call,
+two doubled call counts, a relabelled source call, and a sorted four-source
+path that misses some masks.
+
+## 7. Limitations
+
+The result covers only the unsigned, immutable-source, complete-call interface
+over F3. Fixed call prices must include their full implementation. Input
+admission, coefficient preparation, dispatch and physical costs are additional
+and unknown. No consumer is instantiated. 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. Is the floor attained for n = 7, so that the seven-source optimum is 402
+   rather than 405? By the deletion lemma this decides whether N = 6.
+2. What is the exact optimum for each n ≥ 7 once the floor fails?
+3. Does any concrete consumer use an n-source unsigned F3 batch with a
+   favourable complete invoice?
+
+## Credit
+
+Produced by Nick Petalas. The F3 alphabet and one-source handoff are Riquelme
+Soares's #4189. The mod-three count argument and five-source word come from
+#4225. The connector interface and prefix-readout criterion come from Ross
+Richardson's #943. Apache-2.0.

research/f3-n-source-connector-floor/SOURCES.json

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

research/f3-n-source-connector-floor/TASK.json

@@ -0,0 +1,86 @@
+{
+  "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": "For every source count n, decide whether the unsigned F3 connector (n immutable sources, all 2^n-1 nonzero binary-mask outputs, one arbitrarily dirty restored connector) attains the per-operator floor of three calls per operator, 3(n+2^n-1) calls.",
+  "scope_change_reason": "Keeps the F3 alphabet of PR4189/PR4225 and increases the source count, which the card lists as a scope-change trigger. It decides whether the F3 alphabet's three-per-operator price survives for larger batches, the premise any larger-batch F3 consumer would rely on. The F2 analogue of PR943 loses its floor at five sources.",
+  "bottleneck_link": "Bounds the batch size at which an F3 connector consumer can pay exactly three calls per operator. No physical consumer, admission or transfer is supplied, so no kappa change follows.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after floor words for n<=6, the counting exclusion for n>=14, the deletion lemma and one explicit seven-source upper bound. Exact status of n=7..13 is left open; solver and local-search runs are reported as search failures only.",
+  "outcome": "completed",
+  "evidence": "CERTIFICATE.json supplies restored source paths for n=1..6 and a 21-event seven-source path. verify.py regenerates every readout triple, simulates the literal words with generic noncommuting coefficients, checks the deletion lemma on all 20 single-source deletions, the counting table for n<=64 and five rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is the three-per-operator floor attained for n=7, i.e. is the seven-source optimum 402 or 405 calls?",
+      "why_it_matters": "By the deletion lemma this single case decides whether the attaining set is exactly n<=6; otherwise the threshold lies between 7 and 13.",
+      "first_step": "Run an exhaustive or proof-producing search over restored 21-event paths up to source relabelling, using the window form of README section 3 and a checked UNSAT certificate.",
+      "blocked_by": "A plain SAT encoding did not finish within its time limit; no checkable unsatisfiability proof exists yet."
+    },
+    {
+      "question": "What is the exact optimum for each n>=7 once the floor fails?",
+      "why_it_matters": "A consumer of a large F3 batch needs the exact surcharge, not only that it is positive.",
+      "first_step": "Lower-bound the number of masks realizable by three readouts on a path with S source events, then trade longer source paths against six-readout outputs.",
+      "blocked_by": "No lower bound beyond the next multiple of three is proved here."
+    },
+    {
+      "question": "Does a concrete consumer use an n-source unsigned F3 batch with 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 and price all n+2^n-1 complete primitives, admission and dispatch.",
+      "blocked_by": "No selected-supplier consumer is instantiated."
+    }
+  ],
+  "predecessor_handoff": {
+    "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4225",
+    "head": "397025101d23195a5193c7912e6cd384eccdbf1c",
+    "author": "Nick Petalas",
+    "usage": "Five-source result and mod-three count argument; extended here to every n. No executable dependency."
+  },
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19080529",
+    "upstream_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+    "overlap_scope": "100 live open PR titles, 60 recent account PRs, last 30 handoff comments, find_overlap helper over 340 open PRs and 2971 discussion records. Only PR4189 (n=1) and PR4225 (n=5) study unsigned F3 connectors. Closed work and arbitrary diffs are incompletely covered.",
+    "family_decision": "Local interface result; stop. No construction round is justified without a consumer."
+  }
+}

research/f3-n-source-connector-floor/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": 30,
+      "checks": "Floor words n=1..6, generic coefficient simulation, 20 deletion-lemma checks, counting table n<=64, seven-source 405-call word and five rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Repeat every check under optimized Python; checks use explicit exceptions."
+    }
+  ]
+}