Lower native monomial cutoff and certify the three-axis window 7–10

research/shorter-native-phase-witness/README.md

@@ -0,0 +1,186 @@
+# Shorter constructive witnesses for native monomial identities
+
+This package improves the sufficient tensor-width bound for the affine/quadratic
+Gaussian monomial grammar in [PR #5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369).
+For n>=2 axes, the general cutoff is 2n+3. For three axes, an exact finite
+character calculation improves it further to seven. Thus widths 7,8,9,10
+decide every fixed three-axis identity in this grammar. The complete kappa
+calculation is unchanged.
+
+## Contract and result
+
+Retain the input-phase action and fixed external coefficients:
+
+```text
+U(g,q)e_x = i^q(x) e_g(x),
+q(x) = c + sum_j a_j x_j + 2 sum_(j<k) b_jk x_j x_k modulo 4,
+g in AGL(n,2), c,a_j in Z/4, b_jk in Z/2.
+```
+
+For P in the complex group algebra, let rho_f(P) evaluate each group term at
+its f-th tensor power. The external coefficients stay fixed. Write I_r for
+the ideal generated by [iI]-i^r[1]. Then
+
+```text
+n>=2 and f>=2n+3  imply  ker(rho_f)=I_(f mod 4).
+n=3 and f>=7     imply  ker(rho_f)=I_(f mod 4).
+```
+
+Consequently four consecutive widths starting at either sufficient cutoff
+decide equality for a single fixed P at all positive widths. The same result
+applies entrywise to complete register endpoints. All independent dirty inputs
+and all specified returned roles remain part of the endpoint. A width-dependent
+program cannot be promoted to an all-width identity by four tests.
+
+For nine axes the sufficient window changes from 22..25 to 21..24. This changes
+an algebraic test bound. It does not reduce a physical supplier's paid cost.
+The sharp two-axis cutoff six in PR #5522 remains stronger in that dimension.
+No least representation cutoff for n>=3 is claimed here.
+
+## A nonalternating Gram form saves one column
+
+A phase character has statistics (r,u,v), where r and u_j are modulo four and
+v_jk are modulo two. As in the predecessor, set the binary symmetric matrix M
+by M_jj=u_j mod 2 and M_jk=v_jk. A tuple of points must have Gram matrix M,
+coordinate counts u modulo four, length r modulo four and full affine span.
+
+Choose an invertible binary matrix B whose column sum s differs from u modulo
+two. This is possible for n>=2: use B=I unless u mod 2 is the all-ones vector;
+in that case replace its first column e_1 by e_1+e_2. Start the tuple with zero
+and the n columns of B. It already has full affine span. The residual Gram
+matrix R=M+BB^t has diagonal u+s, which is nonzero. Thus R is nonalternating.
+
+Every nonalternating symmetric binary matrix R has a factor YY^t=R with
+exactly rank(R)<=n columns. Here is an explicit proof and algorithm. Symmetric
+elimination splits the form into unit lines, hyperbolic pairs and a radical.
+There is at least one unit line. A unit z and a hyperbolic pair e,f can be
+replaced by z+e, z+f, z+e+f; these three vectors are orthonormal. Repeat to
+obtain an orthonormal basis v_i for a complement to the radical. Then
+
+```text
+R = sum_i (R v_i)(R v_i)^t.
+```
+
+Indeed the orthonormal vectors resolve the bilinear form on the quotient by
+its radical. This gives the columns of Y and uses polynomial binary linear
+algebra. Nonalternation is essential: a nonzero alternating form can require
+an extra Gram column. The rank lower bound also proves that this factor width
+is exact for the chosen R. Binary symmetric factorization is classical.
+
+Append the columns of Y. The tuple now has the required Gram matrix and length
+at most 2n+1. If its coordinate counts are w modulo four, then u-w is even.
+Append two copies of the single vector z with coordinates (u_j-w_j)/2 modulo
+two, unless z is zero. This changes the coordinate counts as required and
+preserves all pair parities. The length is at most 2n+3.
+
+For any f>=2n+3 with f congruent to r modulo four, append zero points to reach
+f. They preserve coordinate counts, pair counts and affine span. The resulting
+tuple realizes every character at every such f. This proves the improved
+constructive bound.
+
+## Why character witnesses decide the complete endpoint
+
+The predecessor's Fourier argument is retained. Write P as a sum over affine
+maps g and diagonal phases. At a fixed residue r, combine the constant phase
+coefficients. If P is outside I_r, finite Fourier inversion gives an affine
+bucket and a nonconstant phase character with a nonzero Fourier coefficient.
+Use a tuple X with that character and full affine span, and put Y=gX.
+A different affine map cannot send X to Y. The matrix entry from X to Y is
+therefore exactly the nonzero Fourier coefficient. Conversely every element
+of I_r evaluates to zero at residue r. This proves the displayed kernel bounds.
+The four residue ideals have zero intersection, which proves the four-test
+statement. This step neither assumes nor proves that full affine span is
+necessary for representation faithfulness.
+
+## Exact three-axis character calculation
+
+For n=3 there are 2048 characters including the constant residue. For a
+multiplicity vector m on the eight binary addresses, write m=a+4t with
+0<=a_x<=3 and t_x>=0. Define its character by
+
+```text
+r = sum_x a_x modulo 4,
+u_j = sum_x a_x x_j modulo 4,
+v_jk = sum_x a_x x_j x_k modulo 2.
+```
+
+Let d(a) be the affine dimension of its positive support, with d=-1 for the
+empty support. The exact shortest full-span realization of this residue vector
+has length
+
+```text
+L(a) = sum_x a_x + 4(3-d(a)).
+```
+
+Each new supported point requires four copies and increases affine dimension
+by at most one. Conversely any affine subspace extends to the full space by
+exactly 3-d new points. These two facts prove the formula, including empty
+support. Therefore the exact minimum for a character is the minimum of L(a)
+over its residue vectors a in {0,1,2,3}^8. Four-copy zero padding preserves the
+character and full span at every later width of that residue.
+
+The executable checks all 65536 residue vectors and all 2048 characters. The
+maxima of these exact minima, ordered by residue 0,1,2,3, are
+
+```text
+(8,9,10,7).
+```
+
+A separate enumeration of all 43758 nonnegative multiplicity vectors of total
+width at most ten gives exactly the same 2048 minima. Every minimum also has
+an explicit full-span witness. This finite exact certificate and the padding
+argument prove that the three-axis representation has stabilized by width
+seven. They do not exclude stabilization before the full-span witness bound;
+that would require a separate analysis of nontrivial affine stabilizers.
+
+## Evidence and reproduction
+
+```sh
+python3.12 -B scripts/research_package.py --package research/shorter-native-phase-witness
+```
+
+Python 3.12 and the standard library suffice. Normal and optimized warning-strict
+runs print `PASS_SHORTER_NATIVE_PHASE_WITNESS`; the launcher prints
+`PASS_REGISTERED_RESEARCH_PACKAGE`. Each run checks 1023 nonalternating binary
+forms through dimension four, 2624 constructed characters through 17 axes,
+17408 literal Gaussian-phase identities, the two complete three-axis censuses
+above and seven controls. The controls reject an alternating input and show
+that Gram parity alone misses a two-unit linear phase change.
+
+No predecessor executable is imported. These finite checks corroborate the
+all-dimension written proof; no independent human or proof-kernel acceptance
+is claimed. The selected cold replay, native physical emission, full compiler,
+precision, stock, movement and outer-transfer checks were not run.
+
+## Sources and related work
+
+Ali Romman's [pinned PR #5369 proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/native-tensor-cutoff/PROOF.md)
+supplies the exact grammar, Fourier reduction, pair correction, four residues
+and full endpoint contract. It retains Jose Manuel (@jmbarrancoml), Douglas
+Colkitt, ywz65, Chris R (@Clear1nsight), JoyboyBrian, Cinna Davis and the native
+source lineage. The adaptive initial basis is the change to that construction.
+
+Hiroki KUMAZAKI (@kumagi) supplies the sharp two-axis result in
+[PR #5522](https://github.com/CrocSwap/integer-mult-bounds/pull/5522) and its
+[pinned proof](https://github.com/kumagi/integer-mult-bounds/blob/ffb5adf6a2509a7c99f564d13b74fc82a51b5adc/research/two-axis-native-cutoff/PROOF.md).
+Its multiplicity method and warning about the representation-kernel gap guide
+the three-axis calculation. [PR #5521](https://github.com/CrocSwap/integer-mult-bounds/pull/5521)
+audits the general proof and settles one axis. [PR #5526](https://github.com/CrocSwap/integer-mult-bounds/pull/5526)
+treats the larger full-Clifford group; the present grammar excludes Hadamards.
+No result or source in those contributions is edited.
+
+## Open next questions
+
+Determine whether the three-axis representation already stabilizes before
+width seven. Start with the affine pointwise stabilizers for characters whose
+full-span minimum exceeds the width, and compute their common group-algebra
+kernel. A character-realization minimum alone is not a lower bound for the
+complete representation. Physical application still needs a source-bound
+complete endpoint and its full paid invoice.
+
+## Credit
+
+Finite Fourier inversion, binary form classification and affine basis methods
+are classical. Predecessor methods retain the credit above. New proof and
+checks by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0.
+No general literature-priority claim is made.

research/shorter-native-phase-witness/SOURCES.json

@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/native-tensor-cutoff/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "2d92f17cd8e1064028656cd4ff06c1d38f14ebc0",
+      "sha256": "b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041"
+    }
+  ],
+  "external_provenance": [
+    {
+      "repository": "kumagi/integer-mult-bounds",
+      "commit": "ffb5adf6a2509a7c99f564d13b74fc82a51b5adc",
+      "path": "research/two-axis-native-cutoff/PROOF.md",
+      "git_blob": "68c7f71040bac9afc22246892ff60aedf25363bb",
+      "usage": "Read-only proof and scoped handoff; no executable import."
+    }
+  ]
+}

research/shorter-native-phase-witness/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "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": "Lower the general native monomial cutoff and certify the three-axis sufficient window.",
+  "scope_change_reason": "Take the sharper-bound handoff in PR5369, preserving PR5522 exact two-axis result.",
+  "bottleneck_link": "Reduce sufficient algebraic identity-test widths under the complete native endpoint contract.",
+  "budget_minutes": 60,
+  "stop_rule": "Prove the adaptive-basis bound and exact three-axis phase witnesses; do not claim a sharp representation cutoff or physical supplier.",
+  "outcome": "completed",
+  "evidence": "Written proof, exact binary factors and two independent complete multiplicity censuses.",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance.",
+  "open_questions": [
+    {
+      "question": "Does the three-axis representation stabilize before width seven?",
+      "why_it_matters": "The sufficient full-span witness bound need not be the exact representation threshold.",
+      "first_step": "Compute the common group-algebra kernel of the relevant affine pointwise stabilizers.",
+      "blocked_by": "The two-axis sign argument does not supply necessity in three axes."
+    }
+  ]
+}

research/shorter-native-phase-witness/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": "Binary factors, full native phase characters and two independent three-axis multiplicity censuses."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "-O",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Binary factors, full native phase characters and two independent three-axis multiplicity censuses."
+    }
+  ]
+}