Classify mixed-sign orthogonal phase defects at every width (no new κ)

research/mixed-sign-phase-spectrum/PROOF.md

@@ -0,0 +1,165 @@
+# Mixed-sign orthogonal phase spectrum
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Contract and theorem
+
+Let V=F2^n for n>=1 with its ordinary dot product. All vector sums and matrix
+operations below are binary unless a congruence or integer weight is written.
+Fix a sign mask b in V and put
+
+    q_b(x) = wt(x) + 2 b·x modulo 4.
+
+The dot product b·x in this formula is either 0 or 1. Its polarization is
+
+    q_b(x+y) = q_b(x)+q_b(y)-2 x·y modulo 4.
+
+For S in O(n,2), define the row-convention phase defect d_b(S) by
+
+    q_b(S^T x)-q_b(x) = 2 d_b(S)·x modulo 4.                 (1)
+
+The difference has zero polarization, hence is additive; its values are even
+because S preserves x·x. Thus there is a unique binary d_b(S).
+
+**Theorem.** The exact attainable set is
+
+    D_b = {e : q_b(e)=0}
+        = {e : wt(b+e) == wt(b) modulo 4}.                  (2)
+
+For every e in D_b, the symmetric orthogonal involution
+
+    T_e = I + e e^T
+
+has d_b(T_e)=e. Every S has a unique factorization
+
+    S = T_e H,       e=d_b(S),       d_b(H)=0.              (3)
+
+Each fiber has size |O(n,2)|/N_(n,r), where
+
+    r = wt(b) modulo 4,
+    N_(n,r) = sum_{0<=k<=n, k==r modulo 4} binomial(n,k).
+
+These are exact algebraic counts and a written scoped proof. They do not
+price a physical chart change or establish supplier admission.
+
+The equal-sign case b=0, its transvection representative and orthogonal-group
+order are Philipp / mightyOil's PR1300. Gareth Davidson's PR1255 supplies the
+residual gate and row-defect conventions. The present addition is arbitrary
+fixed mixed signs, their changed image and stabilizer, and the corresponding
+literal signed-kernel contract. Classical quadratic-refinement and Gauss-sum
+methods are not claimed as new mathematics independent of this application.
+
+## Necessity from an exact Gaussian sum
+
+The sum over all x of i^(q_b(x)) factors coordinatewise as
+
+    G_b = (1+i)^(n-wt(b)) (1-i)^wt(b)
+        = (1+i)^n (-i)^wt(b).
+
+It is nonzero. Since S^T permutes V, equation (1) gives G_b=G_(b+e), for
+e=d_b(S). Dividing their displayed nonzero expressions shows
+
+    wt(b+e) == wt(b) modulo 4.
+
+No floating-point phase comparison or assumption on the weight of e alone
+is involved. Writing h for the integer number of common 1-bits of b and e,
+
+    wt(b+e)-wt(b) = wt(e)-2h == q_b(e) modulo 4,
+
+because 2h modulo 4 equals twice the binary dot product. This proves the
+equality of the two descriptions in (2). In particular every admissible e
+has even weight.
+
+## A representative for each admissible defect
+
+For even-weight e, e·e=0. Direct multiplication shows
+
+    T_e^T=T_e,       T_e^2=I,       T_e^T T_e=I.
+
+Set a=e·x in {0,1}. Polarization gives
+
+    q_b(T_e x)-q_b(x) = a (q_b(e)-2) modulo 4.
+
+If e is admissible, q_b(e)=0, so this difference is 2e·x. Equation (1)
+therefore gives d_b(T_e)=e. This includes e=0 with T_0=I and proves
+sufficiency for every n and every sign pattern. A nonzero admissible defect
+is corrected by one algebraic rank-one transvection, and cannot be corrected
+by zero such transvections. This counts algebraic factors only.
+
+The transported sign term can also be read directly from PR1300's defect:
+
+    d_b(S) = d_0(S) + b + S b.                             (4)
+
+For even e it yields
+
+    d_b(T_e) = (wt(e)/2 + 1 + b·e) e,
+
+where the coefficient is reduced modulo two. Dropping b+Sb incorrectly
+reuses the equal-sign criterion.
+
+## Cocycle, normalization and exact fibers
+
+Apply (1) first to B^T A^T x, then to A^T x. The result is the twisted cocycle
+
+    d_b(AB) = d_b(A) + A d_b(B).
+
+Let e=d_b(S). Since T_e e=e, the cocycle gives
+
+    d_b(T_e S) = e + T_e e = 0.
+
+Thus H=T_e S proves (3). The e in (3) is prescribed by S, so H is unique.
+The zero-defect maps form a subgroup. Conversely every such H satisfies
+
+    d_b(T_e H)=e.
+
+Multiplication by T_e is therefore a bijection from this subgroup to the
+e fiber. All fibers have equal size. Translation e -> b+e identifies the
+image with all binary vectors of weight congruent to wt(b) modulo four,
+which gives N_(n,r) and the claimed stabilizer count.
+
+For concrete counts use PR1300's credited recurrence
+
+    O_1=1,       O_n=(2^(n-1)-[n odd]) O_(n-1) for n>=2.
+
+At n=6 with one negative axis, N_(6,1)=binomial(6,1)+binomial(6,5)=12.
+There are 23040/12=1920 exact preservers. The equal-sign case instead has
+N_(6,0)=16 and 1440 preservers. These are counts of bases, not a cost saving.
+
+## Literal signed residual
+
+For orthonormal independent active directions u_1,...,u_n, take the product
+of the commuting gates
+
+    C_u^(s) = ((1+s i) I + (1-s i) X_u)/2,
+    X_u f(x)=f(x+u),       s_j=(-1)^b_j.
+
+Independence makes every displacement Ux have one subset expansion. Hence
+its exact convolution coefficient is
+
+    K_(U,b)(Ux) = c_b (-i)^q_b(x),
+    c_b = ((1+i)/2)^n (-i)^wt(b).
+
+For V=US with S orthogonal, coordinates of Ux in V are S^T x. Equation (1)
+then gives
+
+    K_(US,b)(Ux) = (-1)^(d_b(S)·x) K_(U,b)(Ux).
+
+The fixed sign mask indexes the chart's columns on both sides. Permuting
+signs with the axes is a different comparison. The all-nonzero coefficient
+formula proves exact equality iff d_b(S)=0. The convolution commutes because
+binary translations commute, without a native implementation assumption.
+
+At n=5, let b=e_1 and e=e_1+e_2. Then q_b(e)=0 and d_b(T_e)=e, although e
+has weight two. The same transvection has d_0(T_e)=0. Thus the mixed-sign
+boundary differs even for a coordinate swap. Conversely e=e_1+e_2+e_3+e_4
+has weight four but d_b(T_e)=0, so it is not its own mixed-sign defect.
+
+## Remaining obligations
+
+This proof treats an orthonormal active chart and fixed signed C gates.
+It neither generalizes to every nonorthogonal chart nor prices native maps,
+physical routes, source acquisition, dirty restoration, precision, stock,
+fixed tapes or a complete recursive consumer. No selected-frontier change,
+new kappa or complete multiplication theorem follows. The finite verifier
+corroborates (1)-(4); the written argument supplies their universal quantifiers.

research/mixed-sign-phase-spectrum/README.md

@@ -0,0 +1,105 @@
+# Exact phase defects for mixed-sign orthogonal charts
+
+For every binary sign mask b and every width n>=1, the attainable defects of
+orthogonal chart changes are exactly
+
+    D_b = {e : wt(b+e) == wt(b) modulo 4}.
+
+Each defect e has the explicit representative T_e=I+ee^T and the same number
+of realizations. The exact-preserver subgroup has order
+
+    |O(n,2)| / sum_{k==wt(b) modulo 4} binomial(n,k).
+
+This is a scoped written algebraic proof with exact finite corroboration.
+See [PROOF.md](PROOF.md) for the full gate contract and argument. No new
+kappa, physical supplier or selected-frontier change is claimed.
+
+The addition to Philipp / mightyOil's [PR1300](https://github.com/CrocSwap/integer-mult-bounds/pull/1300)
+is an arbitrary fixed mixture of positive and negative residual gates. At
+width five with one negative axis, a weight-two defect is attainable although
+the equal-sign spectrum excludes it. At width six with one negative axis,
+there are 12 defects and 1920 exact preservers, versus the credited equal-sign
+values 16 and 1440. These exact counts are corroborated by the verifier's
+explicit sign/defect enumeration and the inherited group-order recurrence.
+
+This changes the `bit-helper-contract` card to a phase-boundary side result.
+It specifies the algebraic admission criterion for mixed signs before anyone
+prices an actual changed chart. It does not claim a cheaper complete caller.
+The first source discriminator is the width-five one-negative-axis fixture.
+The selected metadata positive control was run separately; no predecessor
+scientific suite was replayed as this contribution.
+
+## Reproduction
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/mixed-sign-phase-spectrum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/mixed-sign-phase-spectrum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mixed-sign-phase-spectrum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/mixed-sign-phase-spectrum --check-source-history
+```
+
+Substitute another CPython 3.12 path elsewhere. The verifier prints
+`PASS_MIXED_SIGN_PHASE_SPECTRUM` inside a JSON receipt whose hashes bind every
+package file. It reads no predecessor executable and writes no files.
+`SOURCES.json` preserves predecessor proofs as historical provenance.
+
+The bounded replay enumerates every orthogonal matrix through width five,
+every sign mask at those widths and every kernel coefficient. It also checks
+the matrix census by independent full binary-matrix enumeration through width
+four; constructs every admissible sign/defect pair through width nine; tests
+every width-four twisted-cocycle pair for every sign mask; and includes ten
+semantic controls. The generated receipt reports 777 orthogonal matrices,
+23,866 matrix/sign pairs, 749,988 literal coefficients, 66,066 full binary
+matrices, 349,524 sign/defect candidates, 87,892 attaining representatives
+and 36,864 cocycle pairs. These are finite checks of the new mixed-sign
+statement, not a predecessor audit.
+
+## Scope and provenance
+
+The scientific base is canonical main `ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`,
+priority revision 7. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146049)
+preceded implementation. The initial cache covered 340 open PRs and 4440
+Discussion records with complete remote pagination. The sparse local search
+was incomplete; targeted `git grep origin/main` and merged-PR searches covered
+the distinctive phase object separately. Search coverage is not novelty proof.
+
+Independent human and formal proof-kernel review are unclaimed. The all-width
+claim rests on the written proof, not extrapolation from the finite checks.
+Physical route/frame costs, native realization, source acquisition, restoration,
+compiler, precision/tape, stock, complete supplier admission and the full
+multiplication theorem remain outside scope. No Lean, Docker or selected
+supplier cold replay was run.
+
+The verifier uses bounded Python allocation, a managed-runtime deviation from
+Power of Ten's fixed-allocation rule. Widths are fixed at 1..5 for group/kernel
+checks, 1..4 for the full-matrix cross-check, and 1..9 for representatives. The
+prefix list is capped at 32768 entries, each matrix has at most nine columns,
+and convolution arrays have at most 32 entries. There is no recursion, child
+process, network access, dynamic code or external dependency. Explicit errors
+preserve all checks under `-O`. Every function has fewer than 60 lines. Warning
+strict normal/optimized replay is the available diagnostic check. A larger
+registered domain must first update these bounds and its measured runtime.
+
+## Open next questions
+
+1. Can a named mixed-sign native helper use the larger exact-preserver subgroup
+   to reduce its complete physical bill? First bind its literal sign mask and
+   compare an explicit phase-preserving chart with all transport/restoration
+   costs. No priced caller is supplied here.
+2. Which defects remain when the permitted orthogonal chart changes must fix
+   a specified set of literal axes? First derive the restricted orbit of q_b
+   on that stabilizer before proposing a synthesis search. The unrestricted
+   representative T_e need not fix those axes.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Philipp / mightyOil's PR1300 supplies the equal-sign defect spectrum, canonical
+transvection and orthogonal-group order. Gareth Davidson's PR1255 supplies the
+C-gate phase contract and row convention. yssite's PR1558 supplies the signed
+Gauss-normalization context, following icekylinx's PR24. Credit Rohan Arun,
+Jeremy Kothe, Hao Yan, Josie Elliston, Douglas Colkitt and the retained
+Clifford/normalization lineage. Classical quadratic-refinement and Gauss-sum
+facts retain their classical status. All predecessor notices stay unchanged.

research/mixed-sign-phase-spectrum/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "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"
+    },
+    {
+      "path": "research/orthogonal-phase-defect-spectrum/README.md",
+      "usage": "provenance",
+      "git_blob": "8912dff64204efb160df1cda12e61b4eba666372",
+      "sha256": "1728301372b1027edeb28b4a88b8c47087d0f5af0b83ca692bed4c732635f532"
+    },
+    {
+      "path": "research/selected1094-chart-phase/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "6ba3890c6c9d919d096965a21d10141ee7cf05b2",
+      "sha256": "1c9010e7c716a9df0264da4749d727c690138509f3335340fb369785cca5e55a"
+    },
+    {
+      "path": "research/signed-gauss-census/README.md",
+      "usage": "provenance",
+      "git_blob": "4d829cb5379ac1ef83c8afaa8c3bc4c7634df55f",
+      "sha256": "3cbf12962eb974302e1dd02232ca52350cf5c9115c0bc135b8c2684e07709913"
+    }
+  ]
+}

research/mixed-sign-phase-spectrum/TASK.json

@@ -0,0 +1,70 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 7,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "original_card": {
+    "id": "bit-helper-contract",
+    "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/r439-bsection-stars-seed01/README.md",
+      "research/r439-copy-path-sharing-barrier/README.md"
+    ],
+    "methods": [
+      "Derive a replacement interface lemma and price its implementation.",
+      "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement."
+    ],
+    "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/r439-bsection-stars-seed01/verify.py"
+      ],
+      "expected": "PASS_R439_BSECTION_STARS",
+      "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.",
+    "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.",
+    "allowed_variations": [
+      "Choose one helper-star or quartet instance; narrow to one boundary implication."
+    ],
+    "scope_change_triggers": [
+      "Changing only source count or scalar addition count without an interface argument."
+    ],
+    "overlap_terms": [
+      "H2_D_frame0_targets_from_helpers",
+      "K_equals_D",
+      "helper-star"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Classify every mixed-sign orthogonal binary chart phase defect, construct one-transvection representatives, and derive exact equal-fiber and stabilizer counts at every width.",
+  "scope_change_reason": "Extend Philipp / mightyOil PR1300 from equal signs to an arbitrary fixed signed C-gate pattern. This is an original phase-boundary side result, not an audit or a replacement H2/K implementation.",
+  "bottleneck_link": "Side result: gives the exact algebraic phase admission criterion for mixed-sign residual charts. No physical rebase or recursive saving follows without a priced actual caller.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first written scoped theorem with literal exact finite corroboration; package it without extending the construction family.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; verify.py exact Gaussian-integer convolution, full small matrix/sign census, constructive representatives, cocycle and ten semantic controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a named mixed-sign native helper use an exact-preserving chart with lower complete physical cost?",
+      "why_it_matters": "Algebraic phase freedom changes no recursive invoice until native and physical costs are charged.",
+      "first_step": "Bind the literal sign mask and price one explicit preserving chart including transport and restoration.",
+      "blocked_by": "No fully priced actual caller or native chart implementation is supplied."
+    },
+    {
+      "question": "Which defects remain when allowed chart changes must fix specified literal axes?",
+      "why_it_matters": "Physical route contracts can forbid the unrestricted representative.",
+      "first_step": "Derive the orbit of q_b under the axis stabilizer before synthesis.",
+      "blocked_by": "The unrestricted T_e need not fix the required axes."
+    }
+  ],
+  "claim_type": "scoped-proof",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146049",
+  "overlap_checked_utc": "2026-10-23T12:54:11Z"
+}