[petalas]

Summary

Claim type: scoped proof over every field of characteristic not 2, with exact finite corroboration. It is not a complete multiplication theorem, and it prices nothing: no κ, word, supplier admission or frontier change.

This answers open question 2 of DreamingOfClouds's merged #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 ρ > 2 with a floor proportional to ρ? Its Lemma 1 gives only min(ρ, 2) there.

Take signs s_dc, s_df, s_ec, s_ef = ±1 with product −1, matrices A_d, A_e of size u×h and B_c, B_f of size h×u, and the 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)

(0 for h ≥ 2u; 2u − h for u ≤ h ≤ 2u; 3u − 2h for u/2 ≤ h ≤ u; 4(u − h) for h ≤ u/2). At u = h = ρ the floor is ρ. It satisfies f(u, h) = 4(u − h) + f(h, u).

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

Proof idea (PROOF.md). The 2×2 sign matrix G has det G = 2·s_dc·s_ef ≠ 0 because the product is −1, so G⊗I_u is invertible of rank 2u. It equals the rank-≤h product [A_d; A_e]·[B_c B_f] plus the block matrix of the four cells, so 2u ≤ h + (sum of the four ranks). The same argument on the h×h products B_y·A_x gives sum ≥ 2h − u. The identity rank(sI − AB) = u − h + rank(sI − BA) joins the two. Attainment is one perturbed block of G⊗I (Schur complement) plus a rank factorisation.

Corollary 2 (Theorem S for any stage size and hub count). Under hypothesis (S) of #6935 with u-unit stages and any h hub coordinates, the hub-removed residual ranks of the 18-stage grid satisfy Σ_{d≠c} R_dc ≥ 72·f(u, h). At u = h = ρ this is 72ρ, which is 144 at ρ = 2.

Proposition 3. At u = h = ρ the total 72ρ is attained, so it is the exact minimum of the abstract matrix problem. The scalar case rests on an exhaustive search (finite certificate): over x, y ∈ {±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 only). Hence 72 is also the largest number of cell-disjoint odd rectangles in the L = 18 grid.

Evidence and reproduction

From the repository root, use CPython 3.12.15 at ~/git/integer-mult-bounds/.venv/bin/python3.12:

~/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/rectangle-law-exact-floor/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/rectangle-law-exact-floor/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rectangle-law-exact-floor
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rectangle-law-exact-floor --check-source-history

Local verification at head e1a8d85236d4c349a534bddc2f3c6bfaae02345d passed all four commands. Both direct modes printed PASS_RECTANGLE_LAW_EXACT_FLOOR and compared the recomputed values with RESULT.json; they took 6.62 s and 6.78 s respectively. The registered runner executed both VERIFY.json commands and printed PASS_REGISTERED_RESEARCH_PACKAGE research/rectangle-law-exact-floor outcome=completed in 13.62 s total. The source-history check printed PASS_RESEARCH_COMMIT_BYTES for 8 files in 0.20 s. The package bytes were unchanged after verification. These are local checks; CI did not certify the package.

The lower bound is a written proof; the verifier does not search for it. It checks:

• 512 explicit configurations over Q (every 1 ≤ u, h ≤ 8, all eight odd sign patterns), each with total rank exactly f(u, h);
• exhaustive minima equal to f(u, h) over F_3 at (u, h) = (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); over F_5 and F_7 at (1,1), (1,2), (2,1). At (3,2) the minimum is 5, above the 4 that 2u − h and 4(u − h) give separately;
• controls: over F_2 the floor is 0 at (1,1) and (2,2); with an even sign product it is 0 over F_3 at (1,1) and (2,2);
• the dual-rank identity on 300 random instances; the 72 disjoint odd rectangles of Root cut laws for two-chain words: hub, rectangle and cut bounds (no new κ) #6935's Lemma 2 (288 cells) recounted; the block-diagonal configuration attaining 72ρ for ρ = 1 to 4; five quoted statements found verbatim in the SHA256-pinned THEOREM.md.

Limitations and unrun obligations

• Hypothesis (S) with u-unit stages is a matrix hypothesis here. Whether any actual root with ρ > 2 satisfies it, and with how many hubs, is not shown. The hub rank law and Theorem H 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. No matching total is claimed away from u = h.
• ⌊(L−1)²/4⌋ is a finite computation for L ≤ 18, not a theorem for all L.
• Root cut laws for two-chain words: hub, rectangle and cut bounds (no new κ) #6935's Lemma 2 and Theorem S are cited and used, not re-proved beyond the finite recount above. No independent human or proof-kernel review is claimed.

Open next questions

1. Exact least grid total for u ≠ h. First step: 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. Blocker: the search space grows as p^(2·L·u·h).
2. Is the scalar minimum ⌊(L−1)²/4⌋ for every L, with 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. Does any connected P104 root satisfy (S) with u > 2, and with how many hubs? First step: the hub rank law of P104 surplus bound, hub rank law and form-capacity lemma with a hypothesis ledger (no kappa) #6881 on a root with N − n = 3. Blocker: no such root is in the repository.

The structured form is in TASK.json.

Related open work

• Conditional κ = 0.00339993 (+0.834% over #6833): host a pair of units at every root call #6883 studies a hosted P104 root with 18 two-unit stages and two added coordinates. This PR concerns the abstract residual-rank floor under hypothesis (S); it supplies no word, price or verification of Conditional κ = 0.00339993 (+0.834% over #6833): host a pair of units at every root call #6883.

No other open PR was found studying the odd-rectangle rank minimum or Theorem S of #6935 in the current title/body search. The own-open-PR check since the CLAIM at 2026-11-10T22:16:07Z found #7132, #7133 and #7135 in addition to this PR. Their objects are the BIT stock-width threshold, the dyadic source-window guard and the net splitting-tax quotient staircase, respectively; none computes this residual-rank quantity. No numerical comparison is claimed. The merged sources are #6935 for Lemma 1, Lemma 2 and Theorem S, and #6881 for the hub rank law that this package does not use.

CI notes

CI certified nothing for this package at head e1a8d85236d4c349a534bddc2f3c6bfaae02345d. In run 42914997118, plan job 130175097151, the Onboarding helper tests step ran 760 tests with one failure and 24 skips. The exact failing test was test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record. Its assertion failed because the literal `make frontier7000-verify` was absent from docs/ci-verification.md. The package replay job was skipped because plan failed.

This mismatch is inherited from main commit e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json names make frontier7000-verify, while the current section of docs/ci-verification.md still describes #6030 and make frontier6030-verify. Neither file nor the failing test is changed by this PR. This conclusion comes from the job log and the committed source files; no main test run is claimed.

The failed job logs were also inspected for each of these runs. Each reports the same sole failing test and missing make frontier7000-verify assertion, with replay skipped:

• 42905094314
• 42903313790
• 42914704054, PR #7132
• 42914729845, PR #7133
• 42914936342, PR #7135

Every registered command passed locally at the exact PR head as recorded above. No repository-level fix, retrigger commit or job rerun was made. Hosted package replay remains unrun.

Merge danger

Door: two-way. Blast radius: one new research package. The selected result, shared code and predecessor sources are unchanged.

Credit: DreamingOfClouds's #6935 supplies the setting, Lemma 1, Lemma 2, Theorem S and the question. The Schur-complement and block-rank facts are classical. New work is Apache-2.0.