From 6896b92a34b6db839a7ba0ddfa0159f56af5c148 Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Fri, 23 Oct 2026 00:57:36 -0700 Subject: [PATCH] Derive Schur first-pivot state weights from sector incidence --- research/schur-split-incidence/PROOF.md | 69 +++++ research/schur-split-incidence/README.md | 44 ++++ research/schur-split-incidence/RESULT.json | 34 +++ research/schur-split-incidence/RETAINED.json | 20 ++ research/schur-split-incidence/SOURCES.json | 36 +++ research/schur-split-incidence/TASK.json | 114 +++++++++ research/schur-split-incidence/VERIFY.json | 30 +++ .../retained/calibration.json | 29 +++ .../retained/continuation-README.md | 87 +++++++ research/schur-split-incidence/verify.py | 235 ++++++++++++++++++ 10 files changed, 698 insertions(+) create mode 100644 research/schur-split-incidence/PROOF.md create mode 100644 research/schur-split-incidence/README.md create mode 100644 research/schur-split-incidence/RESULT.json create mode 100644 research/schur-split-incidence/RETAINED.json create mode 100644 research/schur-split-incidence/SOURCES.json create mode 100644 research/schur-split-incidence/TASK.json create mode 100644 research/schur-split-incidence/VERIFY.json create mode 100644 research/schur-split-incidence/retained/calibration.json create mode 100644 research/schur-split-incidence/retained/continuation-README.md create mode 100644 research/schur-split-incidence/verify.py diff --git a/research/schur-split-incidence/PROOF.md b/research/schur-split-incidence/PROOF.md new file mode 100644 index 0000000000..1d75f36dd3 --- /dev/null +++ b/research/schur-split-incidence/PROOF.md @@ -0,0 +1,69 @@ +# Scalar sector incidence and the seven first-pivot weights + +Work over F2. Fix commuting idempotents P,Q on V with ordered joint sectors V00,V10,V01,V11 of dimensions r00,r10,r01,r11. A scalar split is a vector a and covector b with ba=1; the common first guard is bPa=bQa=1. Scalars, vectors and covectors are labeled; no quotient or division by any sector centralizer is taken in the count. + +## General scalar incidence formula + +Write a=(a_j), b=(b_j), and h=b11 a11. The three guard equations are equivalent to b00 a00=b10 a10=b01 a01=1+h, b11 a11=h. For a sector of dimension r, the simultaneous GL(r,2) action (a,b) -> (ga,bg^-1) has exactly these nonempty types: + +| Type | Incidence | Weight w_r | +|---|---|---:| +| Z | a=0,b=0 | 1 | +| A | a nonzero,b=0 | 2^r-1 | +| B | a=0,b nonzero | 2^r-1 | +| N | a,b nonzero, ba=0 | (2^r-1)(2^(r-1)-1) | +| C | ba=1 | (2^r-1)2^(r-1) | + +For r=0 only Z exists; for r=1 N does not exist. For positive r, count a first, then the covectors in its annihilator or affine complement to obtain these weights. Transitivity follows by extending a nonzero a to a basis, and, when b is nonzero, choosing the remaining basis in ker b (type C) or one vector outside ker b (type N). Types A and B are the single nonzero-vector and nonzero-covector orbits. Thus these are actual incidence orbits, not just ranks with a guessed multiplicity. + +Let T_0(r)={Z,A,B,N} with zero weights omitted and T_1(r)={C}, also omitting zero weights. For every compatible tuple tau in T_(1+h)(r00) x T_(1+h)(r10) x T_(1+h)(r01) x T_h(r11), choose one canonical sector realization, assemble a,b, and form the ordered residual pair R(tau) on ker b. Then, for any simultaneous-conjugacy class O of residual pairs, + + B(O) = sum over h=0,1 and compatible tau with R(tau) in O of product_j w_(r_j)(tau_j). + +This is an all-dimension binary scalar-pivot formula. It does not claim an efficient general residual-classification algorithm or an arbitrary-field theorem. The proof is a disjoint partition into sector orbits: each tuple has the displayed product size, and the product sector group commutes with P,Q and sends the residual pair by simultaneous conjugacy. The guard equations themselves imply ba=1, so there is no extra compatibility factor or completion gauge. Different tuples may reach the same residual class; their weights must be added, not quotiented. + +For x in H=ker b the coordinate-free residual maps are + + Sx = Px + Pa (bPx), Tx = Qx + Qa (bQx). + +Both images lie in H. These are the usual Schur complements in any basis (a,N) with N a basis of H. They have image im P intersect H and kernel H intersect (ker P + ), and the analogous statements hold for Q. The image statement follows since bPa=1 and the displayed formula is the projection within im P onto its intersection with H. The kernel follows from Px in and injectivity of P on . This gives the promised image/kernel interpretation of the incidence types. + +## Profile (1,1,1,2): start with weights 1 and 3 + +Use axes e0,e1,e2,e3,e4 with P=diag(0,1,0,1,1), Q=diag(0,0,1,1,1). For h=0, each one-dimensional sector is forced to C: a_i=b_i=1 for i=0,1,2. Write a=(1,1,1,u), b=(1,1,1,v), vu=0 on the two-dimensional 11 sector. Its four incidence types have weights 1,3,3,3. + +The residual images are {(0,vz,0,z)} and {(0,0,vz,z)}. They coincide exactly when v=0; otherwise their intersection has dimension one. The kernels are spanned respectively by (1,1,0,u),(0,1,1,u) and by (1,0,1,u),(0,1,1,u). They coincide exactly when u=0; otherwise their intersection has dimension one. Consequently Z gives S=T (state 1) with weight 1. A gives equal images and distinct kernels (state 2) with weight 3. B gives distinct images and equal kernels (state 5) with weight 3. N gives both intersections of dimension one (state 6) with weight 3. Sector transitivity proves each is a single residual class. Their intersection dimensions distinguish them, and direct substitution of one canonical seed per type identifies the displayed representatives in the calibration table. For N, the commutator has rank two; hence it cannot merge with any h=1 case below. + +For an explicit coordinate check, the deterministic increasing-vector basis of H used by verify.py gives the following seeds and invertible intertwiners K (all matrices encoded by integer rows). Each row satisfies S_seed K=K S_rep and T_seed K=K T_rep; invertibility is independently checked. These four witnesses make the state identification concrete without an orbit search. + +| Type | a,b | S_seed | T_seed | K | +|---|---|---|---|---| +| Z | 7,7 | (0,0,4,8) | (0,0,4,8) | (2,1,8,4) | +| A | 15,7 | (0,0,5,8) | (0,0,6,8) | (2,3,10,4) | +| B | 7,15 | (4,0,4,8) | (0,4,4,8) | (7,2,4,8) | +| N | 15,23 | (8,0,13,8) | (0,8,14,8) | (6,3,10,4) | + +In particular, the first two weights are 1 and 3 before any centralizer enters. The credited stabilizers 36 and 4 give complete-header multiplicities per coordinate pair of 36 and 12, respectively. Orbit size alone does not encode how many input splits reach that orbit. + +## The h=1 branch + +The 11 sector is C, with weight (4-1)*2=6. Choose a11=e3, b11=e3*. Each of the three one-dimensional sectors is Z,A or B, each of weight one. This gives 27 incidence tuples, independently of the six realizations in sector 11. On H identify coordinates with (x0,x1,x2,x4) by x3=b0 x0+b1 x1+b2 x2. Since a_i b_i=0, the residual maps are the direct sum of the common identity on and the following rank-one projections on F2^3: + + S'=e1 (a1 b0, 1, a1 b2), + T'=e2 (a2 b0, a2 b1, 1). + +Their images are distinct. S'T' is nonzero exactly when sector 10 is A and sector 01 is B; T'S' is nonzero exactly in the opposite case. These cases are mutually exclusive. Each allows three choices for sector 00, hence has three tuples. The remaining 21 tuples have both products zero. + +This is a sufficient three-way classification, not just a rank filter. When both products vanish, the two idempotents commute and simultaneously diagonalize with sector dimensions (1,1,1) on F2^3. When S'T' is nonzero and T'S'=0, write S'=u s and T'=v t. Then s(u)=t(v)=s(v)=1 and t(u)=0. The covectors s,t are independent, so a nonzero vector w spans their common kernel and is outside . The basis (w,v,u) gives the same fixed ordered pair in every such case. Interchanging the roles proves the reverse-product case. Adding the common e4 line gives states 3,4,7 respectively. Their (rank ST,rank TS) are (1,1),(2,1),(1,2); their commutator ranks are 0,1,1. They cannot merge with the four h=0 classes: state 1 has equal maps; states 2 and 5 have equal images or equal kernels; state 6 has rank-two commutator. + +Therefore, in published order, the split weights are + + (1, 3, 21*6, 3*6, 3, 3, 3*6) = (1,3,126,18,3,3,18). + +The h=0 and h=1 contributions are 10 and 162, disjoint because h is an actual scalar attached to the split. They exhaust all common-guard splits by the sector equations. The remaining 496-172 splits fail a common first guard; there is no enumeration of those splits in this proof. + +## Completion and credited continuation + +Each split (a,b) extends to exactly |GL4(F2)|=20160 headers by choosing an ordered basis of H. All 31 nonzero vectors a have 16 covectors b with ba=1, so the total split count is 496 and the complete-header denominator is 9999360. Completion conjugates the residual pair; an orbit with stabilizer z is hit z times per split. Thus first-guard headers in a state number B(O)*20160, while each residual coordinate pair occurs B(O)*z times. These are distinct quantities. + +Sagar Thakrar's retained exact README at commit 93bebe5e1ad3dd17a97ae79f27e1a35edd3630aa proves the complementary-plane continuation rule and reports stabilizers z=(36,4,1,1,4,4,1), depth-two orbit counts f=(100,468,366,816,468,270,816). These are credited premises, not a new continuation/centralizer calculation here. Combining the newly derived inputs with that rule gives sum B*z*f=93564. The per-state contributions are (3600,5616,46116,14688,5616,3240,14688). This recovers the published total without repeating its input census. The numerical continuation table is source-bound but not independently replayed by this package. diff --git a/research/schur-split-incidence/README.md b/research/schur-split-incidence/README.md new file mode 100644 index 0000000000..4d45f97de7 --- /dev/null +++ b/research/schur-split-incidence/README.md @@ -0,0 +1,44 @@ +# First-pivot Schur state weights from sector incidence + +**Scoped binary counting proof; no new kappa.** Prepared by JoyboyBrian with substantial OpenAI Codex (gpt-6-astra) assistance. Apache-2.0. + +For the commuting-idempotent sector profile (1,1,1,2), [PROOF.md](PROOF.md) derives the seven first-pivot split multiplicities **(1,3,126,18,3,3,18)** from vector/covector incidence. It fills the input-count gap explicitly left by Sagar Thakrar's complementary-plane continuation rule. Neither all 496 splits nor GL4 is enumerated. The existing seven-state census, downstream transitions and centralizers remain credited predecessor results. + +The binary scalar-pivot formula applies to arbitrary nonnegative sector dimensions: partition each sector's vector/covector pair into Z/A/B/N/C incidence types, multiply their exact sizes, and add compatible tuples reaching the same residual class. General residual classification is not solved. For this fixed profile, h=0 yields four classes with weights 1,3,3,3; h=1 gives 27 incidence tuples of weight six, grouped as 21,3,3. The proof supplies sufficient image/kernel and rank-one normal forms, rather than assuming that rank fingerprints classify arbitrary projector pairs. + +| Published state | Split weight | Header multiplicity per coordinate pair | Credited full-guard contribution | +|---:|---:|---:|---:| +| 1 | 1 | 36 | 3600 | +| 2 | 3 | 12 | 5616 | +| 3 | 126 | 126 | 46116 | +| 4 | 18 | 18 | 14688 | +| 5 | 3 | 12 | 5616 | +| 6 | 3 | 12 | 3240 | +| 7 | 18 | 18 | 14688 | + +Each split has 20160 full-header completions. The middle column additionally uses the credited centralizers; the final column composes the new input weights with the credited continuation table and sums to 93564. The numerical continuation counts are a retained premise, not an independently rerun result. No physical header selection, odd-field normalizer, supplier admission or selected-frontier change follows. + +## Verification and source boundaries + +```sh +python3.12 -B scripts/research_package.py --package research/schur-split-incidence +python3.12 -B scripts/check_research_commit.py --package research/schur-split-incidence --check-source-history +``` + +Standalone Git-free replay is `python3.12 -I -B verify.py` or `python3.12 -I -O -B verify.py` from this package. Only the Python standard library is used. All checks use explicit failures under optimization. The verifier checks 31 canonical sector tuples against direct Schur maps and actual invertible intertwiners to the seven supplied representatives. Intertwiners are found in the linear solution space of SK=KS0 and TK=KT0, rather than by enumerating GL4. Thirty sector profiles in dimensions two and three compare weighted incidence with direct small split counts, including empty sectors. Five controls reject omitted completion fibres, orbit sizes substituted for incidence, unweighted sector types, omission of the six C realizations, and confusing all splits with admitted splits. RESULT.json fixes the output. + +Tests protect the sector-incidence partition and state mapping. The credible regressions are a missing multiplicity, reversed ordered state, or invalid zero-sector handling. Earlier census/continuation packages do not test this new derivation. The checks call the verifier's mathematical boundary directly; no production exports or flags are introduced. + +[RETAINED.json](RETAINED.json) authenticates the exact original README bytes from thakrarsagar/integer-mult-bounds commit `93bebe5e1ad3dd17a97ae79f27e1a35edd3630aa`, path `research/cbc3b1759ddd5fe5c461c509fecfae56/README.md`, and identifies its Apache-2.0 license and author. The retained calibration JSON is explicitly a small transcription, not an original file. It is compared only after deriving the input weights; it is never a filter defining the incidence classes. Base-main predecessor README/RESULT bytes are provenance-pinned in SOURCES.json. The remote successor is carried as actual package bytes, so standalone replay does not need a shared Git object or network. Its continuation proof/table is credited rather than reimplemented. + +Local checks completed on macOS with Python 3.12; both registered modes pass in under one second each. No heavy historical suite, GL4 census, Lean, Docker, production build or selected cold replay was run. Independent human/proof-kernel acceptance and general residual classification remain open. + +## Scope and attribution + +Canonical base `4c0a359d88f22f05189d51f48387750b801a45d4`, priority revision 7. This changes the formal-interface card to the precise algebraic handoff already claimed at [Discussion4653](https://github.com/CrocSwap/integer-mult-bounds/discussions/4653#discussioncomment-19140794). The root coordinator checked the active overlap/claims; coverage and exclusions are retained in TASK.json. The family decision is narrow: finish this missing input law without another profile census or construction round. + +Credit: Mihir Srivastava #4689 (`3a72fbad148294aa9ca7f900a48dbb10e64232be`) supplies the seven-state table and calibration; ssafwann #4678 (`af9cf805c501e4e9e947c98c0b97b2281b6b6e97`) and #4671 supply sector equations, factor counts and completion arguments; Sagar Thakrar supplies the complementary-plane successor and explicit first-pivot handoff; Nick Petalas #4915/#4597 and earlier scalar/header papers supply centralizer and Schur lineage. MatShep #4762, codyw912 #4735, Ryanson Jonathan, lee-phys, Cinna Davis and the normalizer lineage retain their predecessor credit. The retained successor preserves its own full credit and AI-assistance disclosure. The new claim is the input-incidence derivation, not the published seven-state count, downstream law, or centralizer calculation. + +## Open next questions + +Can the scalar sector-incidence formula be paired with a sufficient residual invariant for larger sector profiles? Start with a symbolic image/kernel decomposition for one changed profile; stop if its state classifier is unspecified rather than running another census. Higher-rank pivots require relative factorization data beyond the five scalar incidence types. Production use separately requires an actual header cover and complete selection, restoration, storage, stock and dispatch costs. These obligations are unknown, not zero. diff --git a/research/schur-split-incidence/RESULT.json b/research/schur-split-incidence/RESULT.json new file mode 100644 index 0000000000..4d42a89bc3 --- /dev/null +++ b/research/schur-split-incidence/RESULT.json @@ -0,0 +1,34 @@ +{ + "split_weights": [ + 1, + 3, + 126, + 18, + 3, + 3, + 18 + ], + "canonical_tuples": 31, + "tiny_profiles": 30, + "semantic_rejections": 5, + "complete_header_fibre": 20160, + "header_per_coordinate_pair": [ + 36, + 12, + 126, + 18, + 12, + 12, + 18 + ], + "credited_full_guard_contributions": [ + 3600, + 5616, + 46116, + 14688, + 5616, + 3240, + 14688 + ], + "credited_full_guard_total": 93564 +} diff --git a/research/schur-split-incidence/RETAINED.json b/research/schur-split-incidence/RETAINED.json new file mode 100644 index 0000000000..029e6ea321 --- /dev/null +++ b/research/schur-split-incidence/RETAINED.json @@ -0,0 +1,20 @@ +[ + { + "retained_path": "retained/continuation-README.md", + "original_path": "research/cbc3b1759ddd5fe5c461c509fecfae56/README.md", + "original_head": "93bebe5e1ad3dd17a97ae79f27e1a35edd3630aa", + "author": "Sagar Thakrar; substantial OpenAI Codex assistance", + "license": "Apache-2.0", + "sha256": "3b8acd0ba3e174c24b56a46a10c29ac1e9d6942650592c9033afc0ea240f9225", + "retention": "exact source bytes" + }, + { + "retained_path": "retained/calibration.json", + "original_path": "research/schur-residual-orbits/RESULT.json", + "original_head": "3a72fbad148294aa9ca7f900a48dbb10e64232be", + "author": "Mihir Srivastava; substantial OpenAI Codex assistance", + "license": "Apache-2.0", + "sha256": "f31f115733e4c4ddc7e7eec72b5b32e19274a9b34b583a4c543b0b2b88e6c8aa", + "retention": "selected numerical fields transcribed for independent calibration; not exact source bytes" + } +] diff --git a/research/schur-split-incidence/SOURCES.json b/research/schur-split-incidence/SOURCES.json new file mode 100644 index 0000000000..22d2771427 --- /dev/null +++ b/research/schur-split-incidence/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "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-header-count/README.md", + "usage": "provenance", + "git_blob": "5e644cf316312c0fdd489c8d33911583f1b88af2", + "sha256": "472295f32ebf3fcdc8daa4137af63db70d9943de7cbb97e47ed272823b2a227e" + }, + { + "path": "research/schur-residual-orbits/README.md", + "usage": "provenance", + "git_blob": "a2361477d9373969ccb7ab0f4f3c4b9919c051ba", + "sha256": "15e2f1a7d4edcc8f71e75ead949928c2ac883a3fb8268bb5827f290de4d28d76" + }, + { + "path": "research/schur-residual-orbits/RESULT.json", + "usage": "provenance", + "git_blob": "20146a875ccf38facac05d771d056d4c336e142b", + "sha256": "9c4a887900c8ca5202aebfb75bd30cf60d0075dcde7333843c7df6e6ebef9a1f" + } + ] +} diff --git a/research/schur-split-incidence/TASK.json b/research/schur-split-incidence/TASK.json new file mode 100644 index 0000000000..5500343273 --- /dev/null +++ b/research/schur-split-incidence/TASK.json @@ -0,0 +1,114 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "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": "Derive first-pivot split-to-residual-state MULTIPLICITIES for the fixed binary commuting-idempotent sector profile(1,1,1,2) from image/kernel incidence data, without enumerating all496 split pairs or GL4. Recover the seven published multiplicities and compose them with the already-proved complementary-plane continuation rule; establish a formula with explicitly stated general hypotheses rather than another adjacent-profile census.", + "scope_change_reason": "PR4689 already enumerated seven states; thakrarsagar commit93bebe5 already derives their downstream transitions without GL4; PR4915 already derives centralizers. The remaining named gap is the INPUT split-incidence law, not orbit sizes, continuation or rank-only classification. Use their proofs as credited premises and isolate why orbit size alone cannot give header incidence.", + "bottleneck_link": "Algebraic side result: supply first-pivot input incidence for a state-aware Schur recursion.", + "budget_minutes": 60, + "stop_rule": "Stop after a proved incidence formula recovering seven weights, or a concrete missing sufficient invariant. No larger-profile/field census, GL4 enumeration, production header claim or rerun of earlier complete guard tables.", + "outcome": "completed", + "evidence": "PROOF.md binary scalar sector-incidence formula; derived seven weights; 31 canonical seeds with explicit invertible intertwiners; 30 tiny direct profiles; five semantic rejections. Credited continuation table is composed, not replayed.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance using gpt-6-astra; task05 is one isolated researcher coordinated by a root agent.", + "open_questions": [ + { + "question": "Can the sector-incidence law scale to higher pivot rank?", + "why_it_matters": "Would enable state-aware header recursion beyond the fixed scalar profile.", + "first_step": "Identify sufficient relative image/kernel invariants for d=2 without a full matrix census.", + "blocked_by": "Classification of multi-dimensional sector factorizations and their simultaneous incidences." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4653#discussioncomment-19140794", + "first_fixture": "Derive the split multiplicities1 and3 for representatives ([0,0,4,8],[0,0,4,8]) and ([0,0,4,8],[0,0,4,9]) from sector incidence. Their centralizers36 and4 yield header-per-orbit weights36 and12; explain why these are distinct quantities before tackling all seven.", + "bounds": "F2 scalar pivot at profile (1,1,1,2); no GL4 or full 496-split enumeration.", + "inherited_obligations": [ + "No production header cover or physical pricing.", + "No selected-frontier change." + ], + "overlap": { + "coverage": "/tmp/imb-brian-b2/overlap.json; 304 open PRs and 4153 discussion records fetched 2026-10-23 07:19 UTC; board.json read. Body/source search, not arbitrary diff or unpublished-work coverage. Recheck live heads before claim.", + "active_exclusions": [ + "partial signed-Pauli chart completion #1166 comment19140242", + "four-frame relative-operator classification #1166 comment19140243", + "physical rounded boundary pages #4182 comment19140225", + "BIT signed dyadic scaling #1317 comment19140224", + "owned-COPY/shared-late-G contact optimization #4611 comment19139586", + "two-row nonunit dirty fanout #5030" + ], + "distinction": "Fresh overlap caught BOTH already-completed followups and excludes them. This is the explicit remaining first-pivot incidence handoff (#1166 comment19130949), separate from active four-frame similarity and signed-Pauli completion." + } +} diff --git a/research/schur-split-incidence/VERIFY.json b/research/schur-split-incidence/VERIFY.json new file mode 100644 index 0000000000..14349cd746 --- /dev/null +++ b/research/schur-split-incidence/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 10, + "checks": "31 canonical incidence seeds; invertible intertwiners; 30 tiny profiles; five semantic rejections; retained bytes; result replay" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 10, + "checks": "Same explicit failures with assertions disabled" + } + ] +} diff --git a/research/schur-split-incidence/retained/calibration.json b/research/schur-split-incidence/retained/calibration.json new file mode 100644 index 0000000000..cd211a360c --- /dev/null +++ b/research/schur-split-incidence/retained/calibration.json @@ -0,0 +1,29 @@ +{ + "split_weights": [ + 1, + 3, + 126, + 18, + 3, + 3, + 18 + ], + "stabilizers": [ + 36, + 4, + 1, + 1, + 4, + 4, + 1 + ], + "depth_two_orbit_counts": [ + 100, + 468, + 366, + 816, + 468, + 270, + 816 + ] +} diff --git a/research/schur-split-incidence/retained/continuation-README.md b/research/schur-split-incidence/retained/continuation-README.md new file mode 100644 index 0000000000..3a908bc509 --- /dev/null +++ b/research/schur-split-incidence/retained/continuation-README.md @@ -0,0 +1,87 @@ +# A complementary-plane rule for the seven binary Schur states + +This is an independent finite check of the seven ordered residual pairs in +[PR #4689](https://github.com/CrocSwap/integer-mult-bounds/pull/4689), pinned at +`3a72fbad148294aa9ca7f900a48dbb10e64232be`. It recovers every remaining +guard-depth count and stabilizer without enumerating GL₄(F₂). The result is a +transition rule for **these supplied representatives**, not an independent +classification of the seven orbits or the 172 admitted first-pivot split pairs. +There is no supplier admission or new κ. + +## Rule and proof + +Let `S,T` act on `V=F₂⁴`. Every ordered basis `(x,y,w₁,w₂)` gives a unique +decomposition `V=U⊕W`, where `U=span(x,y)` and `W=span(w₁,w₂)`. Conversely, each +ordered complementary pair of two-planes has six bases of `U` and six bases of +`W`. There are 35 two-planes, 16 complements per plane, hence +`35·16·6·6=20,160` bases. This partitions GL₄ without listing its elements. + +For `U⊕W`, let `π:V→U` be projection along `W`. In basis `(x,y,w₁,w₂)`, the +leading two-by-two block of a map `A` is the matrix of `πA|U` in `(x,y)`. +Its determinant is one precisely when `πAx` and `πAy` are distinct nonzero +vectors. Its leading one-by-one entry is one precisely when +`πAx∈{x,x+y}`. Both statements follow by writing the two projected vectors +in the basis `(x,y)`; they require no idempotency assumption. + +Therefore, for each `(U,W)` and each of the six ordered pairs `(x,y)` of +distinct nonzero vectors of `U`, the simultaneous first guard is +`πSx,πTx∈{x,x+y}`. The second guard additionally requires both projected +restrictions to be invertible. Multiply each successful choice by six for +the possible ordered bases of `W`. Summing over 560 decompositions yields +the number of bases reaching each depth. The rule is invariant under +simultaneous conjugacy: a change of coordinates bijects the complementary +plane pairs and preserves these projection tests. + +All supplied representatives have `S=diag(0,0,1,1)`. A matrix stabilizing +`S` must preserve `ker S` and `im S`, so it is a two-by-two block diagonal +pair in `GL₂(F₂)×GL₂(F₂)`. There are only 36 such pairs. Filtering them by +`KT=TK` gives stabilizer sizes `36,4,1,1,4,4,1`. Dividing the basis counts +by each size gives orbit-element depth counts, rather than counting the +same orbit element repeatedly. The script checks the published values: + +| State | Stabilizer | Depth 0 | Depth 1 | Depth 2 | +|---:|---:|---:|---:|---:| +| 1 | 36 | 280 | 180 | 100 | +| 2 | 4 | 3192 | 1380 | 468 | +| 3 | 1 | 15120 | 4674 | 366 | +| 4 | 1 | 14448 | 4896 | 816 | +| 5 | 4 | 3192 | 1380 | 468 | +| 6 | 4 | 3528 | 1242 | 270 | +| 7 | 1 | 14448 | 4896 | 816 | + +Using PR #4689's **imported** split-pair multiplicities `1,3,126,18,3,3,18`, +the independently recovered depth-two basis counts sum to 93,564 complete +headers. This agrees with its reported fraction `2599/277760`. Agreement is +an audit of the continuation law and arithmetic; the imported multiplicities +and original all-header denominator are not independently reproved here. + +## Reproduce + +Python 3.10 or newer, standard library only: + +```sh +python3 -B research/cbc3b1759ddd5fe5c461c509fecfae56/plane_count.py +python3 -O -B research/cbc3b1759ddd5fe5c461c509fecfae56/plane_count.py +``` + +Both end with `PASS_PLANE_TRANSITIONS full_guard_headers=93564 +decompositions_per_state=560 no_GL4_enumeration`. The checker has no writes, +network access or predecessor imports. Its two-plane and complement totals, +seven stabilizers, all depth counts, and aggregate are explicit failures even +under `-O`. It does not enumerate GL₄, GL₅ or the first-pivot split pairs. + +## Open next questions + +Derive the first-pivot **state multiplicities** from image/kernel data without +enumerating the 496 split pairs, then connect this rule to a scalable state +recursion. The present 560-decomposition finite sum should be replaced by a +closed orbit or intersection formula before extrapolating to larger fields or +dimensions. Neither this binary count nor PR #4689's table prices a production +header, dirty restoration, stock, dispatch or a complete consumer. + +Credit: Mihir Srivastava's PR #4689 supplies the seven representatives, +split-pair multiplicities and published counts. Its README credits ssafwann's +PR #4678, Nick Petalas's Schur/header work, Ryanson Jonathan's full-guard +census, lee-phys's dimension work and the normalizer lineage. This independent +rule was prepared by Sagar Thakrar with substantial OpenAI Codex assistance. +Apache-2.0. diff --git a/research/schur-split-incidence/verify.py b/research/schur-split-incidence/verify.py new file mode 100644 index 0000000000..142126a11a --- /dev/null +++ b/research/schur-split-incidence/verify.py @@ -0,0 +1,235 @@ +"""Exact binary scalar-incidence checks; no GL4 or 496-split census.""" +from collections import Counter +from itertools import product +from pathlib import Path +import hashlib +import json + +ROOT = Path(__file__).resolve().parent +REPS = [(0, 0, 4, 8), (0, 0, 4, 9), (0, 2, 0, 8), + (0, 2, 2, 8), (0, 4, 4, 8), (0, 4, 4, 9), (0, 6, 0, 8)] +SREP = (0, 0, 4, 8) + + +def require(ok, label): + if not ok: + raise ValueError(label) + + +def dot(a, b): + return (a & b).bit_count() % 2 + + +def apply(matrix, vector): + return sum(dot(row, vector) << i for i, row in enumerate(matrix)) + + +def span(vectors): + out = {0} + for v in vectors: + out |= {x ^ v for x in tuple(out)} + return out + + +def basis(vectors): + out = [] + for v in sorted(vectors): + if v not in span(out): + out.append(v) + return out + + +def rank(matrix): + return len(basis(matrix)) + + +def compose(a, b): + n = len(a) + return tuple(sum(dot(row, sum(((b[k] >> j) & 1) << k for k in range(n))) << j + for j in range(n)) for row in a) + + +def residual(profile, a, b): + n = sum(profile) + masks = [] + offset = 0 + for r in profile: + masks.append(((1 << r) - 1) << offset) + offset += r + p, q = masks[1] | masks[3], masks[2] | masks[3] + require(dot(a, b) == dot(a & p, b) == dot(a & q, b) == 1, 'split/guard') + hb = basis(v for v in range(1 << n) if not dot(b, v)) + coordinates = {0: 0} + for i, v in enumerate(hb): + coordinates.update({x ^ v: c | (1 << i) for x, c in tuple(coordinates.items())}) + matrices = [] + for mask in (p, q): + columns = [coordinates[(v & mask) ^ ((a & mask) if dot(b, v & mask) else 0)] for v in hb] + matrices.append(tuple(sum(((v >> i) & 1) << j for j, v in enumerate(columns)) for i in range(n - 1))) + return tuple(matrices) + + +def fingerprint(s, t): + n = len(s) + si = {apply(s, x) for x in range(1 << n)} + ti = {apply(t, x) for x in range(1 << n)} + common_kernel = sum(apply(s, x) == apply(t, x) == 0 for x in range(1 << n)) + st, ts = compose(s, t), compose(t, s) + return (s == t, len(si & ti), common_kernel, rank(st), rank(ts), rank(tuple(a ^ b for a, b in zip(st, ts)))) + + +def conjugacy_witness(pair, target): + # Solve S*K=K*S0 and T*K=K*T0, then find one invertible solution. + equations = [] + for a, b in zip(pair, target): + for i in range(4): + for j in range(4): + row = 0 + for k in range(4): + if (a[i] >> k) & 1: + row ^= 1 << (4 * k + j) + if (b[k] >> j) & 1: + row ^= 1 << (4 * i + k) + equations.append(row) + pivots = {} + for row in equations: + while row: + pivot = row.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = row + break + row ^= pivots[pivot] + free = [i for i in range(16) if i not in pivots] + solutions = [] + for f in free: + x = 1 << f + for pivot, row in sorted(pivots.items()): + if dot(row, x): + x ^= 1 << pivot + solutions.append(x) + for encoded in sorted(span(solutions)): + k = tuple((encoded >> (4 * i)) & 15 for i in range(4)) + if rank(k) == 4: + require(all(compose(a, k) == compose(k, b) for a, b in zip(pair, target)), 'intertwiner identity') + return k + raise ValueError('no invertible intertwiner') + + +def sector_types(r, h): + require(type(r) is int and r >= 0 and h in (0, 1), 'sector domain') + if r == 0: + return [] if h else [('Z', 0, 0, 1)] + m = (1 << r) - 1 + if h: + return [('C', 1, 1, m * (1 << (r - 1)))] + result = [('Z', 0, 0, 1), ('A', 1, 0, m), ('B', 0, 1, m)] + if r > 1: + result.append(('N', 1, 2, m * ((1 << (r - 1)) - 1))) + return result + + +def incidence(profile): + for h in (0, 1): + choices = [sector_types(r, h if j == 3 else 1 - h) for j, r in enumerate(profile)] + for types in product(*choices): + offset = a = b = 0 + weight = 1 + for r, (_, u, v, w) in zip(profile, types): + a |= u << offset + b |= v << offset + offset += r + weight *= w + yield h, tuple(t[0] for t in types), a, b, weight + + +def derive_state(h, types): + if h == 0: + return {'Z': 0, 'A': 1, 'B': 4, 'N': 5}[types[3]] + if types[1:3] == ('A', 'B'): + return 3 + if types[1:3] == ('B', 'A'): + return 6 + return 2 + + +def gl(n): + result = 1 + for i in range(n): + result *= (1 << n) - (1 << i) + return result + + +def main(): + sources = json.loads((ROOT / 'RETAINED.json').read_text()) + for row in sources: + require(hashlib.sha256((ROOT / row['retained_path']).read_bytes()).hexdigest() == row['sha256'], 'retained source bytes') + fingerprints = [fingerprint(SREP, t) for t in REPS] + require(len(set(fingerprints)) == 7, 'seven states distinct') + weights = [0] * 7 + seeds = [] + for h, types, a, b, w in incidence((1, 1, 1, 2)): + state = derive_state(h, types) + pair = residual((1, 1, 1, 2), a, b) + require(fingerprint(*pair) == fingerprints[state], 'canonical seed state') + conjugacy_witness(pair, (SREP, REPS[state])) + require(all(compose(x, x) == x and rank(x) == 2 for x in pair), 'residual idempotency/rank') + weights[state] += w + seeds.append({'h': h, 'types': types, 'a': a, 'b': b, 'weight': w, 'state': state + 1}) + require(len(seeds) == 31, '31 canonical sector tuples') + require(weights[:2] == [1, 3], 'first fixture') + # The old table is calibration only: derive_state never reads it. + calibration = json.loads((ROOT / 'retained/calibration.json').read_text()) + require(weights == calibration['split_weights'], 'published input calibration') + require(sum(weights) == 172, 'first guard split total') + + # Independent direct splits in dimension two and three, including empty sectors. + tiny = 0 + for n in (2, 3): + for profile in product(range(n + 1), repeat=4): + if sum(profile) != n: + continue + expected = Counter() + for _, _, a, b, w in incidence(profile): + expected[fingerprint(*residual(profile, a, b))] += w + direct = Counter() + offset = 0 + masks = [] + for r in profile: + masks.append(((1 << r) - 1) << offset) + offset += r + for a in range(1, 1 << n): + for b in range(1 << n): + if dot(a, b) == dot(a & (masks[1] | masks[3]), b) == dot(a & (masks[2] | masks[3]), b) == 1: + direct[fingerprint(*residual(profile, a, b))] += 1 + require(direct == expected, 'tiny direct split versus weighted incidence') + tiny += 1 + + z = calibration['stabilizers'] + f = calibration['depth_two_orbit_counts'] + contributions = [w * c * d for w, c, d in zip(weights, z, f)] + require(sum(contributions) == 93564, 'credited continuation composition') + require([weights[i] * z[i] for i in (0, 1)] == [36, 12], 'header per coordinate pair') + controls = 0 + for wrong, correct in [(sum(weights), sum(weights) * gl(4)), + ([gl(4) // c for c in z], weights), + ([1] * 7, weights), + (21, weights[2]), + (496, sum(weights))]: + try: + require(wrong == correct, 'semantic mutant') + except ValueError: + controls += 1 + else: + raise ValueError('semantic mutant accepted') + require(controls == 5, 'all controls rejected') + result = {'split_weights': weights, 'canonical_tuples': len(seeds), 'tiny_profiles': tiny, + 'semantic_rejections': controls, 'complete_header_fibre': gl(4), + 'header_per_coordinate_pair': [w * c for w, c in zip(weights, z)], + 'credited_full_guard_contributions': contributions, + 'credited_full_guard_total': sum(contributions)} + require(result == json.loads((ROOT / 'RESULT.json').read_text()), 'result replay') + print('PASS_SCHUR_SPLIT_INCIDENCE', json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main()