Prove binary deficiency-two spectral completion (no new κ)

research/symplectic-binary-completion/README.md

@@ -0,0 +1,246 @@
+# Binary deficiency-two symplectic spread completion
+
+This contribution was produced by Nick Petalas. Independent human and formal
+proof-kernel review are unclaimed.
+
+## Result and scope
+
+Claim type: scoped written mathematical proof, with exact finite corroboration.
+
+Let n >= 1, and let S consist of 2^n - 1 pairwise trivially intersecting
+Lagrangian subspaces of a nondegenerate alternating 2n-dimensional F2-space.
+A symplectic spread has 2^n + 1 members, so S has deficiency two.
+
+Let Gamma have the uncovered nonzero vectors as vertices. Over F2 these are
+also the uncovered projective points. Two distinct vertices are adjacent
+exactly when their symplectic pairing is one. Write A for the ordinary integer
+adjacency matrix, and put
+
+$$
+N=2(2^n-1),\qquad k=2^{n-1},\qquad Q=kI_N+A.
+$$
+
+Then S extends to a full symplectic spread if and only if Q is singular over
+the rationals. When Q is singular, Gamma is connected and bipartite, Q has
+nullity one, and every nonzero rational kernel vector has two nonzero opposite
+constant values. Its two sign classes are exactly the nonzero vectors of the
+two missing Lagrangians. The unordered completion pair is unique. If Q is
+nonsingular, it is positive definite over the reals and S has no completion.
+
+This answers Open next question 1 in Nick Petalas's
+[odd-field spectral criterion, PR #5248](https://github.com/CrocSwap/integer-mult-bounds/pull/5248).
+That theorem covers q >= 3 and leaves the binary case open because its graph
+order argument fails there. Its proof and verifier are cited, not audited or
+replayed. The new step here is a geometric component lemma using the span of a
+color class. David Ganz's [atlas B098, PR #2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849)
+supplies the original deficiency-two question and its deficiency-one predecessor.
+The signless-Laplacian identity and basic symplectic dimension facts are
+classical. Global literature priority is unclaimed.
+
+This is an algebraic side result, recorded as a changed scope of the
+`formal-interface-lemma` card. It supplies a precise completion interface for
+the atlas. It does not change a supplier, COPY bill, kappa or selected result,
+and it does not prove a complete multiplication theorem.
+
+## Proof
+
+### Hole count and degree
+
+A Lagrangian has 2^n - 1 nonzero vectors. The old members have disjoint nonzero
+sets, so the number of uncovered vectors is
+
+$$
+2^{2n}-1-(2^n-1)^2=2(2^n-1)=N.
+$$
+
+Fix a hole h. For each old Lagrangian L, the functional omega(h,-) on L is
+nonzero. Otherwise h would belong to L-perp = L, contrary to being uncovered.
+Thus exactly 2^(n-1) vectors of L pair to one with h. There are 2^(2n-1) vectors
+in the whole ambient space pairing to one with h. Subtracting the old members
+gives
+
+$$
+\deg_\Gamma(h)=2^{2n-1}-(2^n-1)2^{n-1}=2^{n-1}=k.
+$$
+
+Alternation excludes loops. Therefore Gamma is a simple k-regular graph with
+k > 0.
+
+### The new geometric component lemma
+
+Suppose C is a connected bipartite component, with color classes X and Y.
+Every vertex in X has k distinct neighbors in Y, and conversely, so both color
+classes contain at least k = 2^(n-1) points.
+
+Points in X pair to zero with each other because there are no edges within a
+color class. Their linear span L is isotropic and has dimension at most n.
+An F2-subspace of dimension at most n - 1 has at most 2^(n-1) - 1 nonzero
+vectors, fewer than |X|. Hence dim L = n and L is Lagrangian.
+
+Every hole outside C is orthogonal to every member of X, since an edge would
+put it in C. It therefore lies in L-perp = L. All holes outside C consequently
+pair to zero with one another. They have no edges to C either. Such a vertex
+would have degree zero, contradicting k > 0. There are no holes outside C.
+
+Thus any bipartite component is the whole hole graph. This argument uses the
+symplectic geometry rather than a bound on N/k. In the binary case N = 4k - 2,
+which exceeds the earlier N <= 3k gate when n >= 3.
+
+### Spectral decision and recovery
+
+For every real vector z indexed by the holes,
+
+$$
+z^TQz=\sum_{\{u,v\}\in E(\Gamma)}(z_u+z_v)^2.
+$$
+
+Thus Q is positive semidefinite. Its kernel consists exactly of assignments
+satisfying z_u = -z_v on each edge. On a connected component these assignments
+are determined by one value. An odd cycle forces that value to zero, whereas
+a bipartite component admits the opposite constants on its two color classes.
+Consequently Q is singular if and only if at least one component is bipartite.
+
+The geometric lemma makes that component the whole graph. The kernel is
+one-dimensional. Because Q has integer entries, its nonzero real kernel has a
+nonzero rational vector. Its entries have equal nonzero magnitude and their
+signs recover the unique bipartition X,Y, up to swapping the classes.
+
+Counting edges on either side gives k|X| = k|Y|, and hence
+
+$$
+|X|=|Y|=N/2=2^n-1.
+$$
+
+Each class is pairwise orthogonal and therefore spans an isotropic subspace.
+Its cardinality forces that span to have dimension n and forces the class to
+be its entire nonzero set. These two Lagrangians meet trivially because their
+full nonzero sets are disjoint. They meet every old member trivially because
+they contain only holes. Adding them completes S.
+
+Conversely, a completion partitions all holes into the nonzero sets of two
+Lagrangians. There are no edges within either set, so Gamma is bipartite and
+Q is singular. A connected bipartite graph has only one unordered bipartition,
+which proves uniqueness of the completion pair. Nonsingularity of the positive
+semidefinite Q gives positive definiteness and excludes a completion.
+
+## Exact finite evidence
+
+The standalone verifier constructs four binary models using F_(2^n)^2 and
+
+$$
+\omega((x,y),(x',y'))=\operatorname{Tr}_{F_{2^n}/F_2}(xy'+x'y).
+$$
+
+For n = 1,2,3,4, the field polynomials are respectively X+1, X^2+X+1,
+X^3+X+1 and X^4+X+1. Multiplication permutations certify the finite field
+models. The checker verifies alternation and nondegeneracy directly. It uses
+the old Lagrangians y = ax for every nonzero a, omitting y = 0 and x = 0.
+Every old member is checked for binary linear closure, isotropy and disjointness.
+
+Rational RREF and separate integer Bareiss elimination compute the kernel and
+determinant. A second search enumerates every isotropic subspace whose full
+nonzero set lies among the holes, without using the graph or its spectrum.
+It enumerates every possible completion pair and compares it with sign recovery.
+
+| Ambient F2 dimension | Old members | Holes | Degree | Rank Q | det Q | Hole Lagrangians | Completion pairs |
+|---|---:|---:|---:|---:|---:|---:|---:|
+| 2 | 1 | 2 | 1 | 1 | 0 | 2 | 1 |
+| 4 | 3 | 6 | 2 | 5 | 0 | 2 | 1 |
+| 6 | 7 | 14 | 4 | 13 | 0 | 2 | 1 |
+| 8 | 15 | 30 | 8 | 29 | 0 | 2 | 1 |
+
+The controls reject three invalid partial spreads: wrong deficiency, duplicated
+members and a nonisotropic member. A separate abstract graph is K4,4 disjoint
+from K6 with a perfect matching removed. It has N = 14 and k = 4, exactly the
+binary n = 3 parameters, and a singular Q whose unique kernel has six zero
+entries. Its bipartite component is not the whole graph. The new geometric
+lemma excludes its realization as a valid hole graph. It is an abstract
+control, not a symplectic counterexample.
+
+The connected 14-vertex circulant with steps +/-1 and +/-2 supplies a
+nonbipartite spectral control. Its rational kernel is trivial and its integer
+determinant is 49,760,288. No claim that this graph is a hole graph is made.
+These controls distinguish generic regular-graph facts from the geometric
+implication proved here.
+
+## Reproduction
+
+From the repository root, use CPython 3.12. No third-party packages, predecessor
+verifier, subprocess or network is needed for the mathematical check.
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/symplectic-binary-completion/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/symplectic-binary-completion/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/symplectic-binary-completion
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/symplectic-binary-completion --check-source-history
+```
+
+The direct check prints `PASS_SYMPLECTIC_BINARY_COMPLETION` and the exact
+fixture/control values above. Optional `--receipt /absolute/path/outside-checkout/receipt.json`
+writes a generated receipt containing those results, the interpreter version
+and SHA256 hashes of all five package files. Receipt paths inside the checkout
+are rejected. No receipt is handwritten or committed.
+
+`SOURCES.json` pins the original card, selected-record context and both written
+predecessors as provenance. The mathematical verifier neither imports nor
+replays those predecessors. Hosted CI execution is recorded separately in the
+PR body. Local CPython 3.12.15 normal and optimized checks pass, as do the
+registered replay, syntax check and receipt-path rejection controls. The written
+all-dimension proof is not machine checked.
+
+## Limits and implementation bounds
+
+The theorem covers q = 2 and every n >= 1. The executable controls cover only
+the four specified punctured field spreads and the listed abstract/invalid
+controls. They are not a classification of binary partial spreads. No valid
+noncompletable binary deficiency-two fixture is supplied. In particular, this
+criterion does not assert that every binary deficiency-two partial spread
+completes. Larger deficiencies and nonisotropic partial spreads are outside scope.
+
+The linear algebra is over the rationals and integers, even though the geometry
+is binary. Reducing Q modulo two is not the decision procedure. The algorithm
+is polynomial in the explicit hole inventory, not in n. No proof-assistant
+build, supplier replay or independent human proof review was run. The selected
+construction's five framework assumptions are unaffected.
+
+The verifier has no recursion or dynamic code evaluation. Finite models have
+at most 256 ambient vectors, 30 holes and 30-by-30 matrices. Span enumeration
+is bounded by four rounds and a checked capacity of 4,096 stored subspaces;
+each subspace has at most 16 vectors. All functions are under 60 physical lines.
+Python and Fraction allocate dynamically, a managed-runtime deviation from
+fixed allocation. Explicit finite input sizes bound this work. Runtime checks
+remain enabled under optimized Python. The only indirect call is the bounded
+invalid-input control callback. No shared source or validation policy is changed.
+
+## Open next questions
+
+1. Can the binary criterion be simplified to unconditional completion, or is
+   there a binary deficiency-two noncompletable example? This distinguishes a
+   recognition theorem from an existence theorem. Start with a literature-bound
+   construction or a bounded search at one specified n. A failed finite search
+   would not prove all-dimension completion; no such conclusion is claimed here.
+2. At deficiency at least three, what geometric replacement for two-color
+   recovery can identify the missing Lagrangians? Begin with the hole degree
+   and one literal deficiency-three fixture. The signless kernel argument here
+   only recognizes two color classes and does not settle that question.
+
+## Provenance and overlap
+
+Base: `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8.
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213513)
+records the binary question and source pins. The selected-baseline command was
+run after materializing its omitted sparse inputs. It authenticates metadata,
+not the selected mathematics.
+
+Live open PRs, recent account PRs, handoffs, active Discussions, local question
+reservations, targeted merged searches and main-tree README searches were
+checked before claiming. The `formal-interface-lemma` overlap report includes
+remote pagination and explicitly incomplete sparse local-note coverage.
+The same-account predecessor #5248 was published October 23, outside the last
+24 hours. None of its mathematical checks was rerun. No global novelty or
+exhaustive unpublished-work coverage is claimed.
+
+Credit David Ganz for atlas B098 and the deficiency-two proposal, and Nick
+Petalas for #5248's odd-field criterion and explicit binary question. The new
+geometric component argument and binary extension are the contribution here.
+All predecessor files and credit lines remain unchanged. Apache-2.0.

research/symplectic-binary-completion/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/pure-math-atlas-400/volumes/02-geometry.md",
+      "usage": "provenance",
+      "git_blob": "baef1e69c08c7cbd4dfd020862870fa5161afc86",
+      "sha256": "39fc97bdfa29337b79d1308e35df41e867ce2102d44755fd407aa09ff8352b39"
+    },
+    {
+      "path": "research/symplectic-deficiency-two-spectral/README.md",
+      "usage": "provenance",
+      "git_blob": "0de39befd926911522462f8209221fe95c432757",
+      "sha256": "6c03ec34d9d58d97e12ba56b9c19063888e75ec09fccf1fa7b031f18c905c9d8"
+    }
+  ]
+}

research/symplectic-binary-completion/TASK.json

@@ -0,0 +1,102 @@
+{
+  "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 rational signless-Laplacian completion criterion for binary deficiency-two symplectic partial spreads in every dimension.",
+  "scope_change_reason": "The assignment requires an original result rather than an audit. This takes the explicit binary open question in PR5248, building on David Ganz atlas B098, as an algebraic side result rather than a selected-supplier formalization.",
+  "bottleneck_link": "Algebraic side result for the atlas completion interface. No supplier, kappa or selected-frontier improvement is claimed.",
+  "budget_minutes": 60,
+  "stop_rule": "Package the first proved binary extension; do not extend it to higher deficiency or a classification.",
+  "outcome": "completed",
+  "evidence": "Written all-dimension proof and standalone exact controls for n=1,2,3,4; unique sign recovery independently compared with exhaustive hole-subspace completion search; invalid-input and abstract spectral controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does every binary deficiency-two symplectic partial spread complete, or is there a nonsingular-Q example?",
+      "why_it_matters": "Distinguishes recognition from unconditional existence.",
+      "first_step": "Locate a source-bound example or search a single specified binary dimension.",
+      "blocked_by": "No all-dimension existence argument or valid negative fixture is supplied."
+    },
+    {
+      "question": "Can a geometric invariant recover missing Lagrangians at deficiency at least three?",
+      "why_it_matters": "The two-color kernel criterion addresses only deficiency two.",
+      "first_step": "Derive the hole degree and test one literal deficiency-three fixture.",
+      "blocked_by": "No higher-color recovery implication is proved here."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213513"
+}