Prove exact seven-call minima for 360 Dic3 targets (no new κ)

research/dicyclic-six-call-boundary/README.md

@@ -0,0 +1,186 @@
+# No six-call diagonal sharing in the positive Dic3 alphabet
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+A complete exact search excludes every word of at most six paid calls for
+all **890** three-register diagonal targets whose separate positive-generator
+bill is at least seven. In particular, all **360** targets with separate bill
+seven have exact minimum **seven**. This is a finite certificate for the
+specified formal operation model, not a complete multiplication theorem.
+No new kappa or selected-frontier change is claimed.
+
+This answers the explicit six-call Open next question of Cinna Davis's
+[PR #2069](https://github.com/CrocSwap/integer-mult-bounds/pull/2069),
+[retained package](../bit-dicyclic-diagonal-seed620ca/README.md).
+Its depth-four/five exclusions and earlier state inventory remain credited
+predecessor results. The new deliverable is the complete six-call join and
+the exact seven-call endpoint family. No predecessor executable, state table,
+receipt or unmerged source object is consumed by the new verifier.
+
+## Complete operation model
+
+Let
+
+```
+G = Dic3 = <u,v | u^6=1, v^2=u^3, vuv^-1=u^-1>.
+A = F2[G].
+```
+
+Use exactly three arbitrary dirty registers. A paid call is
+
+```
+D_N(g) = I + ([g]+[1]) N,
+g in {u,v}, N=x y^T, x,y in F2^3, y^T x=1.
+```
+
+All 28 binary rank-one idempotents are permitted, giving 56 operations.
+Every call costs one. Only positive u and v are paid labels. Their inverses
+are algebraic devices in the join, never additional available calls.
+No free address maps, endpoint translations, copies, erasures, clean inputs
+or extra registers are allowed. The full endpoint must be
+`diag([a],[b],[c])` coefficient by coefficient in `M3(A)`.
+Off-diagonal couplings must vanish. A dirty spectator is represented by an
+identity target; its entrance is arbitrary and must return unchanged.
+
+The result also holds if scalar GL3(F2) changes are free between calls.
+They conjugate N to another permitted rank-one idempotent and can be moved
+to one end. Augmentation `[g] -> 1` sends every paid factor and the diagonal
+endpoint to I, so the net scalar factor must be I. This is the predecessor's
+normalization argument, not a claim that arbitrary address changes are free.
+
+Write group elements in order `u^i v^j`, indexed `i+6j`, with `0<=i<6`
+and `0<=j<2`. The shortest positive distances in that order are
+
+```
+0,1,2,2,3,4,1,2,3,3,3,2.
+```
+
+For example, `diag([u^5],[u^2],[u])` has separate bill `4+2+1=7`
+and exact minimum seven. A positive spelling of u^5 is `u u v v`.
+
+## Why the finite search proves the result
+
+Every group-algebra entry is its exact 12-bit coefficient vector. A matrix
+has nine such entries. Hashes select buckets only; state equality compares
+all nine coefficient vectors, so hash collisions cannot merge unequal states.
+
+Construct S, the complete set of products of zero through three calls.
+Breadth-first expansion uses every one of the 56 factors from each newly
+reached state. The numbers of new states are `1,56,2352,92318`, giving
+`|S|=94727`. Keeping one shortest representative preserves every continuation:
+future multiplication depends only on its full matrix, and replacing a
+prefix by a shorter representative cannot exceed the depth limit.
+A separate raw three-loop check covers all `56^3=175616` ordered triples
+and verifies membership in S. All one- and two-call products are checked too.
+These checks support the completeness argument; the new mathematical question
+is the six-call endpoint layer, not the predecessor's inventory count.
+
+Every word of length at most six splits into P Q with both factors in S.
+Each paid factor is invertible, with
+
+```
+D_N(g)^-1 = I + ([g^-1]+[1]) N.
+```
+
+The implementation retains P^-1 and checks `P P^-1=I` by literal formal
+matrix multiplication for every stored state. For a diagonal target T,
+`P Q=T` is equivalent to `Q=P^-1 T`. Column j of P^-1 is therefore
+right-multiplied by its target monomial. The join examines every P and checks
+exact membership of this required Q in S. No symmetry restriction, cut
+relaxation, probabilistic equality or pruning predicate removes candidates.
+
+The independent Python permutation model derives the distances and enumerates
+the complete `12^3` endpoint domain. The distance-counting polynomial is
+`1+2x+4x^2+4x^3+x^4`; its cube independently agrees with the endpoint histogram.
+Exactly 890 targets have bill at least seven. Every one of their 94,727
+prefix lookups is negative, for **84,307,030** lookups in total.
+
+For bill exactly seven, the independent model executes all 360 coordinate
+words. They give literal diagonal formal endpoints, touch no other register,
+and require no cleanup. Their seven-call upper bounds and the exhaustive
+six-call exclusion establish exact minimum seven. All 2,520 single-call
+omissions change the required endpoint.
+
+## Replay and evidence
+
+Use CPython 3.12 and a C++17 compiler. The verifier has no Python dependencies,
+Git dependency or network dependency. CXX may name a different compiler
+executable. From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/dicyclic-six-call-boundary/verify.py --controls
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/dicyclic-six-call-boundary/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dicyclic-six-call-boundary
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dicyclic-six-call-boundary --check-source-history
+```
+
+Substitute another CPython 3.12 path on another machine. Compilation and
+execution use a temporary directory and leave no build products in the package.
+Set TMPDIR to keep temporary files under a chosen scratch directory.
+Successful direct replay prints `PASS_DICYCLIC_SIX_CALL_BOUNDARY` and a generated
+JSON receipt binding every package file by SHA256. `--receipt PATH` saves that
+receipt outside the package. It is never hand-written or required as an input.
+
+Eight positive joins include all direct lengths zero through six and a
+noncommuting heterogeneous target. Native controls compare fast updates and
+inverse updates with literal matrix multiplication on all 3,136 gate pairs,
+and check every retained inverse. Disposable native mutations remove a whole
+inventory depth, destroy the join key, and corrupt the required endpoint.
+Each must fail at its corresponding raw-coverage or positive-join check.
+The Python model uses explicit permutations, rather than the native
+normal-form multiplication formula, for distances and coordinate witnesses.
+
+The complete source history, task card and predecessor README/TASK are
+bibliographic provenance in SOURCES.json. No external scientific input is
+required to execute the verifier. The source-bound selected-baseline metadata
+orientation passed; it is not counted as a scientific replay.
+
+## Scope, implementation limits and credit
+
+This is a complete finite exclusion and exact finite endpoint family, not
+an all-group or arbitrary-register no-sharing theorem. For targets with
+separate bill eight through twelve, it supplies only the lower bound seven.
+The cited #2069 result excludes earlier sharing layers; combined with it,
+any first sharing word in this model has at least seven calls. That combined
+statement retains #2069 as a premise and is not its independent revalidation.
+
+Physical native realization, address/compiler routing, source ownership,
+precision, stock, complete recursive costs and a multiplication theorem are
+unresolved. No Lean, Docker or selected scientific replay was run. Independent
+human and formal proof-kernel review are unclaimed.
+
+The implementation uses no recursion. All mathematical loops have fixed
+bounds of at most 12 group elements, 56 gates, three inventory depths, 178,809
+raw words, 1,728 endpoints and 94,727 stored prefixes. Native functions remain
+below 60 physical lines. Compiler diagnostics use warning-as-error settings.
+Python exceptions keep scientific checks enabled under optimization.
+Managed Python allocation and native unordered-map node allocation are explicit
+fixed-allocation deviations: collection counts are bounded by those finite
+limits, native matrices contain nine 12-bit masks, and the native state vector
+reserves the complete raw-word capacity before expansion. Compiler/process
+calls have 120-second timeouts and temporary resources have scoped cleanup.
+No claim of adversarial compiler containment is made.
+
+Credit Cinna Davis / 1337isnot1337 for #2069's group, alphabet, normalized
+register model, earlier exclusions and explicit six-call question. Credit
+David Govea / davidgovea #720, eumemic #288 and the retained scalar-idempotent
+register-model lineage for the broader framework. Their original files and
+credit lines are unchanged. The new search and exact seven-call family were
+produced by Nick Petalas. Ordinary finite-group and meet-in-the-middle methods
+are classical; no literature-priority claim is intended.
+
+## Open next questions
+
+- Does a seven-call word realize any target with separate bill at least eight?
+  First price one concrete target and derive a structural restriction on its
+  factor words. A depth-four inventory is substantially larger, and no such
+  expansion was run or reserved here. The finite six-call exclusion does not
+  settle that next layer.
+- Can a uniform algebraic invariant replace the finite six-call join?
+  Start with the exact seven-call example above and a named representation;
+  the invariant must charge both positive labels and preserve arbitrary dirt.
+  A nonfaithful represented endpoint alone cannot certify a construction.
+
+These are mathematical side questions. Physical supplier development requires
+a concrete native consumer and a complete paid budget before another
+construction round. TASK.json records their relevance, first steps and blockers.

research/dicyclic-six-call-boundary/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "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/bit-dicyclic-diagonal-seed620ca/README.md",
+      "usage": "provenance",
+      "git_blob": "e7ff43a5e27c9eda993a5f47fedb714393cb9e83",
+      "sha256": "4c66cbf5712d6556c2d1ba33065217175a740f7e8e9a75ef806051e8b2935a90"
+    },
+    {
+      "path": "research/bit-dicyclic-diagonal-seed620ca/TASK.json",
+      "usage": "provenance",
+      "git_blob": "e06934ce905544fd192cd3dcc329337635168014",
+      "sha256": "5aecf38ed85cf40b564f81ad2e5c319d7cf775663b6042f7bb0b8dabd294b9d6"
+    },
+    {
+      "path": "research/bit-three-register-lower-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79",
+      "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"
+    }
+  ]
+}

research/dicyclic-six-call-boundary/TASK.json

@@ -0,0 +1,70 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Decide the complete six-call layer of the positive Dic3 three-register formal group-algebra model, and give exact seven-call minima for its direct-bill-seven targets.",
+  "scope_change_reason": "Take the explicitly open six-call question from Cinna Davis #2069. This is a finite algebraic side result outside the abelian model, with no supplier or kappa claim.",
+  "bottleneck_link": "Tests whether a nonabelian positive alphabet can combine paid diagonal work across arbitrary dirty registers. A finite identity or exclusion alone does not implement the selected bit interface.",
+  "budget_minutes": 60,
+  "stop_rule": "Complete the six-call join and its controls, then package the first result without enlarging depth, group or register count.",
+  "outcome": "negative-result",
+  "evidence": "All 890 targets of separate bill at least seven have no word of at most six calls; 84,307,030 exact joins over 94,727 complete prefix states. All 360 direct-bill-seven targets have exact minimum seven.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does a seven-call sharing word exist for a target of direct bill at least eight?",
+      "why_it_matters": "It is the next possible unresolved sharing layer in the named finite model.",
+      "first_step": "Price one target and derive a structural word restriction before considering a depth-four inventory.",
+      "blocked_by": "No depth-four inventory or physical supplier contract is supplied."
+    },
+    {
+      "question": "Can an algebraic invariant prove the six-call exclusion uniformly?",
+      "why_it_matters": "It could replace a finite search and indicate which hypothesis enables sharing.",
+      "first_step": "Test a named representation on diag([u^5],[u^2],[u]) with both positive labels priced.",
+      "blocked_by": "Any invariant must preserve arbitrary dirt and cannot accept only a quotient endpoint."
+    }
+  ]
+}

research/dicyclic-six-call-boundary/VERIFY.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py",
+        "--controls"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Complete six-call exclusion, exact seven-call family, literal permutation model, raw coverage, eight positive joins and three rejecting native mutations."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Optimized complete replay with scientific checks still enabled."
+    }
+  ]
+}