Prove exact phase defects for charts fixing any binary subspace

research/fixed-subspace-phase-defects/PROOF.md

@@ -0,0 +1,125 @@
+# Phase defects with a pointwise fixed subspace
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let V=F_2^n, n>=1, with its ordinary nondegenerate dot product. Fix b in V,
+a subspace W of V, and the quadratic refinement
+
+    q_b(x) = wt(x) + 2(b dot x) modulo 4.
+
+The dot product in this expression takes values zero and one. Write
+
+    G_W = {S in O(n,2): Sw=w for every w in W}.
+
+Use the row convention of Gareth Davidson #1255 and Nick Petalas #5225:
+
+    q_b(S^T x) - q_b(x) = 2 d_b(S) dot x modulo 4.
+
+The unrestricted mixed-sign theorem of #5225 is a cited premise. It says
+that every defect satisfies q_b(d_b(S))=0, that T_e=I+ee^T has defect e
+whenever q_b(e)=0, and that d_b(AB)=d_b(A)+A d_b(B). No predecessor
+verification or physical implementation is assumed here.
+
+**Restricted image theorem.** The exact defect image of G_W is
+
+    D_(b,W) = {e in W-perpendicular: q_b(e)=0}.               (1)
+
+Every e in this set has the representative T_e inside G_W. Put
+
+    H_(b,W) = {S in G_W: d_b(S)=0}.
+
+Every S in G_W has the unique factorization
+
+    S = T_e H,     e=d_b(S),     H in H_(b,W).                (2)
+
+Each defect fiber has exactly |H_(b,W)| elements. Consequently
+
+    |H_(b,W)| = |G_W| / |D_(b,W)|.                           (3)
+
+This statement permits degenerate W, including totally isotropic subspaces.
+No nondegeneracy assumption or choice of a complement to W is needed.
+
+## Proof of the restriction and its converse
+
+If S fixes W pointwise, its inverse fixes W pointwise too. Orthogonality gives
+S^T=S^-1. For w in W the defining defect identity therefore gives
+
+    2 d_b(S) dot w = q_b(w)-q_b(w) = 0 modulo 4.
+
+Thus d_b(S) belongs to W-perpendicular. The cited unrestricted theorem gives
+q_b(d_b(S))=0, proving necessity in (1).
+
+Conversely, let e belong to the set in (1). Since q_b(e)=0, e has even
+weight, so e dot e=0. The cited transvection identity gives T_e in O(n,2),
+T_e^2=I and d_b(T_e)=e. For every w in W,
+
+    T_e w = w + e(e dot w) = w.
+
+Hence T_e belongs to G_W. This proves sufficiency and the promised attaining
+representative. It also shows that a nonzero defect requires exactly one
+such algebraic rank-one transvection when correcting a chart in G_W.
+This is a factor count, not a paid physical cost.
+
+## Factorization and fibers
+
+For S in G_W, put e=d_b(S) and H=T_e S. Both factors fix W, and the cited
+cocycle gives
+
+    d_b(H) = e + T_e e = e+e = 0.
+
+Here T_e e=e follows from e dot e=0. Thus H belongs to H_(b,W) and S=T_e H.
+The defect e is forced by S, after which H=T_e S is forced, proving
+uniqueness. The cocycle also shows that zero-defect maps form a subgroup
+and that d_b(T_e H)=e for every H in that subgroup. Left multiplication by
+T_e is therefore a bijection onto the e fiber. This proves (2) and (3).
+
+## Literal axes and nested restrictions
+
+Suppose W is spanned by k distinct coordinate vectors. Orthogonality forces
+S to be the identity on those axes and an arbitrary orthogonal map on the
+remaining m=n-k coordinates. Defects vanish on the fixed coordinates.
+Let b_free be b restricted to the free coordinates. Translation
+z -> b_free+z in (1) gives the closed count
+
+    N = sum_{0<=j<=m, j == wt(b_free) modulo 4} binomial(m,j),
+    |H_(b,W)| = |O(m,2)| / N.                               (4)
+
+Use |O(0,2)|=1. The all-fixed case has N=1. In particular, signs on fixed
+axes do not affect this count. This answers the literal-axis question left
+open by #5225.
+
+For arbitrary W_1 contained in W_2, equation (1) gives
+
+    D_(b,W_2) = D_(b,W_1) intersect W_2-perpendicular.         (5)
+
+The actual fixed subspace matters, not only its dimension. At n=4, b=0,
+fixing e_1 leaves only defect zero. Fixing the isotropic vector e_1+e_2
+allows defects zero and (1,1,1,1). Both constraints have dimension one.
+The latter nonzero defect is attained by T_(1,1,1,1), which fixes e_1+e_2
+but moves each of e_1 and e_2. Replacing a required fixed sum by separately
+fixed axes would impose a stronger contract.
+
+## Scope and credit
+
+This is a scoped algebraic proof. The only change from #5225 is the exact
+pointwise-fixed-subspace contract and its consequences above. The sign mask
+remains attached to the chart's columns. Setwise stabilization, unequal input
+and output restrictions and nonorthogonal charts are separate questions.
+The finite verifier corroborates the new restricted statement; it does not
+supply its all-width quantifiers or audit predecessor results.
+
+Credit Nick Petalas #5225 for the unrestricted mixed-sign image, representatives,
+cocycle and explicit literal-axis handoff; Philipp / mightyOil #1300 for the
+equal-sign phase model; Gareth Davidson #1255 for the residual C-gate phase
+and row conventions; and yssite #1558 following icekylinx #24 for the retained
+signed Gauss-normalization context. All existing notices remain unchanged.
+No external literature priority is claimed for quadratic refinements,
+transvections, subgroup fibers or their elementary restriction argument.
+
+No native producer, chart circuit, physical route, data acquisition, dirty-state
+restoration, stock, precision, fixed-tape implementation, compiler or complete
+consumer bill is constructed. Those costs remain unknown. No new kappa,
+supplier admission, selected-frontier change or complete multiplication theorem
+follows. Independent human and formal proof-kernel review are unclaimed.

research/fixed-subspace-phase-defects/README.md

@@ -0,0 +1,128 @@
+# Exact phase defects under fixed-subspace chart constraints
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with exact finite corroboration. This answers
+the literal-axis restriction question left open by merged
+[#5225](https://github.com/CrocSwap/integer-mult-bounds/pull/5225), and permits
+an arbitrary specified binary subspace W, including degenerate W.
+
+For V=F2^n, fixed sign mask b, and q_b(x)=wt(x)+2(b dot x) modulo four, let
+G_W be the orthogonal chart changes fixing W pointwise. The result is
+
+```text
+{d_b(S): S in G_W} = {e in W-perpendicular: q_b(e)=0}.
+T_e = I + e e^T lies in G_W and attains each such e.
+S = T_(d_b(S)) H, with H fixing W and preserving the phase exactly.
+```
+
+All defect fibers have equal size. For k fixed literal axes and m=n-k free
+axes, their number is
+
+```text
+N = sum_{0<=j<=m, j == wt(b_free) mod 4} binomial(m,j).
+```
+
+The exact phase-preserver subgroup has order |O(m,2)|/N. Signs on fixed axes
+do not affect this count. The all-fixed case has N=1.
+
+The actual fixed subspace matters. At n=4 with all positive signs, fixing e1
+permits only defect zero, while fixing e1+e2 permits zero and (1,1,1,1).
+These are constraints of the same dimension. [PROOF.md](PROOF.md) gives the
+all-width argument, attaining representatives, subgroup fibers and these
+specializations. This is a local algebraic result, with no new kappa.
+
+## Evidence and reproduction
+
+The standalone verifier enumerates every orthogonal matrix, subspace and
+sign mask through width five. It checks the restricted images, equal fibers,
+attaining representatives and full factorization for each admissible matrix.
+Its generated counts are:
+
+- 464 subspaces and 13,192 subspace/sign contexts;
+- 30,232 attaining representatives and 168,200 restricted factorizations;
+- 1,364 literal-axis formula contexts;
+- 777 orthogonal matrices and 749,988 literal phase comparisons.
+
+Eight controls distinguish unrestricted charts, fixed sums versus separately
+fixed axes, even weight versus phase zero, transported signs, pointwise versus
+setwise stabilization, zero versus nonzero correction, and capacity rejection.
+These finite checks corroborate the new restriction theorem. The universal
+claim rests on the proof and cited unrestricted theorem, not extrapolation.
+No predecessor executable is imported or replayed.
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/fixed-subspace-phase-defects/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/fixed-subspace-phase-defects/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fixed-subspace-phase-defects
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fixed-subspace-phase-defects --check-source-history
+```
+
+Any CPython 3.12 installation can replace the local interpreter path. The
+verifier prints `PASS_FIXED_SUBSPACE_PHASE_DEFECTS` and a generated JSON receipt
+binding all six package files by SHA256. It writes nothing. The publication
+preflight requires Git history; the direct verifier supports a Git-free export.
+
+## Scope, sources and implementation limits
+
+The base is canonical main de5ec2e7a6074068452f45b1a191b5c72832df4a, priority
+revision 8. [TASK.json](TASK.json) changes the `bit-helper-contract` card to
+this algebraic side result, because #5225 explicitly leaves this route constraint
+open. The card's current selected-binding first step passed. It is metadata
+orientation, not a selected supplier replay. [SOURCES.json](SOURCES.json) pins
+the predecessor proof and README as provenance, alongside the selected record
+and catalogue. They are not runtime inputs to the new verifier.
+
+The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214412)
+followed live open/account PR and Discussion checks, local reservation and
+distinctive main/merged searches. The overlap cache completely paginated 416
+open PRs and 5,307 Discussion records. Sparse local coverage searched 185 of
+7,845 tracked notes; targeted all-main README and merged-PR searches supplemented
+it. Unpublished work and arbitrary historical diffs remain outside that coverage.
+No search establishes external mathematical priority.
+
+The new verifier is bounded at widths 1..5, at most 720 complete matrices,
+374 subspaces and 32 vectors in one width. It has no recursion, subprocesses,
+network, dynamic code or shared mutable state. All functions stay below 60
+physical lines. Explicit exceptions retain the checks under optimized Python;
+both registered commands treat warnings as errors. No additional static analyzer
+is configured or claimed. The only file reads are the six local receipt inputs.
+
+Power of Ten rule 3 deviation: CPython allocates integers and containers during
+finite enumeration. The enforced width bound limits each subspace to 32 vectors,
+the subspace inventory to 374 entries, the group inventory to 720 entries and
+the sign/defect table to 32 by 720 integers. No fixed-allocation claim is made.
+Normal and optimized complete finite replays exercise this domain. Any executable
+width expansion requires a fresh capacity review; the written theorem has no
+such finite-width restriction.
+
+The contract fixes W pointwise and retains orthogonal charts and a fixed sign
+mask. Setwise stabilization and nonorthogonal charts are outside scope. No native
+producer, chart circuit, physical route, acquisition, dirty restoration, stock,
+precision, tape implementation, compiler or complete consumer bill is supplied.
+Those costs remain unknown. No supplier admission, selected-frontier change or
+complete multiplication theorem follows. Lean, Docker and selected scientific
+cold replay were not run. Independent human and formal proof-kernel review are
+unclaimed.
+
+## Open next questions
+
+Can a named native helper exploit one nonzero admissible defect while preserving
+its required literal directions? Start with its actual fixed subspace W and
+sign mask b, and price the T_e chart change with all acquisition, transport and
+restoration costs. Algebraic attainability supplies none of those prices. This
+question is unclaimed here; no further construction expansion is justified by
+this package alone.
+
+## Credit
+
+Nick Petalas #5225 supplies the unrestricted mixed-sign theorem and explicit
+fixed-axis question. Philipp / mightyOil #1300 supplies the equal-sign phase
+model, Gareth Davidson #1255 the residual C-gate contract and row convention,
+and yssite #1558 following icekylinx #24 the signed Gauss-normalization context.
+Credit Rohan Arun, Jeremy Kothe, Hao Yan, Josie Elliston, Douglas Colkitt and the
+retained Clifford/normalization lineage. Classical quadratic refinements,
+transvections and subgroup-fiber arguments retain their classical status.
+All predecessor notices remain unchanged.

research/fixed-subspace-phase-defects/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/mixed-sign-phase-spectrum/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "52457e2cdf873ad649dde6142542840a1e7f2776",
+      "sha256": "cdfc423adaf8623cb9e2d61a9d18aca97e75604d2ab1e9360bdc4e15433a57f9"
+    },
+    {
+      "path": "research/mixed-sign-phase-spectrum/README.md",
+      "usage": "provenance",
+      "git_blob": "19a7b6b1c6b235f12e46f8b1f327d57c7dfe7f2b",
+      "sha256": "2ef5f8bd5d543a2910a3e2cff022add0283a869ff625ddf8c4ecd7b42f8f4472"
+    }
+  ]
+}

research/fixed-subspace-phase-defects/TASK.json

@@ -0,0 +1,93 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "bit-helper-contract",
+    "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "research/g20-helper-split/README.md",
+      "research/g20-conjugation-admission/README.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "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",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "G20",
+      "helper split",
+      "5679",
+      "5708",
+      "independent target"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact mixed-sign orthogonal phase-defect image for chart changes fixing an arbitrary binary subspace pointwise, with attaining transvections, equal fibers and the literal-axis closed count.",
+  "scope_change_reason": "Merged PR5225 explicitly leaves fixed literal axes open. This proves that missing route-constraint lemma, generalized to arbitrary specified subspaces, rather than auditing the unrestricted theorem or constructing a BIT supplier.",
+  "bottleneck_link": "A constrained signed chart can preserve required directions exactly when its defect lies in the proved restricted image. This is an algebraic interface side result; physical synthesis, transport, restoration and complete supplier costs remain unknown.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first verified restricted-image theorem and its literal-axis specialization; do not extend to physical synthesis or new parameter searches.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the all-width restricted image and equal fibers. The standalone verifier covers every subspace/sign context through width five, with 13192 contexts, 30232 attaining representatives, 168200 factorizations and eight controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a named native helper exploit an admissible constrained defect at a lower complete physical cost?",
+      "why_it_matters": "An algebraically legal chart change may still cost more than its benefit.",
+      "first_step": "Bind its exact fixed subspace and signs, then price one explicit T_e chart including acquisition, transport and restoration.",
+      "blocked_by": "No physical chart program, native consumer or complete cost ledger is supplied."
+    }
+  ],
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214412",
+    "checked_main": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+    "priority_revision": 8,
+    "overlap_open_prs": 416,
+    "overlap_discussion_records": 5307,
+    "complete_remote_pagination": true,
+    "sparse_local_notes": 185,
+    "tracked_notes": 7845,
+    "limits": "Targeted main README and merged searches supplement incomplete sparse local coverage. Unpublished work and arbitrary historical diffs are not covered."
+  },
+  "predecessor": {
+    "pr": 5225,
+    "head": "350b7408b11161aa153b5ab74c51fb1881909389",
+    "usage": "Cited unrestricted theorem and explicit open question; no executable imports or audit."
+  }
+}