Prove exact positive Turyn redundancy cost 27R (no κ)

research/turyn-positive-redundancy/PROOF.md

@@ -0,0 +1,103 @@
+# Exact cost of positive redundant Turyn encoders
+
+This scoped result was produced by Nick Petalas. Apache-2.0.
+
+## Contract
+
+Let the port labels be vectors ell_i in F_2^h. For a real column v, charge
+
+    c(v) = dim_F2 span {ell_i : v_i != 0}.
+
+Consider an exact factorization K = A H A^T with finitely many real encoder
+columns and a real symmetric positive definite metric H. The bill is the sum
+of c(a_j). Zero columns cost zero; R counts only nonzero columns. The metric
+and scalar work are granted free. This is an algebraic encoder support bill,
+not a complete physical or recursive invoice. Positive sums of outer products
+are the diagonal-metric case; a dense metric can couple different columns.
+
+## Range lemma
+
+For every such factorization, range(K) = range(A) and rank(K) = rank(A).
+Indeed, for every real x,
+
+    x^T K x = (A^T x)^T H (A^T x).
+
+Positive definiteness makes this zero exactly when A^T x = 0. If Kx = 0
+then x^T Kx = 0, while A^T x = 0 implies Kx = 0 directly. Thus
+ker(K) = ker(A^T). Taking orthogonal complements proves the range identity.
+The argument permits dependent columns, any finite redundancy, arbitrary
+real coefficients and a dense positive definite metric.
+
+## Fixed-kernel cost theorem
+
+Suppose K is positive semidefinite, rank(K) = r > 0, and every nonzero
+v in range(K) has c(v) = h.
+Then every positive definite factorization with R nonzero columns satisfies
+
+    R >= r,  sum_j c(a_j) = h R.
+
+Every column lies in range(K), so every nonzero column costs h. Also
+rank(A) <= R. These prove both conclusions.
+
+Every integer R >= r is attainable. A positive semidefinite K of rank r
+has a real Gram factor K = U U^T with r independent columns. Replace the
+first column by t = R-r+1 identical copies. Give each duplicate weight 1/t
+and every other column weight 1 in a diagonal H. The resulting A H A^T
+is still K, every column is nonzero and H is positive definite. Hence
+the minimum bill at prescribed R is exactly hR. No coefficient-height or
+physical-cost bound is asserted by this construction.
+
+## Turyn specialization and predecessor premises
+
+DominikScholz's [PR598](https://github.com/CrocSwap/integer-mult-bounds/pull/598)
+supplies two results that this package cites without replaying:
+
+1. The full canonical Turyn product kernel has 23,040 ports and real rank
+   512. It is the Gram kernel of the 512 tensor coordinates, up to a positive
+   normalization. See `research/leech-lattice/TURYN.txt`, "Product kernel".
+2. Under the existing direct-sum 27-bit labels, every nonzero real tensor
+   encoder has label-support rank 27. See the final section of
+   `research/turyn-port-labels/PROOF.txt` and its README's explicit restriction
+   to rank-minimal factorizations and encoders in the tensor column space.
+
+The tensor-coordinate matrix has full column rank, so its column space is
+range(K). Applying the theorem gives the exact algebraic optimum
+
+    B(R) = 27 R for every integer R >= 512.
+
+No factorization in this class exists with R < 512. The optimum over all
+finite positive definite factorizations is therefore 13,824. Every nonzero
+redundant column adds exactly 27. The cited tensor Gram factor attains the
+minimum, and duplication attains every larger R. The extension to arbitrary
+positive redundancy is new here; the geometry, rank and support theorem
+remain the predecessor's results. The elementary Gram range identity is
+classical, and no general linear-algebra priority is claimed.
+
+## Why the metric hypothesis matters
+
+Let u = (1,1)^T, K = u u^T and the port labels be e_1,e_2. Every nonzero
+vector in range(K) has label-support rank two.
+
+* For A = I_2 and H = [[1,1],[1,1]], the equality K = A H A^T holds, but
+  H is singular positive semidefinite. Each column of A costs one and lies
+  outside range(K). The formula hR would predict four instead of the actual
+  two. Thus a singular positive semidefinite coupling metric is outside
+  the theorem.
+* For A = [u,e_1,e_1] and H = diag(1,1,-1), the same K is obtained.
+  The outside columns cancel. Its bill is four rather than hR = six.
+  This escapes confinement but does not supply a cheaper Turyn decoder.
+
+A diagonal nonnegative metric can discard its zero-weight terms and apply
+the theorem to the positive-weight terms. A singular dense metric cannot
+generally discard original columns individually, as the first example shows.
+Asymmetric factorizations and signed cancellations remain open routes.
+
+## Verification boundary
+
+The proof is all-size real linear algebra. The verifier checks new bounded
+rational examples, attaining duplications, dense positive definite metric
+changes and the boundary counterexamples. Finite checks do not prove the
+all-size theorem or re-establish the cited PR598 premises. Independent human
+and formal proof-kernel review are unclaimed. No physical supplier, new kappa,
+selected-frontier update or complete multiplication theorem follows. All five
+selected framework assumptions remain separate.

research/turyn-positive-redundancy/README.md

@@ -0,0 +1,114 @@
+# Positive redundancy cannot lower the fixed-label Turyn encoder bill
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+For the full Turyn product kernel with its existing 27-bit labels, the exact
+encoder support bill with R nonzero columns is B(R)=27R for every R>=512,
+when K=A H A^T and H is positive definite. No such factorization exists with
+R<512. The minimum over all finite positive redundancy is therefore 13,824.
+Each additional nonzero column costs exactly 27, even with a dense positive
+definite coupling metric. The metric and scalar operations are granted free.
+
+DominikScholz's [PR598](https://github.com/CrocSwap/integer-mult-bounds/pull/598)
+proves rank 512 and support rank 27 for every nonzero tensor encoder, then
+bounds rank-minimal factorizations. This package cites those results as
+premises. The new step extends the bill to arbitrary positive redundancy.
+Its proof uses the classical positive Gram range identity. No general
+linear-algebra priority is claimed, and no predecessor scientific suite is
+replayed. [PROOF.md](PROOF.md) gives the theorem, attainers and exact limits.
+
+This is a historical changed-geometry side result under the current decoder
+card, rather than a changed selected P104 supplier. The complete signed
+invoice, physical/native realization, ownership, restoration, precision,
+compiler, analytic recovery and the five selected assumptions remain outside
+scope. No new kappa or complete multiplication theorem is claimed. Independent
+human and formal proof-kernel review are unclaimed.
+
+## Reproduce
+
+From the repository root with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/turyn-positive-redundancy/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/turyn-positive-redundancy/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/turyn-positive-redundancy
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/turyn-positive-redundancy --check-source-history
+```
+
+Another CPython 3.12 executable can replace the absolute interpreter path.
+Each direct command prints PASS_TURYN_POSITIVE_REDUNDANCY and generates a
+SHA256 receipt for all six package files and the three cited source texts.
+The registered launcher also prints PASS_REGISTERED_RESEARCH_PACKAGE.
+Authentication of the texts is separate from proving their mathematical
+premises. The direct scientific replay needs no Git or network.
+
+## Evidence and verification design
+
+The executed domains are 2,511 two-by-two Gram cases from all 81 ternary
+encoder matrices and 31 positive definite metrics, 80 rectangular fixtures,
+160 fixed-kernel attainers, two metric boundary counterexamples, nine
+rejecting controls and one zero-column control. The two-by-two rank histogram
+is 31 zero, 992 rank-one and 1,488 rank-two cases. These are enumerated test
+cases, not claims about the number of Turyn objects.
+
+The verifier checks new exact rational examples, including singular encoder
+matrices, dense positive definite metrics, attaining duplicate columns and
+changes of metric coordinates. Two literal counterexamples reject extending
+the individual-column conclusion to singular or indefinite coupling metrics.
+Zero columns and invalid support hypotheses have separate controls. The
+all-size result comes from the written proof, not finite enumeration.
+
+The full-label support premise for the small fixtures is checked independently
+of the encoder columns: for each nonzero binary label functional, restricting
+the kernel to rows on which it is one must retain full real rank. This is
+equivalent to saying no nonzero range vector has its active labels in that
+functional's kernel. It does not enumerate or test the Turyn ports.
+
+All loops are bounded by fixed finite domains. Matrices have at most 32 rows
+or columns including concatenations; label width is at most five. Functions
+are shorter than 60 lines, there is no recursion or dynamic code execution,
+and failures use explicit exceptions that remain active under optimization.
+Files read for authentication and receipts are each bounded to one MiB.
+Warning-strict normal and optimized replays are the available diagnostics.
+No new static-analysis configuration or external dependency is needed.
+
+Power of Ten rule 3 has a managed-runtime deviation in verify.py. Python
+allocates integers, Fractions, lists and dictionaries during this bounded
+finite replay. Fixed dimensions and coefficient grids, streamed cases, no
+retained case history and a 120-second registered timeout constrain resources.
+Normal and optimized replays check the same domains. A physical implementation
+would need a separate fixed-capacity arithmetic and storage analysis.
+
+## Open next questions
+
+1. Can signed or asymmetric factorizations beat 13,824 with these labels?
+   Start with explicit outside-range columns, an exact full kernel identity
+   and every support charge. No such factorization or scalar word is supplied.
+2. Can a singular positive semidefinite metric save complete circuit cost?
+   Price its application and output restoration before counting sparse columns
+   as a gain. The two-port example only demonstrates the theorem's boundary.
+
+Structured questions and blockers are in [TASK.json](TASK.json).
+
+## Credit, provenance and overlap
+
+Credit DominikScholz / PR598 for the explicit opening, geometry, kernel, labels,
+rank and support theorem; R. J. Turyn, J. H. Conway, N. J. A. Sloane, Gabriele
+Nebe and the geometry/native lineage retained by that package. The classical
+Gram range identity and duplication construction are methods, not general
+priority claims. The original source files and their credit are unchanged.
+
+[SOURCES.json](SOURCES.json) pins the three premise texts and the task and
+selected-record provenance at canonical main
+7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8. The source's
+historical nominal kappa is not the selected result. The selected record at
+this base is PR6030 with kappa 0.003125804.
+
+The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362323)
+reserves the positive-redundancy question. Live open PRs, handoffs, local
+reservations, recent account work, current main and merged object/formula
+searches were checked. The cached refresh covered 387 open PRs and 6,319
+Discussion records, with complete remote pagination; its local note coverage
+was sparse, 106 of 8,917 HEAD paths. Direct Git searches supplemented those
+omissions, including the predecessor's text files. Unpublished work and
+arbitrary historical diffs are outside that coverage.

research/turyn-positive-redundancy/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/leech-lattice/TURYN.txt",
+      "usage": "input",
+      "git_blob": "9a167e169c7762e7ecc9e75465b67e29102a4678",
+      "sha256": "8e9e2fff58bf6304f86c2365c3263bc19b2c9332647cce250e52aeffab333fe9"
+    },
+    {
+      "path": "research/turyn-port-labels/PROOF.txt",
+      "usage": "input",
+      "git_blob": "35350a61d166a6e6d12a4c6b9f4d1d18dd13d89c",
+      "sha256": "926af92411e16decd9663efdcf3f97b27926cc6dc57ea799e6d217f01d2d8b0e"
+    },
+    {
+      "path": "research/turyn-port-labels/README.txt",
+      "usage": "input",
+      "git_blob": "86612c51e5c43cb9374e6df4443aac2ac09287a2",
+      "sha256": "d53d200a850e5a92ecb46f860a95e8ba14574c17d9599312fd05b16a8f1db3ff"
+    }
+  ]
+}

research/turyn-positive-redundancy/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "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",
+      "docs/research/recursive-invoice-preflight.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 source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "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": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "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 encoder support bill B(R)=27R for the fixed-label full Turyn kernel, with R nonzero columns and a positive definite coupling metric.",
+  "scope_change_reason": "The card asks for a complete signed-invoice decoder improvement. This is a historical geometry side result that settles the positive-redundancy subclass of PR598's explicitly open redundant-encoder direction. It supplies no changed P104 itinerary or complete supplier.",
+  "bottleneck_link": "Narrows one changed-decoder route: increasing positive Gram redundancy cannot lower this fixed-label support bill. Signed/asymmetric or changed-label models remain open; the selected P104 bottleneck is not improved.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified scoped improvement; do not search signed factorizations after proving the positive case.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the all-size argument; verify.py generates exact finite corroboration and a nine-file SHA256 receipt.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an exact signed or asymmetric factorization of the same full Turyn kernel beat 13,824 under the existing labels?",
+      "why_it_matters": "These factorizations can have encoder columns outside the tensor range and are not excluded by the positive result.",
+      "first_step": "Exhibit explicit outside-range columns and an exact complete kernel identity, then enumerate every column's binary label-support rank.",
+      "blocked_by": "No such lower-bill factorization or fully charged scalar realization is supplied."
+    },
+    {
+      "question": "Can a singular positive semidefinite coupling metric yield a cheaper complete encoder circuit for the same kernel?",
+      "why_it_matters": "The two-port example escapes individual-column confinement, but factoring or applying its metric can restore the cost.",
+      "first_step": "Price one exact source/metric/output circuit including all coupling operations and compare its full encoder and decoder bill.",
+      "blocked_by": "An algebraic coupling metric is granted free here; no physical implementation or cost contract is provided."
+    }
+  ],
+  "source_question": {
+    "source": "PR #598",
+    "author": "DominikScholz",
+    "path": "research/turyn-port-labels/README.txt",
+    "question": "Redundant real factorizations outside the tensor column space are excluded from the rank-minimal encoder bound."
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362323",
+  "playbook": "Autonomous local run",
+  "environment": {
+    "python": "3.12.15",
+    "implementation": "CPython",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "standard library only"
+  }
+}