diff --git a/research/radical-chart-multiplicity/README.md b/research/radical-chart-multiplicity/README.md new file mode 100644 index 0000000000..2f12ca510a --- /dev/null +++ b/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=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. diff --git a/research/radical-chart-multiplicity/SOURCES.json b/research/radical-chart-multiplicity/SOURCES.json new file mode 100644 index 0000000000..277ad46954 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/radical-chart-multiplicity/TASK.json b/research/radical-chart-multiplicity/TASK.json new file mode 100644 index 0000000000..ed1f7f6c9e --- /dev/null +++ b/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" +} diff --git a/research/radical-chart-multiplicity/VERIFY.json b/research/radical-chart-multiplicity/VERIFY.json new file mode 100644 index 0000000000..14a544db99 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/radical-chart-multiplicity/verify.py b/research/radical-chart-multiplicity/verify.py new file mode 100644 index 0000000000..97e5aecccb --- /dev/null +++ b/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()