Exact common-chart multiplicities for square-zero radical targets

research/radical-chart-multiplicity/README.md

@@ -0,0 +1,58 @@
+# Exact common-chart multiplicities for square-zero radical targets
+
+This scoped counting proof answers Open next question 1 of Nick Petalas's [PR #4766](https://github.com/CrocSwap/integer-mult-bounds/pull/4766): how many common projective chart pairs does each radical target admit? The [retained question and source theorem](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/radical-all-field-count/README.md) are fixed at canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf. The result refines the existing reachable/unreachable count. No new kappa is claimed.
+
+Let K=F_q, where q is any prime power. Let R=K plus J be a split central unital K-algebra, with J^2=0 and finite d=dim_K J. A target M is a two-by-two matrix with entries in J. A chart pair means one projective nonzero row [phi] and one projective nonzero column [v] over K. It is admissible when phi M v=0. Let k(M) be the number of these pairs. Pairs that differ only by nonzero scalar factors are counted once.
+
+Put z=q^d and A_r(z)=product_(0<=i<r)(z-q^i), with A_0=1. Across all dimensions, exactly six values of k(M) can occur. At each fixed d their target counts are:
+
+| Admissible pairs k | Number of targets |
+| --- | --- |
+| 0 | A_4+(q^3-q)A_3+q^2(q-1)^2 A_2/2 |
+| 1 | (q+1)^2 A_3+(q+1)^2(q-1)A_2 |
+| 2 | q^2(q+1)^2 A_2/2 |
+| q+1 | 2(q+1)A_2+(q^3-q)A_1 |
+| 2q+1 | (q+1)^2 A_1 |
+| (q+1)^2 | 1 |
+
+Here all A_r have argument z. Some counts vanish at small d. The six displayed k values are distinct for every q>=2. Products with r>d vanish, and the table includes d=0. The zero target is the unique target with all (q+1)^2 admissible pairs.
+
+For q=3,d=2, the counts at k=0,1,2,4,7,16 are respectively 864,1536,3456,576,128,1. Thus 1,536 targets have exactly one common chart, while no target has exactly three. A uniform random projective pair succeeds with probability k/(q+1)^2 for a fixed target. This probability statement does not supply a physical sampler or its cost.
+
+**Proof.** Choose a basis of J and write M=sum_l A_l epsilon_l, with A_l in V=M_2(K). Let S be the orthogonal complement of span(A_l) under the nondegenerate entrywise pairing on V. The admissible pairs are exactly the projective rank-one matrices in S: the matrix with entries phi_i v_j pairs with A_l as phi A_l v. The rank-one locus Q in projective three-space is the determinant quadric. It has (q+1)^2 points, parametrized by P^1(K) times P^1(K).
+
+The following table gives, for each vector dimension s of S, the number of subspaces with each intersection size k=|P(S) intersect Q|:
+
+| s | k : number of subspaces |
+| --- | --- |
+| 0 | 0 : 1 |
+| 1 | 0 : q^3-q; 1 : (q+1)^2 |
+| 2 | 0 : q^2(q-1)^2/2; 1 : (q+1)^2(q-1); 2 : q^2(q+1)^2/2; q+1 : 2(q+1) |
+| 3 | q+1 : q^3-q; 2q+1 : (q+1)^2 |
+| 4 | (q+1)^2 : 1 |
+
+For s=1, projective points outside Q are the invertible matrices modulo scalars, of which there are |GL_2(K)|/(q-1)=q^3-q. For s=2, the projective lines contained in Q fix either projective factor, giving 2(q+1) lines. Two points on Q with neither factor in common span a line with exactly two points on Q: the determinant of a combination of their two rank-one matrices is a nonzero multiple of the product of the two combination coefficients. Counting such unordered pairs gives q^2(q+1)^2/2 secants.
+
+Through each point of Q there are q^2+q+1 projective lines. Two lie on Q and q^2 are secants. The remaining q-1 lines meet Q only at that point. This gives (q+1)^2(q-1) tangents. The total number of projective lines in three-space is (q^2+1)(q^2+q+1), obtained by dividing the number of independent vector pairs by |GL_2(K)|. Subtracting contained lines, secants and tangents gives q^2(q-1)^2/2 external lines. This proof includes characteristic two.
+
+A hyperplane is the kernel of one nonzero matrix functional, up to scalar. A rank-one functional restricts on Q to a product of two linear forms, so its zero set is the union of two ruling lines and has 2q+1 points. There are (q+1)^2 such hyperplanes. An invertible functional gives exactly one projective column for each projective row, hence q+1 points; there are q^3-q such hyperplanes. This proves the s=3 row. The other two dimensions are immediate.
+
+For fixed S of dimension s, its orthogonal complement has dimension 4-s. The coefficient tuple (A_1,...,A_d) must span that fixed complement. Such tuples are full-row-rank (4-s)-by-d matrices and number A_(4-s)(q^d). Multiply each subspace count by this number and collect equal k values. The displayed target table follows. This is a complete finite-field proof, not extrapolation from examples.
+
+**Evidence.** A standalone standard-library verifier directly forms each scalar matrix's projective bilinear-zero mask, intersects masks for every coefficient tuple, and counts the surviving pairs. It covers q=2 with d=0 through 4, q=3 with d=0 through 3, and q=4,5 with d=0 through 2: 1,065,033 target tuples. It independently enumerates 1,928 subspaces in unique reduced row-echelon form and counts their rank-one projective points. Both calculations agree with every cell of the table. Six controls cover predecessor calibration, one-chart targets, a forbidden chart count, F_4 versus integers modulo four, the common-chart condition, and the bounded field domain. Normal and optimized warning-strict CPython 3.12.14 runs pass.
+
+Credit Nick Petalas's [PR #4766](https://github.com/CrocSwap/integer-mult-bounds/pull/4766) for the all-field reachability count and explicit multiplicity question, and his [PR #4745](https://github.com/CrocSwap/integer-mult-bounds/pull/4745) for the arbitrary-word square-zero reachability theorem. The [pinned reachability proof](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/square-zero-radical-reachability/README.md) supplies the paid-cost interpretation: k>0 gives exact formal cost two, while k=0 is unreachable at any word length. That theorem is cited, not independently re-audited here. ToikY's [PR #4334](https://github.com/CrocSwap/integer-mult-bounds/pull/4334) supplies the shared-chart interface; Wentao Li's [PR #4099](https://github.com/CrocSwap/integer-mult-bounds/pull/4099) supplies the right-vector alphabet. The finite-geometry incidence counts are classical; no general literature-priority claim is made.
+
+**Limits.** Only radical targets, two roles, a scalar residue field and square-zero radical are covered. Separate charts for separate radical coordinates are not allowed. Native chart preparation, routing, precision, restoration, stock and the complete supplier/outer bill remain unknown. No selected cold replay, predecessor scientific suite, native build, Lean or Docker run was used. No independent human or proof-kernel acceptance is claimed. Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0.
+
+## Reproduce
+
+```sh
+python3 -B scripts/research_package.py --package research/radical-chart-multiplicity
+```
+
+Use Python 3.12 with the standard library. The normal and optimized commands must print `PASS_RADICAL_CHART_MULTIPLICITY`. The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The checker has no external runtime inputs.
+
+## Open next questions
+
+Bind a restricted common-chart policy to a physical caller and price its choice and emission. The source binding and physical cost model are not supplied by this package. See `TASK.json` for the structured scope.

research/radical-chart-multiplicity/SOURCES.json

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

research/radical-chart-multiplicity/TASK.json

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "This scoped counting proof answers the common-chart multiplicity question in PR #4766. It gives the complete distribution of admissible projective row/column pairs over every finite field and every radical dimension. A six-case table refines the existing reachable/unreachable count.",
+  "scope_change_reason": "This is a scoped interface theorem. It does not complete the original supplier or uniform-transfer task.",
+  "bottleneck_link": "Bind a restricted common-chart policy to a physical caller and price its choice and emission.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the scoped proof, exact controls and bounded registered replay; do not expand to physical lowering.",
+  "outcome": "completed",
+  "evidence": "1,065,033 target tuples, 1,928 independently enumerated subspaces and six controls",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or proof-kernel acceptance is claimed.",
+  "open_questions": [
+    {
+      "question": "Bind a restricted common-chart policy to a physical caller and price its choice and emission.",
+      "why_it_matters": "The abstract result needs an actual caller and a complete cost model.",
+      "first_step": "Bind a restricted common-chart policy to a physical caller and price its choice and emission.",
+      "blocked_by": "No production caller or physical cost model is supplied."
+    }
+  ],
+  "upstream_checkpoint": {
+    "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+    "priority_revision": 7,
+    "checked_at": "2026-10-23T16:59:58.496853+00:00"
+  },
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19150356"
+}

research/radical-chart-multiplicity/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": "1,065,033 target tuples, 1,928 independently enumerated subspaces and six controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "1,065,033 target tuples, 1,928 independently enumerated subspaces and six controls"
+    }
+  ]
+}

research/radical-chart-multiplicity/verify.py

@@ -0,0 +1,132 @@
+"""Exact common-chart multiplicities. Ali Romman with OpenAI Codex. Apache-2.0."""
+from collections import Counter
+from itertools import combinations, product
+import json
+
+
+def require(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def field(q):
+    require(q in (2, 3, 4, 5), 'unsupported field')
+    add = [[(a ^ b) if q == 4 else (a + b) % q for b in range(q)] for a in range(q)]
+    mul = [[0] * q for _ in range(q)]
+    for a, b in product(range(q), repeat=2):
+        if q != 4:
+            mul[a][b] = a * b % q
+        else:
+            x = ((a & 1) * (b & 1)) ^ (((a & 1) * (b >> 1)) << 1)
+            x ^= (((a >> 1) * (b & 1)) << 1) ^ (((a >> 1) * (b >> 1)) * 3)
+            mul[a][b] = x
+    return add, mul
+
+
+def projective(q, n):
+    for pivot in range(n):
+        for tail in product(range(q), repeat=n - pivot - 1):
+            yield (0,) * pivot + (1,) + tail
+
+
+def rref_spaces(q, n, r):
+    for pivots in combinations(range(n), r):
+        free = [(i, j) for i, p in enumerate(pivots) for j in range(p + 1, n) if j not in pivots]
+        for values in product(range(q), repeat=len(free)):
+            rows = [[int(j == p) for j in range(n)] for p in pivots]
+            for (i, j), value in zip(free, values):
+                rows[i][j] = value
+            yield rows
+
+
+def table(q):
+    return {
+        0: {0: 1},
+        1: {0: q**3-q, 1: (q+1)**2},
+        2: {0: q*q*(q-1)**2//2, 1: (q+1)**2*(q-1),
+            2: q*q*(q+1)**2//2, q+1: 2*(q+1)},
+        3: {q+1: q**3-q, 2*q+1: (q+1)**2},
+        4: {(q+1)**2: 1},
+    }
+
+
+def predicted(q, d):
+    answer = Counter()
+    for s, histogram in table(q).items():
+        weight = 1
+        for i in range(4-s):
+            weight *= q**d-q**i
+        for k, count in histogram.items():
+            answer[k] += count * weight
+    return Counter({k: v for k, v in answer.items() if v})
+
+
+def subspaces(q, add, mul):
+    total = 0
+    for s in range(5):
+        actual = Counter()
+        for rows in rref_spaces(q, 4, s):
+            k = 0
+            for coeff in projective(q, s):
+                matrix = [0] * 4
+                for c, row in zip(coeff, rows):
+                    matrix = [add[x][mul[c][y]] for x, y in zip(matrix, row)]
+                k += mul[matrix[0]][matrix[3]] == mul[matrix[1]][matrix[2]]
+            actual[k] += 1
+            total += 1
+        require(actual == table(q)[s], ('subspace table', q, s, actual))
+    return total
+
+
+def target_masks(q, add, mul):
+    charts = list(product(projective(q, 2), repeat=2))
+    masks = []
+    for a, b, c, d in product(range(q), repeat=4):
+        mask = 0
+        for i, (phi, v) in enumerate(charts):
+            row0 = add[mul[a][v[0]]][mul[b][v[1]]]
+            row1 = add[mul[c][v[0]]][mul[d][v[1]]]
+            if add[mul[phi[0]][row0]][mul[phi[1]][row1]] == 0:
+                mask |= 1 << i
+        masks.append(mask)
+    return masks
+
+
+def main():
+    target_total = space_total = 0
+    fixture = None
+    for q, max_d in ((2, 4), (3, 3), (4, 2), (5, 2)):
+        add, mul = field(q)
+        space_total += subspaces(q, add, mul)
+        masks = target_masks(q, add, mul)
+        for d in range(max_d + 1):
+            actual = Counter()
+            for selected in product(masks, repeat=d):
+                common = (1 << ((q+1)**2)) - 1
+                for mask in selected:
+                    common &= mask
+                actual[common.bit_count()] += 1
+                target_total += 1
+            require(actual == predicted(q, d), ('target histogram', q, d, actual))
+            require(sum(actual.values()) == q**(4*d), 'total target count')
+            if (q, d) == (3, 2):
+                fixture = dict(sorted(actual.items()))
+    require(predicted(2, 3)[0] == 1092, 'predecessor unreachable calibration')
+    require(predicted(3, 2)[1] > 0, 'single-chart targets must occur')
+    require(predicted(3, 2)[3] == 0, 'three-chart targets are forbidden')
+    add, mul = field(4)
+    require(add[add[mul[2][2]][2]][1] == 0, 'F4 must not be Z/4')
+    a, b = target_masks(2, *field(2))[1:3]
+    require((a & b).bit_count() < min(a.bit_count(), b.bit_count()), 'charts must be common')
+    try:
+        field(6)
+    except ValueError:
+        pass
+    else:
+        raise ValueError('unsupported field accepted')
+    print(json.dumps(dict(status='PASS_RADICAL_CHART_MULTIPLICITY', target_tuples=target_total,
+                         subspaces=space_total, q3_d2=fixture, controls=6, no_new_kappa=True), sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()