Prove exact four-versus-five rank-three completion (no κ)

research/rank-three-closed-completion/PROOF.md

@@ -0,0 +1,119 @@
+# Exact rank-three alternating completion criterion
+
+This proof and its finite corroboration were produced by Nick Petalas.
+Apache-2.0.
+
+## Statement and credited inputs
+
+Let V be a finite nondegenerate symplectic vector space over F2 with pairing
+w. Let h:U -> V be an injective linear isometry. Write d=h+I,
+K=ker d, D=d(U), and
+
+    b(d(u),d(v)) = w(u,d(v)).
+
+Assume dim D=3 and b is alternating of rank two. Its radical R has
+dimension one. Set U_R=d^-1(R), a subspace of U. All sums and inverse
+images refer to the given V. Spectators required to remain fixed belong
+to U with h(v)=v. Let L(h) be the minimum number of nonzero-axis
+transvections in a symplectic extension of h in V.
+
+**Theorem.** If U_R is contained in K+D, then L(h)=5. Otherwise L(h)=4.
+Moreover, every four-turn extension in this setting has four linearly
+independent, pairwise orthogonal axes.
+
+The new result is the closed-case lower bound and the necessary commuting
+structure. Ali Romman's [#6525](https://github.com/CrocSwap/integer-mult-bounds/pull/6525)
+already proves 4<=L(h)<=5 and constructs four turns when U_R is not
+contained in K+D. Those constructive upper bounds are used as premises;
+they are not reconstructed or audited here. Its r=3 five-turn fixture
+was already known. The new theorem treats every such contract in every
+ambient dimension, rather than just that fixture. Its r>=4 closed case
+remains open and can attain the lower endpoint.
+
+Krzysztof Wojt's #5097 supplies the general displacement-plus-nullity
+bound. Nick Petalas's #5085/#6494, Brian / JoyboyBrian's #5051 and the
+native/compiler lineage retained in #6525 supply the earlier problem
+and constructions. The following lower-bound argument is self-contained.
+Wall forms and binary quadratic forms are classical mathematics; no
+literature-priority claim is made.
+
+## 1. Full displacement and its form
+
+For any symplectic extension S of h, put W=im(S+I). Symplecticity gives
+
+    ker(S+I) = W-perp.
+
+For example, w(v,(S+I)x)=w((S^-1+I)v,x), so orthogonality to W is
+equivalent to S(v)=v. Thus the form
+
+    B((S+I)v,z) = w(v,z),     z in W,
+
+is well-defined and nonsingular. If its left radical contained (S+I)v,
+then v would be in W-perp and its displacement would vanish. Also
+
+    B(x,y)+B(y,x)=w(x,y),     B restricted to D equals b.       (1)
+
+The first identity follows by expanding w(Sv,Su)=w(v,u); the second
+follows from S|U=h. Since b is singular and D has dimension three,
+W cannot equal D. Hence dim W>=4.
+
+A product of t transvections has displacement image contained in the
+span of its t axes. Therefore L(h)>=4. If four turns extend h, their
+axes a1,...,a4 are independent and W is exactly their span.
+
+In execution order, write the intermediate update at turn i as c_i a_i.
+For input v the coefficients obey
+
+    c_i = w(v,a_i) + sum_(j<i) c_j w(a_j,a_i).
+
+The coefficient transformation is triangular with diagonal one. Since
+the axes are independent and V is nondegenerate, the four functionals
+w(-,a_i) are independent, so these coefficients range over F2^4.
+Consequently the matrix of B in the axis basis is upper triangular with
+diagonal one. In particular, the quadratic form q(x)=B(x,x) satisfies
+
+    q(a_i)=1 for every i,     q|D=0,     polar(q)=w|W.          (2)
+
+Thus the vectors with q=1 span W.
+
+## 2. A four-dimensional quadratic obstruction
+
+Let q be a quadratic form on a four-dimensional binary space W, vanishing
+on a three-dimensional subspace D. Suppose its polar form p is nonzero.
+Since D is isotropic of codimension one, p has rank two. Its radical Z
+has dimension two and lies in D. In particular q|Z=0.
+
+The form descends to W/Z, a nondegenerate two-dimensional quadratic
+space. D/Z is a nonzero singular line, so this is the split plane. In
+a suitable basis its form is xy. Over F2 it has exactly one vector
+with value one. Therefore {x:q(x)=1} is one coset of Z in W and spans
+only a three-dimensional subspace. It cannot span W.
+
+Apply this to (2). The anisotropic vectors do span W, so p=0. By (1),
+W is totally isotropic. In particular the four axes commute. This proves
+the extra assertion without assuming any special source coordinates.
+
+## 3. Closed radical lifts contradict four turns
+
+Let 0!=z in R. If U_R is contained in K+D, choose a lift u in U with
+d(u)=z and write u=k+x with k in K and x in D. The extension fixes k.
+Total isotropy gives W contained in W-perp=ker(S+I), and x is in D
+contained in W. Hence S fixes x as well. It fixes u, contradicting
+(S+I)u=d(u)=z!=0.
+
+No four-turn extension exists in the closed case. Together with the
+credited upper bound five this gives L(h)=5. In the escaping case the
+credited four-turn construction attains the lower bound from section 1.
+
+## Scope
+
+This is an unsigned binary label-word theorem with fixed prescribed
+spectators and no ambient enlargement. It does not price Gaussian rank,
+sign or absolute-phase corrections, physical routing, owner cleanup,
+precision, stock, tape, compiler closure or outer recursion. The five
+selected assumptions remain. It supplies no multiplier or new kappa.
+Independent human and formal proof-kernel acceptance are unclaimed.
+
+The verifier checks the new quadratic obstruction and all independent
+four-turn Gram topologies by exact finite arithmetic. It does not certify
+the written arbitrary-dimension proof or replay the credited upper bounds.

research/rank-three-closed-completion/README.md

@@ -0,0 +1,123 @@
+# Exact rank-three alternating completion criterion
+
+Scoped written proof with exact finite corroboration, produced by Nick Petalas.
+
+For a partial binary symplectic isometry h:U -> V, put d=h+I, K=ker d,
+D=d(U), and b(d(u),d(v))=w(u,d(v)). Suppose dim D=3 and b is alternating
+of rank two. Set R=rad b and U_R=d^-1(R). Then the exact unsigned
+transvection minimum in the original ambient space is
+
+    L(h) = 5 if U_R is contained in K+D, and 4 otherwise.
+
+Every four-turn extension necessarily has independent, commuting axes.
+The new [proof](PROOF.md) excludes four turns for every closed contract,
+in every ambient dimension. It settles the r=3 portion of Open next
+question 1 in Ali Romman's [#6525](https://github.com/CrocSwap/integer-mult-bounds/pull/6525).
+That source already supplies the general interval [4,5], the escaping-lift
+four-turn construction and one closed five-turn example. Those are credited
+inputs, not new constructions or audit deliverables. No predecessor
+scientific verifier or numerical receipt is replayed.
+
+The proof uses the quadratic form of a hypothetical four-turn completion.
+A totally singular hyperplane in a four-dimensional binary quadratic space
+with nonzero polar form prevents its anisotropic vectors from spanning.
+Four independent turn axes must span and each has quadratic value one.
+Thus their displacement space is totally isotropic. The completion fixes
+that entire image, which contradicts a nonzero closed radical lift.
+
+## Exact finite evidence
+
+[verify.py](verify.py) enumerates the new obstruction's finite coefficient
+model, without rerunning the known five-turn fixture:
+
+- All 1,024 four-dimensional binary quadratic forms and their 15 hyperplanes.
+  There are 240 totally singular form/hyperplane pairs. All 210 with nonzero
+  polar form have polar rank two and anisotropic span dimension three.
+- All 64 ordered independent four-axis Gram topologies, each realized by a
+  literal chronological word on an eight-dimensional symplectic space.
+  All 16,384 input vectors pass displacement and inverse checks; 65,536
+  Wall basis equalities agree with a separate triangular formula.
+- All 960 topology/hyperplane restrictions. Exactly one canonical pair has
+  alternating residual rank two. Its axes commute and all 16 radical lifts
+  escape K+D. This counts coefficient-model pairs, not all partial isometries.
+- The 180 nonalternating rank-two restrictions with closed left-radical lifts
+  show that alternation is essential. All 256 single-turn omissions damage
+  their whole endpoints. A changed Wall diagonal and zero axis reject for
+  their specific intended reasons.
+
+[RESULT.json](RESULT.json) is generated from these enumerations and binds
+six package sources by SHA256. Default replay recomputes and compares it.
+The written proof supplies the arbitrary-dimension conclusion; finite checks
+corroborate it. The credited upper bounds are mathematical premises, not
+independently certified by this verifier.
+
+## Reproduce
+
+CPython 3.12 and its standard library suffice. From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/rank-three-closed-completion/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/rank-three-closed-completion/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rank-three-closed-completion
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rank-three-closed-completion --check-source-history
+```
+
+Both direct modes print `PASS_RANK_THREE_CLOSED_COMPLETION`. Each registered
+command has a 120-second bound. The standalone verifier needs only this
+package, without Git, network or predecessor executables. After a deliberate
+source edit, `verify.py --write-report` regenerates the receipt only after
+all enumerations and controls succeed.
+
+Base e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8,
+selected #7000. The card's selected-binding orientation passed. Live overlap
+and main searches checked the rank-three, closed, alternating and radical-lift
+formulations and the general completion question. The overlap snapshot covered
+558 open PRs, 7,223 Discussion records and all 10,178 tracked top-level package
+notes at that base. Nested diffs and unpublished work remain outside that
+coverage. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19542394).
+
+## Limits and implementation bounds
+
+Only the closed-case lower bound and commuting necessity are new. Exact
+attainment uses #6525's cited upper bounds. The theorem is binary and fixes
+displacement rank three. Prescribed fixed spectators belong in U. No ambient
+enlargement, signed Gaussian realization, physical costs, owner cleanup,
+precision, stock, tape, compiler closure or outer admission is supplied.
+The five selected assumptions remain. No new kappa or selected-frontier
+change is claimed. Lean, Docker and the selected cold replay are not run.
+Independent human and formal proof-kernel review are unclaimed.
+
+There is no recursion or unbounded search. The largest outer census has
+1,024 forms; words have four axes, coefficient spaces have 16 elements,
+literal spaces have 256 elements and all nested loops have those fixed
+bounds. Functions fit within 60 lines. Explicit exceptions remain active
+under optimized Python. Managed Python allocations are a documented deviation
+from fixed-allocation execution; live collections have the bounds above.
+Warning-strict normal and optimized execution and source compilation provide
+diagnostics. No static type checker is a declared dependency. Explicit
+`--write-report` is the verifier's only mutation.
+
+## Open next questions
+
+1. Classify the alternating closed case at displacement rank four and above.
+   The quadratic obstruction here no longer applies directly; #6525 already
+   gives a closed r=4 contract attaining six turns. Start with minimal Wall
+   extensions containing a totally singular subspace of codimension two,
+   retaining the prescribed radical-lift action. A complete criterion and
+   constructive attaining words are missing.
+2. Bind a qualifying partial contract to an actual signed native contact.
+   State its source, fixed spectators and phase anchor, then price every
+   turn, sign correction and physical operation. A short unsigned word alone
+   gives no recursive supplier improvement.
+
+## Credit
+
+The new lower-bound proof and verifier were produced by Nick Petalas.
+Ali Romman #6525 supplies the question, interval, escaping construction and
+known fixtures. Krzysztof Wojt #5097 supplies the general lower bound and
+zero-form completion; Nick Petalas #5085/#6494 supplies earlier residual-form
+and rank-one work; Brian / JoyboyBrian #5051 supplies signed partial-contract
+compatibility. Credit also David Ganz / Dugongue #4841, Cao Yifan / intqwq,
+Cinna Davis, zxv, Jacob Alan Sussman and the native/compiler lineage retained
+by those sources. Wall forms and binary quadratic forms are classical;
+no literature-priority claim is made. New work is Apache-2.0.

research/rank-three-closed-completion/RESULT.json

@@ -0,0 +1,46 @@
+{
+  "claim_type": "scoped written proof with exact finite corroboration",
+  "failure_controls": 2,
+  "quadratic_census": {
+    "hyperplanes_per_form": 15,
+    "nonzero_polar_pairs": 210,
+    "quadratic_forms": 1024,
+    "totally_singular_pairs": 240
+  },
+  "schema_version": 1,
+  "source_sha256": {
+    "PROOF.md": "76a9d6940954e1713daa69d51ec7f2cc5bd2832f5609cb287db553552875638b",
+    "README.md": "deedfdd99861da222b810b0d003eeb4e75fd8b6269aa8b564f951afd4fd5bbf7",
+    "SOURCES.json": "24ec60eb76794700e5551259beead67ab40e3195426b162feca7d5be349126d3",
+    "TASK.json": "c6ee382f3088b8c1b2e5d9a0b58781ecfd0ff39a9ee767577a972fc98aa525be",
+    "VERIFY.json": "84376ae6324d6688129491c0b26f779a2cb3c4c7ab3ac692fa5ef6169596be5f",
+    "verify.py": "6b8bf3627a10826a14d8c38fc74f66be1b21970a25d29a9af62bd52339a9d23a"
+  },
+  "word_census": {
+    "counts": {
+      "alternating_rank_two_contracts": 1,
+      "escaping_radical_lifts": 16,
+      "gram_topologies": 64,
+      "hyperplane_restrictions": 960,
+      "literal_input_vectors": 16384,
+      "nonalternating_closed_controls": 180,
+      "omitted_turn_controls": 256,
+      "wall_basis_equalities": 65536
+    },
+    "nonalternating_control": {
+      "axes": [
+        1,
+        18,
+        20,
+        8
+      ],
+      "gram_code": 3,
+      "hyperplane_mask": 6,
+      "restricted_rows": [
+        1,
+        0,
+        4
+      ]
+    }
+  }
+}

research/rank-three-closed-completion/SOURCES.json

@@ -0,0 +1,44 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/rank-two-residual-completion/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "5a39770f196692268ba17dfcc4a01cbfe5f7fc40",
+      "sha256": "9e8b66ca71656833e47ea78635bb46f195076fef33cf26cefabac897256dd19f"
+    },
+    {
+      "path": "research/rank-two-residual-completion/README.md",
+      "usage": "provenance",
+      "git_blob": "8008576fd96f1cb925d5ebb990fa2a58a6a75628",
+      "sha256": "b9ff73eb40d38453312a1e5d1f5b0580314173f273bccb355c32019301d7c1af"
+    },
+    {
+      "path": "research/singular-rank-two-pauli/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c8ffbe676f33e14105c188959e47d8aafeaaae3e",
+      "sha256": "bc43da28cf432e370532cdeb1622ce8efb175d497fe83b632d8560fd27c20a5b"
+    }
+  ],
+  "bibliographic_predecessors": [
+    {
+      "pr": 6525,
+      "author": "aliromman",
+      "head": "9797b952ee174f845f682b1a121600416f5c7bd1",
+      "role": "General interval and escaping upper bound; open closed-case question. No predecessor executable replayed."
+    }
+  ]
+}