Prove the exact odd-rectangle residual-rank floor for any stage size and hub count: 72ρ at u = h = ρ (no κ)

research/rectangle-law-exact-floor/PROOF.md

@@ -0,0 +1,140 @@
+# Proof: the exact floor of an odd rectangle of residual ranks
+
+Scoped proof over every field of characteristic not 2. The finite checks in
+`verify.py` corroborate it; they are not part of the proof.
+
+## 0. Setting and statement
+
+Fix a field K with 2 != 0, integers u, h >= 1, and signs s_dc, s_df, s_ec, s_ef in
+{+1, -1} with product -1 (an *odd* rectangle). For A_d, A_e in K^{u x h} and
+B_c, B_f in K^{h x u} put
+
+    C_xy = s_xy I_u - A_x B_y            (x in {d, e}, y in {c, f}),
+    r_xy = rank C_xy,   Sigma = r_dc + r_df + r_ec + r_ef.
+
+This is the cell of Lemma 1 of PR #6935 (DreamingOfClouds, `research/p104-root-cut-laws`) with
+stage size u and hub count h in place of rho = u = h = 2; there it is proved that
+Sigma >= min(rho, 2) for square rho x rho matrices.
+
+**Theorem 1.** The least value of Sigma over all A_x, B_y is
+
+    f(u, h) = max(0, 2u - h, 3u - 2h, 4u - 4h).
+
+Equivalently: f = 0 for h >= 2u; f = 2u - h for u <= h <= 2u; f = 3u - 2h for
+u/2 <= h <= u; f = 4(u - h) for h <= u/2. In particular f(rho, rho) = rho. It satisfies
+the duality f(u, h) = 4(u - h) + f(h, u).
+
+Throughout, G = [[s_dc, s_df], [s_ec, s_ef]]. Because the product of the four signs is -1,
+s_df s_ec = -s_dc s_ef, so
+
+    det G = s_dc s_ef - s_df s_ec = 2 s_dc s_ef != 0.                      (1)
+
+## 1. Lower bounds
+
+**Lemma A (block rank).** Sigma >= 2u - h.
+
+*Proof.* Put M = [A_d; A_e] in K^{2u x h} and N = [B_c  B_f] in K^{h x 2u}. The block matrix
+MN has blocks A_x B_y. Let S = G (x) I_u (a 2u x 2u matrix, blocks s_xy I_u). By (1) S is
+invertible. Then S - MN is the block matrix C = [[C_dc, C_df], [C_ec, C_ef]]. It is the sum of
+four matrices, each zero outside one block and of rank r_xy, so rank C <= Sigma. Hence
+2u = rank S <= rank(MN) + rank C <= h + Sigma. QED
+
+**Lemma B (cell rank through the dual product).** For s != 0, A in K^{u x h}, B in K^{h x u},
+
+    rank(s I_u - A B) = u - h + rank(s I_h - B A).
+
+*Proof.* If (s I_u - AB)v = 0 then ABv = sv, so BA(Bv) = s(Bv); and Bv = 0 would force
+sv = ABv = 0. So v -> Bv maps ker(s I_u - AB) injectively into ker(s I_h - BA). The map
+w -> Aw does the same in the other direction. The kernels have a common dimension d, and the
+ranks are u - d and h - d. QED
+
+**Lemma C (dual block rank).** With D_xy = s_xy I_h - B_y A_x, the sum of the four ranks
+rank D_xy is at least 2h - u.
+
+*Proof.* Put M' = [A_d  A_e] in K^{u x 2h}, N' = [B_c; B_f] in K^{2h x u}. The block matrix
+N'M' has blocks B_y A_x and rank at most u. S' = G^T (x) I_h is invertible by (1), and
+S' - N'M' has the blocks D_xy (row block y, column block x). As in Lemma A,
+2h = rank S' <= u + sum rank D_xy. QED
+
+**Proof of the lower bound.** Lemma B on each cell gives
+Sigma = 4(u - h) + sum rank D_xy. Lemma C then gives Sigma >= 4(u - h) + max(0, 2h - u)
+>= max(4u - 4h, 3u - 2h). Lemma A gives Sigma >= 2u - h, and Sigma >= 0. QED
+
+## 2. Attainment
+
+**Lemma D (one perturbed block).** Let n >= 1 and let G'' = [[a, b], [c, e]] have entries +-1 and
+product abce = -1. For 0 <= k <= n let Pi_k = diag(1^k, 0^(n-k)) and let X be G'' (x) I_n with
+2a Pi_k subtracted from its top-left n x n block. Then rank X = 2n - k.
+
+*Proof.* The bottom-right block e I_n is invertible. For a block matrix [[P, Q], [R, T]] with T
+invertible, rank = rank T + rank(P - Q T^-1 R). Here the Schur complement is
+(a I - 2a Pi_k) - b c e^-1 I = (a - bce) I - 2a Pi_k. From abce = -1 and a^2 = 1 we get
+bce = -a, so a - bce = 2a, and the complement is 2a (I - Pi_k), of rank n - k because
+2 != 0. So rank X = n + (n - k). QED
+
+**Case h >= u.** Let k = max(0, 2u - h) <= u and let X be the matrix of Lemma D with n = u,
+G'' = G. Then rank X = 2u - k <= h. Choose a rank factorisation X = MN with M of width exactly h
+(pad with zero columns), and read A_d, A_e as the top and bottom u rows of M and B_c, B_f as the
+left and right u columns of N. Then A_x B_y is the (x, y) block of X, and
+C_xy = (S - X)_xy, which is zero except C_dc = 2 s_dc Pi_k. So Sigma = k = max(0, 2u - h)
+= f(u, h), because for h >= u the term 2u - h dominates 3u - 2h and 4u - 4h.
+
+**Case h < u.** Let k' = max(0, 2h - u) <= h and let X' be the matrix of Lemma D with n = h and
+G'' = G^T = [[s_dc, s_ec], [s_df, s_ef]]. Then rank X' = 2h - k' <= u. Factor X' = N'M' with N'
+of width exactly u, put B_c, B_f for the top and bottom h rows of N' and A_d, A_e for the left and
+right h columns of M'. Then B_y A_x is the (y, x) block of X', so D_xy = (S' - X')_yx is zero
+except D_dc = 2 s_dc Pi_k'. By Lemma B, Sigma = 4(u - h) + k' = 4(u - h) + max(0, 2h - u)
+= max(4(u - h), 3u - 2h) = f(u, h), because for h < u the term 2u - h is dominated. QED
+
+Rank factorisations exist over every field, and the only place 2 != 0 is used is Lemma D and (1),
+so attainment holds over every field of characteristic not 2. `verify.py` builds the
+factorisations explicitly over Q for 1 <= u, h <= 8 and all eight odd sign patterns.
+
+## 3. Corollary: Theorem S for any stage size and hub count
+
+Hypothesis (S_u) is hypothesis (S) of the source with u x u in place of 2 x 2: L = 18 stages of
+u LOCAL units each (the units of stage d precede those of stage c when d < c), Gamma_dc the
+u x u matrix (y_a . x_b) over all coordinates with a a unit of stage d and b a unit of stage c,
+and sgn(d - c) Gamma_dc = Xi_d H_c with Xi_d, H_c invertible u x u for every d != c. (The source
+writes the unit indices as u and v; here u is the stage size.)
+Take any h hub coordinates; let Xi'_d (u x h) hold the y-entries of stage d at the hubs and
+H'_c (h x u) the x-entries of stage c. The cell with the hubs removed is
+s Xi_d H_c - Xi'_d H'_c = Xi_d (s I - A_d B_c) H_c with A_d = Xi_d^-1 Xi'_d and
+B_c = H'_c H_c^-1, so R_dc = rank(s I - A_d B_c) with s = sgn(d - c), exactly as in the source.
+
+**Corollary 2.** Under (S_u), for any h hubs and char K != 2,
+
+    sum over d != c of R_dc >= 72 f(u, h).
+
+*Proof.* Lemma 2 of the source gives 72 pairwise cell-disjoint rectangles in the 18 x 18
+off-diagonal grid, each with odd sign product (`verify.py` recomputes the 72 rectangles, their
+disjointness and their parity). Apply Theorem 1 to each. QED
+
+At u = h = rho this is 72 rho. For rho = 2 it is the 144 of Theorem S. For two hubs and u >= 4
+units it is 288 (u - 2).
+
+## 4. Exactness at u = h, and the packing number
+
+**Proposition 3.** For u = h = rho and L = 18 the least possible total over all A_d, B_c is
+exactly 72 rho.
+
+*Proof.* The lower bound is Corollary 2. For the upper bound take A_d = x_d I_rho and
+B_c = y_c I_rho with x, y in {+1, -1}^18. The cell is (sgn(d - c) - x_d y_c) I_rho: zero if
+x_d y_c = sgn(d - c), and 2 sgn(d - c) I_rho of rank rho otherwise. An exhaustive search over x
+(2^18 choices, the best y per column) finds the least number of mismatching off-diagonal cells to
+be 72 (finite certificate). The total is then 72 rho. QED
+
+The same search gives ⌊(L - 1)^2 / 4⌋ mismatches for every L from 2 to 18 (finite computation;
+no general-L proof is claimed). Since every odd rectangle forces at least f(1, 1) = 1 mismatch in
+the scalar case, 72 is also the largest number of cell-disjoint odd rectangles in the L = 18 grid:
+a larger packing would contradict the scalar solution with 72 mismatches. So the packing of Lemma 2
+cannot be improved to a larger floor at u = h.
+
+## 5. What is not claimed
+
+* Nothing about whether any root with rho > 2 satisfies (S_u), about the hub rank law, Theorem H,
+  the cut costs or any price. (S_u) is a matrix hypothesis here.
+* For u != h the grid floor 72 f(u, h) is a lower bound only. It is vacuous where f = 0 (for
+  example h >= 2u), and no matching total is claimed away from u = h.
+* Characteristic 2 is excluded: for K = F_2 the matrix G is singular and the floor is 0 at
+  (u, h) = (1, 1) and (2, 2) (checked exhaustively in `verify.py`).

research/rectangle-law-exact-floor/README.md

@@ -0,0 +1,118 @@
+# The exact floor of an odd rectangle of residual ranks, for any stage size and hub count
+
+**Scoped proof over every field of characteristic not 2, with exact finite corroboration.
+No new κ, no word, no price, no supplier admission, no frontier change.**
+
+This answers open question 2 of DreamingOfClouds's [PR #6935](https://github.com/CrocSwap/integer-mult-bounds/pull/6935)
+(`research/p104-root-cut-laws`): does Theorem S, the residual-rank floor 144 for 18 two-unit
+stages, extend to stages of more than two units and to rho > 2 with a floor proportional to rho?
+Its Lemma 1 (the rectangle law) gives only min(rho, 2) when rho > 2.
+
+## Result
+
+Take signs s_dc, s_df, s_ec, s_ef = ±1 with product -1, matrices A_d, A_e of size u by h and B_c, B_f of
+size h by u over a field of characteristic not 2, and the four cells C_xy = s_xy I_u − A_x B_y.
+
+**Theorem 1.** The least possible value of rank C_dc + rank C_df + rank C_ec + rank C_ef is
+
+    f(u, h) = max(0, 2u − h, 3u − 2h, 4u − 4h).
+
+| u \ h | 1 | 2 | 3 | 4 | 5 | 6 |
+|---|---:|---:|---:|---:|---:|---:|
+| 1 | 1 | 0 | 0 | 0 | 0 | 0 |
+| 2 | 4 | 2 | 1 | 0 | 0 | 0 |
+| 3 | 8 | 5 | 3 | 2 | 1 | 0 |
+| 4 | 12 | 8 | 6 | 4 | 3 | 2 |
+| 5 | 16 | 12 | 9 | 7 | 5 | 4 |
+| 6 | 20 | 16 | 12 | 10 | 8 | 6 |
+
+At u = h = rho the floor is rho, not min(rho, 2). The proof is two block-rank inequalities
+(2u = rank of an invertible sign matrix tensored with I_u, bounded by h plus the residual
+ranks, and the same for the h by h products B_y A_x) joined by the identity
+rank(s I − AB) = u − h + rank(s I − BA). Attainment is one perturbed block and a rank
+factorisation. See [PROOF.md](PROOF.md).
+
+**Corollary 2 (Theorem S for any stage size and hub count).** Under hypothesis (S) of the source
+with u-unit stages (invertible u by u factors Xi_d, H_c) and any h hub coordinates, the hub-removed
+residual ranks R_dc of the 18-stage grid satisfy
+
+    sum over d ≠ c of R_dc ≥ 72 f(u, h).
+
+At u = h = rho this is 72 rho (144 at rho = 2, the source's Theorem S).
+
+**Proposition 3.** At u = h = rho the total 72 rho is attained, so it is the exact minimum of the
+abstract matrix problem. The scalar case rests on a finite search: over x, y in {±1}^18 the least
+number of off-diagonal cells with x_d y_c ≠ sgn(d − c) is 72. The same search gives ⌊(L−1)²/4⌋ for
+every L from 2 to 18 (computed, no general-L proof). Hence 72 is also the largest number of
+cell-disjoint odd rectangles in the L = 18 grid.
+
+## Evidence
+
+`verify.py` (standard library; about 20 s; normal and optimized modes):
+
+* the lower bound is a written proof, not a search; the verifier checks the identity
+  rank(s I − AB) = u − h + rank(s I − BA) on 300 random instances over F_3, F_5, F_7, F_11;
+* 512 explicit configurations (every 1 ≤ u, h ≤ 8, all eight odd sign patterns) built by the
+  proof's construction over Q, each with total rank exactly f(u, h);
+* exhaustive minimum over all (A_d, A_e, B_c, B_f), canonical signs, equal to f(u, h) for
+  (u, h) in F_3: (1,1), (1,2), (2,1), (1,3), (3,1), (2,2), and with A_d reduced to its normal form
+  (1,4), (4,1), (2,3), (3,2); in F_5 and F_7: (1,1), (1,2), (2,1). The eight odd sign patterns agree
+  at (1,1), (2,1), (1,2) over F_3. At (3,2) the minimum is 5, above the 4 that either of
+  2u − h and 4(u − h) alone would allow;
+* controls: over F_2 the floor is 0 at (1,1) and (2,2), and with an even sign product it is 0
+  over F_3 at (1,1) and (2,2);
+* the 72 rectangles of Lemma 2 of the source (disjoint, off-diagonal, odd product, 288 cells),
+  and the scalar grid minima for L = 2 to 18;
+* the block-diagonal configuration attains 72 rho exactly for rho = 1 to 4;
+* the five quoted source statements occur verbatim in the pinned `THEOREM.md` (SHA256-bound).
+
+The recomputed values are compared with [RESULT.json](RESULT.json).
+
+## Reproduce
+
+From the repository root:
+
+```sh
+python3.12 -I -B -W error research/rectangle-law-exact-floor/verify.py
+python3.12 -I -O -B -W error research/rectangle-law-exact-floor/verify.py
+python3.12 -B scripts/research_package.py --package research/rectangle-law-exact-floor
+```
+
+Each verifier run ends with `PASS_RECTANGLE_LAW_EXACT_FLOOR`. `--write` regenerates RESULT.json.
+
+## What changed in the task
+
+The card asks about joint helper bases and a legal causal split. This package is a side result:
+a rank inequality for the odd-rectangle step of a hub-removed cut bound. It builds no split and
+changes no paid profile.
+
+## Limitations
+
+* Hypothesis (S) with u-unit stages is a matrix hypothesis. Whether any actual root with rho > 2
+  satisfies it, and how many hub coordinates such a root has, is not shown. The hub rank law and
+  Theorem H of the source are not used or re-derived.
+* For u ≠ h the grid floor 72 f(u, h) is a lower bound only. It is vacuous where f = 0, and no
+  matching total is claimed away from u = h.
+* The scalar minimum ⌊(L−1)²/4⌋ is a finite computation for L ≤ 18, not a theorem for all L.
+* The source's Lemma 2 packing and Theorem S are cited, not replayed beyond the finite recount in
+  `verify.py`. No independent human or proof-kernel review is claimed.
+
+## Open next questions
+
+The structured form is in [TASK.json](TASK.json).
+
+1. **Exact grid total for u ≠ h.** The packing bound need not be tight when u ≠ h. First step: the
+   exact least total on small L by the same separation trick, for example L = 4 to 6 over F_3 at
+   (u, h) = (1, 2) and (2, 1). Blocker: the search space grows as p^(2L·u·h).
+2. **A closed form for every L.** Prove ⌊(L−1)²/4⌋ for the scalar grid and exhibit that many
+   cell-disjoint odd rectangles. First step: read the optimal sign vectors for L = 10 to 18.
+   Blocker: no general packing is exhibited.
+3. **Roots with rho > 2.** Does any connected root satisfy (S) with u > 2, and with how many hubs?
+   First step: the hub rank law of #6881 on a root with N − n = 3. Blocker: no such root is in the
+   repository.
+
+## Credit
+
+This package was produced by Nick Petalas. DreamingOfClouds's PR #6935 supplies the setting, Lemma 1,
+Lemma 2 and Theorem S, and the question; the hub rank law is from the same author's #6881. The
+Schur-complement and block-rank facts are classical. New work is Apache-2.0.

research/rectangle-law-exact-floor/RESULT.json

@@ -0,0 +1,113 @@
+{
+  "claim": "exact odd-rectangle rank floor f(u,h) = max(0, 2u-h, 3u-2h, 4u-4h)",
+  "constructions": {
+    "1,1": 1,
+    "1,2": 0,
+    "1,3": 0,
+    "1,4": 0,
+    "1,5": 0,
+    "1,6": 0,
+    "1,7": 0,
+    "1,8": 0,
+    "2,1": 4,
+    "2,2": 2,
+    "2,3": 1,
+    "2,4": 0,
+    "2,5": 0,
+    "2,6": 0,
+    "2,7": 0,
+    "2,8": 0,
+    "3,1": 8,
+    "3,2": 5,
+    "3,3": 3,
+    "3,4": 2,
+    "3,5": 1,
+    "3,6": 0,
+    "3,7": 0,
+    "3,8": 0,
+    "4,1": 12,
+    "4,2": 8,
+    "4,3": 6,
+    "4,4": 4,
+    "4,5": 3,
+    "4,6": 2,
+    "4,7": 1,
+    "4,8": 0,
+    "5,1": 16,
+    "5,2": 12,
+    "5,3": 9,
+    "5,4": 7,
+    "5,5": 5,
+    "5,6": 4,
+    "5,7": 3,
+    "5,8": 2,
+    "6,1": 20,
+    "6,2": 16,
+    "6,3": 12,
+    "6,4": 10,
+    "6,5": 8,
+    "6,6": 6,
+    "6,7": 5,
+    "6,8": 4,
+    "7,1": 24,
+    "7,2": 20,
+    "7,3": 16,
+    "7,4": 13,
+    "7,5": 11,
+    "7,6": 9,
+    "7,7": 7,
+    "7,8": 6,
+    "8,1": 28,
+    "8,2": 24,
+    "8,3": 20,
+    "8,4": 16,
+    "8,5": 14,
+    "8,6": 12,
+    "8,7": 10,
+    "8,8": 8
+  },
+  "constructions_range": 8,
+  "controls": true,
+  "exhaustive_minima": {
+    "F3:1,1": 1,
+    "F3:1,2": 0,
+    "F3:1,3": 0,
+    "F3:1,4*": 0,
+    "F3:2,1": 4,
+    "F3:2,2": 2,
+    "F3:2,3*": 1,
+    "F3:3,1": 8,
+    "F3:3,2*": 5,
+    "F3:4,1*": 12,
+    "F5:1,1": 1,
+    "F5:1,2": 0,
+    "F5:2,1": 4,
+    "F7:1,1": 1,
+    "F7:1,2": 0,
+    "F7:2,1": 4
+  },
+  "formula_identities": true,
+  "packing_rectangles": 72,
+  "random_grid_trials": 40,
+  "rank_identity_trials": 300,
+  "scalar_grid_minima": {
+    "10": 20,
+    "11": 25,
+    "12": 30,
+    "13": 36,
+    "14": 42,
+    "15": 49,
+    "16": 56,
+    "17": 64,
+    "18": 72,
+    "2": 0,
+    "3": 1,
+    "4": 2,
+    "5": 4,
+    "6": 6,
+    "7": 9,
+    "8": 12,
+    "9": 16
+  },
+  "source_sha256": "c591472a1fdfdda982c6e0a9ddac96c5964cf7b9f933f03cde9d0164c98ff339"
+}

research/rectangle-law-exact-floor/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/p104-root-cut-laws/THEOREM.md",
+      "usage": "input",
+      "git_blob": "0cd25145ef733aad5d6f62e6857921c4656b7e57",
+      "sha256": "c591472a1fdfdda982c6e0a9ddac96c5964cf7b9f933f03cde9d0164c98ff339"
+    }
+  ]
+}