diff --git a/research/schur-invariant-transitions/README.md b/research/schur-invariant-transitions/README.md new file mode 100644 index 0000000000..d5118b9f59 --- /dev/null +++ b/research/schur-invariant-transitions/README.md @@ -0,0 +1,354 @@ +# Split-pivot recurrence and sufficient residual invariants + +Prepared by **codyw912**, with substantial **OpenAI Codex (GPT-6 Astra)** +assistance. Apache-2.0. **No new κ and no selected-frontier change.** + +This package supplies an intrinsic recurrence, a block-intertwiner certificate +for the seven ordered rank-two residuals, and a sufficient rank-one invariant. +The seven-state numerical table and the total **93,564 / 9,999,360** are credited +to **Mihir Srivastava, PR4689**, not claimed as new numbers. The new contribution +is their derivation through small state transitions without generating GL4 or +GL5, together with a proof that the terminal invariant is sufficient. + +**Evidence status:** parent replay on CPython 3.12.13, Linux x86_64, completed +with exit status zero using `python3.12 -B scripts/research_package.py --package +research/schur-invariant-transitions`. Both registered ordinary +`-I -W error -B` and optimized `-I -W error -O -B` commands emitted +`PASS_SCHUR_INVARIANT_TRANSITIONS`; the runner emitted +`PASS_REGISTERED_RESEARCH_PACKAGE`. The replay reproduced 496 initial splits, +172 admitted splits, 784 rank-one pairs, seven exact states, nine rejected +mutations and 93,564/9,999,360 = 2599/277760, including all embedded state and +depth expectations. The expectations remain credited predecessor results; +this is observed regeneration, not a claim to new numerical discoveries. +A separate AI mathematical review found no blocking issue in the recurrence, +stabilizers or invariant-sufficiency proof. Neither that review nor the local +replay constitutes independent human, proof-kernel or hosted approval. The +implementation worker ran no research code, gates, builds or formatters. +Final separate AI static review also reported PASS with no blockers. Parent +reported the shared 331-test suite passing with 11 Windows-specific skips; +this tooling evidence is separate from the mathematical package replay. +No public Discussion claim was posted. Upstream PR creation requires operator +approval; publication status is reported in the handoff. + +## Domain and complete-header recurrence + +All vector spaces in this package are over F2. Requests remain **ordered**. For +idempotents A,B on V of dimension n, let H(n,k;A,B) count complete ordered bases +M such that both M^-1 A M and M^-1 B M have nonzero leading principal minors of +orders 1 through k. Require 0 <= k <= n; GL0 has order one. Neither commutation +nor an equal-rank hypothesis is needed for the recurrence. An impossible guard +has count zero, in particular when k exceeds either rank. + +For a vector a and functional beta satisfying + +``` +beta(a) = beta(Aa) = beta(Ba) = 1, +W = ker(beta), +A'(x) = Ax + Aa beta(Ax), B'(x) = Bx + Ba beta(Bx), x in W, +``` + +we have the exact, basis-independent recurrence + +``` +H(n,0;A,B) = |GL_n(F2)| = product_{j=0}^{n-1}(2^n - 2^j), +H(n,k;A,B) = sum_{admitted (a,beta)} H(n-1,k-1;A',B'). +``` + +The minus sign of the ordinary Schur formula equals plus in F2. The maps land +in W because beta(Aa)=beta(Ba)=1. For A, put c=Aa and t=beta(Ax). +Then A(Ax+ct)=Ax+ct since A²=A and Ac=c. Its beta-value is zero, so applying +the same Schur operator again changes nothing: A'²=A'. The argument for B is +identical. In a basis (a,w1,...,w[n-1]) with the w's in W, A has block form +`[[1,R],[C,D]]`, and A' is `D+CR`. Invertible block elimination gives +`rank(A')=rank(A)-1`. This also proves agreement with the intrinsic map. + +**Completion and guard proof.** A complete header M determines exactly the +split consisting of its first column a and the first row beta of M^-1. +Conversely, for a fixed split, appending any ordered basis of ker(beta) gives +exactly one header with that first column and inverse first row. Thus its +completion fibre has size |GL[n-1]|, not one and not `2^(n-1)|GL[n-1]|`. +At a unit pivot the determinant of each leading (j+1)-block equals the +corresponding leading j-block determinant of the Schur complement. Partitioning +headers by split and applying this identity proves the recurrence. A basis +change on W bijects its complete headers, so the intrinsic notation is valid. +The recurrence applies at every subsequent, possibly **noncommuting**, residual. + +The concrete input is + +``` +P0 = diag(0,1,0,1,1), Q0 = diag(0,0,1,1,1). +``` + +Only guard orders 1,2,3 are required. The 31 nonzero first columns have 16 +splitting functionals each, giving 496 splits and `496*20160=9999360` complete +headers. After an admitted first split the two residuals have dimension four +and rank two; after the next, dimension three and rank one. + +## Rank-two blocks, stabilizers, and certified classification + +Matrices use integer **rows**, bit j representing column j. All representatives +have `S=(0,0,4,8)=diag(0_2,I_2)`. In `ker S ⊕ im S`, write +`T=[[E,F],[G,H]]`. An invertible map commuting with S preserves both summands, +so it is exactly `K=diag(U,V)` with U,V in GL2. It stabilizes T exactly when + +``` +UE=EU, UF=FV, VG=GU, VH=HV. +``` + +This proves that only 6*6=36 candidates, not GL4, need examination. It also +proves the normalization equivalence criterion: after normalizing S, two T's +are equivalent precisely by this block action. + +Here are analytic stabilizer derivations. Let `D=diag(0,1)` and let +`J=e2 e1^t` on F2². In F2 a one-dimensional invertible scalar is one. + +* State 1: E=0, H=I, F=G=0. Every U,V works: 36. +* State 2: E=0, H=I, F=0, G=J. The one nontrivial equation is + `V e2 e1^t = e2 e1^t U`. Equality of nonzero rank-one tensors forces + `V e2=e2` and `e1^t U=e1^t`; each has two choices: 4. +* State 3: E=H=D and F=G=0. Centralizing D preserves its two distinct + eigenlines, hence U=V=I: 1. +* State 4: E=H=D, F=0, G=e1 e2^t. The preceding diagonal equations already + force U=V=I, which satisfies the off-diagonal equation: 1. +* State 5: E=0, H=I, G=0, F=J. Now `U e2=e2` and `e1^t V=e1^t`: + again 2*2=4. +* State 6: E=0, H=I, F=G=J. Both U and V must fix e2 and its annihilating + functional e1^t, hence each is `[[1,0],[c,1]]`, c in F2: 4. +* State 7: E=H=D, G=0, F=J. Again U=V=I: 1. + +The implementation corroborates these constraints on the 36 GL2² pairs per +representative and prints every stabilizer. It builds only their small **block +orbits**, checking these are pairwise disjoint. For each of the admitted initial +splits, it computes a deterministic basis C of `ker S' ⊕ im S'`, finds a block K +with `C^-1 T' C = K T_i K^-1`, and checks the explicit witness L=CK: + +``` +S' L = L S, T' L = L T_i, rank(L)=4. +``` + +All 172 splits, their state assignments, and these invertible witnesses are +printed. Unmatched residuals or overlaps fail; no rank-signature heuristic is +used to force membership. This is completeness for the initial split domain, +**not** a classification of every pair of rank-two projectors in dimension four. + +## Sufficient rank-one invariant: proof, not a guess + +Over F2, each nonzero rank-one idempotent has a unique factorization +`R=u phi`, with u and phi nonzero and phi(u)=1. For an ordered pair +`(R,T)=(u phi,v psi)` on an n-dimensional space use + +``` +I(R,T) = ([u=v], [phi=psi], phi(v), psi(u)), together with n. +``` + +These data are necessary under simultaneous conjugation. They are also +**sufficient**. Define `X:F2² -> V` with columns u,v and `Y:V -> F2²` with rows +phi,psi. The first flag determines ker X (zero or span(1,1)). The second flag +determines im Y (F2² or span(1,1)). The two cross-values determine +`YX=[[1,phi(v)],[psi(u),1]]`. + +Here is the full extension argument, including the potentially missing datum. +Consider two systems X,Y and X',Y' with these three data equal and ambient +dimensions equal. Let L=im X, K=ker Y, and similarly L',K'. Equality of ker X +makes `f0(Xz)=X'z` a well-defined isomorphism L->L'. Equality of YX gives +`Y'f0=Y|L`, so f0 sends L∩K isomorphically onto L'∩K'. Equality of im Y and +ambient dimensions gives dim K=dim K'. Extend this restriction to any +isomorphism fK:K->K'. The maps f0,fK agree on the intersection and therefore +combine to an isomorphism f1:L+K -> L'+K'. It satisfies `Y'f1=Y`. +Finally choose a basis of a complement of Y(L) in the **common** im Y, and +choose a lift in each ambient space for every vector of that basis. Those lifts +complement L+K and L'+K', respectively: the induced maps from these quotients +to im Y/Y(L) are isomorphisms. Mapping corresponding lifts extends f1 to an +invertible f on V with `fX=X'` and `Y'f=Y`. Consequently +`f(u phi)=(u' phi')f` and `f(v psi)=(v' psi')f`. + +Thus no extra datum is missing: the intersection information is already fixed +by ker X, im Y and YX. This is an all-dimension binary proof, not a consequence +of the finite terminal census. Dimension must be retained. For example, when +both flags are zero and both cross-values are one, rank(YX)=1; in dimension two +X and Y would both be invertible, an impossibility. Dimension three admits it. +When either equality flag is one both cross-values must be one. Hence in +**dimension three** there are exactly seven possibilities, all realized below. + +## Terminal counts from consistent linear constraints + +For rank-one requests an admitted split requires +`phi(a)=psi(a)=1` and `beta(a)=beta(u)=beta(v)=1`. For fixed a the last three +constraints are consistent iff every relation among a,u,v has even coefficient +sum. Equivalently the coefficient and augmented matrices have equal ranks. +Thus the exact number of terminal splits is + +``` +g(R,T) = sum_{a: phi(a)=psi(a)=1} + [consistent a,u,v -> 1] * 2^(n-rank(a,u,v)), +H(3,1;R,T) = 6*g(R,T). +``` + +The zero vector never satisfies the first conditions. In particular a=u+v +with u,v distinct gives the odd relation a+u+v=0 and contributes **zero**. +Dropping consistency is not a valid use of the rank formula. + +The following representatives give the terminal class table. Vector and +functional integers have the same least-significant-bit coordinate convention. +The last four rows list the distinct cross-pairings in order. + +| Invariant | (u,phi,v,psi) | g | Derivation in dimension three | +|---|---|---:|---| +| 1111 | (1,1,1,1) | 10 | a=u contributes 4; three other a contribute 2 each | +| 1011 | (1,1,1,3) | 6 | a=u contributes 4; the other allowed a contributes 2 | +| 0111 | (1,1,3,1) | 6 | a=u,v contribute 2 each; two other a contribute 1 | +| 0000 | (1,1,2,2) | 1 | a=3 is inconsistent; a=7 contributes 1 | +| 0001 | (1,1,2,3) | 3 | a=1 contributes 2; a=5 contributes 1 | +| 0010 | (1,3,2,2) | 3 | a=2 contributes 2; a=6 contributes 1 | +| 0011 | (1,3,2,7) | 4 | a=1,2 each contribute 2 | + +The verifier constructs this table and uses invariant lookup in the recurrence. +As an independent finite corroboration, all 28²=784 ordered rank-one pairs are +checked against literal `(a,beta)` split constraints, with no basis enumeration. +Every next-pivot transition is counted with multiplicity; deterministic stdout +contains all seven terminal-type entries, including zeros, for each state. +The ordered-pair populations in the displayed class order are respectively +28,84,84,168,168,168,84, also embedded as exact targets. The seven H(4,2) +values are additionally compared against direct recursive split evaluation +with the GL-order zero-guard base case; memoization is in-memory only. + + +## Expected state and guard-depth tables + +The T rows, b,z,o,f, header weights and full guards below are Mihir's PR4689 +results. Here m counts the next admitted splits, G sums their terminal g-values, +and `H(4,2)=6G`. These m,G and depth targets are the predecessor's depth data +and arithmetic consequences of its table, reproduced by the parent replay. + +| State | T rows | b | z | m | G | o=20160/z | f=6G/z | Header weight | Full guards | +|---|---|---:|---:|---:|---:|---:|---:|---:|---:| +| 1 | (0,0,4,8) | 1 | 36 | 60 | 600 | 560 | 100 | 20160 | 3600 | +| 2 | (0,0,4,9) | 3 | 4 | 44 | 312 | 5040 | 468 | 60480 | 5616 | +| 3 | (0,2,0,8) | 126 | 1 | 30 | 61 | 20160 | 366 | 2540160 | 46116 | +| 4 | (0,2,2,8) | 18 | 1 | 34 | 136 | 20160 | 816 | 362880 | 14688 | +| 5 | (0,4,4,8) | 3 | 4 | 44 | 312 | 5040 | 468 | 60480 | 5616 | +| 6 | (0,4,4,9) | 3 | 4 | 36 | 180 | 5040 | 270 | 60480 | 3240 | +| 7 | (0,6,0,8) | 18 | 1 | 34 | 136 | 20160 | 816 | 362880 | 14688 | + +After the initial admitted guard, let depth d=0,1,2 be the number of further +common guards passed. A next split has |GL3|=168 unrestricted completions, +whereas a successful two-step continuation has |GL2|=6 completions. Conjugation +by GL4 has uniform fibre z onto its orbit (orbit-stabilizer theorem). Therefore + +``` +d0=(20160-168m)/z, d1=(168m-6G)/z, d2=6G/z, +headers per orbit element = b*z, +full guards in initial state = b*6G. +``` + +| State | d0 | d1 | d2 | +|---|---:|---:|---:| +| 1 | 280 | 180 | 100 | +| 2 | 3192 | 1380 | 468 | +| 3 | 15120 | 4674 | 366 | +| 4 | 14448 | 4896 | 816 | +| 5 | 3192 | 1380 | 468 | +| 6 | 3528 | 1242 | 270 | +| 7 | 14448 | 4896 | 816 | + +Summing gives 172 first-admitted splits and 3,467,520 first-guard headers, but +only 93,564 full-guard headers. The full fraction is 2599/277760. State 6 retains +the credited one-block sharp-header count 60,480 and full continuation 3,240. +No uniform weighting of states or orbit elements across distinct initial +fibres is assumed. + +## Reproduction, controls, and boundaries + +Python 3.12 standard library, five files, no third-party imports, external reads, +pending-head objects, network calls, subprocesses, persistent caches or write mode in the +scientific verifier. Direct exported-package execution needs no Git: + +```sh +python3.12 -I -W error -B research/schur-invariant-transitions/verify.py +python3.12 -I -W error -O -B research/schur-invariant-transitions/verify.py +``` + +Each command prints deterministic JSON followed by +`PASS_SCHUR_INVARIANT_TRANSITIONS` only after every explicit check succeeds. +The package runner also checks historical source metadata: + +```sh +python3.12 -B scripts/research_package.py --package research/schur-invariant-transitions +``` + +VERIFY.json proposes a 60-second cap per run, not a measured runtime. The +scientific domain is 496 initial splits, seven 120-split next domains, 36 block +changes per representative, and 784 terminal pairs, plus direct recursive +split evaluation of the seven H(4,2) representatives. There is no GL4/GL5 +generator, no 4x4 raw-matrix census, no native compiler, Lean or selected cold +replay. All failure checks use exceptions rather than disabled-by-`-O` asserts. +Permanent mutation controls reject missing GL2/GL4 completion factors, +commutator-only and product/sum/commutator-rank identification, transposition, +unordered terminal requests, ignored odd relations, omitted Schur correction, +and replacing full guards by first-guard counts. States 1 and 3 have equal +commutator rank but different continuations; states 2 and 5 share the listed +ranks yet are distinct ordered orbits. Transposition exchanges 2/5 and 4/7. + +The recurrence is proved generally for binary idempotents; the seven-state +certificate is only for the displayed sector profile (1,1,1,2). No larger-field +invariant classification is claimed. The binary event is not admission into +the retained odd-q executable normalizer. Physical header selection/emission, +reads, restoration, storage, stock, dispatch and the complete consumer bill +remain unpriced, not zero. No formal proof-kernel or independent human theorem +acceptance is claimed. + +## Provenance, overlap, and credit + +Canonical base is `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, priority revision 7, +selected κ=60403/20000000=0.00302015 from #4470. TASK.json explicitly changes the +`formal-interface-lemma` card to this algebraic side result; it neither discharges +the selected all-size interface obligations nor repeats stale endpoint arithmetic. +SOURCES.json pins only historical canonical-main provenance; VERIFY.json has no +external live inputs. Pending works below are immutable **citations**, not Git +ancestry or executable dependencies. Embedded numeric expectations are openly +transcribed fixtures, not runtime-authenticated remote files. + +* **Mihir Srivastava**, substantial OpenAI Codex assistance, [PR4689](https://github.com/CrocSwap/integer-mult-bounds/pull/4689), + head `3a72fbad148294aa9ca7f900a48dbb10e64232be`: + [seven-state table and proof](https://github.com/CrocSwap/integer-mult-bounds/blob/3a72fbad148294aa9ca7f900a48dbb10e64232be/research/schur-residual-orbits/README.md), + [depth receipt](https://github.com/CrocSwap/integer-mult-bounds/blob/3a72fbad148294aa9ca7f900a48dbb10e64232be/research/schur-residual-orbits/RESULT.json). + All seven numerical states and the total retain this attribution. +* **ssafwann**, substantial OpenAI Codex assistance, [PR4678](https://github.com/CrocSwap/integer-mult-bounds/pull/4678), + head `af9cf805c501e4e9e947c98c0b97b2281b6b6e97`: one-block counts, equal + completion fibres, profile and [released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/4653#discussioncomment-19126925). + [PR4671](https://github.com/CrocSwap/integer-mult-bounds/pull/4671), head + `8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9`, supplies the sector criterion. +* **Nick Petalas**, [PR4597](https://github.com/CrocSwap/integer-mult-bounds/pull/4597), + head `dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb`: block Schur bound and orbit + question; retained [scalar Schur proof](../schur-commutator-criterion/README.md) + supplies residual idempotency/rank and the earlier header lineage. +* **Ryanson Jonathan**, substantial Claude Code (Claude Opus 5.5) assistance: + [full-guard convention and separate-family census](../full-guard-header-census/README.md). + Retain **lee-phys**'s binary sharpness/dimension contributions, **Cinna Davis**'s + PR4100 BIT request context and its normalizer lineage (source527, commdata2338, + Jose Manuel). No predecessor code is imported or copied into this verifier. + +At the final parent checkpoint, canonical origin/main remained +`b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`. The refreshed overlap snapshot +covered 469 open PRs at 2026-10-22T16:48:00.710568+00:00 and 3,624 discussion +records at 2026-10-22T16:48:34.859558+00:00, with complete pagination. All 5,860 +tracked local records were covered; the local snapshot had 5,864 records, +including four from this contribution work. Direct predecessor heads #4689, +#4678, #4671 and #4597 remained unchanged from the cited pins. Coverage does +not include arbitrary remote diffs, closed remote PR bodies or unpublished work; +no novelty or reservation over those domains is asserted. No public Discussion +claim was posted. Upstream PR creation requires operator approval; publication +status is reported in the handoff. + +## Open next questions + +1. **Can a sufficient higher-rank state invariant replace block-orbit matching?** + This is relevant to scalable recursion beyond one binary profile. First derive + the representation data of two image/kernel decompositions and test proposed + invariants against the explicit witnesses here. Block intertwiners certify + this finite domain but are not a general classification; that is the blocker. +2. **Can the state recurrence support an admitted, paid header cover?** The finite + full-guard probability alone supplies no executable cost bound. First state + the actual caller's field and header-selection contract and price emission, + physical reads and restoration. Odd-q admission and the complete consumer bill + remain separate blockers. No expansion or follow-up claim is held here. diff --git a/research/schur-invariant-transitions/SOURCES.json b/research/schur-invariant-transitions/SOURCES.json new file mode 100644 index 0000000000..c652055701 --- /dev/null +++ b/research/schur-invariant-transitions/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/verify.py", + "usage": "provenance", + "git_blob": "c0b2b3df32278ebe712c712060dddadb65a3eb23", + "sha256": "5da438aacee1cbb3d9469787b8b97288deb016336ad3addeed496ca9b36593e9" + } + ] +} diff --git a/research/schur-invariant-transitions/TASK.json b/research/schur-invariant-transitions/TASK.json new file mode 100644 index 0000000000..d3e2ba0202 --- /dev/null +++ b/research/schur-invariant-transitions/TASK.json @@ -0,0 +1,113 @@ +{ + "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": "Prove the binary split-pivot complete-header recurrence, derive the seven rank-two stabilizers by image/kernel blocks, classify initial residuals with explicit ordered intertwiners, prove a sufficient rank-one invariant and recover PR4689's transition and full-guard tables without generating GL4 or GL5.", + "scope_change_reason": "Explicit assignment takes the released residual-state handoff as an algebraic side result rather than a proof-assistant or actual selected-caller binding. The numeric table is credited to Mihir Srivastava; the recurrence and sufficient-invariant derivation are the contribution.", + "bottleneck_link": "A state-aware header recurrence must preserve noncommuting ordered residuals and completion multiplicity. This supplies that algebraic layer but not odd-q caller admission, a paid physical cover, or a new supplier.", + "budget_minutes": 60, + "stop_rule": "Remain within the stated binary profile and rank-one terminal law; do not extend to adjacent profiles, larger fields, formal builds or selected-frontier replays.", + "outcome": "partial", + "evidence": "Parent registered replay completed with exit status zero on CPython 3.12.13, Linux x86_64, using python3.12 -B scripts/research_package.py --package research/schur-invariant-transitions. Ordinary -I -W error -B and optimized -I -W error -O -B commands both emitted PASS_SCHUR_INVARIANT_TRANSITIONS; runner emitted PASS_REGISTERED_RESEARCH_PACKAGE. Observed 496 initial splits, 172 admitted splits, 784 rank-one pairs, seven exact states, nine rejected mutations and 93564/9999360 = 2599/277760, reproducing all embedded state and depth expectations credited to PR4689. Separate AI mathematical review found no blocking issue in recurrence, stabilizers or invariant sufficiency. No independent human, proof-kernel or hosted approval is claimed, and no runtime measurement is claimed. The implementation worker executed no research code, gates, builds or formatters. The partial outcome denotes the scoped algebraic result and remaining caller obligations, not unfinished registered replay. Selected-frontier evidence remains source-binding orientation only, not native selected replay.", + "author": "codyw912", + "ai_assistance": "Substantial OpenAI Codex (GPT-6 Astra) assistance, including separate AI mathematical review. Independent human, proof-kernel and hosted approval are unclaimed.", + "final_parent_review": "Separate final AI static mathematical review PASS with no blockers. Parent reported the shared 331-test suite passing with 11 Windows-specific skips; shared tooling tests are separate from the mathematical package replay. No independent human, proof-kernel or hosted approval is claimed.", + "selected_result_unchanged": "60403/20000000 = 0.00302015, source #4470", + "publication": "No public Discussion claim was posted. Upstream PR creation requires operator approval; publication status is reported in the handoff.", + "overlap": { + "checked_at": "2026-10-22T16:48:34.859558+00:00", + "pull_requests_checked_at": "2026-10-22T16:48:00.710568+00:00", + "open_pull_requests": 469, + "discussion_records": 3624, + "local_notes": 5864, + "tracked_local_records_covered": 5860, + "own_contribution_records": 4, + "pagination": "Complete final parent snapshot; all tracked local records covered.", + "canonical_refresh": "origin/main refreshed unchanged at b58ad9ef4d4e861b0eaa5dba41742bdc072dca51.", + "predecessor_heads_refresh": "Direct heads #4689, #4678, #4671 and #4597 unchanged from citation_heads.", + "limits": ["Arbitrary code diffs", "Closed remote pull-request bodies", "Unpublished work"], + "closest_predecessor": "PR4689: seven-state numerical census using GL4 enumeration. This package derives the recurrence, block stabilizers and sufficient terminal invariant instead. No reservation or priority claim." + }, + "citation_heads": { + "4689": "3a72fbad148294aa9ca7f900a48dbb10e64232be", + "4678": "af9cf805c501e4e9e947c98c0b97b2281b6b6e97", + "4671": "8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9", + "4597": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb" + }, + "predecessor_credit": [ + "Mihir Srivastava, substantial OpenAI Codex assistance: seven-state numerical table and full-guard total, PR4689.", + "ssafwann, substantial OpenAI Codex assistance: sector criterion, one-block count, completion fibres and released residual handoff, PR4671/4678.", + "Nick Petalas: scalar and block Schur proofs and header/orbit lineage, including PR4597.", + "Ryanson Jonathan, substantial Claude Code (Claude Opus 5.5) assistance: literal full-guard convention and separate-family census.", + "lee-phys: binary sharpness and dimension contributions; Cinna Davis: BIT request context; source527, commdata2338 and Jose Manuel: retained normalizer lineage." + ], + "open_questions": [ + { + "question": "Can a sufficient higher-rank invariant replace block-orbit matching?", + "why_it_matters": "A scalable state recursion needs classification beyond one finite binary split domain.", + "first_step": "Derive the representation data of two image/kernel decompositions and compare proposed invariants against the printed block intertwiners.", + "blocked_by": "The present block certificate proves this finite domain, not a general classification." + }, + { + "question": "Can this state recurrence support an admitted and fully paid header cover?", + "why_it_matters": "A guard probability alone gives neither executable admission nor a consumer cost bound.", + "first_step": "State the actual caller's field and selection contract, then price emission, physical reads and restoration.", + "blocked_by": "Odd-q admission and the complete consumer bill remain outside the binary algebraic result." + } + ] +} diff --git a/research/schur-invariant-transitions/VERIFY.json b/research/schur-invariant-transitions/VERIFY.json new file mode 100644 index 0000000000..6334bca84b --- /dev/null +++ b/research/schur-invariant-transitions/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": ["{python}", "-I", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Intrinsic Schur recurrence restrictions, all 496 initial splits, explicit ordered block intertwiners, 36 GL2xGL2 stabilizer cases per representative, seven next-pivot transition rows, sufficient rank-one invariant terminal counts and 784-pair corroboration, all cited state weights/orbit/depth totals, and nine mathematical mutation controls; no GL4 or GL5 generation." + }, + { + "argv": ["{python}", "-I", "-W", "error", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "The same complete mathematical certificate under optimization, with explicit exceptions preserving every rejection control. Deterministic stdout only; no package writes or external scientific inputs." + } + ] +} diff --git a/research/schur-invariant-transitions/verify.py b/research/schur-invariant-transitions/verify.py new file mode 100755 index 0000000000..4ff8276821 --- /dev/null +++ b/research/schur-invariant-transitions/verify.py @@ -0,0 +1,431 @@ +#!/usr/bin/env python3 +"""Binary split-pivot transition certificate; standard library, no external reads. + +codyw912, with substantial OpenAI Codex (GPT-6 Astra) assistance. +Seven-state numerical targets: Mihir Srivastava, PR4689, exact head cited below. +Apache-2.0. No GL4 or GL5 generator is used. +""" + +import json +from collections import Counter +from fractions import Fraction +from functools import cache + + +class CertificateError(ValueError): + """A mathematical premise or certificate equality failed.""" + + +def require(condition, message): + if not condition: + raise CertificateError(message) + + +# Expectations transcribed from Mihir's table, not previously observed here. +TABLE_SOURCE = "https://github.com/CrocSwap/integer-mult-bounds/blob/3a72fbad148294aa9ca7f900a48dbb10e64232be/research/schur-residual-orbits/README.md" +S = (0, 0, 4, 8) +TS = ((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)) +# b, z, orbit, successful orbit elements, header weight, full-guard headers +EXPECTED = ((1, 36, 560, 100, 20160, 3600), + (3, 4, 5040, 468, 60480, 5616), + (126, 1, 20160, 366, 2540160, 46116), + (18, 1, 20160, 816, 362880, 14688), + (3, 4, 5040, 468, 60480, 5616), + (3, 4, 5040, 270, 60480, 3240), + (18, 1, 20160, 816, 362880, 14688)) +EXPECTED_TRANSITIONS = ((60, 600), (44, 312), (30, 61), (34, 136), + (44, 312), (36, 180), (34, 136)) +EXPECTED_DEPTHS = ((280, 180, 100), (3192, 1380, 468), + (15120, 4674, 366), (14448, 4896, 816), + (3192, 1380, 468), (3528, 1242, 270), + (14448, 4896, 816)) + + +def dot(x, y): + return (x & y).bit_count() & 1 + + +def apply(matrix, vector): + return sum(dot(row, vector) << i for i, row in enumerate(matrix)) + + +def columns(vectors, n): + return tuple(sum(((v >> i) & 1) << j for j, v in enumerate(vectors)) + for i in range(n)) + + +def identity(n): + return tuple(1 << i for i in range(n)) + + +def multiply(a, b): + return columns(tuple(apply(a, apply(b, 1 << j)) for j in range(len(b))), len(a)) + + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b)) + + +def independent_basis(vectors): + span = {0} + basis = [] + for v in vectors: + if v not in span: + basis.append(v) + span |= {x ^ v for x in span} + return tuple(basis) + + +def rank(vectors): + return len(independent_basis(vectors)) + + +def coordinates(basis): + result = {0: 0} + for i, v in enumerate(basis): + require(v not in result, "dependent coordinate basis") + result.update({x ^ v: c | (1 << i) for x, c in tuple(result.items())}) + return result + + +def inverse(matrix): + n = len(matrix) + coords = coordinates(tuple(apply(matrix, 1 << j) for j in range(n))) + require(len(coords) == 1 << n, "singular change of basis") + return columns(tuple(coords[1 << j] for j in range(n)), n) + + +def conjugate(matrix, basis_matrix): + return multiply(inverse(basis_matrix), multiply(matrix, basis_matrix)) + + +def gl_order(n): + result = 1 + for i in range(n): + result *= (1 << n) - (1 << i) + return result + + +@cache +def splits(n): + return tuple((a, beta) for a in range(1, 1 << n) + for beta in range(1, 1 << n) if dot(beta, a)) + + +def admitted(a_matrix, b_matrix): + for a, beta in splits(len(a_matrix)): + if dot(beta, apply(a_matrix, a)) and dot(beta, apply(b_matrix, a)): + yield a, beta + + +def restriction(matrix, a, beta, omit_correction=False): + """Intrinsic map on ker(beta), independently checked against block Schur.""" + n = len(matrix) + require(multiply(matrix, matrix) == matrix, "request is not idempotent") + require(dot(beta, a) == dot(beta, apply(matrix, a)) == 1, "not an admitted split") + basis = independent_basis(x for x in range(1, 1 << n) if not dot(beta, x)) + coords = coordinates(basis) + pivot_image = apply(matrix, a) + images = [] + for x in basis: + image = apply(matrix, x) + if not omit_correction and dot(beta, image): + image ^= pivot_image + require(image in coords, "intrinsic Schur image left ker(beta)") + images.append(coords[image]) + residual = columns(tuple(images), n - 1) + header = columns((a,) + basis, n) + block = conjugate(matrix, header) + require(block[0] & 1, "literal pivot was zero") + schur = tuple((block[i] >> 1) ^ ((block[0] >> 1) if block[i] & 1 else 0) + for i in range(1, n)) + require(residual == schur, "intrinsic restriction disagrees with block Schur") + require(multiply(residual, residual) == residual, "residual lost idempotency") + require(rank(residual) == rank(matrix) - 1, "Schur rank decrement failed") + return residual + + +@cache +def H(a_matrix, b_matrix, k): + """Exact complete-header recurrence, retaining the ordered matrix pair.""" + n = len(a_matrix) + require(len(b_matrix) == n and 0 <= k <= n, "invalid recurrence dimension/depth") + require(multiply(a_matrix, a_matrix) == a_matrix + and multiply(b_matrix, b_matrix) == b_matrix, "projectors required") + if k == 0: + return gl_order(n) + return sum(H(restriction(a_matrix, a, beta), restriction(b_matrix, a, beta), k - 1) + for a, beta in admitted(a_matrix, b_matrix)) + + +def block_diagonal(u, v): + return (u[0], u[1], v[0] << 2, v[1] << 2) + + +def block_equations(t, u, v): + e, f = tuple(x & 3 for x in t[:2]), tuple(x >> 2 for x in t[:2]) + g, h = tuple(x & 3 for x in t[2:]), tuple(x >> 2 for x in t[2:]) + return (multiply(u, e) == multiply(e, u) + and multiply(u, f) == multiply(f, v) + and multiply(v, g) == multiply(g, u) + and multiply(v, h) == multiply(h, v)) + + +def block_catalogue(): + # Only GL2 is generated: its two nonzero, unequal columns give six elements. + gl2 = tuple(columns((x, y), 2) for x in range(1, 4) + for y in range(1, 4) if x != y) + require(len(gl2) == gl_order(2) == 6, "GL2 domain mismatch") + catalogue = {} + stabilizers = [] + for state, t in enumerate(TS): + stabilizer = [] + for u in gl2: + for v in gl2: + k = block_diagonal(u, v) + centralizes = block_equations(t, u, v) + require(centralizes == (multiply(t, k) == multiply(k, t)), + "block equations lost a constraint") + if centralizes: + stabilizer.append(k) + normalized_t = multiply(k, multiply(t, inverse(k))) + if normalized_t in catalogue: + require(catalogue[normalized_t][0] == state, + "ordered representatives have intersecting block orbits") + else: + catalogue[normalized_t] = (state, k) + require(len(stabilizer) == EXPECTED[state][1], "wrong block stabilizer order") + stabilizers.append(stabilizer) + return catalogue, stabilizers + + +def classify(s, t, catalogue): + n = len(s) + kernel = independent_basis(x for x in range(1, 1 << n) if apply(s, x) == 0) + image = independent_basis(apply(s, 1 << j) for j in range(n)) + c = columns(kernel + image, n) + require(conjugate(s, c) == S, "kernel/image normalization failed") + normalized_t = conjugate(t, c) + require(normalized_t in catalogue, "residual outside seven proved block orbits") + state, k = catalogue[normalized_t] + witness = multiply(c, k) + require(rank(witness) == 4, "singular state intertwiner") + require(multiply(s, witness) == multiply(witness, S) + and multiply(t, witness) == multiply(witness, TS[state]), + "ordered state intertwiner failed") + return state, witness + + +def outer(u, phi, n): + return tuple(phi if (u >> i) & 1 else 0 for i in range(n)) + + +def rank_one(matrix): + n = len(matrix) + require(rank(matrix) == 1 and multiply(matrix, matrix) == matrix, + "rank-one projector required") + u = next(apply(matrix, 1 << j) for j in range(n) if apply(matrix, 1 << j)) + phi = sum(int(apply(matrix, 1 << j) != 0) << j for j in range(n)) + require(dot(phi, u) == 1 and outer(u, phi, n) == matrix, "rank-one factorization failed") + return u, phi + + +def invariant(r, t): + u, phi = rank_one(r) + v, psi = rank_one(t) + return (int(u == v), int(phi == psi), dot(phi, v), dot(psi, u)) + + +def constraint_count(vectors, n, ignore_odd_relations=False): + # Rank of [v_i | 1] exceeding rank of [v_i] detects inconsistent RHS. + coefficient_rank = rank(vectors) + if not ignore_odd_relations and rank(tuple(v | (1 << n) for v in vectors)) != coefficient_rank: + return 0 + return 1 << (n - coefficient_rank) + + +def terminal_count(r, t, ignore_odd_relations=False): + n = len(r) + u, phi = rank_one(r) + v, psi = rank_one(t) + return sum(constraint_count((a, u, v), n, ignore_odd_relations) + for a in range(1, 1 << n) if dot(phi, a) and dot(psi, a)) + + +def terminal_classes(): + # (u, phi, v, psi); the last four have both flags zero in cross-bit order. + factors = ((1, 1, 1, 1), (1, 1, 1, 3), (1, 1, 3, 1), + (1, 1, 2, 2), (1, 1, 2, 3), (1, 3, 2, 2), (1, 3, 2, 7)) + expected = (10, 6, 6, 1, 3, 3, 4) + table = {} + representatives = {} + for factors_i, g in zip(factors, expected): + u, phi, v, psi = factors_i + r, t = outer(u, phi, 3), outer(v, psi, 3) + key = invariant(r, t) + require(key not in table, "duplicate terminal invariant representative") + require(terminal_count(r, t) == g == sum(1 for _ in admitted(r, t)), + "terminal formula disagrees with independent split equations") + table[key] = g + representatives[key] = (r, t) + # Exhaust all rank-one pairs, not all bases: 28^2 pairs in dimension three. + projectors = tuple(outer(u, phi, 3) for u in range(1, 8) + for phi in range(1, 8) if dot(phi, u)) + counts = Counter() + for r in projectors: + for t in projectors: + key = invariant(r, t) + require(key in table, "missing sufficient invariant class") + require(terminal_count(r, t) == table[key] == sum(1 for _ in admitted(r, t)), + "invariant terminal value is not constant") + counts[key] += 1 + require(len(counts) == 7 and sum(counts.values()) == 784, "rank-one domain mismatch") + require(counts == {(1, 1, 1, 1): 28, (1, 0, 1, 1): 84, (0, 1, 1, 1): 84, + (0, 0, 0, 0): 168, (0, 0, 0, 1): 168, + (0, 0, 1, 0): 168, (0, 0, 1, 1): 84}, + "rank-one invariant population mismatch") + return table, representatives, counts + + +def key_text(key): + return "".join(map(str, key)) + + +def exact_quotient(a, b): + require(b > 0 and a % b == 0, "nonintegral orbit fibre") + return a // b + + +def validate_summary(rows, total, denominator): + require(len(rows) == 7, "ordered state count changed") + for row, target, depths, transition in zip(rows, EXPECTED, EXPECTED_DEPTHS, EXPECTED_TRANSITIONS): + observed = tuple(row[k] for k in ("b", "z", "orbit", "f", "headers", "full_guard_headers")) + require(observed == target, "cited state table mismatch") + require(tuple(row["depths"]) == depths, "guard-depth distribution mismatch") + require((row["m"], row["G"]) == transition, "transition totals mismatch") + require(total == 93564 and denominator == 9999360, "complete full-guard count mismatch") + + +def reject(name, action): + try: + action() + except CertificateError: + return name + raise CertificateError("mutation was accepted: " + name) + + +def check_partition(key, rows): + seen = set() + for row in rows: + value = key(row) + require(value not in seen, "lossy state identification") + seen.add(value) + + +def rank_signature(pair): + s, t = pair + return (rank(s), rank(t), rank(multiply(s, t)), rank(multiply(t, s)), + rank(add(s, t)), rank(add(multiply(s, t), multiply(t, s)))) + + +def controls(rows, catalogue, terminal_reps): + results = [] + missing = [dict(row, full_guard_headers=row["b"] * row["G"]) for row in rows] + results.append(reject("omitted_GL2_completion_factor", + lambda: validate_summary(missing, sum(r["full_guard_headers"] for r in missing), 9999360))) + results.append(reject("omitted_GL4_completion_factor", + lambda: validate_summary([dict(r, headers=r["b"]) for r in rows], 93564, 9999360))) + results.append(reject("commutator_only_state", + lambda: check_partition(lambda p: rank(add(multiply(*p), multiply(p[1], p[0]))), + ((S, TS[0]), (S, TS[2]))))) + require(rows[0]["G"] != rows[2]["G"], "commutator witness lost differing continuations") + results.append(reject("product_sum_commutator_rank_state", + lambda: check_partition(rank_signature, ((S, TS[1]), (S, TS[4]))))) + # Transposition exchanges states 2/5. Swapping also merges distinct ordered + # terminal classes 0001/0010, even though their terminal counts coincide. + transpose = lambda m: columns(m, len(m)) + require(classify(transpose(S), transpose(TS[1]), catalogue)[0] == 4, + "transpose witness no longer exchanges states 2 and 5") + require(classify(transpose(S), transpose(TS[3]), catalogue)[0] == 6, + "transpose witness no longer exchanges states 4 and 7") + results.append(reject("transpose_identification", + lambda: require(classify(S, TS[1], catalogue)[0] + == classify(transpose(S), transpose(TS[1]), catalogue)[0], + "transpose is not an allowed intertwiner"))) + r, t = terminal_reps[(0, 0, 0, 1)] + require(invariant(t, r) == (0, 0, 1, 0), "ordered cross-pairing witness failed") + results.append(reject("unordered_requests", + lambda: require(invariant(r, t) == invariant(t, r), "ordered invariants differ"))) + r, t = terminal_reps[(0, 0, 0, 0)] + require(constraint_count((3, 1, 2), 3) == 0, "odd relation accepted") + results.append(reject("ignored_odd_terminal_relation", + lambda: require(terminal_count(r, t, True) == terminal_count(r, t), + "inconsistent terminal RHS contributes spurious solutions"))) + results.append(reject("omitted_Schur_correction", + lambda: restriction((3, 0), 1, 1, omit_correction=True))) + # The previous witness must have a nonzero correction on its kernel. + results.append(reject("first_guard_substituted_for_full_guard", + lambda: validate_summary(rows, sum(r["headers"] for r in rows), 9999360))) + return results + + +def main(): + catalogue, stabilizers = block_catalogue() + terminal, terminal_reps, terminal_populations = terminal_classes() + p0, q0 = (0, 2, 0, 8, 16), (0, 0, 4, 8, 16) + initial = [] + weights = Counter() + for a, beta in admitted(p0, q0): + s, t = restriction(p0, a, beta), restriction(q0, a, beta) + state, witness = classify(s, t, catalogue) + weights[state] += 1 + initial.append({"a": a, "beta": beta, "state": state + 1, "intertwiner": witness}) + require(len(splits(5)) == 496 and len(initial) == 172, "initial split domain mismatch") + require(gl_order(0) == 1 and gl_order(3) == 168 and gl_order(4) == 20160, + "zero-guard completion order mismatch") + require(H((), (), 0) == 1 and H((0,), (0,), 1) == 0, + "empty completion or impossible guard mishandled") + rows = [] + for state, t in enumerate(TS): + transitions = Counter() + for a, beta in admitted(S, t): + r1, t1 = restriction(S, a, beta), restriction(t, a, beta) + key = invariant(r1, t1) + require(key in terminal, "unclassified next-pivot residual") + require(terminal[key] == terminal_count(r1, t1), "terminal invariant lost a datum") + transitions[key] += 1 + m = sum(transitions.values()) + g_sum = sum(weight * terminal[key] for key, weight in transitions.items()) + b, z = weights[state], len(stabilizers[state]) + full = gl_order(2) * g_sum + require(full == H(S, t, 2), "invariant evaluation disagrees with direct split recurrence") + depths = tuple(exact_quotient(x, z) for x in + (gl_order(4) - gl_order(3) * m, gl_order(3) * m - full, full)) + rows.append({"state": state + 1, "T": t, "b": b, "z": z, + "orbit": exact_quotient(gl_order(4), z), "f": exact_quotient(full, z), + "m": m, "G": g_sum, "H_4_2": full, "depths": depths, + "headers": b * gl_order(4), "headers_per_orbit_element": b * z, + "full_guard_headers": b * full, + "transitions": {key_text(key): transitions.get(key, 0) for key in sorted(terminal)}, + "stabilizer_matrices": stabilizers[state]}) + total = sum(row["full_guard_headers"] for row in rows) + denominator = len(splits(5)) * gl_order(4) + validate_summary(rows, total, denominator) + rejected = controls(rows, catalogue, terminal_reps) + result = {"field": 2, "matrix_encoding": "integer rows, bit j is column j; ordered pairs", + "expected_table_source": TABLE_SOURCE, "states": rows, + "initial_split_certificates": initial, + "terminal_classes": [{"invariant": key_text(key), "g": terminal[key], + "rank_one_pair_population": terminal_populations[key]} + for key in sorted(terminal)], + "split_domains": {"n5": len(splits(5)), "n4": len(splits(4))}, + "admitted_initial_splits": len(initial), "first_guard_headers": sum(r["headers"] for r in rows), + "full_guard_headers": total, "all_headers": denominator, + "full_guard_fraction": str(Fraction(total, denominator)), "rejected_mutations": rejected} + print(json.dumps(result, indent=2, sort_keys=True)) + print("PASS_SCHUR_INVARIANT_TRANSITIONS") + + +if __name__ == "__main__": + main()