Prove the exact order-21 normal-subgroup call tariff (no new κ)

research/order21-normal-tariff/PROOF.md

@@ -0,0 +1,141 @@
+# Exact normal-subgroup tariff in the order-21 algebra
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement and model
+
+Let G be the group C7 semidirect C3 with elements a^i b^j, where
+0 <= i < 7, 0 <= j < 3, and b a b^-1 = a^2. Multiplication is
+
+```text
+(i,j)(k,l) = (i + 2^j k mod 7, j+l mod 3).
+```
+
+Work in the full formal algebra Mat_r(F2[G]). There are w active roles,
+with 1 <= w <= r, and arbitrary exponents 1 <= e_t <= 6. The required
+operator is
+
+```text
+T = diag([a^e_1], ..., [a^e_w], 1, ..., 1).
+```
+
+Every role has arbitrary input. The last r-w roles must be restored as
+operators. A paid call is D_N(g) = I + ([g]+[1])N for any g != 1 in G
+and any rank-one binary idempotent N in Mat_r(F2). Each call costs one.
+Arbitrary GL_r(F2) scalar maps may be interleaved for free. No other
+address maps, clean workspace, COPY or ERASE are free.
+
+**Theorem.** The exact minimum number of paid calls is w, for every
+finite r and every stated exponent list. In particular,
+diag([a],[a^2],[a^4],[a],1,...,1) requires exactly four calls, regardless
+of the number of restored dirty roles.
+
+More precisely, if a word uses c7 paid labels in the normal subgroup
+C7 minus identity, and c3 paid labels outside C7, then
+
+```text
+3 c7 + 2 c3 >= 3w.
+```
+
+Consequently an optimal w-call word uses only normal-subgroup labels.
+This does not claim an exact optimum subject to a prescribed positive c3.
+
+## Representation and rank budget
+
+The polynomial x^3+x+1 has neither zero nor one as a root in F2.
+A reducible cubic over a field has a linear factor, so this polynomial
+is irreducible. Let F8=F2[alpha] with alpha^3=alpha+1. Its multiplicative
+group has order seven. Since alpha is neither zero nor one, its order
+is seven.
+
+For g=a^i b^j, define the binary linear map on F8
+
+```text
+rho(g)(z) = alpha^i z^(2^j).
+```
+
+Frobenius is F2-linear and its third power is identity. Composing the
+displayed maps gives the group multiplication above, so rho extends
+linearly to an algebra homomorphism F2[G] -> Mat_3(F2). In the basis
+1,alpha,alpha^2 its two generators, encoded as binary integer rows, are
+
+```text
+rho(a) = (4,5,2),    rho(b) = (1,4,6).
+```
+
+For 1 <= i <= 6, rho(a^i)+I is multiplication by the nonzero field
+element alpha^i+1, hence has rank three.
+
+For j=1 or 2, a nonzero fixed point of rho(a^i b^j) satisfies
+z^(2^j-1)=alpha^-i. The exponents 2^j-1 are respectively one and three,
+both coprime to seven. Raising to either power therefore permutes F8's
+nonzero elements. There is exactly one nonzero fixed point, together
+with zero. Its kernel as a binary linear map has dimension one, so
+rank(rho(a^i b^j)+I)=2. This proves all represented ranks without a census.
+
+Apply rho to every entry of an r-role operator, viewing the result as
+an ordinary 3r by 3r binary matrix. One paid call has difference from
+identity
+
+```text
+N tensor (rho(g)+I).
+```
+
+The rank of a tensor product over a field is the product of the ranks.
+Thus each normal-subgroup call contributes rank three and every other
+paid label contributes rank two. Meanwhile rank(rho(T)+I)=3w, since
+its active diagonal blocks are invertible and its dirty blocks are zero.
+
+For any equally sized matrices A and B,
+
+```text
+AB-I = (A-I)B + (B-I),
+rank(AB-I) <= rank(A-I) + rank(B-I).
+```
+
+Induction over any finite paid word proves the stated rank budget.
+It is a necessary condition for formal equality. Faithfulness of the
+algebra homomorphism is unnecessary, and no equality in the represented
+algebra is used to certify a formal endpoint.
+
+## Free scalar maps and arbitrary dirty workspace
+
+A scalar map S satisfies S D_N(g) = D_(S N S^-1)(g) S. Moving each free
+scalar map to the right therefore conjugates the paid binary idempotents
+and leaves them inside the declared alphabet. Augmentation [g] -> 1
+sends every paid factor and T to identity. Hence the remaining product
+of free scalar maps must be identity. The normalized word has the same
+paid labels and number of calls, so the rank budget applies unchanged.
+
+The proof holds for every finite r. Identity-target dirty roles add
+zero to the represented target rank. No compression, clean-input
+assumption or bound on the number of workspace roles is used.
+
+Since 3 c7+2 c3 <= 3(c7+c3), the rank budget forces at least w calls.
+If exactly w calls occur, any c3>0 would make the rank budget fail.
+
+## Attainment in the full formal algebra
+
+For each active role t, take N=E_tt and g=a^e_t. This call acts by
+[a^e_t] on that role and identity on every other role. The product of
+these w coordinate calls is exactly T coefficient by coefficient in
+F2[G]. It uses no additional roles and restores every dirty role.
+This establishes the upper bound in the full formal algebra and
+completes the proof.
+
+## Sources and limits
+
+Cinna Davis's PR2011 fixes this group, paid alphabet and conjugacy-orbit
+endpoint, and explicitly leaves four outputs open. The new statement
+settles that question and removes both the fixed role count and the
+restriction against free scalar maps. The original three-role finite
+census is not rerun or claimed as new. Cinna Davis's PR3893 supplies an
+S3 example of the classical representation-rank telescoping method.
+The present contribution is its fixed-point-free F8 application and
+uniform exact order-21 tariff. The F8 and rank facts are elementary
+linear algebra, not new general methods.
+
+Mixed order-three target profiles, nonuniform tariffs, native realization,
+physical movement, precision, stock, recursive costs and the complete
+multiplication theorem are outside this proof. The selected frontier
+is unchanged. No proof-kernel or independent human review is claimed.

research/order21-normal-tariff/README.md

@@ -0,0 +1,140 @@
+# Exact order-21 normal-subgroup call tariff
+
+Scoped algebraic proof with exact finite corroboration. No new kappa.
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+In the full formal algebra F2[C7 semidirect C3], any w nonidentity
+normal-C7 outputs require exactly w paid rank-one idempotent calls.
+This holds for any finite number of arbitrary restored dirty registers
+and with arbitrary free binary scalar mixing. In particular,
+
+```text
+diag([a], [a^2], [a^4], [a], 1, ..., 1)
+```
+
+costs exactly four calls. This settles the four-register question left
+by Cinna Davis's [PR2011](https://github.com/CrocSwap/integer-mult-bounds/pull/2011).
+Its three-register census is a cited predecessor and is not replayed.
+
+[PROOF.md](PROOF.md) defines the complete model. Multiplication and
+Frobenius on F8 give a three-dimensional binary representation. Every
+nonidentity normal-C7 target contributes rank three to the endpoint
+minus identity. A normal-C7 paid label contributes rank three, while
+an outside label contributes rank two. Rank telescoping therefore gives
+
+```text
+3 * normal_calls + 2 * outside_calls >= 3 * target_count.
+```
+
+Coordinate calls attain the bound in the full formal algebra. Every
+optimal word uses only normal-C7 labels. The lower bound is uniform
+in target count, word length and restored workspace size. The finite
+checks corroborate the proof; they do not replace its induction.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/order21-normal-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/order21-normal-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/order21-normal-tariff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/order21-normal-tariff --check-source-history
+```
+
+Any CPython 3.12 installation can replace the local interpreter path.
+The verifier prints `PASS_ORDER21_NORMAL_TARIFF` in a generated JSON
+receipt bound to the SHA256 of all six package files. It writes no files.
+There is no handwritten receipt. Local checks used CPython 3.12.15 on
+macOS arm64. [VERIFY.json](VERIFY.json) registers the normal and optimized
+warning-strict runs, each with a 60-second limit.
+
+The verifier performs these exact checks:
+
+- All 441 products in the new F8 representation, with represented
+  difference ranks zero, three and two on identity, the six nonidentity
+  normal labels and the fourteen outside labels respectively.
+- All 12,320 paid factors on four and five roles. These are all 120 and
+  496 binary rank-one idempotents respectively, at all twenty paid labels.
+  Every represented difference has the proved rank.
+- All 1,296 four-target exponent lists from {1,...,6}, each with one
+  arbitrary dirty role, plus six larger witnesses at widths 5, 8 and 12,
+  each with zero or two dirty roles. All 1,302 products equal their
+  required endpoints coefficient by coefficient in the full formal algebra.
+- One conjugated four-target witness mixes the dirty input through free
+  scalar maps and restores the full operator. A separate 105-dimensional
+  faithful regular-action execution agrees with the formal result.
+- Ten controls reject four call omissions, either missing free scalar map,
+  a changed dirty-role operator, a wrong target exponent, reversed
+  Frobenius and an incorrect outside-label rank charge. All checks remain
+  active under optimized Python.
+
+The complete four-target formal stream is hashed in the generated receipt.
+The predecessor's pair census and certificate numbers are not recomputed.
+No selected operator replay, Lean or Docker run is needed for this theorem,
+and none was run.
+
+## Scope and provenance
+
+The paid alphabet contains every nonidentity group label and every binary
+rank-one idempotent. Its unit call price does not account for native
+realization, routing, frames, precision, stock or recursive child costs.
+Those physical obligations remain unknown. Mixed order-three target
+profiles and nonuniform prices are outside the exact tariff. No supplier
+admission, complete multiplication theorem or selected-frontier change
+follows. Independent human and formal proof-kernel review are unclaimed.
+
+[SOURCES.json](SOURCES.json) binds historical provenance at canonical main
+`ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority revision 7.
+The selected-record and task-card pins are historical. The verifier uses
+no predecessor files or external libraries. [TASK.json](TASK.json)
+records the scope change from bit-new-register-model to this formal
+obstruction. The card's current generic baseline returned
+`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. The first scientific fixture was
+the four-output endpoint above with one restored dirty role.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145540)
+records the question. Live open PRs, recent handoffs, merged PR searches
+and main README terms were checked. The overlap helper covered 315 open
+PRs and 4,392 Discussion records with complete remote pagination. Its
+sparse local search covered only 170 of 6,996 HEAD notes; targeted main
+searches supplement it. These checks do not establish exhaustive novelty.
+
+Build the Lever led to the rerunnable formal and represented checks.
+Prove It Works led to full dirty-operator execution and omission controls.
+Power of Ten kept the replay bounded and read-only. Every function is
+below 60 lines, and no recursion, dynamic evaluation or subprocess is used.
+Matrices have at most 128 rows, formal words at most twelve calls and
+formal executions at most fourteen roles. The faithful regular replay has
+five roles and 105 rows. Loops have bounds from these fixed domains.
+Python allocation is a managed-runtime deviation from static allocation;
+all live collections are bounded by these limits, and input files are
+limited to one MiB each. Warning-strict normal and optimized execution
+provide diagnostics. No separate static analyzer is installed.
+
+## Open next questions
+
+1. What is the exact tariff for mixed normal-C7 and outside order-three
+   target profiles? Begin with one target of each type and combine this
+   represented-rank budget with the quotient C3 character. The current
+   rank budget does not by itself prove that their separate calls are
+   optimal. A full formal attainment or stronger lower bound is needed.
+2. Can a literal native producer and consumer implement these group
+   labels at a useful complete cost? First fix their address action,
+   ownership, routing and restoration contracts, then charge the whole
+   boundary. No physical cost model is supplied here.
+
+The structured questions are in [TASK.json](TASK.json).
+
+## Credit
+
+Cinna Davis's PR2011 supplies the group, formal alphabet, three-output
+problem and explicit four-output question. Its retained register-model
+lineage includes eumemic's PR288 and the original bit-model work.
+Cinna Davis's [PR3893](https://github.com/CrocSwap/integer-mult-bounds/pull/3893)
+provides the S3 example of representation-rank telescoping. Finite-field
+multiplication, Frobenius and the rank inequality are classical. The new
+claim is their uniform exact tariff for normal-subgroup targets in the
+order-21 model, including arbitrary restored workspace and free scalar
+mixing. Every predecessor retains its attribution; no predecessor file
+or credit line is changed.

research/order21-normal-tariff/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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-semidir21-orbit-seed8f89/README.md",
+      "usage": "provenance",
+      "git_blob": "13e399921e5dd556a7ce8645362ffb5d550b5e75",
+      "sha256": "534422d3f152b0f1e4a8357056036d1629b0aee75e58301c7436f5b723260eb0"
+    }
+  ]
+}

research/order21-normal-tariff/TASK.json

@@ -0,0 +1,77 @@
+{
+  "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": "Prove exact cost w for any w nonidentity normal-C7 targets in F2[C7 semidirect C3], for every finite restored dirty workspace and free binary scalar mixing.",
+  "scope_change_reason": "Take Cinna Davis PR2011's explicitly open four-register question, using a representation-rank obstruction rather than a new native supplier or a replay of the three-register census.",
+  "bottleneck_link": "This formal side result closes the normal-subgroup multi-output sharing route in the stated alphabet. Native realization and a fully charged recursive invoice remain unknown.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first exact uniform tariff; do not search mixed target profiles or construct a native supplier.",
+  "outcome": "completed",
+  "evidence": "Written F8 representation and rank-telescoping proof. Exact verifier checks 441 representation products, 12320 paid factors, 1302 full formal coordinate endpoints, one dirty-mixed faithful regular endpoint and ten rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the exact tariff for mixed normal-C7 and outside order-three target profiles?",
+      "why_it_matters": "The current theorem excludes sharing only for all-normal targets.",
+      "first_step": "Study one target of each type using the represented-rank budget and quotient-C3 character, with a full formal endpoint.",
+      "blocked_by": "A stronger lower bound or a cheaper full formal word is missing."
+    },
+    {
+      "question": "Can a literal native caller implement these labels at a useful complete cost?",
+      "why_it_matters": "Only a physical implementation could affect the recursive supplier bill.",
+      "first_step": "Specify the address action, ownership, routing and restoration of one producer/consumer pair and charge every operation.",
+      "blocked_by": "No native boundary contract or complete cost model is supplied."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145540",
+  "claim_type": "scoped algebraic proof with exact finite corroboration",
+  "environment": {
+    "python": "CPython 3.12.15",
+    "platform": "macOS arm64",
+    "dependencies": "standard library only"
+  }
+}