diff --git a/research/schur-residual-orbits/README.md b/research/schur-residual-orbits/README.md new file mode 100644 index 0000000000..a2361477d9 --- /dev/null +++ b/research/schur-residual-orbits/README.md @@ -0,0 +1,239 @@ +# Seven residual Schur-pair states and their full-guard counts + +**Exact finite classification and counting, with a written multiplicity +argument. No new kappa.** Prepared by Mihir Srivastava with substantial +OpenAI Codex assistance, by one agent. Apache-2.0. + +This answers one bounded instance of the residual-state handoff in +[ssafwann's PR4678](https://github.com/CrocSwap/integer-mult-bounds/pull/4678), +continuing the orbit question in Nick Petalas's PR4597. For the binary +commuting projector pair with joint-sector dimensions **(1,1,1,2)**, exactly +**seven ordered simultaneous-conjugacy classes** occur after a common scalar +pivot. Their complete-header weights are not uniform. The census yields +**93,564 full-guard headers out of 9,999,360**, a fraction **2599/277760**. + +The sharp first-step event from PR4678 occupies just one residual class: +its **60,480** headers produce **5,040** distinct coordinate pairs, each +exactly **12** times. Only **3,240** of those headers pass the full guard +chain, a conditional fraction **3/56**. The 60,480 one-block count is credited +corroboration; its orbit classification and continuation count are the new +quantities here. Commutator rank alone cannot determine the continuation law. + +## Fixed sample space and guards + +Work over F2 and fix, before choosing the header, + +```text +P0 = diag(0,1,0,1,1), Q0 = diag(0,0,1,1,1). +``` + +The axes have joint sectors 00,10,01,11,11. Both projectors have rank three. +Choose a complete ordered header M uniformly from GL5(F2) and set +`P=M^-1 P0 M`, `Q=M^-1 Q0 M`. A full guard means that **both** leading +principal minors of each order 1,2,3 are nonzero. Orders 4 and 5 are not +required, since the requests have rank three. This is equivalent to three +successive nonzero scalar pivots without row exchanges. Using `G=M^-1` +gives the earlier `G P0 G^-1` convention and the same uniform sample space. + +Conditional on P[0,0]=Q[0,0]=1, write the Schur complements S,T, of size four. +They are rank-two idempotents. States are orbits of the **ordered** pair +`(S,T)` under `(S,T) -> (K^-1 S K, K^-1 T K)` for K in GL4(F2). +Swapping the requests or transposing them is not part of this equivalence. + +The same result holds for any fixed commuting binary idempotent pair with +these four sector dimensions: simultaneous diagonalization sends it to this +pair, and the fixed basis change permutes the complete-header sample space. +No claim is made for a different sector profile, field or restricted cover. + +## State table + +Every representative below has `S=(0,0,4,8)`. Matrices are encoded as integer +**rows**, with bit j representing column j, least significant bit first. +For example `(0,4,4,9)` has rows `0000`, `0010`, `0010`, `1001` when +columns are printed in increasing index order. The representatives minimize +the ordered tuple of all S rows followed by all T rows within each orbit. + +Here b counts admitted split pairs reaching the state, o is its orbit size, +z its stabilizer size, and f counts orbit elements whose two remaining +guards both pass. Thus `o*z=20160`, header weight is `b*20160`, and the +full-guard contribution is `b*z*f`. + +| State | T rows | rank [S,T] | b | o | z | f | Header weight | Full guards | +|---|---|---:|---:|---:|---:|---:|---:|---:| +| 1 | (0,0,4,8) | 0 | 1 | 560 | 36 | 100 | 20,160 | 3,600 | +| 2 | (0,0,4,9) | 1 | 3 | 5,040 | 4 | 468 | 60,480 | 5,616 | +| 3 | (0,2,0,8) | 0 | 126 | 20,160 | 1 | 366 | 2,540,160 | 46,116 | +| 4 | (0,2,2,8) | 1 | 18 | 20,160 | 1 | 816 | 362,880 | 14,688 | +| 5 | (0,4,4,8) | 1 | 3 | 5,040 | 4 | 468 | 60,480 | 5,616 | +| 6 | (0,4,4,9) | 2 | 3 | 5,040 | 4 | 270 | 60,480 | 3,240 | +| 7 | (0,6,0,8) | 1 | 18 | 20,160 | 1 | 816 | 362,880 | 14,688 | +| Total | | | 172 | | | | 3,467,520 | 93,564 | + +[RESULT.json](RESULT.json) includes every one of the 172 admitted split pairs, +their state assignments, and the exact guard-depth distributions within +each orbit. The total header denominator is `496*20160=9999360`. + +The sharp state 6 has split pairs `(15,23)`, `(23,15)`, `(31,31)` in the +fixed five-axis basis. Its fraction among all first-guard headers is 3/172, +as in PR4678; it is 3/496 among all headers. Its later full-guard fraction +is 270/5040=3/56, giving 3*4*270=3240 headers. + +Two tiny complete-header witnesses use the same integer-row convention in +dimension five. `M=(17,9,11,5,18)` has sharp first Schur commutator and +passes all three leading minors for both requests. `M=(23,3,5,9,16)` also +has sharp first Schur commutator, but fails the next common guard. +RESULT.json includes a passing and a first-guard-only header for every state. + +Two explicit losses of information are useful for future recursion design: + +- States 1 and 3 both have commutator rank zero, but their conditional + full-guard fractions are respectively **5/28** and **61/3360**. + States with commutator rank one also have unequal continuation fractions. +- States 2 and 5 have the same ranks of S, T, ST, TS, S+T and [S,T]. + They are still different orbits: `dim(ker S intersect ker T)` is one + for state 2 and two for state 5. Their continuation fractions happen to + agree. This witness refutes identification of those states by the listed + ranks; it does not claim that their guard counts differ. + +## Why the finite census counts complete headers exactly + +**Split pair and completion.** Let a be the first column of M and b the first +row of M^-1. Then ba=1. Conversely every pair with ba=1 extends to exactly +`|GL4(F2)|` headers: append an arbitrary ordered basis of ker b to a. +There are 31 choices of nonzero a and 16 choices of b with ba=1, hence 496 +split pairs. This is the credited equal-completion argument in PR4678 and +the preceding Petalas header work. No extra factor of 16 is applied after +the split pair has already been chosen. + +The verifier constructs one deterministic kernel basis for each split pair, +inverts the resulting header, and checks the two scalar pivots literally. +Exactly 172 split pairs pass. For any fixed one of them, all other completions +are uniquely `M diag(1,K)` with K in GL4. Block substitution gives + +```text +Schur(diag(1,K)^-1 P diag(1,K)) = K^-1 Schur(P) K. +``` + +Therefore a split pair contributes exactly one entire simultaneous orbit, +with each orbit element reached z times. Split pairs whose seed lies in +the same orbit have identical completion distributions. Summing their b +fibres gives the table's `b*z` multiplicity per orbit element. + +**Residual ranks.** In characteristic two, write +`P=[[1,R],[C,D]]`, so `S=D+CR`. Idempotency gives RC=0, RD=0, DC=0 and +D^2+CR=D. Hence S^2=S; block elimination gives `rank(P)=1+rank(S)`. +The same applies to Q. Thus both residual ranks are two, and exactly two +further scalar guards are required. The determinant identity +`det(P[:j+1,:j+1])=det(S[:j,:j])` at the first unit pivot proves equivalence +with the original orders 2 and 3. Repeating it justifies the guard-depth test. + +**Completeness of classification.** The independent-row generator visits +each ordered basis of F2^4 exactly once: at each level it extends by every +row outside the current span. Its size is `(16-1)(16-2)(16-4)(16-8)=20160`. +For each uncovered seed, the checker explicitly generates its entire orbit, +checks uniform fibre size and orbit-stabilizer equality, and verifies that +it is disjoint from all previously constructed orbits. Every admitted split +pair is assigned. This exhausts the stated finite domain, yielding seven +classes; it is not a random search or an extrapolated general classification. + +For an additional direct check, choose one split pair in each of the seven +classes and form **all 20,160 complete five-dimensional headers** in its +completion fibre. Invert and conjugate the original P0,Q0 and evaluate their +leading minors using the Leibniz determinant formula, without Schur +elimination. All **141,120** direct header cases reproduce the per-class +continuation counts. Applying those counts to the other split pairs uses +the proved orbit-equivariance argument. This is not a raw enumeration of +all 9,999,360 headers. + +## Reproduce and evidence boundaries + +Python 3.12 standard library; no pending executable or external input needed: + +```sh +python3.12 -B scripts/research_package.py --package research/schur-residual-orbits +python3.12 -B scripts/check_research_commit.py --package research/schur-residual-orbits --check-source-history +``` + +The registered normal and optimized (`-O`) modes use explicit exceptions and +compare every scientific field with RESULT.json. Direct Git-free replay is +`python3.12 -I -W error -O -B verify.py` from an exported package. The only +writing mode is explicit `verify.py --write`, which regenerates RESULT.json. + +Verification covers all 496 split pairs, full GL4 orbits for all seven +classes, and the 141,120 literal complete headers above. A separately +enumerated raw domain of all **65,536** four-by-four binary matrices uses +the Leibniz determinant to check that the generated GL4 set is exact. +Seven rejection controls distinguish a singular header, a nonsplit pair, +a zero pivot, omission of the completion multiplier, replacing the full +guard with the first guard, collapsing states by commutator rank, and +collapsing the distinct same-rank states 2 and 5. + +This is author-checked exact finite evidence plus the written reduction; +independent human or proof-kernel acceptance is not claimed. No Lean, Docker, +selected scientific cold replay, large-d classification or physical caller +replay is part of this package. Hosted CI is reported separately in the PR. + +The counted binary shared-header event is an algebraic model. As explained +in the credited projector-header notes, the retained normalizer's executable +domain uses odd q; this F2 census is not an admission check for that caller. +Header selection/emission, physical reads, dirty restoration, owned storage, +stock, dispatch and the full consumer bill remain unpriced. No cost is +implicitly zero and no selected-frontier change follows from these counts. + +## Scope, overlap and credit + +This starts from canonical main `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, +priority revision 7, selected conditional kappa 0.00302015. It takes the fresh +PR4678 handoff in [Discussion4653](https://github.com/CrocSwap/integer-mult-bounds/discussions/4653#discussioncomment-19126925). +The `formal-interface-lemma` card is marked **changed** to this algebraic +side result. The first working object is the handoff's explicit n=5 profile; +the stale balanced-transfer baseline is not used. The family decision is +**narrow** to one state distribution and its continuation law, with no +automatic construction or adjacent-profile census. + +TASK.json records overlap coverage and exact citation pins. At entry, 449 +open PR bodies and 3,608 Discussion records were refreshed. Before submission, +coverage was expanded to all 5,860 tracked in-scope local notes, 453 open PR +bodies (15:59 UTC) and 3,614 Discussion records (16:00 UTC), with no coverage +warnings. Main was refreshed unchanged. Remote closed PR bodies, arbitrary +code diffs, nested source notes and unpublished work remain coverage limits. +PR4678 counts one block for general profiles; this contribution classifies +the subsequent ordered states and counts the remaining guards for one +profile. The earlier full-guard census covers other named families, not +this seven-state distribution. No priority over unknown work is asserted. + +Predecessor credit is retained explicitly: + +- **ssafwann, PR4678**, head `af9cf805c501e4e9e947c98c0b97b2281b6b6e97`, + `research/schur-header-count/README.md`, blob + `5e644cf316312c0fdd489c8d33911583f1b88af2`: the exact one-block count, + this profile, completion-fibre argument and residual-state handoff; + substantial OpenAI Codex assistance. PR4671 supplies its sector criterion. +- **Nick Petalas, PR4597**, head `dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb`: + block-Schur commutator factorization and orbit question. His retained + PR4278 scalar Schur proof and earlier PR4259/4246/4228 header work supply + the commutator and equal-completion lineage. The local scalar note is + provenance-pinned in SOURCES.json; none of its code is imported. +- **Ryanson Jonathan**, the retained `full-guard-header-census`, with + substantial Claude Code (Claude Opus 5.5) assistance: literal leading-minor + guard convention and separate-family census. PR4609/4617 and **lee-phys's + PR4634** retain their binary sharpness and dimension contributions. +- **Cinna Davis**, PR4100's BIT request context, and the earlier normalizer + lineage credited there (source527, commdata2338 and Jose Manuel). + +The source-bound tooling retains its existing contributors' attribution. +The pending PRs are citations, not runtime or provenance dependencies that +would require unpublished Git ancestry. All new files are Apache-2.0. + +## Open next questions + +Can an invariant-based transition rule recover these seven states and their +continuation counts without enumerating GL4? That would turn this exact +finite table into a useful test fixture for a scalable state-aware header +recursion. Start by deriving the stabilizers of the seven displayed pairs +and the next-pivot transitions using their image/kernel decompositions. +The blocker is a proved sufficient state invariant and its transition +multiplicities; commutator rank and the listed product/sum ranks are +insufficient for orbit identity. Larger fields/profiles and an actual +production header cover require a separate scope and cost allowance. +No follow-up claim is held by this package. diff --git a/research/schur-residual-orbits/RESULT.json b/research/schur-residual-orbits/RESULT.json new file mode 100644 index 0000000000..20146a875c --- /dev/null +++ b/research/schur-residual-orbits/RESULT.json @@ -0,0 +1,1055 @@ +{ + "field": 2, + "sector_dimensions": [ + 1, + 1, + 1, + 2 + ], + "matrix_encoding": "integer rows, bit j is column j; ordered pair", + "input_projectors": [ + [ + 0, + 2, + 0, + 8, + 16 + ], + [ + 0, + 0, + 4, + 8, + 16 + ] + ], + "total_splits": 496, + "admitted_splits": 172, + "group_order": 20160, + "all_headers": 9999360, + "first_guard_headers": 3467520, + "full_guard_headers": 93564, + "full_guard_fraction": "2599/277760", + "direct_complete_header_checks": 141120, + "raw_matrix_determinant_checks": 65536, + "controls": 7, + "states": [ + { + "representative": [ + [ + 0, + 0, + 4, + 8 + ], + [ + 0, + 0, + 4, + 8 + ] + ], + "commutator_rank": 0, + "product_rank": 2, + "reverse_product_rank": 2, + "sum_rank": 0, + "common_kernel_dimension": 2, + "orbit_size": 560, + "stabilizer": 36, + "depth_counts_in_orbit": { + "0": 280, + "1": 180, + "2": 100 + }, + "split_pairs": [ + [ + 7, + 7 + ] + ], + "headers": 20160, + "headers_per_orbit_element": 36, + "full_guard_headers": 3600, + "first_guard_only_witness_header": [ + 7, + 3, + 5, + 8, + 16 + ], + "full_guard_witness_header": [ + 25, + 9, + 17, + 2, + 4 + ] + }, + { + "representative": [ + [ + 0, + 0, + 4, + 8 + ], + [ + 0, + 0, + 4, + 9 + ] + ], + "commutator_rank": 1, + "product_rank": 2, + "reverse_product_rank": 2, + "sum_rank": 1, + "common_kernel_dimension": 1, + "orbit_size": 5040, + "stabilizer": 4, + "depth_counts_in_orbit": { + "0": 3192, + "1": 1380, + "2": 468 + }, + "split_pairs": [ + [ + 15, + 7 + ], + [ + 23, + 7 + ], + [ + 31, + 7 + ] + ], + "headers": 60480, + "headers_per_orbit_element": 12, + "full_guard_headers": 5616, + "first_guard_only_witness_header": [ + 7, + 3, + 5, + 9, + 16 + ], + "full_guard_witness_header": [ + 25, + 9, + 17, + 3, + 4 + ] + }, + { + "representative": [ + [ + 0, + 0, + 4, + 8 + ], + [ + 0, + 2, + 0, + 8 + ] + ], + "commutator_rank": 0, + "product_rank": 1, + "reverse_product_rank": 1, + "sum_rank": 2, + "common_kernel_dimension": 1, + "orbit_size": 20160, + "stabilizer": 1, + "depth_counts_in_orbit": { + "0": 15120, + "1": 4674, + "2": 366 + }, + "split_pairs": [ + [ + 8, + 8 + ], + [ + 8, + 9 + ], + [ + 8, + 10 + ], + [ + 8, + 11 + ], + [ + 8, + 12 + ], + [ + 8, + 13 + ], + [ + 8, + 14 + ], + [ + 8, + 15 + ], + [ + 8, + 24 + ], + [ + 8, + 25 + ], + [ + 8, + 26 + ], + [ + 8, + 27 + ], + [ + 8, + 28 + ], + [ + 8, + 29 + ], + [ + 8, + 30 + ], + [ + 8, + 31 + ], + [ + 9, + 8 + ], + [ + 9, + 10 + ], + [ + 9, + 12 + ], + [ + 9, + 14 + ], + [ + 9, + 24 + ], + [ + 9, + 26 + ], + [ + 9, + 28 + ], + [ + 9, + 30 + ], + [ + 10, + 8 + ], + [ + 10, + 9 + ], + [ + 10, + 24 + ], + [ + 10, + 25 + ], + [ + 11, + 8 + ], + [ + 11, + 24 + ], + [ + 12, + 8 + ], + [ + 12, + 9 + ], + [ + 12, + 24 + ], + [ + 12, + 25 + ], + [ + 13, + 8 + ], + [ + 13, + 24 + ], + [ + 14, + 8 + ], + [ + 14, + 9 + ], + [ + 14, + 24 + ], + [ + 14, + 25 + ], + [ + 15, + 8 + ], + [ + 15, + 24 + ], + [ + 16, + 16 + ], + [ + 16, + 17 + ], + [ + 16, + 18 + ], + [ + 16, + 19 + ], + [ + 16, + 20 + ], + [ + 16, + 21 + ], + [ + 16, + 22 + ], + [ + 16, + 23 + ], + [ + 16, + 24 + ], + [ + 16, + 25 + ], + [ + 16, + 26 + ], + [ + 16, + 27 + ], + [ + 16, + 28 + ], + [ + 16, + 29 + ], + [ + 16, + 30 + ], + [ + 16, + 31 + ], + [ + 17, + 16 + ], + [ + 17, + 18 + ], + [ + 17, + 20 + ], + [ + 17, + 22 + ], + [ + 17, + 24 + ], + [ + 17, + 26 + ], + [ + 17, + 28 + ], + [ + 17, + 30 + ], + [ + 18, + 16 + ], + [ + 18, + 17 + ], + [ + 18, + 24 + ], + [ + 18, + 25 + ], + [ + 19, + 16 + ], + [ + 19, + 24 + ], + [ + 20, + 16 + ], + [ + 20, + 17 + ], + [ + 20, + 24 + ], + [ + 20, + 25 + ], + [ + 21, + 16 + ], + [ + 21, + 24 + ], + [ + 22, + 16 + ], + [ + 22, + 17 + ], + [ + 22, + 24 + ], + [ + 22, + 25 + ], + [ + 23, + 16 + ], + [ + 23, + 24 + ], + [ + 24, + 8 + ], + [ + 24, + 9 + ], + [ + 24, + 10 + ], + [ + 24, + 11 + ], + [ + 24, + 12 + ], + [ + 24, + 13 + ], + [ + 24, + 14 + ], + [ + 24, + 15 + ], + [ + 24, + 16 + ], + [ + 24, + 17 + ], + [ + 24, + 18 + ], + [ + 24, + 19 + ], + [ + 24, + 20 + ], + [ + 24, + 21 + ], + [ + 24, + 22 + ], + [ + 24, + 23 + ], + [ + 25, + 8 + ], + [ + 25, + 10 + ], + [ + 25, + 12 + ], + [ + 25, + 14 + ], + [ + 25, + 16 + ], + [ + 25, + 18 + ], + [ + 25, + 20 + ], + [ + 25, + 22 + ], + [ + 26, + 8 + ], + [ + 26, + 9 + ], + [ + 26, + 16 + ], + [ + 26, + 17 + ], + [ + 27, + 8 + ], + [ + 27, + 16 + ], + [ + 28, + 8 + ], + [ + 28, + 9 + ], + [ + 28, + 16 + ], + [ + 28, + 17 + ], + [ + 29, + 8 + ], + [ + 29, + 16 + ], + [ + 30, + 8 + ], + [ + 30, + 9 + ], + [ + 30, + 16 + ], + [ + 30, + 17 + ], + [ + 31, + 8 + ], + [ + 31, + 16 + ] + ], + "headers": 2540160, + "headers_per_orbit_element": 126, + "full_guard_headers": 46116, + "first_guard_only_witness_header": [ + 2, + 4, + 8, + 1, + 16 + ], + "full_guard_witness_header": [ + 8, + 18, + 20, + 1, + 22 + ] + }, + { + "representative": [ + [ + 0, + 0, + 4, + 8 + ], + [ + 0, + 2, + 2, + 8 + ] + ], + "commutator_rank": 1, + "product_rank": 2, + "reverse_product_rank": 1, + "sum_rank": 2, + "common_kernel_dimension": 1, + "orbit_size": 20160, + "stabilizer": 1, + "depth_counts_in_orbit": { + "0": 14448, + "1": 4896, + "2": 816 + }, + "split_pairs": [ + [ + 10, + 12 + ], + [ + 10, + 13 + ], + [ + 10, + 28 + ], + [ + 10, + 29 + ], + [ + 11, + 12 + ], + [ + 11, + 28 + ], + [ + 18, + 20 + ], + [ + 18, + 21 + ], + [ + 18, + 28 + ], + [ + 18, + 29 + ], + [ + 19, + 20 + ], + [ + 19, + 28 + ], + [ + 26, + 12 + ], + [ + 26, + 13 + ], + [ + 26, + 20 + ], + [ + 26, + 21 + ], + [ + 27, + 12 + ], + [ + 27, + 20 + ] + ], + "headers": 362880, + "headers_per_orbit_element": 18, + "full_guard_headers": 14688, + "first_guard_only_witness_header": [ + 2, + 5, + 8, + 9, + 16 + ], + "full_guard_witness_header": [ + 8, + 17, + 18, + 19, + 4 + ] + }, + { + "representative": [ + [ + 0, + 0, + 4, + 8 + ], + [ + 0, + 4, + 4, + 8 + ] + ], + "commutator_rank": 1, + "product_rank": 2, + "reverse_product_rank": 2, + "sum_rank": 1, + "common_kernel_dimension": 2, + "orbit_size": 5040, + "stabilizer": 4, + "depth_counts_in_orbit": { + "0": 3192, + "1": 1380, + "2": 468 + }, + "split_pairs": [ + [ + 7, + 15 + ], + [ + 7, + 23 + ], + [ + 7, + 31 + ] + ], + "headers": 60480, + "headers_per_orbit_element": 12, + "full_guard_headers": 5616, + "first_guard_only_witness_header": [ + 15, + 3, + 5, + 8, + 16 + ], + "full_guard_witness_header": [ + 17, + 9, + 11, + 18, + 4 + ] + }, + { + "representative": [ + [ + 0, + 0, + 4, + 8 + ], + [ + 0, + 4, + 4, + 9 + ] + ], + "commutator_rank": 2, + "product_rank": 2, + "reverse_product_rank": 2, + "sum_rank": 2, + "common_kernel_dimension": 1, + "orbit_size": 5040, + "stabilizer": 4, + "depth_counts_in_orbit": { + "0": 3528, + "1": 1242, + "2": 270 + }, + "split_pairs": [ + [ + 15, + 23 + ], + [ + 23, + 15 + ], + [ + 31, + 31 + ] + ], + "headers": 60480, + "headers_per_orbit_element": 12, + "full_guard_headers": 3240, + "first_guard_only_witness_header": [ + 23, + 3, + 5, + 9, + 16 + ], + "full_guard_witness_header": [ + 17, + 9, + 11, + 5, + 18 + ] + }, + { + "representative": [ + [ + 0, + 0, + 4, + 8 + ], + [ + 0, + 6, + 0, + 8 + ] + ], + "commutator_rank": 1, + "product_rank": 1, + "reverse_product_rank": 2, + "sum_rank": 2, + "common_kernel_dimension": 1, + "orbit_size": 20160, + "stabilizer": 1, + "depth_counts_in_orbit": { + "0": 14448, + "1": 4896, + "2": 816 + }, + "split_pairs": [ + [ + 12, + 10 + ], + [ + 12, + 11 + ], + [ + 12, + 26 + ], + [ + 12, + 27 + ], + [ + 13, + 10 + ], + [ + 13, + 26 + ], + [ + 20, + 18 + ], + [ + 20, + 19 + ], + [ + 20, + 26 + ], + [ + 20, + 27 + ], + [ + 21, + 18 + ], + [ + 21, + 26 + ], + [ + 28, + 10 + ], + [ + 28, + 11 + ], + [ + 28, + 18 + ], + [ + 28, + 19 + ], + [ + 29, + 10 + ], + [ + 29, + 18 + ] + ], + "headers": 362880, + "headers_per_orbit_element": 18, + "full_guard_headers": 14688, + "first_guard_only_witness_header": [ + 2, + 8, + 5, + 9, + 16 + ], + "full_guard_witness_header": [ + 8, + 18, + 17, + 19, + 4 + ] + } + ] +} diff --git a/research/schur-residual-orbits/SOURCES.json b/research/schur-residual-orbits/SOURCES.json new file mode 100644 index 0000000000..69800aa74b --- /dev/null +++ b/research/schur-residual-orbits/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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/schur-commutator-criterion/README.md", + "usage": "provenance", + "git_blob": "6b37342de04f5c42c198dd6ba14cea9845be6f05", + "sha256": "5616da2e708a8425f1bf0bf5c89c236ef8ed0a23d0544d30ae2142ffe167dc01" + }, + { + "path": "research/full-guard-header-census/README.md", + "usage": "provenance", + "git_blob": "01af434ccd5c941f07042ecdc7f3eb02c5125ef3", + "sha256": "577f636fc21c2f51919030f8d97da9c32863d30b91fb5e85f3d5183a3b5ec479" + }, + { + "path": "research/projector-joint-header-density/README.md", + "usage": "provenance", + "git_blob": "b689558801208f62c33fddbc86fc9978240531b2", + "sha256": "ee4993264d668dcb38995aa1e84cbd135ac0776286befe9111b192eef9fd6b43" + } + ] +} diff --git a/research/schur-residual-orbits/TASK.json b/research/schur-residual-orbits/TASK.json new file mode 100644 index 0000000000..e5881bdedf --- /dev/null +++ b/research/schur-residual-orbits/TASK.json @@ -0,0 +1,176 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact residual simultaneous-conjugacy states, complete-header multiplicities and full-guard continuations for one binary sector profile (1,1,1,2), n=5, d=1.", + "scope_change_reason": "Take the fresh, unclaimed PR4678 residual-state handoff rather than the historical formalization card's starting point. This is an algebraic side result and exhaustive finite classification, not a Lean theorem or admission claim.", + "bottleneck_link": "A state-aware shared-header recursion cannot reapply the commuting-pair one-block formula after Schur deletion. The seven-state table and same-commutator-rank counterexample expose exactly the information lost in this small example. No paid supplier budget or kappa gain is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at one n=5 sector profile, an exhaustive orbit census, its complete-header continuation counts and discriminating controls. No automatic general-field or larger-profile scan, physical producer implementation, or selected-frontier change.", + "outcome": "completed", + "evidence": "Written completion-fibre and orbit-stabilizer argument; all 496 split pairs; seven full GL4 orbits; 141120 literal complete-header leading-minor checks; raw determinant census of all 65536 binary 4x4 matrices; seven rejection controls; exact RESULT.json replay. Registered normal and optimized modes are required.", + "author": "Mihir Srivastava", + "ai_assistance": "Substantial OpenAI Codex assistance for research, implementation, writing and verification, by one agent. No subagents used.", + "open_questions": [ + { + "question": "Can an invariant-based transition rule recover the seven-state table and its continuation counts without enumerating GL4?", + "why_it_matters": "It would provide a scalable state-aware recursion instead of incorrectly reusing a commuting-pair one-block law.", + "first_step": "Derive each displayed pair's stabilizer and scalar-pivot transitions from its image/kernel decompositions; reproduce the committed seven-row table.", + "blocked_by": "A proved sufficient state invariant and exact transition multiplicities; commutator rank and the listed simple ranks are insufficient for orbit identity. Physical application also needs an actual header cover and complete cost allowance." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4653#discussioncomment-19126925", + "family_decision": "Narrow to the named residual-state handoff. Mathematical header counts are paid only as counts; production selection, emission, physical reads, restoration, owned storage, stock, dispatch and complete consumer costs remain unknown, not zero.", + "selected_context": { + "kappa": "60403/20000000", + "decimal": "0.00302015", + "reproduce": "make frontier4470-verify", + "scientific_cold_replay_run": false + }, + "environment": { + "python": "3.12.0", + "platform": "Windows-11-10.0.26300-SP0", + "dependencies": "standard library only" + }, + "citations": [ + { + "pr": 4678, + "author": "ssafwann", + "head": "af9cf805c501e4e9e947c98c0b97b2281b6b6e97", + "path": "research/schur-header-count/README.md", + "git_blob": "5e644cf316312c0fdd489c8d33911583f1b88af2", + "role": "One-block law, profile, equal-completion argument and explicit residual-state handoff; cited, no imported executable." + }, + { + "pr": 4597, + "author": "Nick Petalas", + "head": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb", + "role": "Block Schur commutator factorization and simultaneous-orbit question; PR4278/4259/4246/4228 predecessor lineage retained." + }, + { + "author": "Ryanson Jonathan", + "path": "research/full-guard-header-census/README.md", + "head": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "role": "Literal full-guard convention and separate-family census; substantial Claude Code assistance retained." + } + ], + "unrun_obligations": [ + "independent human or proof-kernel review", + "general fields or sector profiles", + "restricted production header cover", + "physical supplier costs and admission", + "selected scientific cold replay", + "Lean", + "Docker" + ], + "overlap": { + "searched_at": "2026-10-22T16:00:30.491362+00:00", + "terms": [ + "residual pair", + "residual-state", + "Schur", + "93564" + ], + "coverage": { + "local": { + "head": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "records": 5862, + "head_records": 5860, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-22T15:59:10.538714+00:00", + "complete_pagination": true, + "records": 453 + }, + "discussions": { + "fetched_at": "2026-10-22T16:00:30.011525+00:00", + "complete_pagination": true, + "records": 3614 + } + }, + "warnings": [], + "nearest_work": "PR4678 has the same one-block scalar count, deliberately corroborated. PR4597 asks about residual orbits but does not classify this n=5 profile. The retained full-guard-header-census treats other families. No duplicate seven-state census located in the refreshed corpora; the matching live Discussion claim is this work.", + "limits": "All tracked top-level README/TASK notes and the local ledger are covered. No arbitrary code-diff, nested source-note, remote closed-PR-body or unpublished coverage. No exhaustive novelty claim." + }, + "upstream_checkpoint": { + "canonical_remote": "https://github.com/CrocSwap/integer-mult-bounds.git", + "fetched_main": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "confirmed_at": "2026-10-22T16:01:40.721377+00:00", + "decision": "Canonical main and priority revision 7 are unchanged from the base; continue the scoped algebraic handoff. Selected record remains 60403/20000000." + } +} diff --git a/research/schur-residual-orbits/VERIFY.json b/research/schur-residual-orbits/VERIFY.json new file mode 100644 index 0000000000..a61815a5cf --- /dev/null +++ b/research/schur-residual-orbits/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact seven-state census, literal full-header determinants, independent raw GL4 census, seven rejecting controls and committed result equality" + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact seven-state census, literal full-header determinants, independent raw GL4 census, seven rejecting controls and committed result equality under -O" + } + ] +} diff --git a/research/schur-residual-orbits/verify.py b/research/schur-residual-orbits/verify.py new file mode 100644 index 0000000000..0ec8eed83c --- /dev/null +++ b/research/schur-residual-orbits/verify.py @@ -0,0 +1,299 @@ +#!/usr/bin/env python3 +"""Exact residual-pair census over F2; no predecessor executable imported. + +Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0. +Matrices are tuples of integer rows; bit j is column j (least significant first). +""" +import argparse +from collections import Counter +from fractions import Fraction +from itertools import permutations, product +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return tuple(1 << i for i in range(n)) + + +def rank(rows): + pivots = {} + for row in rows: + while row: + bit = row.bit_length() - 1 + if bit not in pivots: + pivots[bit] = row + break + row ^= pivots[bit] + return len(pivots) + + +def multiply(a, b): + out = [] + for row in a: + value = 0 + while row: + bit = row & -row + value ^= b[bit.bit_length() - 1] + row ^= bit + out.append(value) + return tuple(out) + + +def inverse(a): + n = len(a) + work = [row | (1 << (n + i)) for i, row in enumerate(a)] + for col in range(n): + pivot = next((i for i in range(col, n) if work[i] & (1 << col)), None) + need(pivot is not None, "singular matrix") + work[col], work[pivot] = work[pivot], work[col] + for i in range(n): + if i != col and work[i] & (1 << col): + work[i] ^= work[col] + return tuple(row >> n for row in work) + + +def from_columns(columns): + return tuple(sum(((v >> i) & 1) << j for j, v in enumerate(columns)) + for i in range(len(columns))) + + +def conjugate(a, k, ki): + return multiply(multiply(ki, a), k) + + +def schur(a): + need(a[0] & 1, "zero pivot") + return tuple((row >> 1) ^ ((a[0] >> 1) if row & 1 else 0) + for row in a[1:]) + + +def commutator(a, b): + return tuple(x ^ y for x, y in zip(multiply(a, b), multiply(b, a))) + + +def gl(n): + """All ordered independent row tuples, each exactly once.""" + def extend(rows, span): + if len(rows) == n: + yield rows + return + for row in range(1, 1 << n): + if row not in span: + yield from extend(rows + (row,), span | {x ^ row for x in span}) + return list(extend((), {0})) + + +def completion(a, b, n): + """Header with first column a and inverse first row b, given b*a=1.""" + need((a & b).bit_count() % 2 == 1, "not a split pair") + basis, span = [], {0} + for v in range(1, 1 << n): + if (v & b).bit_count() % 2 == 0 and v not in span: + basis.append(v) + span |= {x ^ v for x in span} + need(len(basis) == n - 1, "kernel dimension") + m = from_columns([a] + basis) + need(inverse(m)[0] == b, "completion projection") + return m + + +def split_pairs(p, q): + n = len(p) + accepted, total = [], 0 + for a, b in product(range(1, 1 << n), repeat=2): + if (a & b).bit_count() % 2 == 0: + continue + total += 1 + m = completion(a, b, n) + mi = inverse(m) + pm, qm = conjugate(p, m, mi), conjugate(q, m, mi) + if pm[0] & qm[0] & 1: + accepted.append((a, b, schur(pm), schur(qm))) + return total, accepted + + +def guard_depth(pair): + """Number of simultaneous successful scalar pivots (at most rank two).""" + p, q = pair + depth = 0 + while p and p[0] & q[0] & 1: + p, q = schur(p), schur(q) + depth += 1 + return depth + + +def classify(seeds, group): + inverses = [inverse(k) for k in group] + for k, ki in zip(group, inverses): + need(multiply(k, ki) == multiply(ki, k) == identity(4), "group inverse") + orbit_lookup, states = {}, [] + for a, b, s, t in seeds: + pair = (s, t) + if pair in orbit_lookup: + state = states[orbit_lookup[pair]] + else: + images = Counter((conjugate(s, k, ki), conjugate(t, k, ki)) + for k, ki in zip(group, inverses)) + representative = min(images) + stabilizer = images[pair] + need(set(images.values()) == {stabilizer}, "uniform orbit fibres") + need(len(images) * stabilizer == len(group), "orbit-stabilizer") + need(not (images.keys() & orbit_lookup.keys()), "disjoint orbits") + depths = Counter(guard_depth(image) for image in images) + need(set(depths) <= {0, 1, 2}, "rank-two guard depth") + state = { + "representative": representative, + "commutator_rank": rank(commutator(s, t)), + "product_rank": rank(multiply(s, t)), + "reverse_product_rank": rank(multiply(t, s)), + "sum_rank": rank(tuple(x ^ y for x, y in zip(s, t))), + "common_kernel_dimension": 4 - rank(s + t), + "orbit_size": len(images), + "stabilizer": stabilizer, + "depth_counts_in_orbit": dict(sorted(depths.items())), + "split_pairs": [], + } + index = len(states) + for image in images: + orbit_lookup[image] = index + states.append(state) + state["split_pairs"].append([a, b]) + states.sort(key=lambda s: s["representative"]) + for state in states: + count = len(state["split_pairs"]) + state["headers"] = count * len(group) + state["headers_per_orbit_element"] = count * state["stabilizer"] + state["full_guard_headers"] = (state["headers_per_orbit_element"] + * state["depth_counts_in_orbit"].get(2, 0)) + return states + + +def leading_det(a, size): + """Leibniz determinant over F2, independent of elimination/Schur code.""" + parity = 0 + for order in permutations(range(size)): + parity ^= all((a[i] >> j) & 1 for i, j in enumerate(order)) + return int(parity) + + +def direct_header_check(states, group, p, q): + checked = 0 + for state in states: + a, b = state["split_pairs"][0] + m0 = completion(a, b, 5) + depths = Counter() + for k in group: + block = (1,) + tuple(row << 1 for row in k) + m = multiply(m0, block) + mi = inverse(m) + pm, qm = conjugate(p, m, mi), conjugate(q, m, mi) + need(leading_det(pm, 1) == leading_det(qm, 1) == 1, "first guard") + depth = 0 + for size in (2, 3): + if leading_det(pm, size) != 1 or leading_det(qm, size) != 1: + break + depth += 1 + if depth == 2 and "full_guard_witness_header" not in state: + state["full_guard_witness_header"] = m + if depth == 0 and "first_guard_only_witness_header" not in state: + state["first_guard_only_witness_header"] = m + depths[depth] += 1 + checked += 1 + predicted = {d: n * state["stabilizer"] + for d, n in state["depth_counts_in_orbit"].items()} + need(dict(depths) == predicted, "literal complete-header guard counts") + return checked + + +def rejection_controls(states): + def rejected(fn, message): + try: + fn() + except ValueError: + return + raise ValueError("accepted control: " + message) + + rejected(lambda: inverse((1, 1)), "singular header") + rejected(lambda: completion(1, 2, 2), "unsplit inclusion/projection") + rejected(lambda: schur((0, 2)), "zero pivot") + sharp = next(s for s in states if s["commutator_rank"] == 2) + rejected(lambda: need(sharp["headers"] == len(sharp["split_pairs"]), + "omitted completion multiplier"), "counting splits as headers") + rejected(lambda: need(sharp["full_guard_headers"] == sharp["headers"], + "one guard does not imply full guards"), "one-block shortcut") + # Equal commutator ranks do not determine the conditional continuation law. + commuting = [s for s in states if s["commutator_rank"] == 0] + rates = {Fraction(s["full_guard_headers"], s["headers"]) for s in commuting} + rejected(lambda: need(len(rates) == 1, "different continuation rates"), + "commutator-rank-only state") + # Not even all the displayed simple rank invariants distinguish these two. + x, y = states[1], states[4] + keys = ("commutator_rank", "product_rank", "reverse_product_rank", "sum_rank") + need(all(x[k] == y[k] for k in keys), "equal-rank control premise") + rejected(lambda: need(x["common_kernel_dimension"] == y["common_kernel_dimension"], + "different common kernels"), "same simple ranks imply same orbit") + # Cross-check rank and direct determinant by independent 4x4 raw enumeration. + raw_gl = {a for a in product(range(16), repeat=4) if leading_det(a, 4)} + need(raw_gl == set(gl(4)), "raw determinant census equals independent-row GL4") + return 7 + + +def run(): + # Sectors (00,10,01,11,11), fixed before the header is selected. + p, q = (0, 2, 0, 8, 16), (0, 0, 4, 8, 16) + need(multiply(p, p) == p and multiply(q, q) == q, "projectors") + need(multiply(p, q) == multiply(q, p), "commuting input") + total, seeds = split_pairs(p, q) + need(total == 496 and len(seeds) == 172, "split census") + group = gl(4) + need(len(group) == len(set(group)) == 20160, "complete GL4") + for _, _, s, t in seeds: + need(multiply(s, s) == s and multiply(t, t) == t, "residual projectors") + need(rank(s) == rank(t) == 2, "residual ranks") + states = classify(seeds, group) + need(len(states) == 7, "seven residual orbits") + direct_cases = direct_header_check(states, group, p, q) + controls = rejection_controls(states) + header_total = sum(s["headers"] for s in states) + full_total = sum(s["full_guard_headers"] for s in states) + sharp = [s for s in states if s["commutator_rank"] == 2] + need(header_total == 3467520 and full_total == 93564, "complete-header totals") + need(len(sharp) == 1 and sharp[0]["headers"] == 60480, "sharp predecessor count") + need(sharp[0]["full_guard_headers"] == 3240, "sharp full-guard count") + return {"field": 2, "sector_dimensions": [1, 1, 1, 2], + "matrix_encoding": "integer rows, bit j is column j; ordered pair", + "input_projectors": [p, q], "total_splits": total, + "admitted_splits": len(seeds), "group_order": len(group), + "all_headers": total * len(group), "first_guard_headers": header_total, + "full_guard_headers": full_total, + "full_guard_fraction": str(Fraction(full_total, total * len(group))), + "direct_complete_header_checks": direct_cases, + "raw_matrix_determinant_checks": 65536, "controls": controls, + "states": states} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate RESULT.json") + args = parser.parse_args() + result = run() + payload = json.dumps(result, indent=2) + "\n" + path = Path(__file__).with_name("RESULT.json") + if args.write: + path.write_text(payload, encoding="utf-8", newline="\n") + else: + need(json.loads(path.read_text(encoding="utf-8")) == json.loads(payload), + "committed result differs from the exact census") + print("PASS_SCHUR_RESIDUAL_ORBITS") + print(json.dumps({key: value for key, value in result.items() if key != "states"}, + sort_keys=True)) + + +if __name__ == "__main__": + main()