Prove characteristic-two odd-type rank floors 22 and 53 (no new κ)

research/odd-five-char2-minrank/PROOF.md

@@ -0,0 +1,146 @@
+# A strict characteristic-two fitting-rank bound
+
+This is a scoped proof with exact finite corroboration. Let `K` be any field
+of characteristic two and let the labels lie in `F2^5`. Put `j=(1,1,1,1,1)`.
+A label is odd when its coordinate sum is one. The complete type set is
+
+```text
+T = {(q,w): q,w are odd and w dot q = 1}.
+R = {(q,w) in T: q != j and w != j}.
+```
+
+Each type occurs once. A matrix `N` indexed by a type set is fitting when
+its diagonal entries are nonzero and, for distinct positions `s,t`,
+
+```text
+w_s dot q_t = 1 implies N[s,t] = 0.
+```
+
+No symmetry, prescribed off-diagonal values, factorization or positivity
+is assumed. Binary entries embed in the prime subfield of `K`.
+
+**Theorem.** Every fitting matrix on `R` has rank at least 22. Every
+fitting matrix on `T` has rank at least 53. These are lower bounds;
+neither is asserted to be the exact minimum.
+
+Jose Manuel's PR3512 introduced this odd-type fitting boundary and proved
+all-field inequalities. His PR3544 strengthens the odd-dimensional
+inequalities and leaves optimal fitting rank open. We use that model,
+but do not rely on or recheck either inequality. The characteristic-two
+restriction below is essential to the proof and supplies no new rational
+fitting-rank bound.
+
+## 1. Equality in the elementary Hadamard bound
+
+We first give the elementary linear-algebra argument in any field. Let
+`B=W Q^T`, where row `i` of `W` is `w_i^T`, row `i` of `Q` is `q_i^T`,
+and the label dimension is `d`. Suppose a fitting matrix has been
+normalized to diagonal one, so that its entrywise product with `B` is
+the identity. Row scaling by the inverses of the original diagonal
+entries makes this normalization without changing rank or zero entries.
+
+If `N=L H` has rank `r`, define matrices with the indicated entries:
+
+```text
+U[i,(a,k)] = w_i[a] L[i,k],
+V[(a,k),i] = q_i[a] H[k,i].
+```
+
+Here `1 <= a <= d` and `1 <= k <= r`. Their product has entry
+`(UV)[i,j] = (w_i dot q_j) N[i,j]`, so `UV=I_n`. In particular `n<=dr`.
+This is the usual Hadamard rank inequality, proved here directly.
+
+If `n=dr`, both matrices are square and `VU=I_(dr)`. Its `(a,b)` block
+has entries
+
+```text
+sum_i q_i[a] w_i[b] H[k,i] L[i,l] = delta_(a,b) delta_(k,l).
+```
+
+Take its trace over `k=l`. Because
+`sum_k H[k,i] L[i,k] = N[i,i] = 1`, this forces
+
+```text
+sum_i q_i w_i^T = r I_d.                              (1)
+```
+
+Thus (1) is a necessary condition for saturation. The argument does
+not assume that `N` has binary entries. It holds over the full field `K`.
+It is an elementary consequence of tensor factorization and cyclic
+trace; no claim of worldwide novelty for that general observation is made.
+
+## 2. The regular type sum
+
+There are sixteen odd vectors, fifteen different from `j`. For fixed
+odd `q != j`, the two equations
+
+```text
+j dot w = 1, q dot w = 1
+```
+
+are independent, so they define an affine three-space of eight vectors.
+It contains `j`, since `q` is odd and `j dot j=1`. Removing `j` leaves
+seven regular sinks. Consequently `|R|=15*7=105`.
+
+The sum of the vectors in any affine three-space over `F2` is zero.
+Removing `j` therefore makes the seven-vector fiber sum equal to `j`.
+Likewise the sum of all sixteen odd vectors is zero, so the sum of
+the fifteen odd `q != j` is `j`. In characteristic two this gives
+
+```text
+sum_((q,w) in R) q w^T
+  = sum_(odd q != j) q j^T
+  = j j^T
+  = J_5,                                             (2)
+```
+
+where `J_5` is the all-ones matrix. The verifier independently enumerates
+all 105 types and all 25 entries of (2), as well as the seven-element
+fibers. The preceding affine-space argument proves the formula without
+depending on extrapolation from that enumeration.
+
+## 3. The strict lower bound
+
+For `R`, the binary matrix `B[s,t]=w_s dot q_t` factors through `K^5`,
+because the field has characteristic two. Section 1 gives
+`rank N >= 105/5 = 21`. If its rank were 21, equation (1) would force
+the sum in (2) to be `21 I_5 = I_5`. But `J_5 != I_5` over every field:
+each off-diagonal entry is one on the left and zero on the right.
+Thus rank 21 is impossible, and integrality proves `rank N >= 22`.
+
+## 4. Adding the special types
+
+There are sixteen types with `q=j`, sixteen with `w=j`, and one in
+both sets. Thus `|T minus R|=31` and `|T|=136`.
+
+For a type with `q=j`, the corresponding column of `B` is all ones.
+Its column of a fitting `N` is zero except at its nonzero diagonal.
+For a type with `w=j`, the same statement holds for its row. Deleting
+any such row and its matching column reduces rank by exactly one:
+expand around that isolated nonzero column or row, or perform ordinary
+invertible elimination. Deletion does not change any remaining entry.
+Repeat for all 31 special positions. This proves the exact identity
+
+```text
+rank N = 31 + rank N[R,R].
+```
+
+The bound from section 3 now gives `rank N >= 31+22=53`.
+
+## 5. Scope and verification
+
+The universal quantifier covers arbitrary entries in every
+characteristic-two field. The type domains are the complete finite sets
+defined above, with one occurrence per type. No bound for arbitrary
+nonuniform multiplicities, characteristic-zero matrices or a native
+supplier follows. The claim is a scoped obstruction, not a failed-search
+extrapolation, a sharp optimum or a multiplication theorem.
+
+The replay enumerates the new moment certificate and checks exact tensor
+inverses and their block traces in F2, F4 and F8. The tight controls use
+one or two disjoint five-port coordinate classes, including repeated
+types and nonunit diagonal values before normalization. Two nontrivial
+fitting fixtures of ranks 132 and 101 corroborate the special-port rank
+addition, including allowed entries between special and regular positions. These
+finite checks support the written proof; they do not enumerate all
+fitting matrices or replace the proof over arbitrary fields.

research/odd-five-char2-minrank/README.md

@@ -0,0 +1,126 @@
+# Strict rank bounds for the complete five-bit odd-type mask
+
+Scoped mathematical proof with exact finite corroboration. Over every
+field of characteristic two, the complete five-bit odd-type mask has
+fitting rank at least **22 on its 105 regular types**, and at least
+**53 on all 136 admissible types**. These are lower bounds, not exact minima.
+No new kappa is claimed.
+
+Write `j=11111` and let a type be `(q,w)` with both binary labels odd and
+`w dot q=1`. A regular type has `q != j` and `w != j`. Each type occurs
+once. A fitting matrix has arbitrary nonzero diagonal and must have
+`N[s,t]=0` whenever `s != t` and `w_s dot q_t=1`. It may be asymmetric
+and may have arbitrary entries in the full coefficient field.
+
+The elementary Hadamard rank bound gives 21 on the regular types.
+The new step excludes equality. After diagonal normalization, equality
+would make the two square tensor factors inverses. Taking block traces
+forces `sum(q w^T)=21 I_5=I_5`. The actual type sum is `J_5`, the all-ones
+matrix. Its off-diagonal entries contradict this requirement. The 31
+all-ones-source/sink types add rank individually, improving the associated
+full-mask lower bound from 52 to 53. [PROOF.md](PROOF.md) gives the argument.
+
+## Predecessors and scope change
+
+Jose Manuel / jmbarrancoml's [PR3512](https://github.com/CrocSwap/integer-mult-bounds/pull/3512)
+and [PR3544](https://github.com/CrocSwap/integer-mult-bounds/pull/3544) supply
+the odd-type fitting model and leave optimal fitting rank open. PR3544,
+head `6cfa4333a2e593ea092fe4bda686bb172b5b6d22`, proves the stronger
+all-field regular coefficient `17/105` in dimension five. That theorem
+is cited, not audited or replayed. The new result concerns the different,
+characteristic-two boundary; it does not improve the rational bound.
+[SOURCES.json](SOURCES.json) pins the main-retained predecessor documents
+as provenance. The verifier imports no predecessor code or data.
+
+Canonical base is `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority
+revision 7. The complex-rank-shape-decoder card is explicitly changed to
+this algebraic side question. It closes a finite-field equality case
+before a changed fitting model is used as a small-unit surrogate. This
+is not a decoder construction or evidence of a better paid supplier bill.
+The card's historical first command fails on the selected schema with
+`KeyError: 'complex_profile'`; the current schema-aware
+`scripts/research_selected_baseline.py` orientation passes. Neither is
+part of the new proof.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147080)
+proposed exact values 21 and 52. The
+[scope update](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147122)
+records their impossibility and the delivered strict lower bounds.
+Targeted main-tree and merged-PR searches, live open PR bodies and
+Discussion claims, recent same-account work and local reservations were
+checked. The broad scan covers 311 open PRs and 4,484 Discussion records;
+sparse local notes and unpublished work remain incomplete coverage.
+
+## Reproduce
+
+From the repository root with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/odd-five-char2-minrank/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/odd-five-char2-minrank/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/odd-five-char2-minrank
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/odd-five-char2-minrank --check-source-history
+```
+
+Any CPython 3.12 installation can replace the local interpreter path.
+The expected marker is:
+
+```text
+PASS_ODD_FIVE_CHAR2_MINRANK regular_types=105 regular_lower=22 full_types=136 full_lower=53 tensor_fixtures=18 controls=7
+```
+
+The replay enumerates the complete 136-type domain, its 105 regular
+positions, fifteen seven-element fibers and all 25 moment entries.
+Eighteen tight tensor fixtures over F2/F4/F8 check both inverse products,
+block traces and diagonal normalization, including nonbinary field
+coefficients and repeated types. Two full-mask fixtures check exact
+rank addition `132=31+101`. Seven rejection controls cover the impossible
+rank-21 moment, wrong cardinality, a forbidden entry, zero diagonal,
+missing normalization, corrupted tensor and zero inversion.
+
+The verifier writes nothing and emits a fresh receipt bound to all six
+package files and the executed results. Checks remain active with `-O`.
+The written proof supplies the arbitrary-field quantifier; the replay
+neither enumerates all fitting matrices nor certifies a formal proof kernel.
+
+## Limitations and engineering notes
+
+Characteristic zero and odd characteristic, nonuniform type multiplicities,
+sharpness at ranks 22/53, physical factors, frames, ownership, routing,
+restoration, precision, stock, compiler and complete supplier costs remain
+outside this result. No selected-frontier update or complete multiplication
+theorem is claimed. Independent human and formal proof-kernel review are
+unclaimed. Lean, Docker and the selected supplier cold replay are unrun.
+
+The verifier has no recursion, dynamic code, subprocess or network calls.
+Its functions are below 60 lines. It bounds matrices by 136 rows and
+columns, tensor matrices by ten rows and columns, fields by eight elements, package reads
+by six files of at most one MiB, and all loops by these fixed domains.
+Managed Python allocation is a deviation from static allocation; the
+finite domains bound live matrix storage. Seven fixed rejection callbacks
+are a bounded deviation from avoiding indirect calls. Warning-strict normal
+and optimized replay and in-memory compilation supply diagnostics.
+
+## Open next questions
+
+1. Is the regular characteristic-two minimum 22? First seek a cover of the
+   105 types by 22 compatible classes, or an explicit rank-22 factorization.
+   Attainment is the missing obligation; a lower bound alone cannot supply it.
+2. Can the full regular mask admit rank below 22 in characteristic zero?
+   Start with a rational factorization respecting the same zeros, using
+   PR3544's all-field lower bound as a cited premise. The five-column
+   factorization of the binary parity mask does not survive that field change.
+
+Structured questions are in [TASK.json](TASK.json).
+
+## Credit
+
+This contribution was produced by Nick Petalas. Jose Manuel / jmbarrancoml
+supplies the odd-type model, all-field triangular/flag bounds and explicit
+open fitting-rank question in PR3512/3544. Philippe Van Velzen supplies the
+small-unit setting and prior acyclic/Hadamard method; DreamingOfClouds
+supplies the related symmetric-mask Lagrangian and pairing-rank lineage.
+The rank inequality, tensor factorization and cyclic trace are classical.
+The new contribution is the strict characteristic-two bound for these
+complete type sets and its stated proof and exact corroboration.
+Predecessor files and credit are unchanged. Apache-2.0.

research/odd-five-char2-minrank/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/odd-unit-triangular-rank/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "f6ed16234cd1b413efd64ab9b810216051a2d38e",
+      "sha256": "e856fe9e4e7244ef8c18d3d5709fb12023425809042ffe2008038b431d156701"
+    },
+    {
+      "path": "research/odd-unit-triangular-rank/README.md",
+      "usage": "provenance",
+      "git_blob": "ba317318408e91284bc8551fd8704bdac4459f6e",
+      "sha256": "bd627569e44fc7b2a37f339ecf5b19170cb00fbafa5f4607bb8a8d3904b50868"
+    }
+  ]
+}

research/odd-five-char2-minrank/TASK.json

@@ -0,0 +1,78 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md",
+      "research/selected-k8-unrestricted-ends/README.md",
+      "research/eisenstein-reduction-copy-floor/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove strict characteristic-two fitting-rank lower bounds 22 and 53 for the complete five-bit regular and full odd-type masks.",
+  "scope_change_reason": "Replace decoder synthesis with the explicitly open algebraic fitting-rank boundary in Jose Manuel PR3512/3544. This is a finite-field side result, not a supplier or rational decoder improvement.",
+  "bottleneck_link": "A strict finite-field rank obstruction prevents a saturated low-rank surrogate from being mistaken for an attainable small-unit fitting pattern; rational rank and physical costs remain separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified original lower bound. Do not pursue attainment or larger dimensions.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the bounds over every characteristic-two field. verify.py enumerates 136 types, the regular moment, 18 tensor fixtures, two rank-addition fixtures and seven rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is the regular characteristic-two fitting minimum 22?",
+      "why_it_matters": "This would turn the strict obstruction into an exact value.",
+      "first_step": "Seek a cover of all 105 regular types by 22 compatible classes or a literal rank-22 factorization.",
+      "blocked_by": "No attaining matrix is supplied."
+    },
+    {
+      "question": "Can the full regular mask have fitting rank below 22 in characteristic zero?",
+      "why_it_matters": "The retained bit-window application uses rational rather than characteristic-two rank.",
+      "first_step": "Search rational factors with the same zero pattern, citing PR3544 as the all-field lower-bound premise.",
+      "blocked_by": "The binary parity mask does not retain its five-column factorization in characteristic zero."
+    }
+  ]
+}