Prove the first central Schur state collision at pivot size four (no κ)

research/schur-central-alias/PROOF.md

@@ -0,0 +1,131 @@
+# The first central-class alias for sharp nilpotent Schur states
+
+Work over any field of characteristic two. The ordered pair matters: the
+state equivalence is simultaneous conjugacy of S and T, without exchanging
+the two requests. Put K=S+T and Z=K^2.
+
+## Contract and credited premises
+
+Start with commuting idempotents P0,Q0, a size-d common identity pivot,
+and sharp residuals rank(ST-TS)=2d. The compressed product is the nilpotent
+matrix H. Fix the four ordered original sector dimensions r00,r10,r01,r11.
+Let a=dim ker H. The nilpotent normal form and its whole-pair rigidity are
+Malik Safwan / ssafwann's #5267, not new claims here. They require
+
+    r00=d+s00, r10=d+s10, r01=d+s01, r11=d+a+s11,
+
+with nonnegative padding. The minimal residual acts on U^3 plus F^a:
+
+    S(x,y,z,t)=(H(x+z)+Nt, 0, (I+H)(z+x)+Nt, t),
+    T(x,y,z,t)=(0, H(y+z)+Nt, (I+H)(z+y)+Nt, t).
+
+Here im N complements im H. Add scalar pairs (0,0), (1,0), (0,1), (1,1)
+with multiplicities s00,s10,s01,s11. All those statements, including
+admissibility as genuine Schur residuals, are the cited predecessor model.
+Ali Romman's #5287 already determines the complete central Jordan class,
+and Mihir Srivastava's #5360 supplies the general-H ordered gluing theorem.
+No predecessor scientific verifier is used as this contribution's evidence.
+
+The new result is the first same-profile central-class alias, its sharp
+minimum dimension, and the explicit ordered-state separator below. It is
+an obstruction to an ordered-state registry using only the central class.
+It does not contradict a classifier whose declared output is only Z.
+
+## Rank information retained and discarded
+
+Write W=I+H. It is invertible. In coordinates
+u=x+y, v=y+z, w=z, t, the minimal K is
+
+    K(u,v,w,t)=(Hu, Wu+Hv+Nt, Wu, 0).
+
+For every j>=1, its jth power is
+
+    (H^j u,
+     (j mod 2) W H^(j-1)u + H^j v + H^(j-1)Nt,
+     W H^(j-1)u,
+     0).
+
+This follows by multiplying once and induction; no division by two occurs.
+The u-column image is a graph over W im H^(j-1), so has dimension
+rank H^(j-1). Its intersection with the v,t-column image is zero: a zero
+w component forces H^(j-1)u=0 and then every u contribution is zero.
+The v,t-column image has dimension rank H^(j-1), because
+
+    im H^j + im H^(j-1)N = H^(j-1)(im H + im N) = im H^(j-1).
+
+The padding contributes c=s10+s01 to every positive power rank. Therefore
+
+    rank K^j = 2 rank H^(j-1) + c,                   (1)
+    rank Z^j = 2 rank H^(2j-1) + c.                  (2)
+
+Equation (2) is also a rank-sequence restatement of #5287's credited
+characteristic-two Jordan law. At fixed d and fixed original profile, c
+and the total residual dimension are fixed. The multiplicity of eigenvalue
+one is c and all other central blocks are nilpotent. Thus two such central
+classes agree exactly when all odd positive power ranks of H agree.
+In contrast, (1) retains every power rank of H. Nilpotent similarity is
+determined by all power ranks. The normal-form rigidity supplies the converse
+for full ordered pairs with the same H similarity class and profile.
+
+## The collision
+
+Take d=4, original profile (4,4,4,6), and no padding. Compare
+
+    H_A=J3(0) direct-sum J1(0),     H_B=J2(0) direct-sum J2(0).
+
+Both have a=2 and rank H=2. Every odd power of order at least three is zero.
+Hence both fourteen-dimensional central operators have ranks
+
+    rank Z=4, rank Z^2=0,
+
+and full Jordan partition (2,2,2,2,1,1,1,1,1,1).
+A complete central similarity class, rather than just its spectrum, aliases.
+However rank H_A^2=1 and rank H_B^2=0. Equation (1) gives
+
+    rank (S_A+T_A)^3=2,     rank (S_B+T_B)^3=0.
+
+Simultaneous conjugacy would preserve this rank. The two ordered pairs are
+therefore nonconjugate over every field of characteristic two.
+
+## Literal original headers
+
+The standalone checker also constructs original eighteen-dimensional
+commuting projectors; it does not just trust admissibility of a residual.
+In the Jordan convention H e_(i+1)=e_i, let R extract the bottom coordinate
+of each block, and let W=I+H. In sector order 00,10,01,11, use
+
+    P0=diag(0_4,I_4,0_4,I_6),  Q0=diag(0_4,0_4,I_4,I_6).
+    i=(I,I,I,H,R)^T,          pi=(W,W,W,I,0).
+
+The last sector is U plus F^2. The map i is injective, pi i=I,
+pi P0 i=pi Q0 i=I, and pi P0 Q0 i=H. A basis B of ker pi is
+
+    B(x,y,z,t)=(x,y,z,W(x+y+z),t).
+
+Thus M=[i,B] is invertible. Conjugate P0,Q0 by M and delete the common
+identity block by the literal Schur formula D-cb. This yields the two
+witness pairs used by the verifier. All entries are in F2, so their exact
+ranks and equations persist over every extension field of characteristic
+two. The checker constructs an invertible fourteen-dimensional central
+intertwiner as well as checking all stated ranks.
+
+## Minimality
+
+Consider any two states in this nilpotent sharp family at the same d and
+same ordered original profile. Equal central classes imply equal rank Z.
+By (2), their H ranks agree. At d=1,2,3, the nilpotent partitions are,
+respectively,
+
+    (1);  (2),(1,1);  (3),(2,1),(1,1,1).
+
+Within each dimension these partitions have distinct ranks. Equal central
+classes therefore force similar H and, by #5267 rigidity, conjugate ordered
+pairs. This proves the pivot threshold d=4.
+
+At d=4 the only distinct partitions sharing a rank are (3,1) and (2,2),
+both with a=2. Their least possible residual dimension is 3d+a=14, attained
+above. At d>=5 every nilpotent H has a>=1 and residual dimension at least
+3d+a>=16. Thus fourteen is also the least residual dimension for this
+same-d, same-profile nilpotent central alias. The corresponding least
+ambient dimension is eighteen. These minima concern precisely this family;
+no claim is made about arbitrary pairs of idempotents or nonsharp states.

research/schur-central-alias/README.md

@@ -0,0 +1,100 @@
+# Central Schur classes first alias at pivot dimension four
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with exact finite corroboration. In the
+sharp nilpotent identity-pivot Schur family, over every characteristic-two
+field, two ordered residual pairs with the same pivot size and four original
+sector dimensions can have identical complete central similarity classes
+without being simultaneously conjugate. The least pivot size is **four**;
+the least residual and ambient dimensions are **fourteen** and **eighteen**.
+
+The witness has original sector dimensions (4,4,4,6) and compressed products
+J3(0)+J1(0) and J2(0)+J2(0). Both central operators have full Jordan form
+J2(0)^4 + J1(0)^6. The ranks of (S+T)^3 are two and zero, which distinguish
+the ordered states. Consequently a complete central-class key cannot safely
+deduplicate these ordered states. This is a local algebraic obstruction,
+with no new kappa, physical cost saving or supplier-admission claim.
+
+[PROOF.md](PROOF.md) gives the argument and explicit original headers. The
+central class retains precisely the odd positive power ranks of H; the sum
+S+T retains every power rank. The minimality proof uses only the nilpotent
+partitions through size four and the credited whole-pair rigidity theorem.
+
+Credit Malik Safwan / ssafwann [#5267](https://github.com/CrocSwap/integer-mult-bounds/pull/5267)
+for the nilpotent model, admissibility and rigidity; Ali Romman
+[#5287](https://github.com/CrocSwap/integer-mult-bounds/pull/5287) for the
+already complete characteristic-two central law; Mihir Srivastava
+[#5360](https://github.com/CrocSwap/integer-mult-bounds/pull/5360) for the
+general-H ordered gluing boundary; Nick Petalas #4746/#4597, MatShep #4762,
+codyw912 #4735, and the retained Ryanson Jonathan, lee-phys, Cinna Davis,
+source527, commdata2338 and Jose Manuel lineage. Those results are cited
+premises, not replay deliverables. Classical nilpotent power-rank facts are
+not claimed as new.
+
+## Reproduction
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/schur-central-alias/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/schur-central-alias/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/schur-central-alias
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/schur-central-alias --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. Expected direct marker:
+`PASS_SCHUR_CENTRAL_ALIAS`. The verifier writes no files. Its computed receipt
+binds all package source hashes and a digest of both literal witness pairs,
+the explicit central intertwiner, the finite minimality census and controls.
+A receipt is printed, not hand-written or accepted as a mathematical premise.
+
+The exact checks construct two complete eighteen-dimensional original
+headers and fourteen-dimensional residual pairs, verify the common identity
+pivots, prescribed products, idempotence, original commutation and sharp
+commutator rank eight, and compare eight power ranks of each sum and centre.
+An invertible central intertwiner is checked by literal multiplication.
+All eleven nilpotent partitions of sizes one through four and all fourteen
+same-size unordered comparisons give exactly the displayed collision.
+Eight controls cover invalid partitions, singular inversion, a non-square-zero
+central input, a different central class and the ordered-state separator.
+Normal and optimized checks enforce the same explicit exceptions.
+
+The all-field proof relies on the written argument and cited normal form;
+finite evidence is not independent human or formal proof-kernel review.
+The selected source-binding orientation passed at #7000. No predecessor
+scientific suite, selected cold replay, native replay, Lean or Docker ran.
+Physical access, movement, precision, stock, coefficient preparation,
+restoration, dispatch, a complete supplier invoice and all five selected
+framework assumptions remain outside scope.
+
+## Engineering and overlap
+
+The autonomous local run stopped at this first obstruction. The formal-interface-
+lemma card is changed to a written state-information side result; no formal
+caller binding is claimed. The baseline card example was run before the
+experiment. New code uses bounded finite domains, no recursion, functions
+below sixty lines and warning-strict normal/optimized checks. CPython allocation
+is a Power of Ten rule-three deviation: the hard-coded largest matrix is
+18 by 36 during augmented elimination, with bounded live fixture collections.
+No external static analyzer is claimed. The verifier imports no predecessor
+code and has no mutable external resources.
+
+Live open PR bodies, recent handoffs and main-tree README searches were
+checked for Schur central collisions, ordered-pair classification and the
+partitions (3,1)/(2,2). Merged #5287 closes the older characteristic-two
+Jordan-law question; that law is expressly credited. Main #5267/#5360 do not
+claim this minimal central alias. The overlap helper covered 502 open PRs
+and 7,179 Discussion records with complete remote pagination; its sparse
+local coverage was only 193 of 10,178 note paths. Separate Git-tree searches
+covered relevant merged READMEs. Arbitrary diffs and unpublished work remain
+outside that coverage. Source bytes and provenance are pinned in SOURCES.json.
+
+## Open next questions
+
+- Which extra invariant should an actual ordered-state registry retain? Start
+  with the full power-rank profile of S+T in this nilpotent family; a specified
+  consumer, representation and acquisition cost are still required.
+- What is the first central alias outside the sharp nilpotent same-profile
+  family? Start with one explicitly named nonsharp or mixed-primary contract.
+  The present minima do not cover that domain, and no broader census is held.

research/schur-central-alias/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "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/schur-nilpotent-extension/README.md",
+      "usage": "input",
+      "git_blob": "1e738614a419c8f91941886179bdf235e4e5ed52",
+      "sha256": "7e5e74f4e5ddc1793ac6e427a80492d8d978aa78f01f189e33d2831147c9639a"
+    },
+    {
+      "path": "research/schur-primary-gluing/README.md",
+      "usage": "input",
+      "git_blob": "b324f0cfc1886651d5a7954621d872dbec8a65cf",
+      "sha256": "dad194a3bb1211b0605a6c2667b7f40f6ba5c95efafcfa770dc1f85fbc1846d3"
+    },
+    {
+      "path": "research/schur-whole-central-class/README.md",
+      "usage": "input",
+      "git_blob": "d31e16ddebadd946b92beea599dc8e743c5d7092",
+      "sha256": "ecf2a0ac1b9fb353ea8de8aa207af2fc3f63e97f4f6bae06b3d54bebc9ddc903"
+    }
+  ]
+}

research/schur-central-alias/TASK.json

@@ -0,0 +1,109 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "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": "First central-class alias between nonconjugate sharp nilpotent ordered Schur states at the same pivot size and ordered original sector profile, in characteristic two.",
+  "scope_change_reason": "Original state-information obstruction; written algebraic side proof rather than a formal caller binding. The predecessor characteristic-two central law is already complete and is cited.",
+  "bottleneck_link": "Side result: a central-class key cannot deduplicate ordered Schur states. No paid supplier or kappa implication is supplied.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first explicit collision and its minimality proof; leave other families and consumer costs open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; two literal original headers and residual pairs, explicit central intertwiner, 11 partitions and 14 comparisons, eight controls; standalone normal/optimized verifier.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Which extra invariant should an actual ordered-state registry retain?",
+      "why_it_matters": "A complete central-class key loses ordered-state information at the stated first collision.",
+      "first_step": "Specify one consumer and use the full power ranks of S+T in this nilpotent family.",
+      "blocked_by": "No physical consumer, representation or acquisition-cost allowance is supplied."
+    },
+    {
+      "question": "What is the first central alias outside the sharp nilpotent same-profile family?",
+      "why_it_matters": "The dimension minima are scoped, not universal idempotent-pair bounds.",
+      "first_step": "Name one nonsharp or mixed-primary contract before a new comparison.",
+      "blocked_by": "A separately bounded research claim and proof are required; no follow-on scope is held."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19540664",
+  "playbook": "autonomous local run",
+  "source_question": "original",
+  "environment": {
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "requirements": "standard library only"
+  }
+}