Count exact symmetry quotients for width-two projector words (no κ)

research/projector-word-symmetry/PROOF.md

@@ -0,0 +1,200 @@
+# Exact symmetry quotients for odd projector words
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let K=F_q be any finite field. Let X be the rank-one idempotents of
+M_2(K), and put n=q(q+1). For an odd positive integer k=2m+1, consider
+ordered tuples (N_1,...,N_k) in X^k. The following transformations act on
+these tuples:
+
+1. Simultaneous conjugation C_S by a monomial invertible two by two matrix
+   S, with scalar multiples identified.
+2. R(N_1,...,N_k)=(N_k^T,...,N_1^T).
+
+Write epsilon=0 in characteristic two and epsilon=1 otherwise. The number
+of orbits under the group generated by these transformations is exactly
+
+\[
+ \boxed{\frac{n^{2m+1}
+ +2^{2m+1}\left(q-2+\epsilon\frac{q-1}{2}\right)
+ +(q-1)(q+\epsilon)n^m}{4(q-1)}}.                 \tag{1}
+\]
+
+The term containing epsilon is zero in characteristic two. For k=5 the
+orbit counts at q=2,3,4,5 are respectively 1,962; 31,256; 267,072; and
+1,520,110. These counts are exact for this declared action. No maximal
+symmetry group or minimal possible search domain is asserted.
+
+The action preserves the *universal diagonal-pair existence problem* in
+JoyboyBrian's PR6097 and Josie Elliston's PR6137. One representative per
+orbit therefore suffices when searching all groups and label sets for a
+width-two word of this length with distinct diagonal targets, each of
+label length at least three. It also preserves their coefficient-class
+collision relaxation. This is a search reduction, not a proof that the
+representatives refute, and not a new six-call lower bound over any field.
+
+## Why these are safe transformations
+
+For a group G and g in a label set L, write
+
+\[
+ D_N(g)=(I-N)+[g]N\quad\hbox{in }M_2(K[G]).
+\]
+
+The universal target family is diag([a],[b]), where a and b are distinct
+and neither is a product of at most two labels in L. A monomial S either
+fixes E_00,E_11 separately or exchanges them. Thus
+
+\[
+ S D_N(g) S^{-1}=D_{SNS^{-1}}(g)
+\]
+
+preserves the target family, exchanging a,b in the second case. All
+coefficients of the endpoint identity transform, so arbitrary dirty input
+coordinates remain covered. A general scalar change of basis need not
+preserve this diagonal target pattern. This is why the quotient uses its
+monomial normalizer rather than all of GL_2(K).
+
+There is an anti-isomorphism from M_2(K[G]) to M_2(K[G^op]) that transposes
+the scalar matrices and keeps the named group elements. It reverses the
+order of a product. Consequently an identity with projectors N_1,...,N_k
+becomes an identity with N_k^T,...,N_1^T and labels g_k,...,g_1 over G^op.
+The target is still diagonal. The set of group elements expressible by at
+most two labels is unchanged: a length-two product in G^op is the reversed
+product in G, and every ordered pair from L is allowed. Distinctness is
+unchanged too. Applying the transformation twice returns the original
+identity. Thus existence in this universal family is equivalent along R.
+
+This does not grant R as a symmetry of an arbitrary *fixed* oriented group,
+label set and target specification without transporting that specification.
+Equivalently one can identify G^op with G by inversion and transport L,a,b
+to L^{-1},a^{-1},b^{-1}. A caller keeping them fixed needs extra closure.
+
+The collision relaxation is covariant for the same explicit reasons.
+Monomial conjugation permutes the two diagonal equations and rescales or
+exchanges the off-diagonal equations by nonzero scalars. It preserves their
+zero class-sum constraints. Reversal sends a chronological subset
+(i_1,...,i_j) to (k+1-i_j,...,k+1-i_1). It exchanges prefix and suffix
+cancellation, preserves subset cardinalities, and transports target-marker
+and nonidentity restrictions. Thus a feasible equality partition maps to
+a feasible partition in both directions. This assertion concerns the
+relaxation, not a particular branch order, node cap or proof format.
+
+## The finite action
+
+Represent the projective monomial group H by
+
+\[
+ D_t=\begin{pmatrix}t&0\\0&1\end{pmatrix},\qquad
+ S_t=\begin{pmatrix}0&t\\1&0\end{pmatrix},\qquad t\in K^*.
+\]
+
+It has order 2(q-1). Transposition gives
+
+\[
+ R C_S R=C_{S^{-T}}.
+\]
+
+Hence the abstract semidirect product generated by H and R has order
+4(q-1), and every element is C_S or C_S R. Burnside's lemma applies to this
+finite action, whether or not faithfulness is separately established.
+
+An idempotent in X is specified by its image line and its complementary
+kernel line. There are q+1 choices for the image and q for the kernel, so
+|X|=n. Equivalently it has the form
+
+\[
+ N=\begin{pmatrix}a&b\\c&1-a\end{pmatrix},\qquad bc=a(1-a).       \tag{2}
+\]
+
+Trace one excludes both zero and the identity in every characteristic.
+
+## Fixed tuples without reversal
+
+The identity fixes all n projectors. For t!=1, a projector commuting with
+D_t is diagonal, so exactly E_00,E_11 are fixed. A projector commuting
+with S_t must satisfy a=1-a and b=t c. In characteristic two the first
+condition is impossible. In odd characteristic, a=1/2 and (2c)^2=1/t.
+There are two solutions when t is a square and none otherwise. Precisely
+(q-1)/2 nonzero elements are squares in odd characteristic.
+
+It follows that the total number of fixed k-tuples, summed over H, is
+
+\[
+ n^k+2^k\left(q-2+\epsilon\frac{q-1}{2}\right).                 \tag{3}
+\]
+
+## Fixed tuples with reversal
+
+Put T_S(N)=S N^T S^{-1} and h(S)=|Fix(T_S)|. A tuple fixed by C_S R has
+N_i=T_S(N_{k+1-i}), including a fixed middle projector. Also
+
+\[
+ T_S^2(N)=(S S^{-T})N(S S^{-T})^{-1}.                           \tag{4}
+\]
+
+For S=D_t, the matrix S is symmetric, so (4) is the identity. The m
+paired projectors are arbitrary and the middle has h(D_t) choices.
+The equation for the middle is b=t c in (2). It is the condition that the
+projector is self-adjoint for the nondegenerate symmetric form with matrix
+diag(1/t,1). Every nonisotropic image line has exactly one such projector,
+whose kernel is its orthogonal line. Isotropic image lines have none.
+The isotropic-line equation is x^2=-t y^2. In characteristic two it has
+exactly one projective solution for every t, because squaring is bijective.
+In odd characteristic it has two solutions for half the nonzero t and
+none for the other half. Therefore
+
+\[
+ \sum_{t\ne0}h(D_t)=q(q-1).                                   \tag{5}
+\]
+
+For S=S_t, direct calculation gives
+
+\[
+ T_{S_t}(N)=\begin{pmatrix}1-a&t b\\c/t&a\end{pmatrix}.
+\]
+
+Its fixed point condition includes 2a=1. There are no fixed projectors in
+characteristic two. In odd characteristic, t!=1 forces b=c=0, which is
+incompatible with bc=1/4. For t=1 there are q-1 choices, one for each
+nonzero b with c=(4b)^{-1}. Since S_1 is symmetric, (4) is again the
+identity. Every other S_t contributes zero, since it has no fixed middle.
+Combining this with (5), the total fixed k-tuples over the reversal coset is
+
+\[
+ n^m(q-1)(q+\epsilon).                                        \tag{6}
+\]
+
+Adding (3) and (6), then dividing by 4(q-1), proves (1) by Burnside's lemma.
+This proves all finite fields and every odd positive k. Finite execution
+below corroborates the proof; it does not replace its universal argument.
+
+## Canonical enumeration and its certificate
+
+Order X lexicographically in a declared field encoding. Encode a tuple as
+the corresponding base-n integer. Its canonical representative is the
+minimum of its 4(q-1) images. This minimum is unchanged along an orbit,
+and two tuples have the same minimum exactly when they lie in the same
+orbit. No coefficient, label or target marker may be dropped when a later
+solver transports an instance to that representative.
+
+The standalone verifier constructs F_2,F_3,F_4,F_5,F_7,F_8,F_9 and checks
+their field operations. It obtains X independently by all matrix entries
+and by outer products u v^T with v^T u=1. It counts the fixed projectors
+under every declared transformation and checks (1) at k=1,3,5. A separate
+complete orbit enumeration covers every length-five tuple at q=2,3,4,5.
+It marks each orbit in a bounded byte array, rejects intersections with
+previous orbits, and requires every tuple to be covered. Its representative
+digest and orbit-size histogram are generated from that enumeration.
+
+The verifier also expands new formal positional words coefficientwise to
+check conjugation and opposite-group covariance. It rejects transpose
+without reversal and a nonmonomial scalar adapter as incorrect substitutes.
+These checks import no predecessor scientific code and make no decision
+about whether a collision representative is feasible.
+
+The written theorem is a scoped algebraic proof. No independent human or
+formal proof-kernel acceptance, new kappa, native implementation, complete
+supplier invoice or discharge of the selected five assumptions is claimed.

research/projector-word-symmetry/README.md

@@ -0,0 +1,143 @@
+# Exact symmetry quotients for width-two projector words
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+This is a scoped algebraic proof with exact finite corroboration. It answers
+the symmetry-reduction blocker in Open next question 1 of Josie Elliston's
+[PR6137](https://github.com/CrocSwap/integer-mult-bounds/pull/6137), building on
+JoyboyBrian's [PR6097](https://github.com/CrocSwap/integer-mult-bounds/pull/6097).
+Their collision obstructions are cited premises, not audit or replay targets.
+No predecessor scientific executable is imported or run.
+
+## Result
+
+Let X be the rank-one idempotents of M_2(F_q), n=q(q+1), k=2m+1 an odd
+positive integer, and epsilon=0 for even q and 1 for odd q. Simultaneous
+monomial conjugation and reversal with transpose preserve the universal
+width-two diagonal-pair search family. Their action has exactly
+
+\[
+ \frac{n^{2m+1}+2^{2m+1}\left(q-2+\epsilon\frac{q-1}{2}\right)
+       +(q-1)(q+\epsilon)n^m}{4(q-1)}
+\]
+
+orbits on X^k. [PROOF.md](PROOF.md) proves the reduction, the finite-field
+formula and the covariance of the coefficient-class collision relaxation.
+The monomial group preserves the unordered pair of coordinate projectors.
+Reversal with transpose transports the group to its opposite. A fixed
+oriented group/label/target problem needs its specification transported too.
+
+For five calls the exact domain counts are:
+
+| Field | All projector tuples | Representatives under the declared action |
+|---|---:|---:|
+| F2 | 7,776 | 1,962 |
+| F3 | 248,832 | 31,256 |
+| F4 | 3,200,000 | 267,072 |
+| F5 | 24,300,000 | 1,520,110 |
+
+The standalone verifier enumerates every tuple in this table, independently
+of the fixed-point formula. It supplies a deterministic canonical-index
+function, orbit-size histograms and hashes of the sorted representative
+indices. Counts are search-domain cardinalities, not measured speedups.
+No claim is made that this is the largest safe symmetry group.
+
+This removes one specific prerequisite for a smaller collision search.
+It does not run that search, refute a new field, reproduce the predecessor's
+F2/F3 results, or certify any group realization of a relaxed partition.
+The investigation stops at this first verified reduction.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/projector-word-symmetry
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/projector-word-symmetry/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/projector-word-symmetry/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/projector-word-symmetry --check-source-history
+```
+
+Use an equivalent CPython 3.12 path on another machine. The direct marker is
+`PASS_PROJECTOR_WORD_SYMMETRY`. Each direct run emits a generated JSON receipt
+with counts, representative digests and SHA256 hashes of all six package
+files. It writes no files and needs neither Git nor network access. No
+hand-written receipt is used as evidence. Registered normal and optimized
+commands both cover the complete table and use explicit checks that survive
+Python optimization.
+
+The finite checks also construct the fields of orders 2,3,4,5,7,8,9, compare
+two projector inventories, count every fixed projector, and check the formula
+at lengths 1,3,5. New formal positional words test conjugation and
+opposite-group covariance. Fifteen rejecting controls and two semantic
+controls distinguish invalid replay inputs, transpose without reversal, and
+a scalar adapter outside the target normalizer. These finite checks
+corroborate the universal written proof, which is not a formal-kernel proof.
+
+## Scope and credit
+
+The base is canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`,
+priority revision 8, selected PR6030. The selected binding orientation passed;
+it was metadata orientation rather than a scientific replay. The
+`bit-new-register-model` card changes explicitly to this formal search-domain
+side result. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373332)
+records the question. [SOURCES.json](SOURCES.json) pins historical provenance;
+there are no live or executable predecessor dependencies.
+
+Josie Elliston / PR6137 supplies the explicit symmetry blocker and the F3
+context. JoyboyBrian / PR6097 supplies the diagonal-pair model, collision
+relaxation and F2 context. Retain Josie Elliston / PR6048, Nick Petalas /
+PR6038, Wentao Li / PR4089/4093, Cinna Davis / PR2246 and their credited
+register-model lineage. Projector conjugacy, orthogonal projections over
+finite fields and Burnside's lemma are classical. The contribution is the
+explicit quotient, exact orbit formula and standalone canonical enumeration
+for this search family; global literature priority is unclaimed.
+
+Before claiming, live handoffs and active Discussions, open PRs, this
+account's recent work, local reservations, all-main README searches and
+merged PR searches were checked for the object, formula and general form.
+The overlap snapshot covered 555 open PRs and 6,593 Discussion records with
+complete remote pagination. Its sparse local scan omitted 8,787 main note
+paths; the separate Git searches covered all main READMEs for the named
+terms. Arbitrary historical diffs and unpublished work remain limits.
+Searches are not a novelty certificate.
+
+No new kappa, physical speedup, supplier admission, selected-frontier change,
+complete multiplication theorem or discharge of any of the five selected
+framework assumptions is claimed. Native conversion, scalar/frame/movement
+costs, restoration, precision, compiler closure and a complete paid consumer
+remain outside the result. No Lean, Docker or historical scientific suite ran.
+
+## Open next questions
+
+Can the F4 or F5 representatives settle the five-call existence question?
+Start by transporting every coefficient equation and cancellation rule to
+the canonical tuple, then emit an independently checkable refutation or an
+actual group realization. No such solver or certificate is supplied here.
+The quotient alone proves no new call minimum.
+
+Can a specified Frobenius action reduce this domain further? Prove covariance
+and count its fixed tuples before omitting cases. The present group need not
+be maximal. [TASK.json](TASK.json) records these questions, their relevance,
+first steps and blockers. No follow-up is reserved.
+
+## Verifier bounds
+
+The verifier has no recursion, subprocess, network access, dynamic code
+execution or mutable shared store. Field orders are restricted to the seven
+listed values, tuple lengths to 1,3,5, and complete tuple enumeration to
+24,300,000 entries per field. A census owns one byte array of that size;
+its orbit set has at most sixteen indices. Fields checked without a complete
+census have at most ninety projectors and thirty-two transformations.
+Coefficient expansion has at most thirty-two words. All functions fit
+within sixty physical lines. Invalid domains fail explicitly.
+
+Power of Ten rule 3 has a managed-runtime deviation in verify.py. Python
+integers, tuples, dictionaries and arithmetic temporaries allocate during
+replay; the platform cannot provide allocation-free interpreted execution.
+The enforced finite domains above bound live storage. The byte array is
+allocated once before each census and released on return. A larger census
+must first change and justify the explicit capacity gate. Warning-strict
+normal and optimized execution provide the supported interpreted diagnostics;
+no external static analyzer or proof assistant is assumed installed.

research/projector-word-symmetry/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/diagonal-pair-collision-audit/README.md",
+      "usage": "provenance",
+      "git_blob": "7b8d36d096438ee17b91de51d7e3e9dc32a9cf06",
+      "sha256": "5ab441cf115d5e188a01bc5c06b0299732b99d79e7c84f1aab4daa0aaf4c2b78"
+    },
+    {
+      "path": "research/diagonal-pair-five-call-collisions/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "75a4586f3ab6f3533ba4660a3178aaa226ca38c6",
+      "sha256": "3d607f594f34c5779508f70bd6afc76989107c5f74e0522021305e8cf9b538b0"
+    }
+  ]
+}