diff --git a/research/rectangle-law-exact-floor/PROOF.md b/research/rectangle-law-exact-floor/PROOF.md new file mode 100644 index 0000000000..558719e2b6 --- /dev/null +++ b/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`). diff --git a/research/rectangle-law-exact-floor/README.md b/research/rectangle-law-exact-floor/README.md new file mode 100644 index 0000000000..2adb130624 --- /dev/null +++ b/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. diff --git a/research/rectangle-law-exact-floor/RESULT.json b/research/rectangle-law-exact-floor/RESULT.json new file mode 100644 index 0000000000..673c77b3d6 --- /dev/null +++ b/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" +} diff --git a/research/rectangle-law-exact-floor/SOURCES.json b/research/rectangle-law-exact-floor/SOURCES.json new file mode 100644 index 0000000000..6625cd34c0 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/rectangle-law-exact-floor/TASK.json b/research/rectangle-law-exact-floor/TASK.json new file mode 100644 index 0000000000..f323f8b024 --- /dev/null +++ b/research/rectangle-law-exact-floor/TASK.json @@ -0,0 +1,129 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "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", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.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": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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", + "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": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "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": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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 least sum of the four residual ranks of one odd sign rectangle, cells s_xy I_u - A_x B_y with A_x of size u by h and B_y of size h by u, over every field of characteristic not 2: f(u,h) = max(0, 2u-h, 3u-2h, 4u-4h). Corollary: the residual-rank floor of Theorem S of PR6935 (research/p104-root-cut-laws) becomes 72 f(u,h) for 18 stages of u units with h hub coordinates, which is 72 rho at u = h = rho and exact there; the scalar 18-stage minimum is 72 by finite search. Matrix hypothesis only; no root, word, price or kappa.", + "scope_change_reason": "The card asks for a joint helper basis or causal split. This package instead answers open question 2 of PR6935: whether Theorem S extends to stages of more than two units and to rho > 2 with a floor proportional to rho. It is a rank inequality for the odd-rectangle step of a hub-removed cut bound and does not build or price a split.", + "bottleneck_link": "Side result. It removes the restriction to two-unit stages and two hubs from the residual-rank floor of PR6935's Theorem S, as a statement about matrices. It does not change any paid profile, supplier, invoice or kappa, and it does not show that a root with rho > 2 exists.", + "budget_minutes": 60, + "stop_rule": "Stop when the exact rectangle minimum is proved for all (u,h) with matching constructions and the 18-stage corollary is stated at the strength proved. Do not extend to a pricing, to the hub rank law, to roots with rho > 2, or to a total for u != h.", + "outcome": "completed", + "evidence": "verify.py (standard library, about 20 s, normal and optimized): identities f(u,h) = 4(u-h) + f(h,u); 512 explicit configurations over Q for 1 <= u,h <= 8 and all eight odd sign patterns with total exactly f(u,h); exhaustive minima equal to f(u,h) over F_3 at (1,1),(1,2),(2,1),(1,3),(3,1),(2,2) and, with A_d reduced to normal form, (1,4),(4,1),(2,3),(3,2), over F_5 and F_7 at (1,1),(1,2),(2,1); eight sign patterns agree at three small cases; characteristic-2 and even-sign controls; the 72 disjoint odd rectangles of the source recounted; scalar 18-stage minimum 72 and minima floor((L-1)^2/4) for L = 2 to 18; block-diagonal attainment of 72 rho for rho = 1 to 4; 300 random trials of the dual-rank identity; source statements matched in the pinned THEOREM.md. PROOF.md gives the written proof of the lower and upper bounds.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact least total over the 18-stage grid when u differs from h?", + "why_it_matters": "Corollary 2 is a lower bound there; the packing bound need not be tight, so the true floor for stages with more units than hubs is unknown.", + "first_step": "Compute the exact least total on small L (4 to 6) over F_3 at (u,h) = (1,2) and (2,1) by the same separation of the four-cycle sum.", + "blocked_by": "The search space grows as p^(2*L*u*h); a structural argument for the grid, beyond the single rectangle, is not known." + }, + { + "question": "Is the scalar grid minimum floor((L-1)^2/4) for every L, with that many cell-disjoint odd rectangles?", + "why_it_matters": "It would give the exact residual-rank floor rho*floor((L-1)^2/4) at u = h = rho for any number of stages, not only L = 18.", + "first_step": "Read the optimal sign vectors for L = 10 to 18 from verify.py and guess the pattern, then exhibit the packing.", + "blocked_by": "The value is verified only for L <= 18; no general packing or matching construction is written." + }, + { + "question": "Does any connected P104 root satisfy hypothesis (S) with u > 2, and with how many hub coordinates?", + "why_it_matters": "Corollary 2 only matters for words whose hub-removed blocks factor with invertible u by u stage factors; no such root with N - n > 2 is in the repository.", + "first_step": "Apply the hub rank law of PR6881 to a root with N - n = 3 and test the factorisation of the stage blocks.", + "blocked_by": "No root with N - n > 2 is available, and Theorem H of PR6935 only bounds the hub count from below." + } + ] +} diff --git a/research/rectangle-law-exact-floor/VERIFY.json b/research/rectangle-law-exact-floor/VERIFY.json new file mode 100644 index 0000000000..322f2b273a --- /dev/null +++ b/research/rectangle-law-exact-floor/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-root-cut-laws/THEOREM.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Recomputes RESULT.json: constructions for 1<=u,h<=8 and all odd sign patterns over Q, exhaustive finite-field minima, controls, 72-rectangle packing, scalar grid minima, source quotes bound to THEOREM.md." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same checks with assertions disabled (every check uses an explicit exception)." + } + ] +} diff --git a/research/rectangle-law-exact-floor/verify.py b/research/rectangle-law-exact-floor/verify.py new file mode 100644 index 0000000000..a148f294d7 --- /dev/null +++ b/research/rectangle-law-exact-floor/verify.py @@ -0,0 +1,479 @@ +#!/usr/bin/env python3 +"""Verifier for the exact odd-rectangle rank floor (standard library only). + +Claim checked (proof in PROOF.md). Fix a field K of characteristic not 2, +sizes u, h >= 1, and signs s_dc, s_df, s_ec, s_ef in {+1,-1} with product -1. +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. +Then the least 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). + +The lower bound is a proof (PROOF.md); this script checks the attaining +constructions exactly over Q, minimises exhaustively over small finite +fields, checks the 18-stage grid corollary and binds the quoted source text. + +Run: python3 -I -B research/rectangle-law-exact-floor/verify.py + python3 -I -B research/rectangle-law-exact-floor/verify.py --write (regenerate RESULT.json) +""" +import hashlib +import itertools +import json +import os +import random +import sys +from fractions import Fraction + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.dirname(os.path.dirname(HERE)) +RESULT_PATH = os.path.join(HERE, "RESULT.json") +SOURCE_REL = "research/p104-root-cut-laws/THEOREM.md" +MAX_DIM = 8 # construction range: 1 <= u, h <= MAX_DIM +GRID_L = 18 # number of stages in Theorem S of the source package +RHO_RANGE = (1, 2, 3, 4) +SIGN_PATTERNS = [s for s in itertools.product((1, -1), repeat=4) if s[0] * s[1] * s[2] * s[3] == -1] +CANONICAL = (1, -1, 1, 1) # (s_dc, s_df, s_ec, s_ef); every odd pattern is switching-equivalent to it + + +def need(condition, message): + """Fail loudly; unlike assert this survives python -O.""" + if not condition: + raise AssertionError(message) + + +def formula(u, h): + return max(0, 2 * u - h, 3 * u - 2 * h, 4 * u - 4 * h) + + +# ---------------------------------------------------------------- linear algebra + +def zeros(m, n): + return [[Fraction(0)] * n for _ in range(m)] + + +def matmul(a, b): + need(len(a[0]) == len(b), "shape mismatch in matmul") + cols = list(zip(*b)) + return [[sum(x * y for x, y in zip(row, col)) for col in cols] for row in a] + + +def block_sign_matrix(g, size, transpose=False): + """Kronecker product of the 2x2 sign matrix g (or its transpose) with I_size.""" + out = zeros(2 * size, 2 * size) + for x in range(2): + for y in range(2): + sign = g[y][x] if transpose else g[x][y] + for i in range(size): + out[x * size + i][y * size + i] = Fraction(sign) + return out + + +def rank_q(rows): + """Rank over Q by exact Gaussian elimination.""" + m = [[Fraction(x) for x in r] for r in rows] + rank = 0 + for c in range(len(m[0]) if m else 0): + piv = next((r for r in range(rank, len(m)) if m[r][c] != 0), None) + if piv is None: + continue + m[rank], m[piv] = m[piv], m[rank] + lead = m[rank][c] + m[rank] = [x / lead for x in m[rank]] + for r in range(len(m)): + if r != rank and m[r][c] != 0: + f = m[r][c] + m[r] = [x - f * y for x, y in zip(m[r], m[rank])] + rank += 1 + return rank + + +def rank_mod(rows, p): + """Rank over the prime field F_p.""" + m = [[x % p for x in r] for r in rows] + rank = 0 + for c in range(len(m[0]) if m else 0): + piv = next((r for r in range(rank, len(m)) if m[r][c]), None) + if piv is None: + continue + m[rank], m[piv] = m[piv], m[rank] + inv = pow(m[rank][c], -1, p) + m[rank] = [(x * inv) % p for x in m[rank]] + for r in range(len(m)): + if r != rank and m[r][c]: + f = m[r][c] + m[r] = [(x - f * y) % p for x, y in zip(m[r], m[rank])] + rank += 1 + return rank + + +def factor_q(p_mat, r): + """Return (M, N) with p_mat = M N, M of width exactly r, N of height exactly r.""" + rows, cols = len(p_mat), len(p_mat[0]) + m = [[Fraction(x) for x in row] for row in p_mat] + pivots, rank = [], 0 + for c in range(cols): + piv = next((i for i in range(rank, rows) if m[i][c] != 0), None) + if piv is None: + continue + m[rank], m[piv] = m[piv], m[rank] + lead = m[rank][c] + m[rank] = [x / lead for x in m[rank]] + for i in range(rows): + if i != rank and m[i][c] != 0: + f = m[i][c] + m[i] = [x - f * y for x, y in zip(m[i], m[rank])] + pivots.append(c) + rank += 1 + need(rank <= r, "rank %d exceeds factor width %d" % (rank, r)) + left = [[Fraction(p_mat[i][c]) for c in pivots] + [Fraction(0)] * (r - rank) for i in range(rows)] + right = [m[k][:] for k in range(rank)] + [[Fraction(0)] * cols for _ in range(r - rank)] + return left, right + + +# ---------------------------------------------------------------- constructions + +def cells(u, signs, a_d, a_e, b_c, b_f): + s_dc, s_df, s_ec, s_ef = signs + out = {} + for name, s, a, b in (("dc", s_dc, a_d, b_c), ("df", s_df, a_d, b_f), + ("ec", s_ec, a_e, b_c), ("ef", s_ef, a_e, b_f)): + prod = matmul(a, b) + out[name] = [[Fraction(s if i == j else 0) - prod[i][j] for j in range(u)] for i in range(u)] + return out + + +def construct_primal(u, h, signs): + """Case h >= u: one perturbed block of S = G (x) I_u, then rank factorisation.""" + s_dc, s_df, s_ec, s_ef = signs + g = [[s_dc, s_df], [s_ec, s_ef]] + k = max(0, 2 * u - h) + p_mat = block_sign_matrix(g, u) + for i in range(k): + p_mat[i][i] -= 2 * s_dc # block (d,c) of S - W, W = 2 s_dc Pi, rank Pi = k + left, right = factor_q(p_mat, h) + a_d, a_e = left[:u], left[u:] + b_c = [row[:u] for row in right] + b_f = [row[u:] for row in right] + return a_d, a_e, b_c, b_f + + +def construct_dual(u, h, signs): + """Case h < u: build B_y A_x first (an h-dimensional problem through width u).""" + s_dc, s_df, s_ec, s_ef = signs + g = [[s_dc, s_df], [s_ec, s_ef]] + k2 = max(0, 2 * h - u) + p_mat = block_sign_matrix(g, h, transpose=True) # rows (c,f), columns (d,e) + for i in range(k2): + p_mat[i][i] -= 2 * s_dc + n_mat, m_mat = factor_q(p_mat, u) # p_mat = n_mat m_mat, widths u + a_d = [row[:h] for row in m_mat] + a_e = [row[h:] for row in m_mat] + b_c, b_f = n_mat[:h], n_mat[h:] + return a_d, a_e, b_c, b_f + + +def construct(u, h, signs): + return construct_primal(u, h, signs) if h >= u else construct_dual(u, h, signs) + + +def check_construction(u, h, signs): + a_d, a_e, b_c, b_f = construct(u, h, signs) + need(len(a_d) == u and len(a_d[0]) == h and len(b_c) == h and len(b_c[0]) == u, "factor shapes") + total = sum(rank_q(c) for c in cells(u, signs, a_d, a_e, b_c, b_f).values()) + need(total == formula(u, h), "construction (%d,%d,%s) gives %d, formula %d" % (u, h, signs, total, formula(u, h))) + return total + + +def check_all_constructions(): + table = {} + for u in range(1, MAX_DIM + 1): + for h in range(1, MAX_DIM + 1): + totals = {check_construction(u, h, s) for s in SIGN_PATTERNS} + need(totals == {formula(u, h)}, "attainment (%d,%d)" % (u, h)) + table["%d,%d" % (u, h)] = formula(u, h) + return table + + +def check_formula_identities(): + for u in range(1, 40): + for h in range(1, 40): + need(formula(u, h) == 4 * (u - h) + formula(h, u), "duality %d %d" % (u, h)) + need(formula(u, h) >= max(0, 2 * u - h), "block bound") + if h >= 2 * u: + need(formula(u, h) == 0, "zero region") + for u in range(1, 40): + need(formula(u, u) == u, "diagonal value") + return True + + +# ---------------------------------------------------------------- finite-field minima + +def all_matrices(rows, cols, p): + for flat in itertools.product(range(p), repeat=rows * cols): + yield tuple(tuple(flat[r * cols:(r + 1) * cols]) for r in range(rows)) + + +def rank_table(u, h, p, mats_a, mats_b, signs_needed): + """T[s][i][j] = rank over F_p of s I - A_i B_j, cached on the product matrix.""" + cache = {} + tables = {s: [[0] * len(mats_b) for _ in mats_a] for s in signs_needed} + for i, a in enumerate(mats_a): + for j, b in enumerate(mats_b): + prod = tuple(tuple(sum(a[r][t] * b[t][c] for t in range(h)) % p for c in range(u)) for r in range(u)) + for s in signs_needed: + key = (prod, s) + if key not in cache: + cache[key] = rank_mod([[((s if r == c else 0) - prod[r][c]) % p for c in range(u)] + for r in range(u)], p) + tables[s][i][j] = cache[key] + return tables + + +def normal_forms(u, h): + forms = [] + for r in range(min(u, h) + 1): + forms.append(tuple(tuple(1 if (i == j and i < r) else 0 for j in range(h)) for i in range(u))) + return forms + + +def exhaustive_minimum(u, h, p, signs=CANONICAL, reduce_by_symmetry=False): + """Exact minimum over F_p; the sum separates once A_d and A_e are fixed.""" + mats = list(all_matrices(u, h, p)) + mats_b = list(all_matrices(h, u, p)) + s_dc, s_df, s_ec, s_ef = signs + sign_values = sorted({s % p for s in signs}) + tab = rank_table(u, h, p, mats, mats_b, sign_values) + index = {m: i for i, m in enumerate(mats)} + firsts = [index[m] for m in normal_forms(u, h)] if reduce_by_symmetry else range(len(mats)) + best = None + for i_d in firsts: + for i_e in range(len(mats)): + via_c = min(tab[s_dc % p][i_d][j] + tab[s_ec % p][i_e][j] for j in range(len(mats_b))) + via_f = min(tab[s_df % p][i_d][j] + tab[s_ef % p][i_e][j] for j in range(len(mats_b))) + if best is None or via_c + via_f < best: + best = via_c + via_f + return best + + +EXHAUSTIVE_FULL = [(1, 1, 3), (1, 2, 3), (2, 1, 3), (1, 3, 3), (3, 1, 3), (2, 2, 3), (1, 1, 5), (1, 2, 5), + (2, 1, 5), (1, 1, 7), (2, 1, 7), (1, 2, 7)] +EXHAUSTIVE_REDUCED = [(1, 4, 3), (4, 1, 3), (2, 3, 3), (3, 2, 3)] + + +def check_exhaustive(): + found = {} + for (u, h, p) in EXHAUSTIVE_FULL: + got = exhaustive_minimum(u, h, p) + need(got == formula(u, h), "exhaustive F_%d (%d,%d): %d vs %d" % (p, u, h, got, formula(u, h))) + found["F%d:%d,%d" % (p, u, h)] = got + for (u, h, p) in EXHAUSTIVE_REDUCED: + got = exhaustive_minimum(u, h, p, reduce_by_symmetry=True) + need(got == formula(u, h), "exhaustive reduced F_%d (%d,%d): %d vs %d" % (p, u, h, got, formula(u, h))) + found["F%d:%d,%d*" % (p, u, h)] = got + for s in SIGN_PATTERNS: # all eight odd patterns agree (switching lemma), small cases + for (u, h) in ((1, 1), (2, 1), (1, 2)): + need(exhaustive_minimum(u, h, 3, signs=s) == formula(u, h), "pattern %s (%d,%d)" % (s, u, h)) + return found + + +def check_controls(): + """The hypotheses are needed: characteristic 2 and even sign products break the floor. + + Also a discriminating control: at (u, h) = (3, 2) the two single-argument bounds both give 4, + but the exhaustive minimum over F_3 is 5, so the third term 3u - 2h is not removable. + """ + weak = max(0, 2 * 3 - 2, 4 * (3 - 2)) + need(weak == 4 and exhaustive_minimum(3, 2, 3, reduce_by_symmetry=True) == 5 > weak, "weak bound control") + need(exhaustive_minimum(1, 1, 2, signs=(1, 1, 1, 1)) == 0 < formula(1, 1), "char 2 control (1,1)") + need(exhaustive_minimum(2, 2, 2, signs=(1, 1, 1, 1)) == 0 < formula(2, 2), "char 2 control (2,2)") + need(exhaustive_minimum(1, 1, 3, signs=(1, 1, 1, 1)) == 0, "even product control") + need(exhaustive_minimum(2, 2, 3, signs=(1, 1, 1, 1)) == 0, "even product control (2,2)") + return True + + +# ---------------------------------------------------------------- the two proof identities + +def check_rank_identity(trials=300, seed=20261110): + """rank(sI_u - AB) = u - h + rank(sI_h - BA) for s != 0 (used in the proof).""" + rng = random.Random(seed) + for _ in range(trials): + u, h = rng.randint(1, 5), rng.randint(1, 5) + p = rng.choice((3, 5, 7, 11)) + s = rng.choice((1, p - 1)) + a = [[rng.randrange(p) if rng.random() < 0.7 else 0 for _ in range(h)] for _ in range(u)] + b = [[rng.randrange(p) if rng.random() < 0.7 else 0 for _ in range(u)] for _ in range(h)] + ab = [[sum(a[i][t] * b[t][j] for t in range(h)) % p for j in range(u)] for i in range(u)] + ba = [[sum(b[i][t] * a[t][j] for t in range(u)) % p for j in range(h)] for i in range(h)] + left = rank_mod([[(s if i == j else 0) - ab[i][j] for j in range(u)] for i in range(u)], p) + right = rank_mod([[(s if i == j else 0) - ba[i][j] for j in range(h)] for i in range(h)], p) + need(left == u - h + right, "rank identity failed") + return trials + + +# ---------------------------------------------------------------- the 18-stage grid + +def sgn(x): + return (x > 0) - (x < 0) + + +def packing_rectangles(): + rects = [] + for i in range(1, 10): + for j in range(i + 1, 10): + rects.append(((i, j), (i + 9, j), (i + 9, j + 9), (i, j + 9))) + rects.append(((j, i), (j + 9, i), (j + 9, i + 9), (j, i + 9))) + return rects + + +def check_packing(): + rects = packing_rectangles() + need(len(rects) == 72, "72 rectangles") + used = set() + for rect in rects: + prod = 1 + for (d, c) in rect: + need(1 <= d <= GRID_L and 1 <= c <= GRID_L and d != c, "off-diagonal cell") + prod *= sgn(d - c) + need(prod == -1, "odd sign product") + need(len({d for d, _ in rect}) == 2 and len({c for _, c in rect}) == 2, "rectangle shape") + for cell in rect: + need(cell not in used, "cells overlap") + used.add(cell) + need(len(used) == 288, "288 cells") + return len(rects) + + +def best_sign_vectors(length): + """Least number of off-diagonal cells where x_d y_c != sgn(d-c); returns (count, x, y).""" + full = (1 << length) - 1 + pats = [sum(1 << d for d in range(length) if d > c) for c in range(length)] + masks = [full & ~(1 << c) for c in range(length)] + best, best_x = None, 0 + for x in range(1 << length): + total = 0 + for c in range(length): + a = bin((x ^ pats[c]) & masks[c]).count("1") + total += min(a, length - 1 - a) + if best is not None and total >= best: + break + else: + best, best_x = total, x + y = [] + for c in range(length): + a = bin((best_x ^ pats[c]) & masks[c]).count("1") + y.append(1 if a <= length - 1 - a else -1) + xs = [1 if (best_x >> d) & 1 else -1 for d in range(length)] + return best, xs, y + + +def grid_total(rho, xs, ys): + """Sum over d != c of rank(s_dc I - x_d y_c I_rho) for the block-diagonal configuration.""" + total = 0 + for d in range(len(xs)): + for c in range(len(ys)): + if d != c: + cell = [[Fraction(sgn(d - c) - xs[d] * ys[c]) if i == j else Fraction(0) for j in range(rho)] + for i in range(rho)] + total += rank_q(cell) + return total + + +def check_grid(): + mins = {} + for length in range(2, GRID_L + 1): + best, xs, ys = best_sign_vectors(length) + need(best == (length - 1) ** 2 // 4, "grid minimum L=%d" % length) + mins[str(length)] = best + best, xs, ys = best_sign_vectors(GRID_L) + need(best == 72, "18-stage scalar minimum") + for rho in RHO_RANGE: + need(grid_total(rho, xs, ys) == 72 * rho, "block-diagonal attainment rho=%d" % rho) + return mins + + +def random_grid_floor(trials=40, seed=7): + """Random (A_d, B_c) over F_p never beat 72 f(u,h) on the 18-stage grid (corroboration only).""" + rng = random.Random(seed) + floor_rects = len(packing_rectangles()) + for _ in range(trials): + u, h = rng.randint(1, 4), rng.randint(1, 4) + p = rng.choice((3, 5)) + mats_a = [[[rng.randrange(p) for _ in range(h)] for _ in range(u)] for _ in range(GRID_L + 1)] + mats_b = [[[rng.randrange(p) for _ in range(u)] for _ in range(h)] for _ in range(GRID_L + 1)] + total = 0 + for d in range(1, GRID_L + 1): + for c in range(1, GRID_L + 1): + if d != c: + ab = [[sum(mats_a[d][i][t] * mats_b[c][t][j] for t in range(h)) % p for j in range(u)] + for i in range(u)] + total += rank_mod([[(sgn(d - c) if i == j else 0) - ab[i][j] for j in range(u)] + for i in range(u)], p) + need(total >= floor_rects * formula(u, h), "random grid below the floor") + return trials + + +# ---------------------------------------------------------------- source binding + +QUOTES = [ + "R_dc + R_ec + R_ef + R_df >= min(rho, 2)", + "the 72 quadruples", + "Then sum over d != c of R_dc >= 144.", + "Not claimed: any statement for stages of more than two units, or for rho > 2 beyond Lemma 1.", + "R_dc = rank(s I - A_d B_c)", +] + + +def check_source(): + with open(os.path.join(ROOT, SOURCE_REL), "rb") as handle: + raw = handle.read() + with open(os.path.join(HERE, "SOURCES.json")) as handle: + sources = json.load(handle) + pinned = {row["path"]: row["sha256"] for row in sources["files"]} + digest = hashlib.sha256(raw).hexdigest() + need(pinned.get(SOURCE_REL) == digest, "THEOREM.md bytes differ from the pin") + text = raw.decode("utf-8") + for quote in QUOTES: + need(quote in text, "quote missing from the source: %r" % quote) + return digest + + +# ---------------------------------------------------------------- driver + +def compute_result(): + result = { + "claim": "exact odd-rectangle rank floor f(u,h) = max(0, 2u-h, 3u-2h, 4u-4h)", + "source_sha256": check_source(), + "formula_identities": check_formula_identities(), + "constructions_range": MAX_DIM, + "constructions": check_all_constructions(), + "rank_identity_trials": check_rank_identity(), + "exhaustive_minima": check_exhaustive(), + "controls": check_controls(), + "packing_rectangles": check_packing(), + "scalar_grid_minima": check_grid(), + "random_grid_trials": random_grid_floor(), + } + return result + + +def main(argv): + write = "--write" in argv + result = compute_result() + text = json.dumps(result, indent=2, sort_keys=True) + "\n" + if write: + with open(RESULT_PATH, "w") as handle: + handle.write(text) + print("wrote", RESULT_PATH) + else: + with open(RESULT_PATH) as handle: + need(handle.read() == text, "RESULT.json differs from the recomputed result") + print("PASS_FORMULA_IDENTITIES_AND_DUALITY") + print("PASS_CONSTRUCTIONS_ALL_SIGN_PATTERNS_%dx%d" % (MAX_DIM, MAX_DIM)) + print("PASS_EXHAUSTIVE_FINITE_FIELD_MINIMA") + print("PASS_CHARACTERISTIC_TWO_AND_EVEN_SIGN_CONTROLS") + print("PASS_GRID_72_RECTANGLES_AND_SCALAR_MINIMUM_72") + print("PASS_RECTANGLE_LAW_EXACT_FLOOR") + return 0 + + +if __name__ == "__main__": + sys.exit(main(sys.argv[1:]))