Prove exact eight-call tariff for four inverse C3 targets (no κ)

research/c3-four-inverse-tariff/PROOF.md

@@ -0,0 +1,98 @@
+# Four inverse cyclic targets need eight calls
+
+This scoped proof was produced by Nick Petalas. New work is Apache-2.0.
+
+Let A=F2[g]/(g^3+1), the full formal group algebra F2[C3]. There are
+exactly four scalar roles, each with arbitrary dirty input in A. The paid
+alphabet consists of
+
+    D_N(g) = I + (1+g) N,
+    N = u v^T over F2, v^T u = 1.
+
+Each call costs one. Any binary invertible scalar matrix is free. The
+required complete endpoint is T=g^2 I_4. No extra role, clean allocation,
+erasure, free g^2 call or free address operation is allowed.
+
+**Theorem.** The minimum paid-call count is eight.
+
+## Remove free scalar bridges
+
+For any S in GL_4(F2), conjugation sends D_N(g) to D_(SNS^-1)(g).
+Move every scalar bridge to one endpoint, conjugating the intervening
+couplings. Augmentation g=1 sends every paid factor to I and sends T to I.
+Thus the remaining scalar endpoint factor is I. This reduces every program
+to a product of paid factors with the same count and legal binary couplings.
+It accounts for arbitrary interleaved scalar changes, not only a fixed basis.
+
+## Only five calls could improve on eight
+
+Write F4=F2[w]/(w^2+w+1). Specialize g to w. Put d=1+w=w^2. Each paid
+factor is I+dN and has determinant w, since N is a rank-one idempotent.
+The target is w^2 I_4 and has determinant w^8=w^2. A k-call word therefore
+requires k=2 modulo 3. Also rank(T-I)=4 in F4. Telescoping a product of k
+rank-one increments bounds rank(T-I) by k. Among k<8, only k=5 survives.
+These are necessary conditions on a formal identity; specialization is not
+used as a sufficient formal-endpoint test in the proof.
+
+## A product with four independent update directions
+
+Consider four factors F_i=I+d u_i v_i^T with binary u_i,v_i and v_i^T u_i=1,
+in chronological order i=1,2,3,4. If rank(F_4 F_3 F_2 F_1-I)=4, their four
+image vectors u_i are independent. Indeed the image of the product minus I
+lies in span_F4(u_1,u_2,u_3,u_4), by telescoping left updates. Binary vectors
+are independent over F4 exactly when they are independent over F2.
+
+Conjugate by the binary matrix with columns u_1,...,u_4. Each factor now
+updates only row i, and its binary row functional a_i has a_ii=1. Let L
+and U be the strict lower and strict upper parts of the binary matrix with
+rows a_i. If M is the final product, its i-th row satisfies
+
+    M_i = e_i^T + d (sum_(j<i) a_ij M_j + sum_(j>=i) a_ij e_j^T).
+
+Earlier rows already have their final values; later rows are still their
+identity rows. Consequently
+
+    (I+d L) M = I+d(I+U).                              (1)
+
+This is a row-once identity for the stated four factors. It does not assume
+that their functionals or projectors commute.
+
+Suppose, in addition, M=d I+P with P binary. Substitute in (1), use
+w^2=w+1 and d^2=w, and compare the coefficients of 1 and w. They give
+
+    I+P+LP = U,
+        L+LP = U.
+
+Subtracting gives P=I+L. A strict lower triangular L makes I+L invertible.
+Thus such a four-factor product requires rank_F2(P)=4. In particular it
+cannot have rank(P)=1.
+
+## Exclude five calls
+
+Assume F_4 F_3 F_2 F_1 F_0 = d I, with five legal paid factors after
+specialization. Since F_0^-1=I+w N_0, removing the chronological first
+factor gives
+
+    F_4 F_3 F_2 F_1 = (d I)(I+w N_0) = d I+N_0.       (2)
+
+The right side minus I is w I+N_0. It is invertible: on im(N_0) it is
+multiplication by w+1, and on ker(N_0) by w. Both scalars are nonzero.
+The preceding four-direction lemma applies. Its binary basis change sends
+N_0 to a binary rank-one projector P, while leaving d I fixed. Equation
+(2) would therefore require rank(P)=4. This contradicts rank(P)=1.
+Five calls are impossible, completing the lower bound.
+
+## Attainment and scope
+
+On each coordinate role apply its coordinate projector twice. This is eight
+positive-g calls and gives g^2 on that role, hence T exactly in the full
+formal algebra. All four input columns remain arbitrary. There are no
+spectators to restore and no auxiliary input is silently set to zero.
+
+The argument proves this four-role tariff only. In a larger register space
+the target with restored spectators is no longer a scalar matrix. Removing
+the first factor then need not leave the full-rank four-direction situation
+above. No lower bound with extra roles is claimed. Additional paid labels,
+nonbinary scalar coefficients and different endpoints also need new analysis.
+No native, physical or recursive supplier cost follows from the formal count.
+Independent human and formal proof-kernel review are unclaimed.

research/c3-four-inverse-tariff/README.md

@@ -0,0 +1,122 @@
+# Four inverse C3 targets have exact eight-call cost
+
+Four copies of the inverse of a single order-three label cannot share a
+saving in the stated binary register model. The endpoint
+`diag(g^2,g^2,g^2,g^2)` in the full formal algebra `F2[C3]` needs exactly
+**eight positive-g rank-one idempotent calls**, even with free interleaved
+`GL_4(F2)` scalar mixing and arbitrary dirty inputs on all four roles.
+
+Claim type: scoped algebraic proof with exact finite corroboration. This is
+an original changed-alphabet side result for `bit-new-register-model`.
+It supplies no new kappa or selected-frontier change.
+
+[PROOF.md](PROOF.md) proves the lower bound without enumeration. Rank and
+determinant reduce every possible saving to five calls. Remove the first
+factor. The remaining four updates have independent binary image directions,
+so each changes one row exactly once in their image basis. Comparing the two
+F4 coefficients in that triangular factorization would force a rank-one
+projector to have rank four. Eight coordinate calls attain the endpoint in
+the full group ring.
+
+## Exact evidence and reproduction
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/c3-four-inverse-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/c3-four-inverse-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/c3-four-inverse-tariff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/c3-four-inverse-tariff --check-source-history
+```
+
+Another CPython 3.12 installation can replace the absolute interpreter path.
+Expected scientific output is `PASS_C3_FOUR_INVERSE_TARIFF minimum=8
+five_call_hits=0`. The runner also prints `PASS_REGISTERED_RESEARCH_PACKAGE`.
+The committed-byte check requires a publication commit and full Git history.
+
+The read-only verifier performs two exact meet-in-the-middle exclusions.
+Scalarity of the target permits simultaneous binary conjugation of the
+chronological first coupling to E00. Each remaining four-factor word splits
+into two products of length at most two. The F4 packed-row engine and a
+separate full F2[C3] coefficient-convolution engine each enumerate 8,361
+distinct such products and test all 8,361 complements. Both find zero hits.
+Full-ring augmentation and F4 together are also checked to distinguish all
+eight group-ring elements. Product representatives are safe because only
+the complete product affects a later factor; no sampling is used.
+
+Additional checks enumerate all 65,536 binary four-by-four matrices to confirm
+the complete 120-projector inventory, construct a normalization basis for
+each projector, and check all 4,096 row-once binary functional choices in
+the proof's factorization identity. The eight-call witness passes every
+formal coefficient and all twelve faithful regular-action dirty-input columns.
+All eight single-call omissions reject. Six controls include positive identity,
+one-call and five-call joins, nilpotent rejection and order-three identities.
+All acceptance checks remain active with Python optimization enabled.
+
+Every run prints a generated JSON receipt bound to all package files by
+SHA256. There is no handwritten receipt and no generated checkout output.
+The mathematical proof and finite checks are separate evidence.
+
+## Sources and overlap
+
+Canonical base is `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision
+8. The current selected-source baseline passed its binding checks only.
+[SOURCES.json](SOURCES.json) pins the historical catalogue and selected record;
+no predecessor executable or scientific receipt is imported or replayed.
+The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221497)
+reserved the original four-role five-call question.
+
+The retained eumemic register model and its subsequent finite-group work
+supply the context. Wentao Li's #2513 cyclic 2-power theorem concerns a
+characteristic-two chain ring and unit-cost arbitrary nonidentity powers.
+It does not address this odd-order semisimple algebra with only positive g
+paid. Ross Richardson's #4269 cubic caller uses rational rank-one nilpotent
+shears over Q[N]/(N^3-1), rather than binary rank-one idempotent label calls.
+Cinna Davis's #1799 uses C3 for a three-destination complex fanout family,
+which is a different object. These results are cited, not re-checked.
+
+Entry overlap covered 341 open PRs and 5,523 Discussion records with complete
+remote pagination. The sparse local search covered 243 of 8,136 tracked note
+paths; distinctive main-tree searches and merged/all-state PR searches
+supplemented it. Unpublished work, arbitrary diffs and absent local notes
+remain outside that coverage. No search is a proof of novelty.
+
+## Limitations and implementation constraints
+
+The theorem fixes exactly four dirty roles and permits only the positive g
+label, binary rank-one idempotent couplings and binary scalar mixing.
+Extra restored roles, g^2 as an independent paid label, clean state,
+nonbinary mixing and restricted finite-address realizations are outside scope.
+All physical scalar, frame, access, ownership, routing, restoration, native,
+compiler, precision, stock, tape and complete supplier invoices are unpriced.
+No complete multiplication theorem is claimed. Independent human and formal
+proof-kernel review are unclaimed. Lean, Docker, the selected cold replay and
+predecessor scientific suites were not run.
+
+The verifier has no recursion, dynamic execution, external solver, subprocess
+or dependency. Its largest fixed inventories are 65,536 four-bit-row matrices
+and two 8,361-entry product tables. Loop bounds are fixed in the code, and
+functions stay under 60 physical lines. CPython's integer/tuple/dictionary
+allocation and iterator dispatch are managed-runtime deviations from Power of
+Ten rules 3 and 9. The fixed domains bound live storage; the same warning-strict
+normal and optimized commands check both implementations. A larger-role replay
+would require a new explicit capacity bound before expanding these domains.
+
+## Open next questions
+
+Can one additional restored dirty role lower the eight-call count for the
+same four inverse targets? First retain the same alphabet and analyze how the
+first update can meet both the target and spectator subspaces. The current
+scalar-target argument no longer applies, and no five-role search was run.
+A physical positive-g primitive and a complete paid caller would be required
+before any formal saving could affect the BIT budget.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Credit eumemic's register
+framework, Ali Romman's retained rank-one register context, Wentao Li's
+cyclic-root work, Ross Richardson's separate cubic-caller boundary and the
+finite-group contributors for the surrounding questions. The new four-role
+obstruction and its verifier are the contribution here. Elementary finite-field,
+rank and determinant arguments are classical; global literature priority is
+unclaimed. New work is Apache-2.0. Predecessor files and credit are unchanged.

research/c3-four-inverse-tariff/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/c3-four-inverse-tariff/TASK.json

@@ -0,0 +1,64 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "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": "Exact positive-g call tariff for four inverse cyclic targets over F2[C3], on exactly four arbitrary dirty roles with free binary scalar mixing.",
+  "scope_change_reason": "The original card requests a changed supplier model with native pricing. This original bounded experiment instead proves a formal-algebra obstruction for a specified odd-order alphabet; it is a side result with no native realization or complete invoice.",
+  "bottleneck_link": "Changed BIT primitives may help the next supplier cap. This excludes a five-call sharing attempt before native development; it does not alter the currently binding complex supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified new construction or sharp obstruction. The first exact result is minimum eight on four roles; do not extend to extra roles.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; two exact 8361-candidate joins, complete projector inventory, row-once identity checks and full dirty formal witness.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can one additional restored dirty role reduce the same four inverse target tariff?",
+      "why_it_matters": "The present scalar-target proof cannot constrain this changed endpoint and a saving could motivate a new primitive.",
+      "first_step": "Keep the positive-g alphabet and analyze the first coupling relative to target and spectator subspaces before a bounded five-role search.",
+      "blocked_by": "No five-role lower bound, witness, native realization or complete physical invoice is supplied."
+    }
+  ]
+}

research/c3-four-inverse-tariff/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Scoped proof corroboration, both exact joins, projector inventory, triangular identity, full formal witness and semantic controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "All acceptance predicates remain active under optimized Python"
+    }
+  ]
+}