From 5fb3936dfc8082f438f21c72dd6ca49ff4366ae7 Mon Sep 17 00:00:00 2001 From: Riquelme Soares <104222380+hevlyo@users.noreply.github.com> Date: Tue, 20 Oct 2026 09:09:04 -0300 Subject: [PATCH] Prove the exact F3 minimum for the one-source additive connector. Over F3 every correct word needs multiples of three B and A calls, so length at least 6, and exactly six length-6 words attain it. --- research/f3-additive-connector-1x1/README.md | 81 +++++++++++++++++++ .../f3-additive-connector-1x1/SOURCES.json | 24 ++++++ research/f3-additive-connector-1x1/TASK.json | 62 ++++++++++++++ .../f3-additive-connector-1x1/VERIFY.json | 18 +++++ research/f3-additive-connector-1x1/verify.py | 64 +++++++++++++++ 5 files changed, 249 insertions(+) create mode 100644 research/f3-additive-connector-1x1/README.md create mode 100644 research/f3-additive-connector-1x1/SOURCES.json create mode 100644 research/f3-additive-connector-1x1/TASK.json create mode 100644 research/f3-additive-connector-1x1/VERIFY.json create mode 100644 research/f3-additive-connector-1x1/verify.py diff --git a/research/f3-additive-connector-1x1/README.md b/research/f3-additive-connector-1x1/README.md new file mode 100644 index 0000000000..2370445689 --- /dev/null +++ b/research/f3-additive-connector-1x1/README.md @@ -0,0 +1,81 @@ +# Exact F3 minimum for the one-source additive connector + +**Scoped interface bound; no new kappa.** The selected record is unchanged. + +## Scope + +Chooser seed `04cbf2cbcf13a1a4ea434b5ef3acf93b` drew `connector-alphabet-change` +on priority revision 7, base `12fa8c5c844be21bfefb38a19503fbd867a11244`. +Live alphabet extensions already cover arity-four source events, joint +outputs, high-arity toggles and the direct product call. The starting +[universal-connector-boundary](../universal-connector-boundary/README.md) +README already states that ordinary addition in odd characteristic does not +inherit the F2 construction. This package keeps the same operators + +```text +B: z += x +A: y += z +``` + +and changes only that characteristic-two premise on the minimal one-source +one-output identity with arbitrary dirty `x`, `y` and `z`. + +## What is established + +Over F2 the word `BABA` meets every dirty input and restores `z`; no shorter +word in this alphabet does. Over F3 that word fails. + +Track the affine state + +```text +z = zx·x + zz·z0 +y = yx·x + yy·y0 + yz·z0 +``` + +with initial `(zx,zz,yx,yy,yz)=(0,1,0,1,0)`. Each `B` adds 1 to `zx`. Each `A` +adds the current `zz` to `yz`; `B` never changes `zz`, so `zz` stays 1 and +each `A` adds 1 to `yz`. A correct final state is `(0,1,1,1,0)`, so the number +of `B` calls and the number of `A` calls are each multiples of 3. Hence every +correct word has length at least 6. + +Over F3, with arbitrary dirty x, y and z, every correct word in the additive alphabet {B, A} for the one-source one-output identity has length at least 6, and length 6 is attained by exactly six words. + +An exhaustive enumeration finds no correct word of length at most 5 and +exactly these six length-6 witnesses, each with three `B` and three `A`: + +```text +BBAABA BABBAA BAABAB +ABBAAB ABABBA AABABB +``` + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/f3-additive-connector-1x1 +``` + +Expected marker: `PASS_F3_ADDITIVE_CONNECTOR_1X1`. + +## Limits + +This does not price a five-source F3 batch, signed patterns, nonlinear +readouts or a physical supplier. The predecessor package's full 945-pairing +replay was not run in this partial checkout. No selected-frontier change is +claimed. + +## Open next questions + +For the five-source all-31-mask batch over F3 with the same additive alphabet, +what is the exact optimum? The F2 optimum is 74. A first step is to search +restored words whose per-label counts are multiples of three, starting from a +short positive witness. No such witness is pinned here. + +## Credit + +The F2 alphabet and 1x1 four-call control come from +`research/universal-connector-boundary` and the later direct-call audit +lineage. The signed F3 connector of #1349 is a different interface and is not +replayed. Riquelme Soares (@hevlyo), with substantial AI assistance in the +search, bound and write-up. Apache-2.0. No independent human review is claimed. diff --git a/research/f3-additive-connector-1x1/SOURCES.json b/research/f3-additive-connector-1x1/SOURCES.json new file mode 100644 index 0000000000..43dd0d3ca1 --- /dev/null +++ b/research/f3-additive-connector-1x1/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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": "provenance", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ] +} diff --git a/research/f3-additive-connector-1x1/TASK.json b/research/f3-additive-connector-1x1/TASK.json new file mode 100644 index 0000000000..416986ee1e --- /dev/null +++ b/research/f3-additive-connector-1x1/TASK.json @@ -0,0 +1,62 @@ +{ + "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": "In the fixed additive alphabet {B: z += x, A: y += z}, what is the exact minimum complete-call length of the one-source one-output identity over F3 with arbitrary dirty x, y and z?", + "scope_change_reason": "The starting README already states that ordinary addition in odd characteristic does not inherit the F2 construction. Live alphabet-extension PRs already cover arity-four source events, joint outputs, high-arity toggles and the direct product call. This package keeps the same two operators and changes only the characteristic-two premise those extensions still rely on for dirt cancellation.", + "bottleneck_link": "Paired A readouts cancel connector dirt only because 1+1=0. In F3 that cancellation fails, so the inherited four-call 1x1 witness is not available and the recursive interface bill rises before any larger census.", + "budget_minutes": 60, + "stop_rule": "Stop at the exact 1x1 F3 minimum. Do not extend to five sources, signed patterns or a new operator family.", + "outcome": "completed", + "evidence": "Over F3 every correct word needs a multiple of three B calls and a multiple of three A calls, so length at least 6. An exhaustive search finds no correct word of length at most 5 and exactly six words of length 6, all with three B and three A: BBAABA, BABBAA, BAABAB, ABBAAB, ABABBA, AABABB. The F2 control BABA remains length 4.", + "author": "Riquelme Soares (@hevlyo)", + "ai_assistance": "Substantial AI assistance was used for the exhaustive search, the modular lower bound, the verifier and the write-up. No independent human review is claimed.", + "open_questions": [ + { + "question": "For the five-source all-31-mask batch over F3 with the same additive alphabet, what is the exact optimum?", + "why_it_matters": "The F2 optimum is 74. The 1x1 lift from 4 to 6 already shows a 50% local increase; the batch ratio is unknown.", + "first_step": "Search restored words with each of five B labels used a multiple of three times and each of 31 A labels used a multiple of three times, starting from a short positive witness.", + "blocked_by": "The search space is much larger than the 945 F2 pairings, and no F3 five-source witness is pinned here." + } + ] +} diff --git a/research/f3-additive-connector-1x1/VERIFY.json b/research/f3-additive-connector-1x1/VERIFY.json new file mode 100644 index 0000000000..78155481a0 --- /dev/null +++ b/research/f3-additive-connector-1x1/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Checks the F2 BABA control, the mod-3 B/A count lower bound, exhausts all words of length at most 5, and accepts exactly the six length-6 witnesses." + } + ] +} diff --git a/research/f3-additive-connector-1x1/verify.py b/research/f3-additive-connector-1x1/verify.py new file mode 100644 index 0000000000..6d6c2b2f9d --- /dev/null +++ b/research/f3-additive-connector-1x1/verify.py @@ -0,0 +1,64 @@ +"""Exact F3 minimum for the one-source one-output additive connector.""" + +from itertools import product +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +WITNESSES = ("BBAABA", "BABBAA", "BAABAB", "ABBAAB", "ABABBA", "AABABB") +LEMMA = ( + "Over F3, with arbitrary dirty x, y and z, every correct word in the " + "additive alphabet {B, A} for the one-source one-output identity has " + "length at least 6, and length 6 is attained by exactly six words." +) + + +def require(ok, why): + if not ok: + raise SystemExit(why) + + +def run(word, mod): + # z = zx*x + zz*z0; y = yx*x + yy*y0 + yz*z0 + zx, zz, yx, yy, yz = 0, 1, 0, 1, 0 + for op in word: + if op == "B": + zx = (zx + 1) % mod + elif op == "A": + yx = (yx + zx) % mod + yz = (yz + zz) % mod + else: + require(False, "unknown operator") + return zx, zz, yx, yy, yz + + +def correct(word, mod): + return run(word, mod) == (0, 1, 1, 1, 0) + + +def main(): + require(LEMMA in (PACKAGE / "README.md").read_text(encoding="utf-8"), "README dropped the lemma") + require(correct("BABA", 2), "F2 control BABA failed") + require(not correct("BABA", 3), "F2 witness must fail over F3") + + # Lower bound: B adds 1 to zx; A adds zz=1 to yz. Both finals need 0 mod 3. + require(min(b + a for b in range(3, 10, 3) for a in range(3, 10, 3)) == 6, + "count lower bound is not 6") + for length in range(1, 6): + for word in product("BA", repeat=length): + text = "".join(word) + require(not correct(text, 3), "unexpected short witness " + text) + + found = [] + for word in product("BA", repeat=6): + text = "".join(word) + if correct(text, 3): + found.append(text) + require(text.count("B") == 3 and text.count("A") == 3, "length-6 witness must use 3+3") + require(tuple(found) == WITNESSES, "witness list changed: " + repr(found)) + for text in WITNESSES: + require(correct(text, 3), "listed witness failed: " + text) + print("PASS_F3_ADDITIVE_CONNECTOR_1X1") + + +if __name__ == "__main__": + main()