Prove sharp zero-phase witness length 2n+2 for n=2 mod 4 (no κ)

research/zero-phase-even-residue/PROOF.md

@@ -0,0 +1,149 @@
+# Shortest zero-phase tuples when n is two modulo four
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement and boundary
+
+Let n=4k+2, k>=0. A tuple x_1,...,x_f in F_2^n has zero
+nonconstant quadratic phase when
+
+    sum_t x_tj = 0 mod 4,
+    sum_t x_tj x_tl = 0 mod 2  for j<l.
+
+Repeated points are permitted. Its affine span must be all of F_2^n.
+The minimum possible length is exactly
+
+    F(n) = 2n+2.
+
+In particular the first new dimension beyond the small two-axis case is
+n=6, where the minimum is 14. The proof is uniform in k. The finite
+checks below corroborate it; they do not enumerate all tuples at n=6.
+
+This answers the zero-character part of the other-axis-residues question
+in [Ali Romman's PR #5635](https://github.com/CrocSwap/integer-mult-bounds/pull/5635).
+It does not assert that every phase character has a full-span tuple at
+length 2n+2, or identify the complete representation-kernel cutoff.
+
+## 1. The code associated with a tuple
+
+For each j let c_j=(x_1j,...,x_fj) be its binary coordinate row. Let C
+be their binary span. The phase conditions imply that C is doubly even,
+meaning every codeword has weight divisible by four. Indeed each generator
+has weight divisible by four, pairwise intersections have even size, and
+
+    wt(a+b) = wt(a)+wt(b)-2|supp(a) intersect supp(b)|.
+
+The generators are pairwise orthogonal. Bilinearity makes the entire span
+self-orthogonal, so the displayed identity proves the weight assertion
+inductively. Conversely, a doubly even row span has precisely the required
+weight and intersection conditions.
+
+Full affine span is equivalent to rank(C)=n and 1_f not belonging to C.
+A dependence between the homogeneous rows (1_f,c_1,...,c_n) is exactly a
+nonzero affine equation vanishing at every tuple point. This is the
+code/phase interface used in #5635 and Joseph Anglada's #5542, credited
+here as a predecessor lemma.
+
+## 2. A two-coset Gauss-sum obstruction
+
+Suppose a tuple of length at most N=2n+1 exists. Append zero points to
+reach length N. The n rows stay independent and generate a doubly even
+code C in F_2^N. Self-orthogonality gives dim C-perp=N-n=n+1.
+Every word of C has even weight, so 1_N belongs to C-perp. Since N is
+odd, 1_N is not in C. Hence
+
+    C-perp = C direct-sum <1_N>.
+
+For any x in F_2^N, sum i^wt(x+c) over c in C. Double evenness gives
+
+    sum_(c in C) i^wt(x+c) = i^wt(x) sum_(c in C) (-1)^(x dot c).
+
+The inner character sum is zero unless x belongs to C-perp, and equals
+2^n otherwise. Summing by cosets of C therefore leaves exactly two
+contributing cosets, C and 1_N+C. Consequently
+
+    (1+i)^N = sum_(x in F_2^N) i^wt(x) = 2^n (1+i^N).
+
+But n=4k+2 gives N=8k+5. The left side is -2^n(1+i), whereas the right
+side is +2^n(1+i). This contradiction excludes every f<=2n+1.
+
+The coset calculation is classical binary coding theory. The new step
+here is its application to the n=2 mod 4 zero-phase boundary, which the
+cited #5635 result leaves open. No new coding classification is claimed.
+
+## 3. An attaining tuple of length 2n+2
+
+On each of k disjoint eight-column blocks use the four rows
+
+    11111111
+    10101010
+    11001100
+    11110000
+
+and on six final columns use the two rows
+
+    111100
+    110011.
+
+All other entries of each row are zero. There are 4k+2=n independent
+rows and 8k+6=2n+2 columns. Each eight-column block has independent,
+doubly even, mutually orthogonal rows. The final two rows have weights
+four and intersection two. Disjoint blocks preserve these properties.
+Thus the columns give a zero-phase tuple.
+
+The final block's row span consists of 000000 and three weight-four
+words, and does not contain 111111. The all-one word on all columns
+therefore cannot lie in the full row span. The homogeneous rank is n+1,
+so the tuple has full affine span. This attains the lower bound.
+
+At n=6 the six rows are the four displayed eight-column rows extended
+by six zeroes and the two displayed six-column rows preceded by eight
+zeroes. This is a completely explicit 14-column witness.
+
+## 4. First visibility of the cited zero-phase residual
+
+This corollary uses, without re-proving or replaying, #5635 Sections 3-4.
+In that grammar let A_n be its cuspidal affine cancellation element. Its
+coefficient at the identity is Psi(1)>0, and it annihilates every tuple
+of proper affine span. Let E_r be its diagonal Fourier projector onto
+zero nonconstant phase and width residue r modulo four. Set P_r=A_n E_r.
+These are fixed group-algebra elements over Q(i); their coefficients
+stay outside tensor powers.
+
+For each r the first positive matching width where P_r is visible is
+
+    L_r = 2n+2 + ((r-(2n+2)) mod 4).
+
+Below L_r every tuple surviving E_r has proper affine span by Section 2,
+so A_n kills it. At a wrong residue E_r is zero. At L_r append zero
+points to the Section 3 witness. This preserves both phase and full
+affine span. Only the identity affine map fixes this ordered tuple, so
+its diagonal coefficient under P_r is Psi(1)>0. Further groups of four
+zero points show visibility at every larger matching width.
+
+Thus for n=6 these first-visible widths are (16,17,14,15), in residue
+order (0,1,2,3). They are thresholds for this zero-phase residual, not
+claimed thresholds for the complete representation kernel. In particular,
+P_r lies outside the central ideal I_r yet vanishes at every smaller
+matching positive width, giving a necessary test-width obstruction.
+No all-character upper certificate is supplied.
+
+## Verification and limits
+
+The standalone checker constructs this new family, evaluates its literal
+phase generators and homogeneous ranks, exhausts all ordered two-axis
+tuples through length six, and checks the exact Gaussian-integer
+contradiction. Its source proof is authenticated but no predecessor
+executable is imported or run. The corollary inherits #5635's cuspidal
+cancellation lemma and Green's classical character theorem as cited
+mathematical inputs. It does not expand a large affine group.
+
+There is no new kappa, physical native caller, paid invoice, compiler,
+precision, tape, stock or complete multiplication theorem. Independent
+human and formal proof-kernel review are unclaimed. The selected frontier
+and all five framework assumptions retain their status.
+
+Credit Ali Romman #5635/#5529/#5369/#5622, Joseph Anglada #5542, Hiroki
+KUMAZAKI #5522, Mihir Srivastava #5521, Jose Manuel, ywz65, Chris R and
+the retained native/phase lineage. The length-eight doubly-even code,
+finite-field character orthogonality and Gauss-sum method are classical.

research/zero-phase-even-residue/README.md

@@ -0,0 +1,88 @@
+# Sharp zero-phase native witness length for n=2 mod 4
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For every n=4k+2>=2, the shortest binary tuple with zero nonconstant
+quadratic phase and full affine span has exactly **2n+2 columns**.
+At six axes the minimum is 14. A two-coset Gauss-sum contradiction gives
+the lower bound; disjoint length-eight code blocks and a six-column block
+attain it. [PROOF.md](PROOF.md) gives the uniform argument and explicit rows.
+
+The cited cuspidal cancellation lemma of Ali Romman's
+[PR #5635](https://github.com/CrocSwap/integer-mult-bounds/pull/5635) then
+makes the first-visible widths of its zero-phase residual exactly
+`L_r=2n+2+((r-(2n+2)) mod 4)`. At six axes these are `(16,17,14,15)` in
+residue order `(0,1,2,3)`. These are **not claimed complete native cutoff
+thresholds**. An upper construction for every phase character remains open.
+
+This is a scoped algebraic proof with finite corroboration, answering part
+of #5635's explicit other-axis-residues question. The new unbounded domain
+starts at six axes. Two axes supply a small exhaustive control. No new
+kappa, physical supplier or selected-frontier change is claimed.
+
+## Evidence and reproduction
+
+Use the repository CPython 3.12 interpreter from the worktree root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/zero-phase-even-residue
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/check_research_commit.py --package research/zero-phase-even-residue --check-source-history
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/zero-phase-even-residue/verify.py
+```
+
+On another machine substitute a CPython 3.12 executable. Standard library
+only. The direct verifier prints `PASS_ZERO_PHASE_EVEN_RESIDUE` in its
+JSON receipt; the registered runner prints `PASS_REGISTERED_RESEARCH_PACKAGE`.
+Receipt hashes bind every package file and the exact cited source proof.
+No receipt is handwritten, and the verifier writes no files.
+
+The bounded check covers 132 attaining padded tuples on dimensions
+2,6,...,130, 20 independent literal-column checks, 1,092 explicit codewords,
+33 exact Gaussian-integer contradictions, two other-residue controls and
+18 rejected malformed or mathematically invalid inputs. The complete
+ordered two-axis census has 5,461 tuples and 174,752 literal phase checks.
+There are exactly 90 full-span zero-phase tuples at length six and none
+at shorter lengths. Each of those 90 is a permutation of `(1,1,2,2,3,3)`.
+This finite census does not stand in for the all-size proof.
+
+[VALIDATION.md](VALIDATION.md) records capacities and verification limits.
+No predecessor executable, fixture or reported count is replayed. Its proof
+is cited and source-bound as an input for the residual corollary.
+
+## Limits
+
+The complete all-character kernel cutoff, efficient expansion of a large
+group-algebra residual, actual native inputs and returns, paid invoices,
+compiler, precision, tapes and stock are outside this result. The corollary
+uses #5635's cuspidal cancellation lemma and its classical character-theory
+input. Independent human and formal proof-kernel review are unclaimed.
+All five framework assumptions retain their status.
+
+The original formal-interface card is explicitly changed to a written
+native-interface side result. This does not discharge a selected all-size
+assumption. Base main is `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority
+revision 8. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216168).
+Published overlap was checked through current open PRs and Discussion
+claims, with separate main/merged searches. Sparse local notes and unpublished
+work remain coverage limits; a search with no hit does not prove novelty.
+
+## Open next questions
+
+- Determine whether every nonconstant phase character has a full-affine-span
+  realization at the proposed widths in six dimensions. Start with a
+  character-orbit reduction and a constructive upper bound. The present
+  theorem handles only the zero character, so it does not settle this.
+- Determine the complete test cutoff in the other higher-dimensional residue
+  classes. Start with a matching all-character upper construction; the
+  existence of a zero-phase witness alone is insufficient.
+
+## Credit
+
+Credit Ali Romman #5635 for the question and code/phase/cuspidal interface,
+#5369/#5529/#5622 for the retained grammar and Fourier framework, Joseph
+Anglada #5542, Hiroki KUMAZAKI #5522, Mihir Srivastava #5521, Jose Manuel,
+ywz65, Chris R and the retained native/phase contributors. Doubly-even
+codes, character orthogonality, Gauss sums and Green's character theorem
+are classical. No global literature-priority claim is made. New work is
+the n=2 mod 4 length theorem, its attaining family and zero-phase
+first-visibility application.

research/zero-phase-even-residue/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/nine-axis-cutoff-sharpness/PROOF.md",
+      "usage": "input",
+      "git_blob": "1ba92a64c521f25f7aa50ff95731ba893be5fe56",
+      "sha256": "e4e38b0559b0d64de095bee68c0d7bddc61020e843d75f8ca66e3c7b6655a8c3"
+    }
+  ]
+}

research/zero-phase-even-residue/TASK.json

@@ -0,0 +1,103 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "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_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "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": "Prove the exact zero-nonconstant-phase full-affine-span tuple length 2n+2 for n=2 modulo four, and apply the cited cuspidal cancellation lemma to first visibility of that zero-phase residual.",
+  "scope_change_reason": "The formal-interface card is narrowed away from proof-assistant formalization and selected callers to the explicitly open other-axis-residues question in Ali Romman PR5635. This is a written native-interface side result, not a discharge of a selected framework assumption.",
+  "bottleneck_link": "A sharp phase-specific witness length gives a necessary test-width obstruction for the fixed native monomial grammar; an all-character upper bound and physical supplier admission remain separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first exact length theorem; do not expand into a complete cutoff or a larger construction.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; verify.py exact finite corroboration and generated hash-bound stdout receipt",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does every phase character admit a full-span tuple at the proposed six-axis widths?",
+      "why_it_matters": "A matching all-character upper certificate could settle the complete native cutoff.",
+      "first_step": "Reduce six-axis phase characters by affine equivalence, then construct and check one tuple per orbit.",
+      "blocked_by": "Only the zero-character length is established here."
+    },
+    {
+      "question": "What are the complete native test cutoffs in the remaining higher-axis residue classes?",
+      "why_it_matters": "Zero-phase visibility alone does not characterize the full kernel.",
+      "first_step": "Find a matching all-character upper construction and compare its worst character with a scoped lower witness.",
+      "blocked_by": "No general matching all-character upper bound below the cited 2n+3 guarantee is supplied."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216168",
+  "question_source": "PR #5635"
+}