Prove the exact pairing spectrum of every standard-coordinate Dn puncture

research/dn-coordinate-pairing-spectrum/README.md

@@ -0,0 +1,151 @@
+# Exact pairing spectrum for every standard-coordinate D_n puncture
+
+For any subset of the projective roots `2e_i +/- 2e_j` of `D_n`, with its
+**fixed standard-coordinate Gram decoder**, the minimum COPY cost over every
+admissible binary pairing is twice the number of represented coordinate edges.
+This includes asymmetric pairings. Consequently no such puncture has cost below
+its number of root lines. A puncture ties exactly when it is a union of complete
+opposite-sign pairs.
+
+This answers the pairing-minimization handoff in Aaron Wang's
+[PR 2272](https://github.com/CrocSwap/integer-mult-bounds/pull/2272), Open next
+questions item 2, retained by
+[PR 2518](https://github.com/CrocSwap/integer-mult-bounds/pull/2518).
+All 1,023 previously observed D5 ties remain optimal over **all** admissible B.
+The new result is the arbitrary-pairing theorem and exact cost distribution;
+the B0 puncture counts and original root model belong to those predecessors
+and DreamingOfClouds's
+[PR 2125](https://github.com/CrocSwap/integer-mult-bounds/pull/2125).
+
+## Model and theorem
+
+Let `n >= 2`, and choose any nonempty subset S of the `n(n-1)` root lines,
+represented once by `2e_i+2e_j` and `2e_i-2e_j` for `i<j`.
+For each coordinate j let `I_j` be the live roots having nonzero j-th coordinate.
+Use the exact decoder `Gram(S) = sum_j p_j p_j^T` with these coordinate columns.
+An admissible matrix B over F2 has diagonal one and `B_ts=0` for distinct
+nonorthogonal roots. All ordered entries at orthogonal pairs are free;
+symmetry is an optional additional constraint. The raw cost, without a floor w,
+is `C(B) = sum_j rank_F2 B[I_j,I_j]`.
+
+Count the underlying unordered coordinate edges `{i,j}`:
+
+- m edges have both signs present; s edges have just one; e=m+s.
+- v=2m+s is the number of live root lines.
+- d is the number of unordered live-root pairs on disjoint coordinate edges.
+- k is the number of the m complete sign pairs whose **two directed** mate
+  entries in B are not both one.
+
+Then, for every admissible B,
+
+```text
+C(B) = 2e + 2k.
+min_B C(B) = 2e = v+s.
+sum_{admissible directed B} z^C(B) = 2^(2d) z^(2e) (1+3z^2)^m.
+sum_{admissible symmetric B} z^C(B) = 2^d z^(2e) (1+z^2)^m.
+```
+
+Every minimizer has both entries equal to one at each complete sign pair.
+Its entries between disjoint edges are arbitrary. Thus there are exactly
+`2^(2d)` directed minimizers and `2^d` symmetric minimizers. Dense orthogonal B0
+is one minimizer; no monotonicity of binary rank is assumed.
+
+## Proof
+
+Two distinct roots in the same coordinate support I_j either lie on the same
+coordinate edge or on two different edges sharing j. In the latter case their
+inner product is `+4` or `-4`, hence both pairing entries are forced zero.
+The former case is the opposite-sign pair on that edge, and is orthogonal.
+Reordering I_j by coordinate edge therefore makes its principal pairing block
+block diagonal. A single root contributes `[1]`, of rank one. A complete pair
+contributes `[[1,a],[b,1]]`. Over F2 this block has rank one precisely when
+`a=b=1`, and rank two for the other three choices. Rank adds across these blocks.
+
+Every represented coordinate edge occurs in exactly two supports, its endpoints.
+Its singleton or good mate block therefore contributes two to C; a bad mate
+block contributes four. This proves `C=2e+2k` and the minimum. Since
+`v=2m+s`, the minimum equals `v+s`; equality with v is equivalent to `s=0`.
+
+All distinct orthogonal root pairs are either the just-described mates or have
+disjoint coordinate edges. A disjoint-edge pair cannot belong together to any
+I_j, so neither of its directed entries affects any block being priced. There
+are exactly 2d independent such bits, giving the factor `2^(2d)`. Each complete
+mate has one good directed assignment and three bad assignments, with cost
+increment two in the bad case. Multiplying their independent generating
+factors proves the directed polynomial. Symmetry identifies the two entries:
+each disjoint pair leaves one free bit and each mate has one good/one bad
+assignment, proving the symmetric polynomial. This proves the all-n statement,
+not merely its checked finite instances.
+
+For all punctures of D_n, put `E=binom(n,2)`. There are `2^E-1` tied nonempty
+punctures, because each edge is absent or complete. The number of punctures
+whose minimum exceeds v by j is
+`binom(E,j) * 2^E - [j=0]`: choose the j singleton edges and their signs,
+and independently omit or complete the other E-j edges. The subtraction removes
+the empty puncture. For full D5, `(e,m,d)=(10,10,60)`, minimum 20, with `2^120`
+directed or `2^60` symmetric optimizers. These large counts follow from the proof;
+the verifier does not enumerate that many matrices.
+
+## Exact checks and boundaries
+
+`verify.py` implements root geometry, admissibility, actual binary row elimination,
+and an independent row-span cardinality rank algorithm. It does not import any
+predecessor code. The source order and scale agree with PR2272's D(n) constructor.
+`RESULT.json` is regenerated in full and compared, including every reported field.
+
+- D3: all 342 nonempty relevant pairing states, with both rank algorithms.
+- D4: all 117,648 relevant pairing states over all 4,095 punctures, checking each
+  puncture's directed and symmetric coefficient distribution. Disjoint-edge bits
+  are fixed at zero in this finite census; their freedom is proved above. This is
+  a quotient census, **not** enumeration of all admissible D4 matrices.
+- D5: all 1,048,575 nonempty punctures at B0; every principal subblock rank used
+  in the lookup (1,280 total) is checked by both rank algorithms. The exact margin
+  histogram has 1,023 ties and matches the formula. This independently reproduces
+  predecessor counts as a positive control, not a new B0 census claim.
+- 360 deterministic directed admissible pairing samples in D2 through D10,
+  with disjoint-edge entries varying independently; direct rank bills match.
+- Controls reject a missing diagonal and nonorthogonal nonzero entries. An
+  inadmissible all-ones pairing on D3 would give cost 3 < 6. The four directed
+  mate assignments cost `[4,4,4,2]`, so merely one directed bit being set does
+  not obtain the rank-one cost. Finally the same singleton Gram `[8]` costs two
+  in the standard basis but one with factors `(1,0)` and `(8,0)`, showing why
+  the fixed coordinate-decoder hypothesis is essential for the exact formula.
+
+This does not minimize over other factor bases, overcomplete factorizations,
+different roots, or physical helper circuits. In particular it proves neither
+the general T^2 threshold law nor a supplier, legal compiler, or new exponent.
+The exact decoder identity follows directly from Gram construction; COPY pricing
+is a scoped algebraic model, not a complete physical gate bill.
+
+## Reproduce
+
+Python 3.12+, standard library, from the repository root:
+
+```sh
+python3 -I -O -B research/dn-coordinate-pairing-spectrum/verify.py
+python3 -I -O -B research/dn-coordinate-pairing-spectrum/test_boundary.py
+python3 scripts/research_package.py --package research/dn-coordinate-pairing-spectrum
+```
+
+The verifier is read-only by default and uses explicit checks that survive `-O`.
+To regenerate, pass `--out` with a nonexistent filename; overwrite is refused.
+The boundary test exercises a Git-free package export, corrupted and missing
+receipts, full regeneration, and exclusive output. The symbolic all-n proof is
+the written argument above, not a Lean proof or an implication of finite testing.
+
+## Open next questions
+
+1. Can changing the factor basis of a tied D5 puncture lower cost below v when
+   B is optimized jointly? This matters because the coordinate proof no longer
+   applies. Start with one elementary basis shear and classify support changes;
+   the blocker is the infinite rational factorization family.
+2. Can the same two-by-two block argument be extended to a non-coordinate root
+   alphabet? This would identify a broader obstruction. Start by characterizing
+   intersections of factor supports; larger orthogonal induced blocks need new
+   rank bounds and need not decompose into independent mate blocks.
+
+Contributor: ywz65, with substantial OpenAI Codex assistance in derivation,
+implementation and writing. Separate AI review is recorded in TASK.json when
+completed; no independent human review is claimed. Exact predecessor heads,
+catalogue, selected-record pins, selection and overlap freshness are recorded in
+SOURCES.json and TASK.json. No frozen source or selected frontier is changed.

research/dn-coordinate-pairing-spectrum/RESULT.json

@@ -0,0 +1,138 @@
+{
+  "controls": {
+    "directed_mate_costs_00_01_10_11": [
+      4,
+      4,
+      4,
+      2
+    ],
+    "invalid_diagonal_rejected": true,
+    "invalid_forced_zero_rejected": true,
+    "same_singleton_gram_standard_changed_costs": [
+      2,
+      1
+    ]
+  },
+  "d5": {
+    "direct_subblock_ranks": 1280,
+    "minimum_minus_v_histogram": {
+      "0": 1023,
+      "1": 10240,
+      "2": 46080,
+      "3": 122880,
+      "4": 215040,
+      "5": 258048,
+      "6": 215040,
+      "7": 122880,
+      "8": 46080,
+      "9": 10240,
+      "10": 1024
+    },
+    "punctures": 1048575,
+    "roots_sha256": "0a5014fc83a0e1a925b88a77e2474d74c78a0eab9fa18bac19ee478ea94512bb",
+    "ties": 1023
+  },
+  "directed_sample_cases": 360,
+  "formula": "cost=2e+2k; directed polynomial=2^(2d)*z^(2e)*(1+3z^2)^m",
+  "full_families": {
+    "2": {
+      "complete_pairs": 1,
+      "directed_optimizers": 1,
+      "disjoint_root_pairs": 0,
+      "minimum": 2,
+      "symmetric_optimizers": 1,
+      "tied_punctures": 1,
+      "v": 2
+    },
+    "3": {
+      "complete_pairs": 3,
+      "directed_optimizers": 1,
+      "disjoint_root_pairs": 0,
+      "minimum": 6,
+      "symmetric_optimizers": 1,
+      "tied_punctures": 7,
+      "v": 6
+    },
+    "4": {
+      "complete_pairs": 6,
+      "directed_optimizers": 16777216,
+      "disjoint_root_pairs": 12,
+      "minimum": 12,
+      "symmetric_optimizers": 4096,
+      "tied_punctures": 63,
+      "v": 12
+    },
+    "5": {
+      "complete_pairs": 10,
+      "directed_optimizers": 1329227995784915872903807060280344576,
+      "disjoint_root_pairs": 60,
+      "minimum": 20,
+      "symmetric_optimizers": 1152921504606846976,
+      "tied_punctures": 1023,
+      "v": 20
+    },
+    "6": {
+      "complete_pairs": 15,
+      "directed_optimizers": 2348542582773833227889480596789337027375682548908319870707290971532209025114608443463698998384768703031934976,
+      "disjoint_root_pairs": 180,
+      "minimum": 30,
+      "symmetric_optimizers": 1532495540865888858358347027150309183618739122183602176,
+      "tied_punctures": 32767,
+      "v": 30
+    },
+    "7": {
+      "complete_pairs": 21,
+      "directed_optimizers": 7331559403129590068331208687020758653624765228075687047537011123791632385370343464792392772051104864109916034360063928339045596353810784435313926666640532382851295822842678298180301122938618566718730242107326783353838221723324821405531849499257419595776,
+      "disjoint_root_pairs": 420,
+      "minimum": 42,
+      "symmetric_optimizers": 2707685248164858261307045101702230179137145581421695874189921465443966120903931272499975005961073806735733604454495675614232576,
+      "tied_punctures": 2097151,
+      "v": 42
+    },
+    "8": {
+      "complete_pairs": 28,
+      "directed_optimizers": 53751763281617910977034964721174741663008655940159144344713614863023080529278140407534961311242814229395876005424258737427374269437649287838907097277355371953699677593812086481959272740614049029887514406997074265172418391397657360248197162683969074191332475296524902658098222332595908741751391477587362636344728828453617536494627356792601450307397806688631445746074774556850081722840606116959452930981773324385740577251592339045231114992186734509188416434115341010544191353505352737718761080737479237042176,
+      "disjoint_root_pairs": 840,
+      "minimum": 56,
+      "symmetric_optimizers": 7331559403129590068331208687020758653624765228075687047537011123791632385370343464792392772051104864109916034360063928339045596353810784435313926666640532382851295822842678298180301122938618566718730242107326783353838221723324821405531849499257419595776,
+      "tied_punctures": 268435455,
+      "v": 56
+    },
+    "9": {
+      "complete_pairs": 36,
+      "directed_optimizers": 20639866688192249678690979427047744716670419422978338405490767656712605070613300830961151335902735607601692030339466006139980896685912793208440823179426475068368459772139688719662053454545441962864930352619700970232691192549708975533834320861293755528582525396944795278184961346348121152405537193811559544560528122472766855879578363826574119600278907314987542926997237378746730499786212713008347110671443879490481628971586456347856297569099192539115056245819004213727631262285862613802315336376080691028745451394187818329012215737168247703065165176763236436188268622714806030476205940112438517662309257595469092710023367459009590744249233592976505063469657896200879783774178059516715294055766886940027007433396687814278648206918025537489162479394046257364519031954709690026927019765539112214281096766958661032472041467681013226556685362979770990378092763807981815343641872998542497684604695404128952469438857216,
+      "disjoint_root_pairs": 1512,
+      "minimum": 72,
+      "symmetric_optimizers": 143665816004337822710282600285310394341474369045835074863414468709543787931907367746179403311452034095731304066234112071267510472464260955153084575408147254672957261763907982395337943906645864229014250227057207826232751957053220218983971305018634078800548055251973907806245884614087189937340865371691338441989956445051526543084039211962387469415699218979531585795574920384684004258007709014706216763392717018544247025174258411677231986785008489302218244096,
+      "tied_punctures": 68719476735,
+      "v": 72
+    },
+    "10": {
+      "complete_pairs": 45,
+      "directed_optimizers": 155302392568755602954703791645117509171853024379829526053941914979869764308014137101580853703257316967419024475301219529235426499580989700492471117592130679578703743169643269465601721348541513593756461576285693343335323948307757460714948112300799739460308904920802096954409942913408096419432033412736062772643941590080446853373252364634969631941189995619518198884520714851905373673786301803818992437528114546902893524109693619934375650827402974283364443639166789257783558287754544152762072425073758073874087673853749491025245350759370202288198641756277483105286855126452445186433581045273785395216218774302137457946970241887040423778769507844532372395126914334350410060838193463467701758259122737262877689997254446028894627441507215258630083149823214021914691630385344730360124370246246101179225617171359948255502820724998630578414563433771734039885865200126640849581418101617590256731549974180011798541810287432442790284651150068406362365126351529058374781998017317605130002324359837801578063898318531549204801679097327112281643491227164405147112572736443606882046580363487549058621262011237393353206539463047834322740801769791931408446565925701470542859326548992533299683757135685782623491909977496699208378601007696438296190884956558923555954397532301018024430186240362810108284785909687389090161977695156919530083589605517157247030242165705875087062283656720276403790904286872963087972571265678945386772020563763263215540821764049192071134806571089438720182703434060588593593872862671044732442467813100983236427776,
+      "disjoint_root_pairs": 2520,
+      "minimum": 90,
+      "symmetric_optimizers": 394084245522141626953485431836389151728191722497516426553221541823493367658800961065564478638820000356056388337167035542074008945401913950236214360506399705231203021164366069389563701733455174652493802096528279659381259483508916176782516892616322154881870596505654577774329808187256502370468256875376316278135937985788160888518809137837873180086327183792757748702946460720720770436177477377229784500022657580657233628383930137914619684009220791267089768552182903618603146950084219242780072578071648001265726679873751772302343114358428552134991938056446803917216962620267368806273089867659639177213488960155211698149211030681779788578141054359274289556411400436598704927821275214881488970218576557325551889577507340928956338410400961096026352642413831783448576,
+      "tied_punctures": 35184372088831,
+      "v": 90
+    }
+  },
+  "relevant_censuses": [
+    {
+      "independent_row_span": true,
+      "n": 3,
+      "punctures": 63,
+      "relevant_pairings": 342,
+      "symmetric_relevant_pairings": 124
+    },
+    {
+      "independent_row_span": false,
+      "n": 4,
+      "punctures": 4095,
+      "relevant_pairings": 117648,
+      "symmetric_relevant_pairings": 15624
+    }
+  ],
+  "schema_version": 1,
+  "scope": "fixed standard D_n coordinate Gram decoder"
+}

research/dn-coordinate-pairing-spectrum/SOURCES.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11"
+    },
+    {
+      "path": "research/root-unit-decoder-lemmas/README.md",
+      "usage": "provenance",
+      "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9",
+      "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb"
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 2125,
+      "head": "d9eb80ac183bb4df185ca044fd65432b817333bb",
+      "path": "research/char2-threshold/README.md",
+      "git_blob": "33f55f270d2676aaabd094176e2b52cde7c5c5de",
+      "sha256": "65e4b34276b5b6c31f105d4c36fa5a8a5f530f4a8bc1f41711f2e73dee1f8ea1",
+      "usage": "DreamingOfClouds root/polar pairing model and original root table; not imported."
+    },
+    {
+      "pr": 2272,
+      "head": "50e12c263fa443ba587fd6b205f2fc2825d10de1",
+      "path": "research/polar-law-small-t-screen/README.md",
+      "git_blob": "836a35b2a7043421a5464db8ea023d6a3b480175",
+      "sha256": "09d6b28c1b5850502484a3e4f69a346e3463b30d2e6ab6062552f45ed1dffea6",
+      "usage": "Aaron Wang D4/D5 B0 puncture census and explicit pairing-minimization handoff; independently reproduced as control."
+    },
+    {
+      "pr": 2518,
+      "head": "5ccad6aa04409ee2805d5638aa0fc84c76bbb881",
+      "path": "research/polar-law-t7-overcomplete-screen/README.md",
+      "git_blob": "3d7a42855310f5251452bdb003300275b538efc3",
+      "sha256": "ed9c61d8616fa4bc86a9d28d66f49aa774ef25fe56a4e3c895b69bf784e7880f",
+      "usage": "Aaron Wang further root/overcomplete screen, retaining pairing-minimization handoff; distinct fixed-frame scope."
+    }
+  ]
+}